Efficient Scaling-Invariant Checking of Timed Bisimulation

摘要

Bisimulation is an important notion for the verification of distributed systems. Timed bisimulation is its natural extension to real tiem 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.