Symbolic Model Checking of Infinite-State Systems Using Narrowing

Escobar, Santiago; Meseguer, José

Permalink

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

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