{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T10:30:21Z","timestamp":1777113021014,"version":"3.51.4"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"S2","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>We consider verification problems for transition systems enriched with a metric structure. We believe that these metric transition systems are particularly suitable for the analysis of cyber-physical systems in which metrics can be naturally defined on the numerical variables of the embedded software and on the continuous states of the physical environment. We consider verification of bounded and unbounded safety properties, as well as bounded liveness properties. The transition systems we consider are nondeterministic, finitely branching, and with a finite set of initial states. Therefore, bounded safety\/liveness properties can always be verified by exhaustive exploration of the system trajectories. However, this approach may be intractable in practice, as the number of trajectories usually grows exponentially with respect to the considered bound. Furthermore, since the system we consider can have an infinite set of states, exhaustive exploration cannot be used for unbounded safety verification. For bounded safety properties, we propose an algorithm which combines exploration of the system trajectories and state space reduction using merging based on a bisimulation metric. The main novelty compared to an algorithm presented recently by Lerda et al. [2008] consists in introducing a tuning parameter that improves the performance drastically. We also establish a procedure that allows us to prove unbounded safety from the result of the bounded safety algorithm via a refinement step. We then adapt the algorithm to handle bounded liveness verification. Finally, the effectiveness of the approach is demonstrated by applying it to the analysis of implementations of an embedded control loop.<\/jats:p>","DOI":"10.1145\/2331147.2331164","type":"journal-article","created":{"date-parts":[[2012,9,11]],"date-time":"2012-09-11T22:21:06Z","timestamp":1347402066000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Verification of Safety and Liveness Properties of Metric Transition Systems"],"prefix":"10.1145","volume":"11","author":[{"given":"Antoine","family":"Girard","sequence":"first","affiliation":[{"name":"Laboratoire Jean Kuntzmann, Universit\u00e9 de Grenoble"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gang","family":"Zheng","sequence":"additional","affiliation":[{"name":"Project ALIEN, INRIA Lille-Nord Europe"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"2623","author":"Alur R.","unstructured":"Alur , R. , Dang , T. , and Ivancic , F . 2003. Progress on reachability analysis of hybrid systems using predicate abstraction . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 2623 . Springer, Berlin, 4--19. Alur, R., Dang, T., and Ivancic, F. 2003. Progress on reachability analysis of hybrid systems using predicate abstraction. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2623. Springer, Berlin, 4--19."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2009.40"},{"key":"e_1_2_1_4_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Ssience","volume":"1790","author":"Asarin E.","unstructured":"Asarin , E. , Dang , T. , Maler , O. , and Bournez , O . 2000. Approximate reachability analysis of piecewise-linear dynamical systems . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Ssience , vol. 1790 . Springer, Berlin, 20--31. Asarin, E., Dang, T., Maler, O., and Bournez, O. 2000. Approximate reachability analysis of piecewise-linear dynamical systems. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Ssience, vol. 1790. Springer, Berlin, 20--31."},{"key":"e_1_2_1_5_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"1569","author":"Chutinan A.","unstructured":"Chutinan , A. and Krogh , B. H . 1999. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 1569 . Springer, Berlin, 76--90. Chutinan, A. and Krogh, B. H. 1999. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1569. Springer, Berlin, 76--90."},{"key":"e_1_2_1_6_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 2000. Model Checking. MIT Press Cambridge MA. Clarke E. M. Grumberg O. and Peled D. 2000. Model Checking . MIT Press Cambridge MA."},{"key":"e_1_2_1_7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. Lecture Note in Computer Science","volume":"2619","author":"Clarke E. M.","unstructured":"Clarke , E. M. , Fehnker , A. , Han , Z. , Krogh , B. H. , Stursberg , O. , and Theobald , M . 2003. Verification of hybrid systems based on counterexample-guided abstraction refinement . In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Note in Computer Science , vol. 2619 . Springer, Berlin, 192--207. Clarke, E. M., Fehnker, A., Han, Z., Krogh, B. H., Stursberg, O., and Theobald, M. 2003. Verification of hybrid systems based on counterexample-guided abstraction refinement. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Note in Computer Science, vol. 2619. Springer, Berlin, 192--207."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science","volume":"3142","author":"de Alfaro L.","unstructured":"de Alfaro , L. , Faella , M. , and Stoelinga , M . 2004. Linear and branching metrics for quantitative transition systems . In Proceedings of the International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science , vol. 3142 . Springer, Berlin, 97--109. de Alfaro, L., Faella, M., and Stoelinga, M. 2004. Linear and branching metrics for quantitative transition systems. In Proceedings of the International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 3142. Springer, Berlin, 97--109."},{"key":"e_1_2_1_9_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"4416","author":"Donz\u00e9 A.","unstructured":"Donz\u00e9 , A. and Maler , O . 2007. Systematic simulation using sensitivity analysis . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 4416 . Springer, Berlin, 174--189. Donz\u00e9, A. and Maler, O. 2007. Systematic simulation using sensitivity analysis. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 4416. Springer, Berlin, 174--189."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_22"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.895849"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_21"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00602-9_16"},{"key":"e_1_2_1_18_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"4416","author":"Julius A. A.","unstructured":"Julius , A. A. , Fainekos , G. E. , Anand , M. , Lee , I. , and Pappas , G. J . 2007. Robust test generation and coverage for hybrid systems . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 4416 . Springer, Berlin, 329--342. Julius, A. A., Fainekos, G. E., Anand, M., Lee, I., and Pappas, G. J. 2007. Robust test generation and coverage for hybrid systems. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 4416. Springer, Berlin, 329--342."},{"key":"e_1_2_1_19_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"2623","author":"Kapinski J.","unstructured":"Kapinski , J. , Krogh , B. H. , Maler , O. , and Stursberg , O . 2003. On systematic simulation of open continuous systems . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 2623 . Springer, Berlin, 283--297. Kapinski, J., Krogh, B. H., Maler, O., and Stursberg, O. 2003. On systematic simulation of open continuous systems. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2623. Springer, Berlin, 283--297."},{"key":"e_1_2_1_20_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"1790","author":"Kurzhanski A. B.","unstructured":"Kurzhanski , A. B. and Varaiya , P . 2000. Ellipsoidal techniques for reachability analysis . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 1790 . Springer, Berlin, 202--214. Kurzhanski, A. B. and Varaiya, P. 2000. Ellipsoidal techniques for reachability analysis. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1790. Springer, Berlin, 202--214."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_40"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_25"},{"key":"e_1_2_1_23_1","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science","volume":"2469","author":"Maler O.","unstructured":"Maler , O. , Krogh , B. H. , and Mahfoudh , M . 2002. On control with bounded computational resources . In Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science , vol. 2469 . Springer, Berlin, 147--164. Maler, O., Krogh, B. H., and Mahfoudh, M. 2002. On control with bounded computational resources. In Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 2469. Springer, Berlin, 147--164."},{"key":"e_1_2_1_24_1","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"Milner , R. 1989. Communication and Concurrency . Prentice Hall , Upper Saddle River, NJ. Milner, R. 1989. Communication and Concurrency. Prentice Hall, Upper Saddle River, NJ."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_17"},{"key":"e_1_2_1_26_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"2993","author":"Prajna S.","unstructured":"Prajna , S. and Jadbabaie , A . 2004. Safety verification of hybrid systems using barrier certificates . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 2993 . Springer, Berlin, 477--492. Prajna, S. and Jadbabaie, A. 2004. Safety verification of hybrid systems using barrier certificates. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2993. Springer, Berlin, 477--492."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_37"},{"key":"e_1_2_1_28_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"2993","author":"Sankaranarayanan S.","unstructured":"Sankaranarayanan , S. , Sipma , H. , and Manna , Z . 2004. Constructing invariants for hybrid systems . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 2993 . Springer, Berlin 539--554. Sankaranarayanan, S., Sipma, H., and Manna, Z. 2004. Constructing invariants for hybrid systems. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2993. Springer, Berlin 539--554."},{"key":"e_1_2_1_29_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"2623","author":"Stursberg O.","unstructured":"Stursberg , O. and Krogh , B. H . 2003. Efficient representation and computation of reachable sets for hybrid systems . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 2623 . Springer, Berlin, 482--497. Stursberg, O. and Krogh, B. H. 2003. Efficient representation and computation of reachable sets for hybrid systems. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2623. Springer, Berlin, 482--497."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2003.814621"},{"key":"e_1_2_1_32_1","volume-title":"Hybrid Systems: Computation and Control. Lecture Notes in Computer Science","volume":"4416","author":"Weiss G.","unstructured":"Weiss , G. and Alur , R . 2007. Automata based interfaces for control and scheduling . In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science , vol. 4416 . Springer, Berlin, 601--613. Weiss, G. and Alur, R. 2007. Automata based interfaces for control and scheduling. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 4416. Springer, Berlin, 601--613."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.35"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00602-9_30"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2331147.2331164","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2331147.2331164","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:48:50Z","timestamp":1750236530000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2331147.2331164"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":34,"journal-issue":{"issue":"S2","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1145\/2331147.2331164"],"URL":"https:\/\/doi.org\/10.1145\/2331147.2331164","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8]]},"assertion":[{"value":"2009-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}