Symbolic model checking of infinite-state systems using narrowing

Santiago Escobar, José Meseguer

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


Rewriting is a general and expressive way of specifying concurrent systems, where concurrent transitions are axiomatized by rewrite rules. Narrowing is a complete symbolic method for model checking reachability properties. We show that this method can be reinterpreted as a lifting simulation relating the original system and the symbolic system associated to the narrowing transitions. Since the narrowing graph can be infinite, this lifting simulation only gives us a semi-decision procedure for the failure of invariants. However, we propose new methods for folding the narrowing tree that can in practice result in finite systems that symbolically simulate the original system and can be used to algorithmically verify its properties. We also show how both narrowing and folding can be used to symbolically model check systems which, in addition, have state predicates, and therefore correspond to Kripke structures on which ACTL* and LTL formulas can be algorithmically verified using such finite symbolic abstractions.

Original languageEnglish (US)
Title of host publicationTerm Rewriting and Applications - 18th International Conference, RTA 2007, Proceedings
Number of pages16
ISBN (Print)9783540734475
StatePublished - 2007
Event18th International Conference on Rewriting Techniques and Applications, RTA 2007 - Paris, France
Duration: Jun 26 2007Jun 28 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4533 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other18th International Conference on Rewriting Techniques and Applications, RTA 2007

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


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

Cite this