Coping with strong fairness

• Autorzy: Latvala T. , Heljanko K.
• Języki publikacji: EN

Abstrakty

EN

We consider the verification of linear temporal logic (LTL) properties of Petri nets, where the transitions can have both weak and strong fairness constraints. Allowing the transitions to have weak or strong fairness constraints simplifies the modeling of systems in many cases. We use the automata theoretic approach to model checking. To cope with the strong fairness constraints efficiently we employ Streett automata where appropriate. We present memory efficient algorithms for both the emptiness checking and counterexample generation problems for Streett automata.

Słowa kluczowe

EN

verification; model checking; fairness; Streett automata; counterexamples

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2000
• Tom: Vol. 43, Nr 1-4
• Strony: 175--193
• Opis fizyczny: bibliogr. 19 poz.

Twórcy

autor

Latvala T.

autor

Heljanko K.

• Laboratory for Theoretical Computer Science, Helsinki University of Technology, P.O. Box 9700, FIN- 02015 HUT, Finland,