Paper Info
Title
Ideal abstractions for well-structured transition systems
Abstract
Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system.
Year
DOI
Venue
2012
10.1007/978-3-642-27940-9_29
VMCAI
Keywords
Field
DocType
well-structured transition system,abstract domain,inherent precision loss,guaranteed termination,abstract interpretation,acceleration-based algorithm,ideal abstraction,well-quasi-ordered state space,formal analysis,flattable wsts,attractive target,infinite state system
Abstraction,Programming language,Computer science,Abstract interpretation,Theoretical computer science,Operator (computer programming),Acceleration,Covering set,State space,Undecidable problem
Conference
Volume
ISSN
Citations 
7148
0302-9743
15
PageRank 
References 
Authors
0.62
25
3
Name
Order
Citations
PageRank
Damien Zufferey135822.61
Thomas Wies251528.26
Thomas A. Henzinger3148271317.51