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

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JOERGENSEN Kenneth Yrke LARSEN Kim G. SRBA Jiří

Year of publication 2012
Type Article in Periodical
Magazine / Source Electronic Proceedings of Theoretical Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Web Web
Doi http://dx.doi.org/10.4204/EPTCS.102.13
Field Informatics
Keywords verification; timed automata; reachability; discretization
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info