Skip to main content
Conference Proceedings

Model checking abstract state machines with answer set programming

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2005) 3835 LNAI 443-458
DOI: 10.1007/11591191_31
3Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Answer Set Programming (ASP) has been demonstrated as an effective tool in various application areas, including formal verification. In this paper we present Bounded Model Checking (BMC) of Abstract State Machines (ASMs) based on ASP. We show how to succinctly translate an ASM and a temporal property into a logic program and solve the BMC problem for the ASM by computing an answer set for the corresponding program. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given. © Springer-Verlag Berlin Heidelberg 2005.

Cite

CITATION STYLE

APA

Tang, C. K. F., & Ternovska, E. (2005). Model checking abstract state machines with answer set programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3835 LNAI, pp. 443–458). https://doi.org/10.1007/11591191_31

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free