Shrinktech is a tool for robustness analysis of timed automata based on the results described in [SBM14]. A tool paper was presented in [San13].
The tool can be used to check whether a given timed automaton is robust to guard shrinkings: whether the behaviour is preserved when all guards of the form l <= x <= u, are transformed to l+delta <= x <= u-delta', for some unknown values delta, delta'. Each atomic guard is shrunk by different parameters, and the tool synthesizes values for these that ensure behaviour preservation.
Using shrinkability analysis, one can make sure that possible behaviours of the system are still present under perturbations. For instance, if clocks are used to model lower and upper bounds (say by l <= x <= u) on possible waiting times, shrinking means to forbid that the system acts on the boundaries of this interval. Thus, shrinkability analysis can complement the analysis by guard enlargement of [DDR05,DDMR08], and make sure that the model is robust to slight removal of behaviour. For example, this can help detect timing anomalies in scheduling, see [BMS12]. See here for an explanation of a timed automaton that is not shrinkable.
Moreover, following the same idea, one can actually use timed automata with shrunk guards to derive an implementation with imprecise clocks. In fact, the behaviour of a shrunk automaton under bounded guard enlargement is included in that of the initial automaton. Shrinkability is then a sufficient condition for the implementability of a timed automaton model. This approach is detailed in [SBM14].
Source code and binaries (Linux i386): shrinktech-1.0.tar.gz
The column sim-graph shows the number of states and the number of transitions of the finite automaton F w.r.t. which the shrinkability is checked. An asterisk indicates bounded shrinkability, where only a portion of the time-abstract bisimulation graph was shown to be simulated by the shrunk automaton.
| Model | states | trans | clocks | sim-graph | time | shrinkable |
| Lip-Sync Prot. (Exact) | 230 | 680 | 5 | 4000/8350* (subgraph) | 9s | No |
| Lip-Sync Prot. (Interval) | 230 | 680 | 5 | 501/1282* (subgraph) | 9s | Yes* |
| Lip-Sync Prot. (Interval) | 230 | 680 | 5 | 4484/48049* (subgraph) | 28s | No |
| Phone Prot. | 11 | 16 | 5 | 63/271 | 0.3s | No |
| Philips Audio Prot. | 446 | 2097 | 2 | 437/2734 | 46s | Yes |
| Root Contention Prot. | 65 | 138 | 6 | 500/3455* (subgraph) | 7s | No |
| Train Gate Controller | 68 | 199 | 11 | 952/8540 | 34s | No |
| Fischer’s Protocol 3 | 152 | 464 | 3 | 472/4321 | 20s | Yes |
| Fischer’s Protocol 4 | 752 | 2864 | 4 | 4382/65821 | 310min | Yes |
| Fischer’s Protocol 5 | 3552 | 16192 | 5 | 10000/10000* (trace) | 42s | Yes* |
| And-Or Circuit | 12 | 20 | 4 | 80/497 | 1.3s | Yes |
| Flip-Flop Circuit | 22 | 34 | 5 | 30/64 | 0.9s | Yes |
| Latch Circuit (Interval) | 32 | 77 | 7 | 105/364 | 1.6s | Yes |
| Latch Circuit (Exact) | 32 | 77 | 7 | 100/331 | 0.6s | No |
[SBM14] Ocan Sankur, Patricia Bouyer, Nicolas Markey. Shrinking timed automata In Information and Computation 234, pages 107 - 132. 2014.
[San13] Ocan Sankur. Shrinktech: A Tool for the Robustness Analysis of Timed Automata In CAV'13 LNCS 8044, pages 1006-1012. Springer, 2013.
[SBM11] O. Sankur, P. Bouyer, N. Markey. Shrinking Timed Automata. FSTTCS 2011.
[BMS12] P. Bouyer, N. Markey, O. Sankur. Robust reachability in timed automata: A game-based approach. ICALP 2012.
[DDR05] M. de Wulf, L. Doyen, J.-F. Raskin. Almost ASAP semantics: From timed models to timed implementations. FAC, 17(3):319-341, 2005
[DDMR08] M. de Wulf, L. Doyen, N. Markey, J.-F. Raskin. Robust safety of timed automata. FMSD, 33(1-3):45-84, 2008.