Citation
Tom Henzinger, Rupak Majumdar, Vinayak Prabhu. "Quantifying similarities between timed systems.". Proceedings of the Third International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 3829, Springer, 2005, 226-241, September, 2005.

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

Electronic downloads

• http://mtc.epfl.ch/~tah/Publications/quantifying_similarities_between_timed_systems.html

• HTML

  Tom Henzinger, Rupak Majumdar, Vinayak Prabhu. <a
  href="http://chess.eecs.berkeley.edu/pubs/94.html"
  >Quantifying similarities between timed
  systems.</a>, Proceedings of the Third International
  Conference on Formal Modeling and Analysis of Timed Systems
  (FORMATS), Lecture Notes in Computer Science 3829, Springer,
  2005, 226-241, September, 2005.

• Plain text

  Tom Henzinger, Rupak Majumdar, Vinayak Prabhu.
  "Quantifying similarities between timed systems.".
  Proceedings of the Third International Conference on Formal
  Modeling and Analysis of Timed Systems (FORMATS), Lecture
  Notes in Computer Science 3829, Springer, 2005, 226-241,
  September, 2005.

• BibTeX

  @inproceedings{HenzingerMajumdarPrabhu05_QuantifyingSimilaritiesBetweenTimedSystems,
      author = {Tom Henzinger and Rupak Majumdar and Vinayak Prabhu},
      title = {Quantifying similarities between timed systems.},
      booktitle = {Proceedings of the Third International Conference
                on Formal Modeling and Analysis of Timed Systems
                (FORMATS), Lecture Notes in Computer Science 3829,
                Springer, 2005},
      pages = {226-241},
      month = {September},
      year = {2005},
      abstract = {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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/94.html}
  }
  

Posted by Vinayak Prabhu on 12 May 2006.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.