Reference:

J. Esparza and S. Melzer. Model checking LTL using constraint programming. In Proc. of Application and Theory of Petri Nets'97, 1997.

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 approach to model-checking and on the notion of T-invariant. We analyse the computational complexity of the test, implement it using 2lp – a constraint programming tool, and apply it to two case studies.

Suggested BibTeX entry:

@inproceedings{EM97,
    author = {J. Esparza and S. Melzer},
    booktitle = {Proc. of Application and Theory of {P}etri Nets'97},
    title = {Model Checking {LTL} using Constraint Programming},
    year = {1997}
}