Answer Set Programming and Bounded Model Checking

13 years 9 months ago
Answer Set Programming and Bounded Model Checking
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.
Keijo Heljanko, Ilkka Niemelä
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where ASP
Authors Keijo Heljanko, Ilkka Niemelä
Comments (0)