{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:51Z","timestamp":1750308711314,"version":"3.41.0"},"reference-count":94,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0820072 and CCF-0926194"],"award-info":[{"award-number":["CCF-0820072 and CCF-0926194"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2014,1]]},"abstract":"<jats:p>Timed automata are state-machine-like structures used to model real-time systems. Since their invention in the early 1990s, a number of often subtly differing variants have appeared in the literature; one of this article\u2019s key contributions is defining, highlighting, and reconciling these differences. The article achieves this by defining a baseline theory of timed automata, characterizing each variant both syntactically and semantically, and giving, when possible, syntactic and semantic conversion to and from the baseline version. This article also surveys various extensions to the basic timed-automaton framework.<\/jats:p>","DOI":"10.1145\/2518102","type":"journal-article","created":{"date-parts":[[2014,2,7]],"date-time":"2014-02-07T14:22:52Z","timestamp":1391782972000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["A menagerie of timed automata"],"prefix":"10.1145","volume":"46","author":[{"given":"Peter","family":"Fontana","sequence":"first","affiliation":[{"name":"University of Maryland, College Park, MD"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, MD"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.018"},{"key":"e_1_2_1_2_1","volume-title":"Timed Automata. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV\u201999)","volume":"1633","author":"Alur Rajeev","year":"1999","unstructured":"Rajeev Alur . 1999 . Timed Automata. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV\u201999) , Nicolas Halbwachs and Doron Peled (Eds.) , Vol. 1633 . Springer, Berlin, 8--22. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-48683-6_3 10.1007\/3-540-48683-6_3 Rajeev Alur. 1999. Timed Automata. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV\u201999), Nicolas Halbwachs and Doron Peled (Eds.), Vol. 1633. Springer, Berlin, 8--22. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-48683-6_3"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113766"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"e_1_2_1_5_1","volume-title":"Dill","author":"Alur Rajeev","year":"1990","unstructured":"Rajeev Alur and David L . Dill . 1990 . Automata for modeling real-time systems. In ICALP\u201990: Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP\u201990), Michael S. Paterson (Ed.), Vol. 443 . Springer , Berlin, 322--335. DOI: http:\/\/dx.doi.org\/10.1007\/BFb0032042 10.1007\/BFb0032042 Rajeev Alur and David L. Dill. 1990. Automata for modeling real-time systems. In ICALP\u201990: Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP\u201990), Michael S. Paterson (Ed.), Vol. 443. Springer, Berlin, 322--335. DOI: http:\/\/dx.doi.org\/10.1007\/BFb0032042"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_5"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.733959"},{"key":"e_1_2_1_11_1","first-page":"83","article-title":"Challenges in timed languages: From applied theory to basic theory","volume":"1","author":"Asarin Eugene","year":"2004","unstructured":"Eugene Asarin . 2004 . Challenges in timed languages: From applied theory to basic theory . Bulletin of the European Association for Theoretical Computer Science 1 , 83 (June 2004), 106--120. Eugene Asarin. 2004. Challenges in timed languages: From applied theory to basic theory. Bulletin of the European Association for Theoretical Computer Science 1, 83 (June 2004), 106--120.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_2_1_12_1","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press , Cambridge, MA . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_13_1","volume-title":"Larsen","author":"Behrmann Gerd","year":"2004","unstructured":"Gerd Behrmann , Alexandre David , and Kim G . Larsen . 2004 . A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems, Marco Bernardo and Flavio Corradini (Eds.). Lecture Notes in Computer Science, Vol. 3185 . Springer , Berlin, 200--236. DOI: http:\/\/dx.doi.org\/10.1007\/b110123 10.1007\/b110123 Gerd Behrmann, Alexandre David, and Kim G. Larsen. 2004. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems, Marco Bernardo and Flavio Corradini (Eds.). Lecture Notes in Computer Science, Vol. 3185. Springer, Berlin, 200--236. DOI: http:\/\/dx.doi.org\/10.1007\/b110123"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561163_8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629335.1629342"},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Computer Science","volume-title":"Lectures on Concurrency and Petri Nets, J\u00f6rg Desel, Wolfgang Reisig, and Grzegorz Rozenberg (Eds.)","author":"Bengtsson Johan","unstructured":"Johan Bengtsson and Wang Yi. 2004. Timed automata: Semantics, algorithms and tools . In Lectures on Concurrency and Petri Nets, J\u00f6rg Desel, Wolfgang Reisig, and Grzegorz Rozenberg (Eds.) . Lecture Notes in Computer Science , Vol. 3098 . Springer , Berlin , 87--124. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-27755-2_3 10.1007\/978-3-540-27755-2_3 Johan Bengtsson and Wang Yi. 2004. Timed automata: Semantics, algorithms and tools. In Lectures on Concurrency and Petri Nets, J\u00f6rg Desel, Wolfgang Reisig, and Grzegorz Rozenberg (Eds.). Lecture Notes in Computer Science, Vol. 3098. Springer, Berlin, 87--124. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00075-2"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/646511.759229"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/305052.305055"},{"volume-title":"Can decision diagrams overcome state space explosion in real-time verification&quest","author":"Beyer Dirk","key":"e_1_2_1_20_1","unstructured":"Dirk Beyer and Andreas Noack . 2003. Can decision diagrams overcome state space explosion in real-time verification&quest ; In Proceedings of the 23rd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201903), Hartmut K\u00f6onig, Monika Heiner, and Adam Wolisz (Eds.). Lecture Notes in Computer Science, Vol. 2767 . Springer , Berlin, 193--208. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-39979-7_13 10.1007\/978-3-540-39979-7_13 Dirk Beyer and Andreas Noack. 2003. Can decision diagrams overcome state space explosion in real-time verification&quest; In Proceedings of the 23rd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201903), Hartmut K\u00f6onig, Monika Heiner, and Adam Wolisz (Eds.). Lecture Notes in Computer Science, Vol. 2767. Springer, Berlin, 193--208. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-39979-7_13"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/646878.710305"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/646738.702093"},{"volume-title":"Untameable timed automata&excl","author":"Bouyer Patricia","key":"e_1_2_1_24_1","unstructured":"Patricia Bouyer . 2003. Untameable timed automata&excl ; In Proceedings of the 20th Annual Symposium on Theoretical Aspects of Computer Science (STACS\u201903), Helmut Alt and Michel Habib (Eds.). Lecture Notes in Computer Science, Vol. 2607 . Springer , Berlin, 620--631. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-36494-3_54 10.1007\/3-540-36494-3_54 Patricia Bouyer. 2003. Untameable timed automata&excl; In Proceedings of the 20th Annual Symposium on Theoretical Aspects of Computer Science (STACS\u201903), Helmut Alt and Michel Habib (Eds.). Lecture Notes in Computer Science, Vol. 2607. Springer, Berlin, 620--631. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-36494-3_54"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.002"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.044"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_13"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-010-9127-4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.003"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2362701.2362702"},{"volume-title":"Model Checking Timed Automata","author":"Bouyer Patricia","key":"e_1_2_1_31_1","unstructured":"Patricia Bouyer and Fran\u00e7ois Laroussinie . 2010. Model Checking Timed Automata . ISTE , London , 111--140. DOI: http:\/\/dx.doi.org\/10.1002\/9780470611012.ch4 10.1002\/9780470611012.ch4 Patricia Bouyer and Fran\u00e7ois Laroussinie. 2010. Model Checking Timed Automata. ISTE, London, 111--140. DOI: http:\/\/dx.doi.org\/10.1002\/9780470611012.ch4"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_10"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the IFIP TC6\/WG6.1\u201421st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201901)","volume":"69","author":"Bowman Howard","year":"2001","unstructured":"Howard Bowman . 2001 . Time and action lock freedom properties for timed automata . In Proceedings of the IFIP TC6\/WG6.1\u201421st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201901) , Myungchui Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee (Eds.) , Vol. 69 . Kluwer, B.V., Deventer, The Netherlands, 119--134. DOI: http:\/\/dx.doi.org\/10.1007\/0-306-47003-9_8 10.1007\/0-306-47003-9_8 Howard Bowman. 2001. Time and action lock freedom properties for timed automata. In Proceedings of the IFIP TC6\/WG6.1\u201421st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201901), Myungchui Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee (Eds.), Vol. 69. Kluwer, B.V., Deventer, The Netherlands, 119--134. DOI: http:\/\/dx.doi.org\/10.1007\/0-306-47003-9_8"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0010-7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646735.701625"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/157485.164585"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_38_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 1999 . Model Checking. MIT Press , Cambridge, MA. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the IEEE Conference on Emerging Technologies and Factory Automation (EFTA\u201907)","author":"Deligiannis V.","year":"2007","unstructured":"V. Deligiannis and S. Manesis . 2007. A survey on automata-based methods for modelling and simulation of industrial systems . In Proceedings of the IEEE Conference on Emerging Technologies and Factory Automation (EFTA\u201907) . IEEE, Piscataway, NJ, 398--405. DOI: http:\/\/dx.doi.org\/10.1109\/EFTA. 2007 .4416795 10.1109\/EFTA.2007.4416795 V. Deligiannis and S. Manesis. 2007. A survey on automata-based methods for modelling and simulation of industrial systems. In Proceedings of the IEEE Conference on Emerging Technologies and Factory Automation (EFTA\u201907). IEEE, Piscataway, NJ, 398--405. DOI: http:\/\/dx.doi.org\/10.1109\/EFTA.2007.4416795"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/646512.695332"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-011-0148-2"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.52"},{"key":"e_1_2_1_43_1","volume-title":"A Mathematical Introduction to Logic","author":"Enderton Herbert B.","unstructured":"Herbert B. Enderton . 2001. A Mathematical Introduction to Logic ( 2 nd ed.). Harcourt\/Academic Press , San Diego, CA . Herbert B. Enderton. 2001. A Mathematical Introduction to Logic (2nd ed.). Harcourt\/Academic Press, San Diego, CA.","edition":"2"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_2"},{"key":"e_1_2_1_45_1","volume-title":"A First Course in Abstract Algebra","author":"Fraleigh John B.","unstructured":"John B. Fraleigh . 1999. A First Course in Abstract Algebra ( 6 th ed.). Addison-Wesley, Boston , MA. John B. Fraleigh. 1999. A First Course in Abstract Algebra (6th ed.). Addison-Wesley, Boston, MA.","edition":"6"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667062.1667063"},{"key":"e_1_2_1_48_1","series-title":"Lecture Notes in Computer Science","volume-title":"Liveness in timed and untimed systems","author":"Gawlick Rainer","unstructured":"Rainer Gawlick , Roberto Segala , J\u00f8rgen S\u00f8gaard-Andersen , and Nancy Lynch . 1994. Liveness in timed and untimed systems . In Automata, Languages and Programming, Serge Abiteboul and Eli Shamir (Eds.). Lecture Notes in Computer Science , Vol. 820 . Springer , Berlin , 166--177. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-58201-0_66 10.1007\/3-540-58201-0_66 Rainer Gawlick, Roberto Segala, J\u00f8rgen S\u00f8gaard-Andersen, and Nancy Lynch. 1994. Liveness in timed and untimed systems. In Automata, Languages and Programming, Serge Abiteboul and Eli Shamir (Eds.). Lecture Notes in Computer Science, Vol. 820. Springer, Berlin, 166--177. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-58201-0_66"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779879.1779894"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779934.1779953"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.09.014"},{"key":"e_1_2_1_52_1","volume-title":"Technical Report ADA462244. Naval Research Laboratory.","author":"Heitmeyer C. L.","year":"1993","unstructured":"C. L. Heitmeyer , B. G. Labaw , and R. D. Jeffords . 1993 . A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems . Technical Report ADA462244. Naval Research Laboratory. C. L. Heitmeyer, B. G. Labaw, and R. D. Jeffords. 1993. A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems. Technical Report ADA462244. Naval Research Laboratory."},{"key":"e_1_2_1_53_1","doi-asserted-by":"crossref","unstructured":"T. A.\n      Henzinger O.\n      Kupferman and \n      M.Y.\n      Vardi\n  . \n  1996\n  . A space-efficient on-the-fly algorithm for real-time model checking. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR\u201996) Ugo Montanari and Vladimiro Sassone (Eds.). Number 1119 in \n  Lecture Notes in Computer Science\n  . \n  Springer Berlin 514--529. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-61604-7_73     10.1007\/3-540-61604-7_73\nT. A. Henzinger O. Kupferman and M.Y. Vardi. 1996. A space-efficient on-the-fly algorithm for real-time model checking. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR\u201996) Ugo Montanari and Vladimiro Sassone (Eds.). Number 1119 in Lecture Notes in Computer Science. Springer Berlin 514--529. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-61604-7_73","DOI":"10.1007\/3-540-61604-7_73"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICA\u201992)","author":"Henzinger T. A.","year":"1992","unstructured":"T. A. Henzinger , X. Nicollin , J. Sifakis , and S. Yovine . 1992. Symbolic model checking for real-time systems . In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICA\u201992) . IEEE, Piscataway, NJ, USA, 394--406. DOI: http:\/\/dx.doi.org\/10.1109\/LICS. 1992 .185551 10.1109\/LICS.1992.185551 T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. 1992. Symbolic model checking for real-time systems. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICA\u201992). IEEE, Piscataway, NJ, USA, 394--406. DOI: http:\/\/dx.doi.org\/10.1109\/LICS.1992.185551"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694456"},{"key":"e_1_2_1_58_1","series-title":"Lecture Notes in Computer Science","volume-title":"Reachability-time games on timed automata","author":"Jurdzi\u0144ski Marcin","unstructured":"Marcin Jurdzi\u0144ski and Ashutosh Trivedi . 2007. Reachability-time games on timed automata . In Automata, Languages and Programming, Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki (Eds.). Lecture Notes in Computer Science , Vol. 4596 . Springer , Berlin , 838--849. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-73420-8_72 10.1007\/978-3-540-73420-8_72 Marcin Jurdzi\u0144ski and Ashutosh Trivedi. 2007. Reachability-time games on timed automata. In Automata, Languages and Programming, Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki (Eds.). Lecture Notes in Computer Science, Vol. 4596. Springer, Berlin, 838--849. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-73420-8_72"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS\u201903)","author":"Kaynar D. K.","year":"2003","unstructured":"D. K. Kaynar , N. Lynch , R. Segala , and F. Vaandrager . 2003. Timed I\/O automata: A mathematical framework for modeling and analyzing real-time systems . In Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS\u201903) . IEEE, Piscataway, NJ, 166--177. DOI: http:\/\/dx.doi.org\/10.1109\/REAL. 2003 .1253264 10.1109\/REAL.2003.1253264 D. K. Kaynar, N. Lynch, R. Segala, and F. Vaandrager. 2003. Timed I\/O automata: A mathematical framework for modeling and analyzing real-time systems. In Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS\u201903). IEEE, Piscataway, NJ, 166--177. DOI: http:\/\/dx.doi.org\/10.1109\/REAL.2003.1253264"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.2200\/S00310ED1V01Y201011DCT005"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.envsoft.2011.08.005"},{"key":"e_1_2_1_62_1","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematical Foundations of Computer Science, Jir\u00ed Wiedermann and Petr H\u00e1jek (Eds.)","author":"Laroussinie Fran\u00e7ois","unstructured":"Fran\u00e7ois Laroussinie , Kim Larsen , and Carsten Weise . 1995. From timed automata to logic\u2014and back . In Mathematical Foundations of Computer Science, Jir\u00ed Wiedermann and Petr H\u00e1jek (Eds.) . Lecture Notes in Computer Science , Vol. 969 . Springer Berlin Heidelberg , Berlin\/ Heidelberg, Germany , 529--539. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-60246-1_158 10.1007\/3-540-60246-1_158 Fran\u00e7ois Laroussinie, Kim Larsen, and Carsten Weise. 1995. From timed automata to logic\u2014and back. In Mathematical Foundations of Computer Science, Jir\u00ed Wiedermann and Petr H\u00e1jek (Eds.). Lecture Notes in Computer Science, Vol. 969. Springer Berlin Heidelberg, Berlin\/Heidelberg, Germany, 529--539. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-60246-1_158"},{"key":"e_1_2_1_63_1","volume-title":"CMC: A tool for compositional model-checking of real-time systems. In Proceedings of the Formal Description Techniques and Protocol Specification","author":"Laroussinie Fran\u00e7ois","year":"1998","unstructured":"Fran\u00e7ois Laroussinie and Kim Guldstrand Larsen . 1998 . CMC: A tool for compositional model-checking of real-time systems. In Proceedings of the Formal Description Techniques and Protocol Specification , Testing and Verification, Stan Budkowski, Ana Cavalli, and Elie Najm (Eds.). Springer US , Philadelphia, PA , 439--456. DOI: http:\/\/dx.doi.org\/10.1007\/978-0-387-35394-4_27 10.1007\/978-0-387-35394-4_27 Fran\u00e7ois Laroussinie and Kim Guldstrand Larsen. 1998. CMC: A tool for compositional model-checking of real-time systems. In Proceedings of the Formal Description Techniques and Protocol Specification, Testing and Verification, Stan Budkowski, Ana Cavalli, and Elie Najm (Eds.). Springer US, Philadelphia, PA, 439--456. DOI: http:\/\/dx.doi.org\/10.1007\/978-0-387-35394-4_27"},{"volume-title":"Mathematical Foundations of Programming Semantics, Stephen Brookes, Michael Main","author":"Larsen Kim","key":"e_1_2_1_64_1","unstructured":"Kim Larsen and Wang Yi. 1994. Time abstracted bisimulation: Implicit specifications and decidability . In Mathematical Foundations of Programming Semantics, Stephen Brookes, Michael Main , Austin Melton , Michael Mislove, and David Schmidt (Eds.). Lecture Notes in Computer Science, Vol. 802 . Springer , Berlin, 160--176. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-58027-1_8 10.1007\/3-540-58027-1_8 Kim Larsen and Wang Yi. 1994. Time abstracted bisimulation: Implicit specifications and decidability. In Mathematical Foundations of Programming Semantics, Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt (Eds.). Lecture Notes in Computer Science, Vol. 802. Springer, Berlin, 160--176. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-58027-1_8"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2623"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/646731.703698"},{"volume-title":"Real-Time: Theory in Practice","author":"Lynch Nancy","key":"e_1_2_1_67_1","unstructured":"Nancy Lynch and Frits Vaandrager . 1992. Forward and backward simulations for timing-based systems . In Real-Time: Theory in Practice , J. de Bakker, C. Huizing, W. de Roever, and G. Rozenberg (Eds.). Lecture Notes in Computer Science, Vol. 600 . Springer , Berlin, 397--446. DOI: http:\/\/dx.doi.org\/10.1007\/BFb0032002 10.1007\/BFb0032002 Nancy Lynch and Frits Vaandrager. 1992. Forward and backward simulations for timing-based systems. In Real-Time: Theory in Practice, J. de Bakker, C. Huizing, W. de Roever, and G. Rozenberg (Eds.). Lecture Notes in Computer Science, Vol. 600. Springer, Berlin, 397--446. DOI: http:\/\/dx.doi.org\/10.1007\/BFb0032002"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211907"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68413-8_6"},{"key":"e_1_2_1_73_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Conference on Concurrency Theory (CONCUR\u201991), Jos Baeten and Jan Groote (Eds.)","author":"Merritt Michael","unstructured":"Michael Merritt , Francesmary Modugno , and Mark Tuttle . 1991. Time-constrained automata . In Proceedings of the Conference on Concurrency Theory (CONCUR\u201991), Jos Baeten and Jan Groote (Eds.) . Lecture Notes in Computer Science , Vol. 527 . Springer , Berlin , 408--423. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-54430-5_103 10.1007\/3-540-54430-5_103 Michael Merritt, Francesmary Modugno, and Mark Tuttle. 1991. Time-constrained automata. In Proceedings of the Conference on Concurrency Theory (CONCUR\u201991), Jos Baeten and Jan Groote (Eds.). Lecture Notes in Computer Science, Vol. 527. Springer, Berlin, 408--423. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-54430-5_103"},{"volume-title":"Communication and Concurrency","author":"Milner R.","key":"e_1_2_1_74_1","unstructured":"R. Milner . 1989. Communication and Concurrency . Prentice-Hall , Upper Saddle River, NJ. R. Milner. 1989. Communication and Concurrency. Prentice-Hall, Upper Saddle River, NJ."},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032355"},{"volume-title":"Real-Time Systems: Formal Specification and Automatic Verification","author":"Olderog Ernst-R\u00fcdiger","key":"e_1_2_1_76_1","unstructured":"Ernst-R\u00fcdiger Olderog and Henning Dierks . 2008. Real-Time Systems: Formal Specification and Automatic Verification . Cambridge University Press , New York, NY . Ernst-R\u00fcdiger Olderog and Henning Dierks. 2008. Real-Time Systems: Formal Specification and Automatic Verification. Cambridge University Press, New York, NY."},{"key":"e_1_2_1_77_1","volume-title":"Applications and Theory of Petri Nets","author":"Penczek Wojciech","year":"2004","unstructured":"Wojciech Penczek and Agata P\u00f3\u0142rola . 2004. Specification and model checking of temporal properties in time Petri nets and timed automata . In Applications and Theory of Petri Nets 2004 , Jordi Cortadella and Wolfgang Reisig (Eds.). Lecture Notes in Computer Science, Vol. 3099 . Springer , Berlin, 37--76. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-27793-4_4 10.1007\/978-3-540-27793-4_4 Wojciech Penczek and Agata P\u00f3\u0142rola. 2004. Specification and model checking of temporal properties in time Petri nets and timed automata. In Applications and Theory of Petri Nets 2004, Jordi Cortadella and Wolfgang Reisig (Eds.). Lecture Notes in Computer Science, Vol. 3099. Springer, Berlin, 37--76. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-27793-4_4"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.1265734"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2671"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.159840"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0118-0"},{"key":"e_1_2_1_82_1","volume-title":"Proceedings of the 7th International Conference on Computer Aided Verification (CAV\u201995)","volume":"939","author":"Oleg","unstructured":"Oleg V. Sokolsky and Scott A. Smolka. 1995. Local model checking for real-time systems . In Proceedings of the 7th International Conference on Computer Aided Verification (CAV\u201995) , Pierre Wolper (Ed.) , Vol. 939 . Springer, Berlin, 211--224. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-60045-0_52 10.1007\/3-540-60045-0_52 Oleg V. Sokolsky and Scott A. Smolka. 1995. Local model checking for real-time systems. In Proceedings of the 7th International Conference on Computer Aided Verification (CAV\u201995), Pierre Wolper (Ed.), Vol. 939. Springer, Berlin, 211--224. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-60045-0_52"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00134-6"},{"key":"e_1_2_1_84_1","volume-title":"Proceedings of the 7th International Conference on Concurrency Theory (CONCUR\u201996)","volume":"1119","author":"Tasiran Serdar","unstructured":"Serdar Tasiran , Rajeev Alur , Robert P. Kurshan , and Robert K. Brayton . 1996. Verifying abstractions of timed systems . In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR\u201996) , Ugo Montanari and Vladimiro Sassone (Eds.) , Vol. 1119 . Springer, Berlin, 546--562. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-61604-7_75 10.1007\/3-540-61604-7_75 Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, and Robert K. Brayton. 1996. Verifying abstractions of timed systems. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR\u201996), Ugo Montanari and Vladimiro Sassone (Eds.), Vol. 1119. Springer, Berlin, 546--562. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-61604-7_75"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507245"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008734703554"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.5555\/646542.696201"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0135-4"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2004.831197"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.68"},{"volume-title":"Wiley Encyclopedia of Computer Science and Engineering","author":"Wang Farn","key":"e_1_2_1_91_1","unstructured":"Farn Wang . 2007. Specification Formalisms and Models . In Wiley Encyclopedia of Computer Science and Engineering , Benjamin Wah (Ed.). John Wiley & Sons , 2775--2789. DOI: http:\/\/dx.doi.org\/10.1002\/9780470050118.ecse410 10.1002\/9780470050118.ecse410 Farn Wang. 2007. Specification Formalisms and Models. In Wiley Encyclopedia of Computer Science and Engineering, Benjamin Wah (Ed.). John Wiley & Sons, 2775--2789. DOI: http:\/\/dx.doi.org\/10.1002\/9780470050118.ecse410"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_24"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.71"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"},{"volume-title":"Lectures on Embedded Systems (Lecture Notes in Computer Science), Grzegorz Rozenberg and Frits W","author":"Yovine Sergio","key":"e_1_2_1_95_1","unstructured":"Sergio Yovine . 1998. Model checking timed automata . In Lectures on Embedded Systems (Lecture Notes in Computer Science), Grzegorz Rozenberg and Frits W . Vaandrager (Eds.), Vol. 1494 . Springer , Berlin , 114--152. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-65193-4_20 10.1007\/3-540-65193-4_20 Sergio Yovine. 1998. Model checking timed automata. In Lectures on Embedded Systems (Lecture Notes in Computer Science), Grzegorz Rozenberg and Frits W. Vaandrager (Eds.), Vol. 1494. Springer, Berlin, 114--152. DOI: http:\/\/dx.doi.org\/10.1007\/3-540-65193-4_20"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562436_8"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.22"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2518102","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2518102","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:13Z","timestamp":1750277653000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2518102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1]]},"references-count":94,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,1]]}},"alternative-id":["10.1145\/2518102"],"URL":"https:\/\/doi.org\/10.1145\/2518102","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"type":"print","value":"0360-0300"},{"type":"electronic","value":"1557-7341"}],"subject":[],"published":{"date-parts":[[2014,1]]},"assertion":[{"value":"2013-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}