Skip to Main content Skip to Navigation
Conference papers

Reachability in Parameterized Systems: All Flavors of Threshold Automata

Jure Kukovec 1 Igor Konnov 2, 3 Josef Widder 1
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Threshold automata, and the counter systems they define, were introduced as a framework for parameterized model checking of fault-tolerant distributed algorithms. This application domain suggested natural constraints on the automata structure, and a specific form of acceleration, called single-rule acceleration: consecutive occurrences of the same automaton rule are executed as a single transition in the counter system. These accelerated systems have bounded diameter, and can be verified in a complete manner with bounded model checking. We go beyond the original domain, and investigate extensions of threshold automata: non-linear guards, increments and decrements of shared variables, increments of shared variables within loops, etc., and show that the bounded diameter property holds for several extensions. Finally, we put single-rule acceleration in the scope of flat counter automata: although increments in loops may break the bounded diameter property, the corresponding counter automaton is flattable, and reachability can be verified using more permissive forms of acceleration.
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Igor Konnov Connect in order to contact the contributor
Submitted on : Monday, September 10, 2018 - 2:05:48 PM
Last modification on : Wednesday, November 3, 2021 - 7:57:50 AM
Long-term archiving on: : Tuesday, December 11, 2018 - 2:54:34 PM


Files produced by the author(s)




Jure Kukovec, Igor Konnov, Josef Widder. Reachability in Parameterized Systems: All Flavors of Threshold Automata. CONCUR 2018 - 29th International Conference on Concurrency Theory, Sep 2018, Beijing, China. ⟨10.4230/LIPIcs.CONCUR.2018.19⟩. ⟨hal-01871142⟩



Les métriques sont temporairement indisponibles