{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T10:37:13Z","timestamp":1774262233114,"version":"3.50.1"},"reference-count":156,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2010,2]]},"abstract":"<jats:p>The increasing relevance of areas such as real-time and embedded systems, pervasive computing, hybrid systems control, and biological and social systems modeling is bringing a growing attention to the temporal aspects of computing, not only in the computer science domain, but also in more traditional fields of engineering.<\/jats:p><jats:p>This article surveys various approaches to the formal modeling and analysis of the temporal features of computer-based systems, with a level of detail that is also suitable for nonspecialists. In doing so, it provides a unifying framework, rather than just a comprehensive list of formalisms.<\/jats:p><jats:p>The article first lays out some key dimensions along which the various formalisms can be evaluated and compared. Then, a significant sample of formalisms for time modeling in computing are presented and discussed according to these dimensions. The adopted perspective is, to some extent, historical, going from \u201ctraditional\u201d models and formalisms to more modern ones.<\/jats:p>","DOI":"10.1145\/1667062.1667063","type":"journal-article","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T19:20:32Z","timestamp":1267557632000},"page":"1-59","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Modeling time in computing"],"prefix":"10.1145","volume":"42","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[{"name":"ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dino","family":"Mandrioli","sequence":"additional","affiliation":[{"name":"Politecnico di Milano"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Morzenti","sequence":"additional","affiliation":[{"name":"Politecnico di Milano"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[{"name":"Politecnico di Milano"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,3,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186058"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Alur R. and Madhusudan P . 2004 . Decision problems for timed automata: A survey. In Revised Lectures from the International School on Formal Methods for the Design of Computer Communication and Software Systems: Formal Methods for the Design of Real-Time Systems (SFM--RT'04) M. Bernardo and F. Corradini Eds. Lecture Notes in Computer Science vol. 3185 Springer Berlin 1--24. Alur R. and Madhusudan P. 2004. Decision problems for timed automata: A survey. In Revised Lectures from the International School on Formal Methods for the Design of Computer Communication and Software Systems: Formal Methods for the Design of Real-Time Systems (SFM--RT'04) M. Bernardo and F. Corradini Eds. Lecture Notes in Computer Science vol. 3185 Springer Berlin 1--24.","DOI":"10.1007\/978-3-540-30080-9_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Alur R. and Kurshan R. P . 1995 . Timing analysis in COSPAN. In Proceedings of the 3rd DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems. R. Alur et al. Eds. Lecture Notes in Computer Science vol. 1066 Springer Berlin 220--231. Alur R. and Kurshan R. P. 1995. Timing analysis in COSPAN. In Proceedings of the 3rd DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems. R. Alur et al. Eds. Lecture Notes in Computer Science vol. 1066 Springer Berlin 220--231.","DOI":"10.1007\/BFb0020948"},{"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\/174644.174651"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1025"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Alur R. Courcoubetis C. Henzinger T. A. and Ho P . -H . 1993 . Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems R. L. Grossman et al. Eds. Lecture Notes in Computer Science vol. 736 Springer Berlin 209--229. Alur R. Courcoubetis C. Henzinger T. A. and Ho P.-H. 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems R. L. Grossman et al. Eds. Lecture Notes in Computer Science vol. 736 Springer Berlin 209--229.","DOI":"10.1007\/3-540-57318-6_30"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1992.267774"},{"key":"e_1_2_1_12_1","volume-title":"Real Time: Theory in Practice. Lecture Notes in Computer Science","volume":"600","author":"Alur R."},{"key":"e_1_2_1_13_1","volume-title":"Proc. IEEE 88","author":"Antsaklis P. J.","year":"2000"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018913028597"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the IEEE Real Time Technology and Applications Symposium. IEEE","author":"Archer M."},{"key":"e_1_2_1_16_1","first-page":"106","article-title":"Challenges in timed languages: From applied theory to basic theory","volume":"83","author":"Asarin E.","year":"2004","journal-title":"Bull. EATCS"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/506147.506151"},{"key":"e_1_2_1_18_1","series-title":"BRICS Notes Series","volume-title":"Process Algebra: Open Problems and Future Directions, L. Aceto et al. Eds.","author":"Baeten J. C. M."},{"key":"e_1_2_1_19_1","unstructured":"Baeten J. C. M. 2004. A brief history of process algebra. Tech. rep. CSR 04--02 Department of Mathematics and Computer Science Technische Universiteit Eindhoven. Baeten J. C. M. 2004. A brief history of process algebra. Tech. rep. CSR 04--02 Department of Mathematics and Computer Science Technische Universiteit Eindhoven."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Baeten J. C. M. and Middelburg C. A. 2002. Process Algebra with Timing. Monographs in Theoretical Computer Science. Springer Berlin. Baeten J. C. M. and Middelburg C. A. 2002. Process Algebra with Timing. Monographs in Theoretical Computer Science. Springer Berlin.","DOI":"10.1007\/978-3-662-04995-2"},{"key":"e_1_2_1_21_1","volume-title":"Process Algebra. Cambridge Tracts in Theoretical Computer Science","volume":"18","author":"Baeten J. C. M."},{"key":"e_1_2_1_22_1","volume-title":"Selected Papers by Hans Bekific","author":"Bekic H."},{"key":"e_1_2_1_23_1","unstructured":"Bekic H. 1971. Towards a mathematical theory of processes. Tech. rep. 25.125 IBM Laboratory Vienna. Published in Bekic {1984}. Bekic H. 1971. Towards a mathematical theory of processes. Tech. rep. 25.125 IBM Laboratory Vienna. Published in Bekic {1984}."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/349194.349197"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Bengtsson J. and Yi W . 2004 . Timed automata: Semantics algorithms and tools. In Lectures on Concurrency and Petri Nets Advances in Petri Nets (ACPN'03) J. Desel et al. Eds. Lecture Notes in Computer Science vol. 3098 . Springer Berlin 87--124. Bengtsson J. and Yi W. 2004. Timed automata: Semantics algorithms and tools. In Lectures on Concurrency and Petri Nets Advances in Petri Nets (ACPN'03) J. Desel et al. Eds. Lecture Notes in Computer Science vol. 3098. Springer Berlin 87--124.","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"e_1_2_1_26_1","unstructured":"Bergstra J. A. Ponse A. and Smolka S. A. (eds.). 2001. Handbook of Process Algebra. Elsevier Amsterdam. Bergstra J. A. Ponse A. and Smolka S. A. (eds.). 2001. Handbook of Process Algebra. Elsevier Amsterdam."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.75415"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00)","volume":"1855","author":"Bienmuller T."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008700623084"},{"key":"e_1_2_1_31_1","unstructured":"Booch G. and Bryan D. 1994. Software Engineering with ADA. Addison-Wesley Reading MA. Booch G. and Bryan D. 1994. Software Engineering with ADA. Addison-Wesley Reading MA."},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. and St\u00e4rk R. F. 2003. Abstract State Machines. A Method for High--Level System Design and Analysis. Springer Berlin. B\u00f6rger E. and St\u00e4rk R. F. 2003. Abstract State Machines. A Method for High--Level System Design and Analysis. Springer Berlin.","DOI":"10.1007\/978-3-642-18216-7"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11590156_35"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Bozga M. Graf S. Ober I. Ober I. and Sifakis J . 2004 . The IF toolset. In Revised Lectures from the International School on Formal Methods for the Design of Computer Communication and Software Systems: Formal Methods for the Design of Real-Time Systems (SFM-RT'04) M. Bernardo and F. Corradini (Eds.) Lecture Notes in Computer Sciences Vol. 3185 . Springer Berlin 237--267. Bozga M. Graf S. Ober I. Ober I. and Sifakis J. 2004. The IF toolset. In Revised Lectures from the International School on Formal Methods for the Design of Computer Communication and Software Systems: Formal Methods for the Design of Real-Time Systems (SFM-RT'04) M. Bernardo and F. Corradini (Eds.) Lecture Notes in Computer Sciences Vol. 3185. Springer Berlin 237--267.","DOI":"10.1007\/978-3-540-30080-9_8"},{"key":"e_1_2_1_35_1","unstructured":"Brainerd W. S. and Landweber L. H. 1974. Theory of Computation. Wiley New York. Brainerd W. S. and Landweber L. H. 1974. Theory of Computation. Wiley New York."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.654885"},{"key":"e_1_2_1_37_1","first-page":"1989","article-title":"Information processing systems. Open systems interconnection (LOTOS). A formal description technique based on the temporal ordering of observational behaviour","volume":"8807","author":"Brinksma E.","year":"1989","journal-title":"ISO. ISO"},{"key":"e_1_2_1_38_1","unstructured":"Burns A. and Baxter G. 2006. Time bands in systems structure. In Structure for Dependability D. Besnard et al. Eds. Springer Berlin. Burns A. and Baxter G. 2006. Time bands in systems structure. In Structure for Dependability D. Besnard et al. Eds. Springer Berlin."},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Cassandras C. G. and Lafortune S. 1999. Introduction to Discrete Event Systems. Kluwer Academic Amsterdam. Cassandras C. G. and Lafortune S. 1999. Introduction to Discrete Event Systems. Kluwer Academic Amsterdam.","DOI":"10.1007\/978-1-4757-4070-7"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Cassez F. Henzinger T. A. and Raskin J . -F . 2002 . A comparison of control problems for timed and hybrid systems. In Proceedings of the 5th International Workshop on Hybrid Systems : Computation and Control (HSCC'02). C. Tomlin and M.R. Greenstreet Eds. Lecture Notes in Computer Science vol. 2289 Springer Berlin 134--148. Cassez F. Henzinger T. A. and Raskin J.-F. 2002. A comparison of control problems for timed and hybrid systems. In Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control (HSCC'02). C. Tomlin and M.R. Greenstreet Eds. Lecture Notes in Computer Science vol. 2289 Springer Berlin 134--148.","DOI":"10.1007\/3-540-45873-5_13"},{"key":"e_1_2_1_41_1","unstructured":"Cerone A. 1993. A net-based approach for specifying real-time systems. PhD dissertation Universit\u00e0 degli Studi di Pisa Dip. di Informatica. TD--16\/93. Cerone A. 1993. A net-based approach for specifying real-time systems. PhD dissertation Universit\u00e0 degli Studi di Pisa Dip. di Informatica. TD--16\/93."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00008-5"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_2_1_44_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 2000. Model Checking. MIT Press Cambridge MA. Clarke E. M. Grumberg O. and Peled D. A. 2000. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.25088\/ComplexSystems.15.1.1","article-title":"Universality in elementary cellular automata","volume":"15","author":"Cook M.","year":"2004","journal-title":"Complex Syst."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 6th International Workshop on Software Specification and Design. 92--101","author":"Corsetti E."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.07.002"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00169-J"},{"key":"e_1_2_1_49_1","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E. A."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_51_1","unstructured":"Eriksson H.-E. Penker M. Lyons B. and Fado D. 2003. UML 2 Toolkit. Wiley New York. Eriksson H.-E. Penker M. Lyons B. and Fado D. 2003. UML 2 Toolkit. Wiley New York."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.265634"},{"key":"e_1_2_1_53_1","doi-asserted-by":"crossref","unstructured":"Flake S. and Mueller W . 2002 . An OCL extension for real--time constraints. In Object Modeling with the OCL T. Clark and J. Warmer Eds. Lecture Notes in Computer Science vol. 2263 Springer Berlin 150--171. Flake S. and Mueller W. 2002. An OCL extension for real--time constraints. In Object Modeling with the OCL T. Clark and J. Warmer Eds. Lecture Notes in Computer Science vol. 2263 Springer Berlin 150--171.","DOI":"10.1007\/3-540-45669-4_8"},{"key":"e_1_2_1_54_1","doi-asserted-by":"crossref","unstructured":"Francez N. 1986. Fairness. Monographs in Computer Science. Springer Berlin. Francez N. 1986. Fairness. Monographs in Computer Science. Springer Berlin.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/1423684.1423699"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459358"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_16"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567462"},{"key":"e_1_2_1_59_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of Temporal Logic in Specification (TLS'87), B. Banieqbal et al. Eds.","author":"Gabbay D. M."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2006.8"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/383876.383877"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2779"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062578"},{"key":"e_1_2_1_64_1","unstructured":"Ghezzi C. Jazayeri M. and Mandrioli D. 2002. Fundamentals of Software Engineering 2nd ed. Prentice Hall Englewood Cliffs NJ. Ghezzi C. Jazayeri M. and Mandrioli D. 2002. Fundamentals of Software Engineering 2nd ed. Prentice Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.67597"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(90)90074-V"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940078"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.54292"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the 2nd IEEE Symposium on Logic in Computer Science (LICS'87)","author":"Harel D."},{"key":"e_1_2_1_72_1","unstructured":"Heitmeyer C. L. and Mandrioli D. (Eds.). 1996. Formal Methods for Real-Time Computing. Wiley New York. Heitmeyer C. L. and Mandrioli D. (Eds.). 1996. Formal Methods for Real-Time Computing. Wiley New York."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701319"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370629.2370631"},{"key":"e_1_2_1_79_1","unstructured":"Hoare C. A. R. 1985. Communicating Sequential Processes. Prentice Hall Englewood Cliffs NJ. Hoare C. A. R. 1985. Communicating Sequential Processes. Prentice Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_81_1","unstructured":"Holzmann G. J. 2003. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Reading MA. Holzmann G. J. 2003. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Reading MA."},{"key":"e_1_2_1_82_1","doi-asserted-by":"crossref","unstructured":"Hopcroft J. E. Motwani R. and Ullman J. D. 2000. Introduction to Automata Theory Languages and Computation 2nd ed. Addison-Wesley Reading MA. Hopcroft J. E. Motwani R. and Ullman J. D. 2000. Introduction to Automata Theory Languages and Computation 2nd ed. Addison-Wesley Reading MA.","DOI":"10.1145\/568438.568455"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6313045"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.368134"},{"key":"e_1_2_1_85_1","unstructured":"Kamp J. A. W. 1968. Tense logic and the theory of linear order. PhD dissertation University of California Los Angeles. Kamp J. A. W. 1968. Tense logic and the theory of linear order. PhD dissertation University of California Los Angeles."},{"key":"e_1_2_1_86_1","unstructured":"Katz R. H. and Borriello G. 2004. Contemporary Logic Design 2nd Ed. Prentice-Hall Englewood Cliffs NJ. Katz R. H. and Borriello G. 2004. Contemporary Logic Design 2nd Ed. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_87_1","doi-asserted-by":"crossref","unstructured":"Kesten Y. and Pnueli A . 1992 . Timed and hybrid statecharts and their textual representation. In Proceedings of the 2nd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'92). J. Vytopil Ed. Lecture Notes in Computer Science vol. 571 Springer Berlin 591--620. Kesten Y. and Pnueli A. 1992. Timed and hybrid statecharts and their textual representation. In Proceedings of the 2nd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'92). J. Vytopil Ed. Lecture Notes in Computer Science vol. 571 Springer Berlin 591--620.","DOI":"10.1007\/3-540-55092-5_32"},{"key":"e_1_2_1_88_1","unstructured":"Khalil H. 1995. Nonlinear Systems 2nd ed. Prentice-Hall Englewood Cliffs NJ. Khalil H. 1995. Nonlinear Systems 2nd ed. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_89_1","first-page":"83","article-title":"Theory of Functions. Parts 1 and 2 (in one volume). Dover","volume":"8","author":"Knopp K.","year":"1996","journal-title":"Ch."},{"key":"e_1_2_1_90_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the REX Workshop: Real-Time: Theory in Practice. J. W. de Bakkeret al. Eds.","author":"Koymans R."},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19630090502"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_94_1","volume-title":"Mason Ed., Information Processing","volume":"83","author":"Lamport L.","year":"1983"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567463"},{"key":"e_1_2_1_96_1","volume-title":"Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)","author":"Laroussinie F."},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_98_1","volume-title":"Proceedings of 3rd Workshop on Logic of Programs. Lecture Notes in Computer Science","volume":"193","author":"Lichtenstein O."},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.006"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_2_1_101_1","volume-title":"Concurrency: State Models &amp","author":"Magee J.","year":"1999"},{"key":"e_1_2_1_102_1","unstructured":"Mandrioli D. and Ghezzi C. 1987. Theoretical Foundations of Computer Sciences. Wiley New York. Mandrioli D. and Ghezzi C. 1987. Theoretical Foundations of Computer Sciences. Wiley New York."},{"key":"e_1_2_1_103_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Berlin. Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Berlin.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1955.tb03788.x"},{"key":"e_1_2_1_105_1","unstructured":"Mendelson E. 1997. Introduction to Mathematical Logic 4th Ed. Chapman and Hall. Mendelson E. 1997. Introduction to Mathematical Logic 4th Ed. Chapman and Hall."},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"e_1_2_1_107_1","volume-title":"Lecture Notes in Computer Science","volume":"92","author":"Milner R.","year":"1980"},{"key":"e_1_2_1_108_1","unstructured":"Milner R. 1989. Communication and Concurrency. Prentice-Hall Englewood Cliffs NJ. Milner R. 1989. Communication and Concurrency. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_109_1","volume-title":"Automata Studies. Annals of Mathematical Studies","author":"Moore E. F."},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/133233.129397"},{"key":"e_1_2_1_111_1","doi-asserted-by":"crossref","unstructured":"Moszkowski B. 1986. Executing Temporal Logic Programs. Cambridge University Press. Moszkowski B. 1986. Executing Temporal Logic Programs. Cambridge University Press.","DOI":"10.1007\/3-540-15670-4_6"},{"key":"e_1_2_1_112_1","unstructured":"Moszkowski B. 1983. Reasoning about digital circuits. PhD dissertation Tech. rep. STAN-CS-83-970 Department of Computer Science Stanford University. Moszkowski B. 1983. Reasoning about digital circuits. PhD dissertation Tech. rep. STAN-CS-83-970 Department of Computer Science Stanford University."},{"key":"e_1_2_1_113_1","doi-asserted-by":"crossref","unstructured":"Nicollin X. Olivero A. Sifakis J. and Yovine S . 1993 . Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems R.L. Grossman et al. Eds. Lecture Notes in Computer Science vol. 736 . Springer Berlin 149--178. Nicollin X. Olivero A. Sifakis J. and Yovine S. 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems R.L. Grossman et al. Eds. Lecture Notes in Computer Science vol. 736. Springer Berlin 149--178.","DOI":"10.1007\/3-540-57318-6_28"},{"key":"e_1_2_1_114_1","doi-asserted-by":"crossref","unstructured":"Nicollin X. and Sifakis J . 1991 . An overview and synthesis of timed process algebras. In Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV'91) K. G. Larsen and A. Skou (Eds.) Lecture Notes in Computer Sciences Vol. 575 . Springer Berlin 376--398. Nicollin X. and Sifakis J. 1991. An overview and synthesis of timed process algebras. In Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV'91) K. G. Larsen and A. Skou (Eds.) Lecture Notes in Computer Sciences Vol. 575. Springer Berlin 376--398.","DOI":"10.1007\/3-540-55179-4_36"},{"key":"e_1_2_1_115_1","unstructured":"Odifreddi P. 1999. Classical Recursion Theory. North Holland Amsterdam. Odifreddi P. 1999. Classical Recursion Theory. North Holland Amsterdam."},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1145\/295558.295560"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1109\/87.572129"},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(92)90045-L"},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.80145"},{"key":"e_1_2_1_120_1","unstructured":"Ostroff J. S. 1989. Temporal Logic for Real Time Systems. Wiley New York. Ostroff J. S. 1989. Temporal Logic for Real Time Systems. Wiley New York."},{"key":"e_1_2_1_121_1","doi-asserted-by":"crossref","unstructured":"Ouimet M. and Lundqvist K . 2007 a. The TASM toolset: Specification simulation and formal verification of real-time systems. In Proceedings of the 19th International Conference on Computer-Aided Verification (CAV'07) W. Damm and H. Hermanns Eds. Lecture Notes in Computer Science vol. 4590 . Springer Berlin 126--130. Ouimet M. and Lundqvist K. 2007a. The TASM toolset: Specification simulation and formal verification of real-time systems. In Proceedings of the 19th International Conference on Computer-Aided Verification (CAV'07) W. Damm and H. Hermanns Eds. Lecture Notes in Computer Science vol. 4590. Springer Berlin 126--130.","DOI":"10.1007\/978-3-540-73368-3_15"},{"key":"e_1_2_1_122_1","volume-title":"Proceedings of the 14th International Workshop on Abstract State Machines (ASM'07)","author":"Ouimet M."},{"key":"e_1_2_1_123_1","unstructured":"Papadimitriou C. H. 1994. Computational Complexity. Addison-Wesley Reading MA. Papadimitriou C. H. 1994. Computational Complexity. Addison-Wesley Reading MA."},{"key":"e_1_2_1_124_1","unstructured":"Peron A. 1993. Synchronous and asynchronous models for statecharts. Tech. rep. TD-21\/93 Dipartimento di Informatica Universita di Pisa. Peron A. 1993. Synchronous and asynchronous models for statecharts. Tech. rep. TD-21\/93 Dipartimento di Informatica Universita di Pisa."},{"key":"e_1_2_1_125_1","volume-title":"Infinite Words. Pure and Applied Mathematics","volume":"141","author":"Perrin D."},{"key":"e_1_2_1_126_1","unstructured":"Peterson J. L. 1981. Petri Net Theory and the Modeling of Systems. Prentice-Hall Englewood Cliffs NJ. Peterson J. L. 1981. Petri Net Theory and the Modeling of Systems. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_127_1","volume-title":"Proceedings of IFIP Congress. North Holland","author":"Petri C. A.","year":"1963"},{"key":"e_1_2_1_128_1","doi-asserted-by":"crossref","unstructured":"Pnueli A. and Shalev M . 1991 . What is in a step: On the semantics of statecharts. In Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS'91) T. Ito and A.R. Meyer Eds. Lecture Notes in Computer Science vol. 526 Springer Berlin 244--264. Pnueli A. and Shalev M. 1991. What is in a step: On the semantics of statecharts. In Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS'91) T. Ito and A.R. Meyer Eds. Lecture Notes in Computer Science vol. 526 Springer Berlin 244--264.","DOI":"10.1007\/3-540-54415-1_49"},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_130_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90030-8"},{"key":"e_1_2_1_131_1","doi-asserted-by":"publisher","DOI":"10.5555\/3405"},{"key":"e_1_2_1_132_1","doi-asserted-by":"crossref","unstructured":"Rescher N. and Urquhart A. 1971. Temporal Logic. Springer Berlin. Rescher N. and Urquhart A. 1971. Temporal Logic. Springer Berlin.","DOI":"10.1007\/978-3-7091-7664-1"},{"key":"e_1_2_1_133_1","unstructured":"Rogers H. Jr. 1987. Theory of Recursive Functions and Effective Computability. MIT Press Cambridge MA. Rogers H. Jr. 1987. Theory of Recursive Functions and Effective Computability. MIT Press Cambridge MA."},{"key":"e_1_2_1_134_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.63249"},{"key":"e_1_2_1_135_1","unstructured":"Roscoe A. W. 1997. The Theory and Practice of Concurrency. Prentice-Hall Englewood Cliffs NJ. Roscoe A. W. 1997. The Theory and Practice of Concurrency. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_136_1","doi-asserted-by":"crossref","unstructured":"Rutten J. Kwiatkowska M. Norman G. and Parker D. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. American Mathematical Society. Rutten J. Kwiatkowska M. Norman G. and Parker D. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. American Mathematical Society.","DOI":"10.1090\/crmm\/023"},{"key":"e_1_2_1_137_1","unstructured":"Schneider S. 2000. Concurrent and Real-Time Systems: The CSP Approach. Wiley New York. Schneider S. 2000. Concurrent and Real-Time Systems: The CSP Approach. Wiley New York."},{"key":"e_1_2_1_138_1","volume-title":"Proceedings of the 4th Conference on Advances in Modal Logic. P. Balbiani et al. Eds., King's College Publications, 393--436","author":"Schnoebelen P.","year":"2002"},{"key":"e_1_2_1_139_1","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806720"},{"key":"e_1_2_1_140_1","unstructured":"Sipser M. 2005. Introduction to the Theory of Computation 2nd Ed. Course Technology. Sipser M. 2005. Introduction to the Theory of Computation 2nd Ed. Course Technology."},{"key":"e_1_2_1_141_1","unstructured":"Skogestad S. and Postlethwaite I. 2005. Multivariable Feedback Control: Analysis and Design 2nd Ed. Wiley New York. Skogestad S. and Postlethwaite I. 2005. Multivariable Feedback Control: Analysis and Design 2nd Ed. Wiley New York."},{"key":"e_1_2_1_142_1","unstructured":"Sommerville I. 2004. Software Engineering 7th Ed. Addison Wesley Reading MA. Sommerville I. 2004. Software Engineering 7th Ed. Addison Wesley Reading MA."},{"key":"e_1_2_1_143_1","unstructured":"TGI. Petri nets tools database. https:\/\/2.zoppoz.workers.dev:443\/http\/www.informatik.unihamburg.de\/TGI\/PetriNets\/tools\/quick.html. TGI. Petri nets tools database. https:\/\/2.zoppoz.workers.dev:443\/http\/www.informatik.unihamburg.de\/TGI\/PetriNets\/tools\/quick.html."},{"key":"e_1_2_1_144_1","volume-title":"Handbook of Theoretical Computer Science","author":"Thomas W."},{"key":"e_1_2_1_145_1","unstructured":"UML05. 2005. UML 2.0 superstructure specification. Tech. rep. formal\/05-07-04 Object Management Group. UML05. 2005. UML 2.0 superstructure specification. Tech. rep. formal\/05-07-04 Object Management Group."},{"key":"e_1_2_1_146_1","unstructured":"UML04. 2004. Unified modeling language specification. Tech. rep. formal\/04-07-02 Object Management Group. UML04. 2004. Unified modeling language specification. Tech. rep. formal\/04-07-02 Object Management Group."},{"key":"e_1_2_1_147_1","volume-title":"Lecture Notes in Computer Science","volume":"251","author":"van der Schaft A."},{"key":"e_1_2_1_148_1","unstructured":"van Eijk P. H. J. Vissers C. A. and Diaz M. (Eds.). 1989. The Formal Description Technique LOTOS. Elsevier Science Amsterdam. van Eijk P. H. J. Vissers C. A. and Diaz M. (Eds.). 1989. The Formal Description Technique LOTOS. Elsevier Science Amsterdam."},{"key":"e_1_2_1_149_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 8th BANFF Higher Order Workshop Conference on Logics for Concurrency: Structure versus Automata","author":"Vardi M. Y."},{"key":"e_1_2_1_150_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694478"},{"key":"e_1_2_1_151_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"von der Beeck M."},{"key":"e_1_2_1_152_1","unstructured":"Warmer J. B. and Kleppe A. G. (Eds.). 1999. The Object Constraint Language. Addison-Wesley Reading MA. Warmer J. B. and Kleppe A. G. (Eds.). 1999. The Object Constraint Language. Addison-Wesley Reading MA."},{"key":"e_1_2_1_153_1","unstructured":"Weisstein E. W. Real analytic function. MathWorld. https:\/\/2.zoppoz.workers.dev:443\/http\/mathworld.wolfram.com\/RealAnalyticFunction.html. Weisstein E. W. Real analytic function. MathWorld. https:\/\/2.zoppoz.workers.dev:443\/http\/mathworld.wolfram.com\/RealAnalyticFunction.html."},{"key":"e_1_2_1_154_1","doi-asserted-by":"publisher","DOI":"10.1145\/359763.359798"},{"key":"e_1_2_1_155_1","unstructured":"Wolfram S. 1994. Cellular Automata and Complexity. Perseus Books Group. Wolfram S. 1994. Cellular Automata and Complexity. Perseus Books Group."},{"key":"e_1_2_1_156_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/1667062.1667063","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/1667062.1667063","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:41:30Z","timestamp":1750250490000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/1667062.1667063"}},"subtitle":["A taxonomy and a comparative survey"],"short-title":[],"issued":{"date-parts":[[2010,2]]},"references-count":156,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["10.1145\/1667062.1667063"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/1667062.1667063","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2]]},"assertion":[{"value":"2007-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-03-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}