Constraint logic programming for local and symbolic model-checking
2000 (English)In: Computational Logic — CL 2000: First International Conference London, UK, July 24–28, 2000 Proceedings / [ed] John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv and Peter J. Stuckey, Springer Berlin/Heidelberg, 2000, Vol. 1861, 384-398 p.Chapter in book (Refereed)
We-propose a model checking scheme for a semantically complete fragment of CTL by combining techniques from constraint logic programming, a restricted form of constructive negation and tabled resolution. Our approach is symbolic in that it encodes and manipulates sets of states using constraints, it supports local model checking using goal-directed computation enhanced by tabulation. The framework is parameterized by the constraint domain and supports any finite constraint domain closed under disjunction, projection and complementation. We show how to encode our fragment of CTL in constraint logic programming, we outline an abstract execution model for the resulting type of programs and provide a preliminary evaluation of the approach.
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2000. Vol. 1861, 384-398 p.
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 1861
Engineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-49508DOI: 10.1007/3-540-44957-4_26ISBN: 978-3-540-67797-0 (Print)ISBN: 978-3-540-44957-7 (online)OAI: oai:DiVA.org:liu-49508DiVA: diva2:270404