Answer Set Programming and Bounded Model Checking (2001)
AUTHORS:
Heljanko Keijo
,
Niemelä Ilkka
BOOKTITLE:
Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning
PAGES:
90--96
URL:
http://users.ics.tkk.fi/kepa/publications/
@inproceedings{ hn2001:asp, editor = "Provetti, Alessandro and Son, Tran Cao", author = {Heljanko, Keijo and Niemel{\"a}, Ilkka}, publisher = "AAAI Press, Technical Report SS-01-01", title = "Answer Set Programming and Bounded Model Checking", url = "http://users.ics.tkk.fi/kepa/publications/", booktitle = "Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning", address = "Stanford, USA", 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.", month = "March", juforank = "NA", flags = "copy SA-LO-00-02 SA-IN-98-01", year = "2001", keywords = "logic programs, stable models, symbolic model checking, Petri nets", pages = "90--96" }