Bisimulation is an important notion for the verification of distributed systems. Timed bisimulation is its natural extension to real time systems. Timed bisimulation is known to be decidable for timed automata using the so-called region technique. We present a new, top down approach to timed bisimulation which applies the zone technique from the theory of hybrid systems. In contrast to the original decision algorithm, our method has a better space complexity and is scaling invariant: altering the time scale does not effect the space complexity.
Keywords algorithms and data structures - automata and formal languages - program specification and verification - decidability - real-time systems