Model checking LTL using constraint programming

13Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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].

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free