[{"language":[{"iso":"eng"}],"month":"12","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"None","title":"Automatic rectangular refinement of affine hybrid systems","publisher":"Springer Nature","_id":"4536","date_updated":"2026-10-23T08:52:52Z","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","doi":"DOI: 10.1007/11603009_13","citation":{"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.","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>.","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>","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>.","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>"},"publication_identifier":{"eisbn":["9783540316169"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783540309468"]},"abstract":[{"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. ","lang":"eng"}],"volume":3829,"OA_type":"closed access","author":[{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"}],"day":"13","page":"144 - 161","date_created":"2018-12-11T12:09:22Z","date_published":"2005-12-13T00:00:00Z","intvolume":"      3829","status":"public","year":"2005","extern":"1","type":"conference","conference":{"location":"Uppsala, Sweden","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","end_date":"2005-09-28","start_date":"2005-09-26"},"publist_id":"190","publication_status":"published","fulldoi":"https://doi.org/DOI: 10.1007/11603009_13","publication":"Proceedings of the Third international conference on Formal Modeling and Analysis of Timed Systems"},{"date_created":"2018-12-11T12:08:56Z","date_published":"2005-12-13T00:00:00Z","intvolume":"      3829","status":"public","extern":"1","year":"2005","type":"conference","conference":{"location":"Uppsala, Sweden","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","end_date":"2005-09-28","start_date":"2005-09-26"},"publist_id":"273","publication_status":"published","fulldoi":"https://doi.org/10.1007/11603009_18","publication":"Proceedings of the Third international conference on Formal Modeling and Analysis of Timed Systems","volume":3829,"OA_type":"closed access","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"},{"first_name":"Vinayak","full_name":"Prabhu, Vinayak","last_name":"Prabhu"}],"day":"13","page":"226 - 241","title":"Quantifying similarities between timed systems","_id":"4455","publisher":"Springer Nature","date_updated":"2026-10-23T09:39:39Z","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","doi":"10.1007/11603009_18","citation":{"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>","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>.","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.","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.","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>","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.","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>."},"abstract":[{"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.","lang":"eng"}],"publication_identifier":{"isbn":["9783540309468"],"eisbn":["9783540316169"]},"language":[{"iso":"eng"}],"month":"12","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"None"}]