Abstract | ||
---|---|---|
Quasi-equal clocks reduction for networks of timed automata yields significant savings in verification costs of properties of timed automata by replacing clocks in equivalence classes by representative clocks. In this work we present the theoretical analysis that quantifies and justifies those savings. We propose new space and time bounds that characterise a less expensive model checking effort in transformed networks wrt. The effort in original networks with quasi-equal clocks. Additionally, we carry out improvements to our transformation algorithm in order to maximize savings wrt. Space and time, and we eliminate all remaining semantic assumptions on networks introduced to soundly apply the reduction of clocks. |
Year | DOI | Venue |
---|---|---|
2016 | 10.1109/TIME.2016.10 | 2016 23rd International Symposium on Temporal Representation and Reasoning (TIME) |
Keywords | Field | DocType |
Quasi-Equal Clocks,Model Checking,Space Complexity,Time Complexity,Networks of Timed Automata,State-Space Explotion | Synchronization,Model checking,Computer science,Spacetime,Automaton,Transformation algorithm,Theoretical computer science,Equivalence class,Cost accounting,Benchmark (computing) | Conference |
ISBN | Citations | PageRank |
978-1-5090-3826-8 | 0 | 0.34 |
References | Authors | |
8 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Christian Herrera | 1 | 18 | 2.42 |
Bernd Westphal | 2 | 65 | 4.39 |