Clock Reduction in Timed Automata While Preserving Design Parameters

Yancinkaya B., Aydın Göl E.

2019 IEEE/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE), Montreal, Canada, 27 May 2019 identifier identifier

  • Publication Type: Conference Paper / Full Text
  • Doi Number: 10.1109/formalise.2019.00010
  • City: Montreal
  • Country: Canada
  • Keywords: timed automata, clock reduction, bisimulation
  • Middle East Technical University Affiliated: Yes


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.