Ideal abstractions for well-structured transition systems

Damien Zufferey, Thomas Wies, Thomas A. Henzinger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
Pages445-460
Number of pages16
DOIs
StatePublished - 2012
Event13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012 - Philadelphia, PA, United States
Duration: Jan 22 2012Jan 24 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7148 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
Country/TerritoryUnited States
CityPhiladelphia, PA
Period1/22/121/24/12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Ideal abstractions for well-structured transition systems'. Together they form a unique fingerprint.

Cite this