Witnesses and Counterexamples for Timed Bisimulation

Alexander Lieb, Malte Lochau

Timed automata provide a modeling formalism for time-critical properties of reactive systems with discrete-state/continuous-time behaviors. To handle the infinite state space of ti…