Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Coping with strong fairness

Latvala T., Heljanko K.

Fundamenta Informaticae

2000

Vol. 43, Nr 1-4

175-193

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.

Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri Nets

Heljanko K.

Fundamenta Informaticae

1999

Vol. 37, Nr 3

247-268

McMillan has presented a deadlock detection method for Petri nets based on finite complete prefixes (i.e. net unfoldings). The approach transforms the PSPACE-complete deadlock detec-tion problem for a 1-safe Petri net into a potentially exponentially larger NP-complete prob-lem of deadlock detection for a finite complete prefix. McMillan devised a branch-and-bound algorithm for deadlock detection in prefixes. Recently, Melzer and Römer have presented another approach, which is based on solving mixed integer programming problems. In this work it is shown that instead of using mixed integer programming, a constraint-based logic programming framework can be employed, and a linear-size, translation from deadlock detec-tion in prefixes into the problem of finding a stable model of a logic program is presented. As a side result also such a translation for solving the reachability problem is devised. Correct-ness proofs of both the translations are presented. Experimental results are given from an im-plementation combining the prefix generator of the PEP-tool, the translation, and an imple-mentation of a constraint-based logic programming framework, the smodels system. The ex-periments show the proposed approach to be quite competitive, when compared to the ap-proaches of McMillan and Melzer/Römer.