TY - GEN
T1 - Ideal abstractions for well-structured transition systems
AU - Zufferey, Damien
AU - Wies, Thomas
AU - Henzinger, Thomas A.
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84856138122&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84856138122&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-27940-9_29
DO - 10.1007/978-3-642-27940-9_29
M3 - Conference contribution
AN - SCOPUS:84856138122
SN - 9783642279393
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 445
EP - 460
BT - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
T2 - 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
Y2 - 22 January 2012 through 24 January 2012
ER -