---
OA_type: closed access
_id: '4536'
abstract:
- lang: eng
  text: 'We show how to automatically construct and refine rectangular abstractions
    of systems of linear differential equations. From a hybrid automaton whose dynamics
    are given by a system of linear differential equations, our method computes automatically
    a sequence of rectangular hybrid automata that are increasingly precise overapproximations
    of the original hybrid automaton. We prove an optimality criterion for successive
    refinements. We also show that this method can take into account a safety property
    to be verified, refining only relevant parts of the state space. The practicability
    of the method is illustrated on a benchmark case study. '
acknowledgement: Supported in part by the AFOSR MURI grant F49620-00-1-0327 and the
  NSF grants CCR-0208875 and CCR-0225610.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jean
  full_name: Raskin, Jean
  last_name: Raskin
citation:
  ama: 'Doyen L, Henzinger TA, Raskin J. Automatic rectangular refinement of affine
    hybrid systems. In: <i>Proceedings of the Third International Conference on Formal
    Modeling and Analysis of Timed Systems</i>. Vol 3829. Springer Nature; 2005:144-161.
    doi:<a href="https://doi.org/DOI: 10.1007/11603009_13">DOI: 10.1007/11603009_13</a>'
  apa: 'Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2005). Automatic rectangular
    refinement of affine hybrid systems. In <i>Proceedings of the Third international
    conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 3829, pp.
    144–161). Uppsala, Sweden: Springer Nature. <a href="https://doi.org/DOI: 10.1007/11603009_13">https://doi.org/DOI:
    10.1007/11603009_13</a>'
  chicago: 'Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Automatic Rectangular
    Refinement of Affine Hybrid Systems.” In <i>Proceedings of the Third International
    Conference on Formal Modeling and Analysis of Timed Systems</i>, 3829:144–61.
    Springer Nature, 2005. <a href="https://doi.org/DOI: 10.1007/11603009_13">https://doi.org/DOI:
    10.1007/11603009_13</a>.'
  ieee: L. Doyen, T. A. Henzinger, and J. Raskin, “Automatic rectangular refinement
    of affine hybrid systems,” in <i>Proceedings of the Third international conference
    on Formal Modeling and Analysis of Timed Systems</i>, Uppsala, Sweden, 2005, vol.
    3829, pp. 144–161.
  ista: 'Doyen L, Henzinger TA, Raskin J. 2005. Automatic rectangular refinement of
    affine hybrid systems. Proceedings of the Third international conference on Formal
    Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis
    of Timed Systems, LNCS, vol. 3829, 144–161.'
  mla: 'Doyen, Laurent, et al. “Automatic Rectangular Refinement of Affine Hybrid
    Systems.” <i>Proceedings of the Third International Conference on Formal Modeling
    and Analysis of Timed Systems</i>, vol. 3829, Springer Nature, 2005, pp. 144–61,
    doi:<a href="https://doi.org/DOI: 10.1007/11603009_13">DOI: 10.1007/11603009_13</a>.'
  short: L. Doyen, T.A. Henzinger, J. Raskin, in:, Proceedings of the Third International
    Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature,
    2005, pp. 144–161.
conference:
  end_date: 2005-09-28
  location: Uppsala, Sweden
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
  start_date: 2005-09-26
date_created: 2018-12-11T12:09:22Z
date_published: 2005-12-13T00:00:00Z
date_updated: 2026-10-23T08:52:52Z
day: '13'
doi: 'DOI: 10.1007/11603009_13'
extern: '1'
fulldoi: 'https://doi.org/DOI: 10.1007/11603009_13'
intvolume: '      3829'
language:
- iso: eng
month: '12'
oa_version: None
page: 144 - 161
publication: Proceedings of the Third international conference on Formal Modeling
  and Analysis of Timed Systems
publication_identifier:
  eisbn:
  - '9783540316169'
  eissn:
  - 1611-3349
  isbn:
  - '9783540309468'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
publist_id: '190'
status: public
title: Automatic rectangular refinement of affine hybrid systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 3829
year: '2005'
...
---
OA_type: closed access
_id: '4455'
abstract:
- lang: eng
  text: 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.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
  and the NSF grants CCR-0208875, CCR-0225610, and CCR-0427202.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Vinayak
  full_name: Prabhu, Vinayak
  last_name: Prabhu
citation:
  ama: 'Henzinger TA, Majumdar R, Prabhu V. Quantifying similarities between timed
    systems. In: <i>Proceedings of the Third International Conference on Formal Modeling
    and Analysis of Timed Systems</i>. Vol 3829. Springer Nature; 2005:226-241. doi:<a
    href="https://doi.org/10.1007/11603009_18">10.1007/11603009_18</a>'
  apa: 'Henzinger, T. A., Majumdar, R., &#38; Prabhu, V. (2005). Quantifying similarities
    between timed systems. In <i>Proceedings of the Third international conference
    on Formal Modeling and Analysis of Timed Systems</i> (Vol. 3829, pp. 226–241).
    Uppsala, Sweden: Springer Nature. <a href="https://doi.org/10.1007/11603009_18">https://doi.org/10.1007/11603009_18</a>'
  chicago: Henzinger, Thomas A, Ritankar Majumdar, and Vinayak Prabhu. “Quantifying
    Similarities between Timed Systems.” In <i>Proceedings of the Third International
    Conference on Formal Modeling and Analysis of Timed Systems</i>, 3829:226–41.
    Springer Nature, 2005. <a href="https://doi.org/10.1007/11603009_18">https://doi.org/10.1007/11603009_18</a>.
  ieee: T. A. Henzinger, R. Majumdar, and V. Prabhu, “Quantifying similarities between
    timed systems,” in <i>Proceedings of the Third international conference on Formal
    Modeling and Analysis of Timed Systems</i>, Uppsala, Sweden, 2005, vol. 3829,
    pp. 226–241.
  ista: 'Henzinger TA, Majumdar R, Prabhu V. 2005. Quantifying similarities between
    timed systems. Proceedings of the Third international conference on Formal Modeling
    and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis of Timed
    Systems, LNCS, vol. 3829, 226–241.'
  mla: Henzinger, Thomas A., et al. “Quantifying Similarities between Timed Systems.”
    <i>Proceedings of the Third International Conference on Formal Modeling and Analysis
    of Timed Systems</i>, vol. 3829, Springer Nature, 2005, pp. 226–41, doi:<a href="https://doi.org/10.1007/11603009_18">10.1007/11603009_18</a>.
  short: T.A. Henzinger, R. Majumdar, V. Prabhu, in:, Proceedings of the Third International
    Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature,
    2005, pp. 226–241.
conference:
  end_date: 2005-09-28
  location: Uppsala, Sweden
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
  start_date: 2005-09-26
date_created: 2018-12-11T12:08:56Z
date_published: 2005-12-13T00:00:00Z
date_updated: 2026-10-23T09:39:39Z
day: '13'
doi: 10.1007/11603009_18
extern: '1'
fulldoi: https://doi.org/10.1007/11603009_18
intvolume: '      3829'
language:
- iso: eng
month: '12'
oa_version: None
page: 226 - 241
publication: Proceedings of the Third international conference on Formal Modeling
  and Analysis of Timed Systems
publication_identifier:
  eisbn:
  - '9783540316169'
  isbn:
  - '9783540309468'
publication_status: published
publisher: Springer Nature
publist_id: '273'
status: public
title: Quantifying similarities between timed systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 3829
year: '2005'
...