Affiliations: Laboratory for Theoretical Computer Science, Helsinki University of Technology, P.O. Box 9700, FIN-02015 HUT, Finland. Timo.Latvala@hut.fi | Laboratory for Theoretical Computer Science, Helsinki University of Technology P.O. Box 5400, FIN-02015 HUT, Finland. Keijo.Heljanko@hut.fi
Note: [] Address for correspondence: Laboratory for Theoretical Computer Science, Helsinki University of Technology, P.O. Box 9700, FIN-02015 HUT, Finland
Note: [] Address for correspondence: Laboratory for Theoretical Computer Science, Helsinki University of Technology, P.O. Box 9700, FIN-02015 HUT, Finland
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.
Keywords: Verification, model checking, fairness, Streett automata, counterexamples
