## Quantifying Similarities between Timed Systems

*
Thomas A. Henzinger,
Rupak Majumdar, and Vinayak Prabhu*

We define quantitative similarity functions between timed transition
systems that measure the degree of closeness of two systems as a real,
in contrast to the traditional boolean yes/no approach to timed
simulation and language inclusion. Two systems are close if for each
timed trace of one system, there exists a corresponding timed trace in
the other system with the same sequence of events and closely
corresponding event timings. We show that timed CTL is robust with
respect to our quantitative version of bisimilarity, in particular, if
a system satisfies a formula, then every close system satisfies a
close formula. We also define a discounted version of CTL over timed
systems, which assigns to every CTL formula a real value that is
obtained by discounting real time. We prove the robustness of
discounted CTL by establishing that close states in the bisimilarity
metric have close values for all discounted CTL formulas.

*Proceedings of the Third International Conference on
Formal Modeling and Analysis of Timed Systems*
(FORMATS),
Lecture Notes in Computer Science 3829,
Springer, 2005, pp. 226-241.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2005 Springer.