Checking Timed Bisimilarity with Virtual Clocks

TL;DR

This paper introduces a novel zone-based method using virtual clocks for checking timed bisimilarity in timed automata, offering a more efficient alternative to traditional region graphs.

Contribution

It proposes a new semantics representation for timed automata with virtual clocks, enabling more practical and efficient timed bisimilarity checking.

Findings

The new method produces significantly smaller state representations than region graphs.

Experimental results demonstrate the efficiency of the approach on common timed automata models.

No existing practical tool for automated timed bisimilarity checking was available before this work.

Abstract

Timed automata are a widely used formalism for specifying the discrete-state/continuous-time behavior of time-critical reactive systems. For the fundamental verification problem of comparing two timed automata, it has been shown that timed trace equivalence is undecidable, while timed bisimulation is decidable. The corresponding decidability proof uses region graphs, a finite but space-consuming characterization of timed automata semantics. Most verification tools use zone graphs instead, a symbolic and, on average, more space-efficient representation of timed automata semantics. However, zone graphs provide correct results only for those verification tasks that are reducible to reachability problems, and are too imprecise for timed bisimilarity checking. To the best of our knowledge, there is currently no practical tool for automated timed bisimilarity checking. In this paper, we propose a new representation of timed automata semantics that extends zone graphs by so-called virtual clocks. Our zone-based construction is, on average, significantly smaller than the corresponding region graph representation. We also present experimental results obtained by applying our tool implementation to timed automata models, which are often used to evaluate timed automata analysis techniques.