Name
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. |
Year | Venue | Field |
|---|---|---|
2018 | CONCUR | Discrete mathematics,Parameterized complexity,Model checking,Computer science,Automaton,Reachability,Distributed algorithm,Counter automaton,Acceleration,Bounded function |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jure Kukovec | 1 | 1 | 0.75 |
| Igor Konnov | 2 | 57 | 12.06 |
| Josef Widder | 3 | 229 | 23.99 |