Ideal Abstractions for Well-Structured Transition Systems

stractions for Well-Structured Transition Systems Damien Zufferey1 , Thomas Wies2 , and Thomas A. Henzinger1 1 IST Austria 2 New York University 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 ed termination. Our analysis is an abstract interpre...

• Type: Journal
• Year: 2012
• Where: VMCAI
• Authors: Damien Zufferey, Thomas Wies, Thomas A. Henzinger
• Keywords: Attractive Target, Generic Algorithms, Prototype Implementation, Software Engineering, VMCAI 2012