Coping with Strong Fairness (2000)
AUTHORS:
Latvala Timo
,
Heljanko Keijo
JOURNAL:
Fundamenta Informaticae
VOLUME:
43
PAGES:
175--193
URL:
http://users.ics.tkk.fi/kepa/publications/
@article{ LatHel:Fundamenta2000, author = "Latvala, Timo and Heljanko, Keijo", publisher = "IOS Press", title = "Coping with Strong Fairness", url = "http://users.ics.tkk.fi/kepa/publications/", journal = "Fundamenta Informaticae", number = "1--4", abstract = "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.", volume = "43", juforank = "2", flags = "copy SA-LO-00-02", year = "2000", keywords = "verification, model checking, fairness, Streett automata, counterexamples", pages = "175--193" }