The model-checking problem for 1-safe Petri nets and hneartime 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 approach to model-checking and on the notion of T-invariant. We analyse the computational complexity of the test, implement it using 21p-a constraint programming tool, and apply it to two case studies. This paper is a (very) abbreviated version of [6].
CITATION STYLE
Esparza, J., & Melzer, S. (1997). Model checking LTL using constraint programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1248, pp. 1–20). Springer Verlag. https://doi.org/10.1007/3-540-63139-9_26
Mendeley helps you to discover research relevant for your work.