




Publications  Model Checking LTL using Constraint Programming





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 modelchecking problem for 1safe Petri nets and lineartime temporal logic (LTL) consists of deciding, given a 1safe 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 automatatheoretic approach to modelchecking and on the notion of Tinvariant. 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}
}




