Abstract
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.
[45] Verification of Liveness Properties on Closed Timed-Arc Petri Nets
[45] Verification of Liveness Properties on Closed Timed-Arc Petri Nets
Original language | English |
---|---|
Journal | Electronic Proceedings in Theoretical Computer Science |
Volume | 102 |
Pages (from-to) | 141-155 |
Number of pages | 15 |
ISSN | 2075-2180 |
DOIs | |
Publication status | Published - 2012 |
Event | 7th International Conference on Systems Software Verification - NICTA, Sydney, Australia Duration: 28 Nov 2012 → 30 Nov 2012 Conference number: 7 |
Conference
Conference | 7th International Conference on Systems Software Verification |
---|---|
Number | 7 |
Location | NICTA |
Country/Territory | Australia |
City | Sydney |
Period | 28/11/2012 → 30/11/2012 |
Keywords
- timed automata; verification; reachability; discretization