TY - GEN
T1 - Symbolic model checking of infinite-state systems using narrowing
AU - Escobar, Santiago
AU - Meseguer, José
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=38049123677&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38049123677&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-73449-9_13
DO - 10.1007/978-3-540-73449-9_13
M3 - Conference contribution
AN - SCOPUS:38049123677
SN - 9783540734475
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 153
EP - 168
BT - Term Rewriting and Applications - 18th International Conference, RTA 2007, Proceedings
PB - Springer
T2 - 18th International Conference on Rewriting Techniques and Applications, RTA 2007
Y2 - 26 June 2007 through 28 June 2007
ER -