Structural counter abstraction

Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey

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

Abstract

Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system's reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber's stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.
Pages62-77
Number of pages16
Volume7795 LNCS
DOIs
StatePublished - 2013
Event19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013 - Rome, Italy
Duration: Mar 16 2013Mar 24 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7795 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
CountryItaly
CityRome
Period3/16/133/24/13

Fingerprint

Topology
Communication
Termination
Liveness
Concurrent Systems
Heap
Transition Systems
Thread
Abstraction
Concurrent
Finite Set
Complex Systems
Prototype
Approximation
Range of data
Model

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Bansal, K., Koskinen, E., Wies, T., & Zufferey, D. (2013). Structural counter abstraction. In Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc. (Vol. 7795 LNCS, pp. 62-77). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7795 LNCS). https://doi.org/10.1007/978-3-642-36742-7_5

Structural counter abstraction. / Bansal, Kshitij; Koskinen, Eric; Wies, Thomas; Zufferey, Damien.

Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. Vol. 7795 LNCS 2013. p. 62-77 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7795 LNCS).

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

Bansal, K, Koskinen, E, Wies, T & Zufferey, D 2013, Structural counter abstraction. in Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. vol. 7795 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7795 LNCS, pp. 62-77, 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, 3/16/13. https://doi.org/10.1007/978-3-642-36742-7_5
Bansal K, Koskinen E, Wies T, Zufferey D. Structural counter abstraction. In Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. Vol. 7795 LNCS. 2013. p. 62-77. (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-36742-7_5
Bansal, Kshitij ; Koskinen, Eric ; Wies, Thomas ; Zufferey, Damien. / Structural counter abstraction. Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. Vol. 7795 LNCS 2013. pp. 62-77 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{aa7c3df793da44e9a49d121d9df92d31,
title = "Structural counter abstraction",
abstract = "Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system's reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber's stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.",
author = "Kshitij Bansal and Eric Koskinen and Thomas Wies and Damien Zufferey",
year = "2013",
doi = "10.1007/978-3-642-36742-7_5",
language = "English (US)",
isbn = "9783642367410",
volume = "7795 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "62--77",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.",

}

TY - GEN

T1 - Structural counter abstraction

AU - Bansal, Kshitij

AU - Koskinen, Eric

AU - Wies, Thomas

AU - Zufferey, Damien

PY - 2013

Y1 - 2013

N2 - Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system's reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber's stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.

AB - Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system's reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber's stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.

UR - http://www.scopus.com/inward/record.url?scp=84874447997&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84874447997&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-36742-7_5

DO - 10.1007/978-3-642-36742-7_5

M3 - Conference contribution

SN - 9783642367410

VL - 7795 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 62

EP - 77

BT - Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.

ER -