Answer Set Programming and Bounded Model Checking

Reference:

Keijo Heljanko and Ilkka Niemelä. Answer set programming and bounded model checking. In Alessandro Provetti and Tran Cao Son, editors, Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning, pages 90–96, Stanford, USA, March 2001. AAAI Press, Technical Report SS-01-01.

Abstract:

In this paper bounded model checking of asynchronous concurrent systems is introduced as a promising application area for answer set programming. This is an extension of earlier work where bounded model checking has been used for verification of sequential digital circuits. As the model of asynchronous systems a generalization of communicating automata, 1-safe Petri nets, are used. A mapping from bounded reachability and deadlock detection problems of 1-safe Petri nets to stable model computation is devised. Some experimental results on solving deadlock detection problems using the mapping and the Smodels system are presented. They indicate that the approach is quite competitive when searching for short executions of the system leading to deadlock.

Keywords:

logic programs, stable models, symbolic model checking, Petri nets

Suggested BibTeX entry:

@inproceedings{hn2001:asp,
    address = {Stanford, USA},
    author = {Keijo Heljanko and Ilkka Niemel{\"a}},
    booktitle = {Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning},
    editor = {Alessandro Provetti and Tran Cao Son},
    month = {March},
    pages = {90--96},
    publisher = {AAAI Press, Technical Report SS-01-01},
    title = {Answer Set Programming and Bounded Model Checking},
    year = {2001},
}