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
Volume7148 LNCS
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Transition Systems
Set Covering
Termination
Ordered Space
Abstract Interpretation
Formal Analysis
Completion
Abstraction
State Space
Prototype
Target
Computing
Operator
Simulation

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Zufferey, D., Wies, T., & Henzinger, T. A. (2012). Ideal abstractions for well-structured transition systems. In Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings (Vol. 7148 LNCS, pp. 445-460). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7148 LNCS). https://doi.org/10.1007/978-3-642-27940-9_29

Ideal abstractions for well-structured transition systems. / Zufferey, Damien; Wies, Thomas; Henzinger, Thomas A.

Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings. Vol. 7148 LNCS 2012. p. 445-460 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7148 LNCS).

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

Zufferey, D, Wies, T & Henzinger, TA 2012, Ideal abstractions for well-structured transition systems. in Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings. vol. 7148 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7148 LNCS, pp. 445-460, 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012, Philadelphia, PA, United States, 1/22/12. https://doi.org/10.1007/978-3-642-27940-9_29
Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well-structured transition systems. In Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings. Vol. 7148 LNCS. 2012. p. 445-460. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-27940-9_29
Zufferey, Damien ; Wies, Thomas ; Henzinger, Thomas A. / Ideal abstractions for well-structured transition systems. Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings. Vol. 7148 LNCS 2012. pp. 445-460 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{de1d8c69d1964b6a9a1994ef9b82e716,
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.",
author = "Damien Zufferey and Thomas Wies and Henzinger, {Thomas A.}",
year = "2012",
doi = "10.1007/978-3-642-27940-9_29",
language = "English (US)",
isbn = "9783642279393",
volume = "7148 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "445--460",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings",

}

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

SN - 9783642279393

VL - 7148 LNCS

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

ER -