Clock Reduction in Timed Automata while Preserving Design Parameters
Timed automata (TA) are widely used to model and verify real-time systems. In a TA, the real valued variables, called clocks, measure the time passed between events. The verification of TA is exponential in the number of clocks. That constitutes a bottleneck for its application in large systems. To address this issue, we propose a novel clock reduction method. We aim at reducing the number of clocks by developing a position (location and transition) based mapping for clocks. Motivated by that the locations and transitions of the automaton reflect the modeled system’s physical properties and design parameters; the proposed method changes the clock constraints based on their positions to reduce the total number of clocks. To guarantee correctness, we prove that the resulting automaton is timed bisimilar to the original one. Finally, we present empirical results for the solution, which show that the proposed method significantly reduces the clock count without changing design parameters of the system.
Mon 27 MayDisplayed time zone: Eastern Time (US & Canada) change
08:40 - 10:30 | |||
08:40 10mDay opening | Welcome by the Chairs FormaliSE | ||
08:50 25mFull-paper | Epistemic Model Checking of Distributed Commit Protocols with Byzantine faults FormaliSE | ||
09:15 25mFull-paper | Clock Reduction in Timed Automata while Preserving Design Parameters FormaliSE Beyazit Yalcinkaya Middle East Technical University, Ebru Aydin Gol Middle East Technical University | ||
09:40 25mFull-paper | Rigorous Design and Deployment of IoT Applications FormaliSE Ajay Krishna Inria Grenoble, France, Michel Le Pallec Nokia Bell Labs, Radu Mateescu INRIA, Ludovic Noirie Nokia Bell Labs, Gwen Salaün University of Grenoble Alpes | ||
10:05 25mFull-paper | Static Analysis for Worst-Case Battery Utilization FormaliSE |