5 papers
TACO: A Toolsuite for the Verification of Threshold Automata
Paul Eichler, Tom Baumeister, Mouhammad Sakr +3
We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches…
Parametric disjunctive timed networks
Étienne André, Swen Jacobs, Engel Lefaucheux
We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition…
Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
Paul Eichler, Swen Jacobs, Chana Weil-Kennedy
We introduce a new framework for verifying systems with a parametric number of concurrently running processes. The systems we consider are well-structured with respect to a specifi…
Parameterized Verification of Timed Networks with Clock Invariants
Étienne André, Swen Jacobs, Shyam Lal Karra +1
We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed n…
Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Tom Baumeister, Paul Eichler, Swen Jacobs +2
Threshold automata are a computational model that has proven to be versatile in modeling threshold-based distributed algorithms and enabling their completely automatic parameterize…