Benutzer: Gast  Login
Dokumenttyp:
Technical Report 
Autor(en):
Javier Esparza; Stephan Melzer 
Titel:
Model Checking LTL using Constraint Programming 
Abstract:
The model-checking problem for 1-safe Petri nets and linear-time temporal logic (LTL) consists of deciding, given a 1-safe Petri net and a formula of LTL, whether the Petri net satisfies the property encoded by the formula. This paper introduces a semidecision test for this problem. By a semidecision test we understand a procedure which may answer `yes', in which case the Petri net satisfies the property, or `don't know'. The test is based on a variant of the so called automata-theoretic approac...    »
 
Stichworte:
Verifikation; Petrinetze; Constraint Programming; Automaten-theoretischer Ansatz; Snapshot-Algorithmus; Leader-Election 
Jahr:
1997 
Jahr / Monat:
1997-04-01 00:00:00 
Seiten/Umfang:
43