Abstract logical model checking of infinite-state systems using narrowing

Kyungmin Bae, Santiago Escobar, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

A concurrent system can be naturally specified as a rewrite theory R = (∑,E,R) where states are elements of the initial algebra T∑/E and concurrent transitions are axiomatized by the rewrite rules R. Under simple conditions, narrowing with rules R modulo equations E can be used to symbolically represent the system's state space by means of terms with logical variables. We call this symbolic representation a logical state space and it can also be used for model checking verification of LTL properties. Since in general such a logical state space can be infinite, we propose several abstraction techniques for obtaining either an over-approximation or an underapproximation of the logical state space: (i) a folding abstraction that collapses patterns into more general ones, (ii) an easy-to-check method to define (bisimilar) equational abstractions, and (iii) an iterated bounded model checking method that can detect if a logical state space within a given bound is complete. We also show that folding abstractions can be faithful for safety LTL properties, so that they do not generate any spurious counterexamples. These abstraction methods can be used in combination and, as we illustrate with examples, can be effective in making the logical state space finite. We have implemented these techniques in the Maude system, providing the first narrowing-based LTL model checker we are aware of.

Original languageEnglish (US)
Title of host publication24th International Conference on Rewriting Techniques and Applications, RTA 2013
EditorsFemke van Raamsdonk
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages81-96
Number of pages16
ISBN (Electronic)9783939897538
ISBN (Print)9783939897538
DOIs
StatePublished - Jan 1 2013
Event24th International Conference on Rewriting Techniques and Applications, RTA 2013 - Eindhoven, Netherlands
Duration: Jun 24 2013Jun 26 2013

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume21
ISSN (Print)1868-8969

Other

Other24th International Conference on Rewriting Techniques and Applications, RTA 2013
CountryNetherlands
CityEindhoven
Period6/24/136/26/13

Keywords

  • Infinite states
  • Model checking
  • Narrowing
  • Rewrite theories

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Abstract logical model checking of infinite-state systems using narrowing'. Together they form a unique fingerprint.

Cite this