Time-Darts: A Data Structure for Verification of Closed Timed Automata
| Autoři | |
|---|---|
| Rok publikování | 2012 |
| Druh | Článek v odborném periodiku |
| Časopis / Zdroj | Electronic Proceedings of Theoretical Computer Science |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | Web |
| Doi | http://dx.doi.org/10.4204/EPTCS.102.13 |
| Obor | Informatika |
| Klíčová slova | verification; timed automata; reachability; discretization |
| Popis | Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. In comparison, discretization offers an easy alternative, with all operations having linear-time complexity in the number of clocks, and yet valid for a large class of closed systems. Unfortunately, fine-grained discretization causes itself a state-space explosion. We introduce a new data structure called time-darts for the symbolic representation of state-spaces of timed automata. Compared with the complete discretization, a single time-dart allows to represent an arbitrary large set of states, yet the time complexity of operations on time-darts remain linear in the number of clocks. We prove the correctness of the suggested reachability algorithm and perform several experiments in order to compare the performance of time-darts and the complete discretization. The main conclusion is that in all our experiments the time-dart method outperforms the complete discretization and it scales significantly better for models with larger constants. |
| Související projekty: |