Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-23T20:35:03.173Z Has data issue: false hasContentIssue false
  • English
  • Français

Bounded LTL model checking with stable models

Published online by Cambridge University Press:  31 July 2003

KEIJO HELJANKO  and
ILKKA NIEMELÄ
KEIJO HELJANKO
Affiliation:
Laboratory for Theoretical Computer Science, Department of Computer Science and Engineering, Helsinki University of Technology, P.O. Box 5400, FIN-02015 HUT, Finland (e-mail: [email protected])
ILKKA NIEMELÄ
Affiliation:
Laboratory for Theoretical Computer Science, Department of Computer Science and Engineering, Helsinki University of Technology, P.O. Box 5400, FIN-02015 HUT, Finland (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, bounded model checking of asynchronous concurrent systems is introduced as a promising application area for answer set programming. As the model of asynchronous systems a generalisation of communicating automata, 1-safe Petri nets, are used. It is shown how a 1-safe Petri net and a requirement on the behaviour of the net can be translated into a logic program such that the bounded model checking problem for the net can be solved by computing stable models of the corresponding program. The use of the stable model semantics leads to compact encodings of bounded reachability and deadlock detection tasks as well as the more general problem of bounded model checking of linear temporal logic. Correctness proofs of the devised translations are given, and some experimental results using the translation and the Smodels system are presented.

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 3 , Issue 4-5 , July 2003 , pp. 519 - 550
Copyright
© 2003 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

This is an extended version of a paper titled “Bounded LTL model checking with stable models” presented at the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR' 2001), Vienna, Austria, September 2001.