Model Checking Abstract State Machines with Answer Set Programming | Zendy

Calvin Kai Fan Tang | Zendy; Eugenia Ternovska | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Model Checking Abstract State Machines with Answer Set Programming

Author(s) -

Calvin Kai Fan Tang,

Eugenia Ternovska

Publication year - 2005

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/11591191_31

Subject(s) - answer set programming , computer science , abstract state machines , model checking , programming language , set (abstract data type) , state (computer science) , bounded function , theoretical computer science , logic programming , logic program , property (philosophy) , stable model semantics , finite state machine , semantics (computer science) , mathematics , mathematical analysis , philosophy , operational semantics , epistemology

The quality of a computer system can be enhanced by modelling its design and verifying the correctness of the design before implementation is done. Abstract State Machines (ASMs) provide a mathematical framework for system modelling, while Model Checking is a technology for verification of system properties. Together, they form a powerful tool for checking systems. Bounded Model Checking (BMC) based on Answer Set Programming (ASP) is a competitive model checking approach due to its ability to compactly encode BMC problems. In this paper, we present a method of applying ASP to BMC of ASMs. Given an ASM and a temporal property, we show how to efficiently translate the BMC problem for the ASM into a problem of answer set computation. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research