Malte Lochau

Checking Timed Bisimilarity with Virtual Clocks

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...