Time-Darts: A Data Structure for Verification of Closed Timed Automata

Varování

Publikace nespadá pod Fakultu sportovních studií, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JOERGENSEN Kenneth Yrke LARSEN Kim G. SRBA Jiří

Rok publikování 2012
Druh Článek v odborném periodiku
Časopis / Zdroj Electronic Proceedings of Theoretical Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info