University of Illinois Urbana-Champaign

Symbolic Model Checking of Infinite-State Systems Using Narrowing

Escobar, Santiago; Meseguer, José

Content Files
Symbolic Model Checking of Infinite-State Systems Using Narrowing.pdf

Permalink

https://hdl.handle.net/2142/11292

Description

Title
Symbolic Model Checking of Infinite-State Systems Using Narrowing
Author(s)
  • Escobar, Santiago
  • Meseguer, José
Issue Date
2007-02
Keyword(s)
computer science
Date of Ingest
2009-04-21T20:16:05Z
Abstract
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.
Type of Resource
text
Genre of Resource
Technical Report
Permalink
http://hdl.handle.net/2142/11292
Copyright and License Information
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections

Research and Tech Reports - Computer Science PRIMARY