Peter Fontana
Skip Abstract Section
Abstract
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’s 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.
- Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler. 2006. Scheduling with timed automata. Theoretical Computer Science 354, 2 (2006), 272--300. DOI: http://dx.doi.org/10.1016/j.tcs.2005.11.018 Google Scholar
Digital Library
- Rajeev Alur. 1999. Timed Automata. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV’99), Nicolas Halbwachs and Doron Peled (Eds.), Vol. 1633. Springer, Berlin, 8--22. DOI: http://dx.doi.org/10.1007/3-540-48683-6_3 Google ScholarDigital Library
- Rajeev Alur, Costas Courcoubetis, and David Dill. 1990. Model-checking for real-time systems. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS’90). IEEE Computer Society, Philadelphia, PA, 414--425. DOI: http://dx.doi.org/10.1109/LICS.1990.113766Google ScholarCross Ref
- Rajeev Alur, Costas Courcoubetis, and David Dill. 1993a. Model-checking in dense real-time. Information and Computation 104, 1 (May 1993), 2--34. DOI: http://dx.doi.org/10.1006/inco.1993.1024 Google ScholarDigital Library
- Rajeev Alur and David L. Dill. 1990. Automata for modeling real-time systems. In ICALP’90: Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP’90), Michael S. Paterson (Ed.), Vol. 443. Springer, Berlin, 322--335. DOI: http://dx.doi.org/10.1007/BFb0032042 Google ScholarDigital Library
- Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126, 2 (April 1994), 183--235. DOI: http://dx.doi.org/10.1016/0304-3975(94)90010-8 Google ScholarDigital Library
- Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. 1993b. Parametric real-time reasoning. In Proceedings of the 25th Annual ACM Symposium on Theory of Computing (STOC’93). ACM, New York, NY, 592--601. DOI: http://dx.doi.org/10.1145/167088.167242 Google ScholarDigital Library
- Rajeev Alur, Salvatore La Torre, and P. Madhusudan. 2005. Perturbed timed automata. In HSSC’05: Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control (HSSC’05), Manfred Morari and Lothar Thiele (Eds.), Vol. 3414. Springer, Berlin, 70--85. DOI: http://dx.doi.org/10.1007/978-3-540-31954-2_5 Google ScholarDigital Library
- Rajeev Alur and Parthasarathy Madhusudan. 2004. Decision problems for timed automata: A survey. In SMF-RT’04: Proceedings of Formal Methods for the Design of Real-Time Systems (SMF-RT’04), Marco Bernado and Flavio Corradini (Eds.), Vol. 3185. Springer, Berlin, 1--24. DOI: http://dx.doi.org/10.1007/978-3-540-30080-9_1Google ScholarCross Ref
- Aurore Annichini, Eugene Asarin, and Ahmed Bouajjani. 2000. Symbolic techniques for parametric reasoning about counter and clock systems. In CAV’00: Proceedings of the 12th International Conference on Computer Aided Verification (CAV’00), E. Emerson and Aravinda Sistla (Eds.), Vol. 1855. Springer, Berlin, 419--434. DOI: http://dx.doi.org/10.1007/10722167_32 Google ScholarDigital Library
- 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.Google Scholar
- Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA. Google ScholarDigital Library
- 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/b110123Google Scholar
- Gerd Behrmann, Kim Larsen, and Jacob Rasmussen. 2005. Priced timed automata: Algorithms and applications. In Formal Methods for Components and Objects, Frank de Boer, Marcello Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Lecture Notes in Computer Science, Vol. 3657. Springer, Berlin, 162--182. DOI: http://dx.doi.org/10.1007/11561163_8 Google ScholarDigital Library
- Ramzi Ben Salah, Marius Dorel Bozga, and Oded Maler. 2009. Compositional timing analysis. In Proceedings of the 7th ACM International Conference on Embedded Software (EMSOFT’09). ACM, New York, NY, 39--48. DOI: http://dx.doi.org/10.1145/1629335.1629342 Google ScholarDigital Library
- Johan Bengtsson and Wang Yi. 2004. Timed automata: Semantics, algorithms and tools. In Lectures on Concurrency and Petri Nets, Jörg 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_3Google Scholar
- Béatrice Bérard and Catherine Dufourd. 2000. Timed automata and additive clock constraints. Inform. Process. Lett. 75, 1--2 (2000), 1--7. DOI: http://dx.doi.org/10.1016/S0020-0190(00)00075-2 Google ScholarDigital Library
- Béatrice Bérard, Paul Gastin, and Antoine Petit. 1996. On the power of non-observable actions in timed automata. In Proceedings of the 13th Annual Symposium on Theoretical Aspects of Computer Science (STACS’96), Claude Puech and Rüdiger Reischuk (Eds.). Lecture Notes in Computer Science, Vol. 1046. Springer, Berlin, 255--268. DOI: http://dx.doi.org/10.1007/3-540-60922-9_22 Google ScholarDigital Library
- Béatrice Bérard, Antoine Petit, Volker Diekert, and Paul Gastin. 1998. Characterization of the expressive power of silent transitions in timed automata. Fundam. Inf. 36, 2--3 (November 1998), 145--182. Google ScholarDigital Library
- Dirk Beyer and Andreas Noack. 2003. Can decision diagrams overcome state space explosion in real-time verification? In Proceedings of the 23rd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE’03), Hartmut Köonig, 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_13Google Scholar
- Sébastien Bornot and Joseph Sifakis. 1998. On the composition of hybrid systems. In Proceedings of the 1st International Workshop in Hybrid Systems: Computation and Control (HSCC’98), Thomas Henzinger and Shankar Sastry (Eds.). Lecture Notes in Computer Science, Vol. 1386. Springer, Berlin, 49--63. DOI: http://dx.doi.org/10.1007/3-540-64358-3_31 Google ScholarDigital Library
- Sébastien Bornot, Joseph Sifakis, and Stavros Tripakis. 1998. Modeling urgency in timed systems. In Proceedings of the International Symposium on Compositionality: The Significant Difference (COMPOS’97), Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli (Eds.). Lecture Notes in Computer Science, Vol. 1536. Springer, Berlin, 103--129. DOI: http://dx.doi.org/10.1007/3-540-49213-5_5 Google ScholarDigital Library
- Patricia Bouyer. 2002. Timed Automata May Cause Some Troubles. Technical Report RS-02-35. BRICS-Aalborg University.Google Scholar
- Patricia Bouyer. 2003. Untameable timed automata! In Proceedings of the 20th Annual Symposium on Theoretical Aspects of Computer Science (STACS’03), 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 Google ScholarDigital Library
- Patricia Bouyer. 2006. Weighted timed automata: Model-checking and games. Electronic Notes in Theoretical Computer Science 158, (2006), 3--17. DOI: http://dx.doi.org/10.1016/j.entcs.2006.04.002 Google ScholarDigital Library
- Patricia Bouyer. 2009. Model-checking timed temporal logics. Electronic Notes in Theoretical Computer Science 231, (March 2009), 323--341. DOI: http://dx.doi.org/10.1016/j.entcs.2009.02.044 Google ScholarDigital Library
- Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Larsen. 2005. Optimal strategies in priced timed game automata. In Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS’04), Kamal Lodaya and Meena Mahajan (Eds.). Lecture Notes in Computer Science, Vol. 3328. Springer, Berlin, 423--429. DOI: http://dx.doi.org/10.1007/978-3-540-30538-5_13 Google ScholarDigital Library
- Patricia Bouyer, Franck Cassez, and François Laroussinie. 2011. Timed modal logics for real-time systems. Journal of Logic, Language and Information 20, 2 (2011), 169--203. DOI: http://dx.doi.org/10.1007/s10849-010-9127-4 Google ScholarDigital Library
- Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. 2004. Updatable timed automata. Theoretical Computer Science 321, 2--3 (2004), 291--345. DOI: http://dx.doi.org/10.1016/j.tcs.2004.04.003 Google ScholarDigital Library
- Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. 2009. Undecidability results for timed automata with silent transitions. Fundamenta Informaticae 92, 1 (January 2009), 1--25. DOI: http://dx.doi.org/10.3233/FI-2009-0063 Google ScholarDigital Library
- Patricia Bouyer and François Laroussinie. 2010. Model Checking Timed Automata. ISTE, London, 111--140. DOI: http://dx.doi.org/10.1002/9780470611012.ch4Google Scholar
- Patricia Bouyer, François Laroussinie, and Pierre-Alain Reynier. 2005. Diagonal constraints in timed automata: Forward analysis of timed systems. In Proceedings of the 3rd International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’05), Paul Pettersson and Wang Yi (Eds.). Lecture Notes in Computer Science, Vol. 3829. Springer, Berlin, 112--126. DOI: http://dx.doi.org/10.1007/11603009_10 Google ScholarDigital Library
- Howard Bowman. 2001. Time and action lock freedom properties for timed automata. In Proceedings of the IFIP TC6/WG6.1—21st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE’01), 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 Google ScholarDigital Library
- H. Bowman and R. Gomez. 2006. How to stop time stopping. Formal Aspects of Computing 18, 4 (December 2006), 459--493. Google ScholarCross Ref
- Franck Cassez and Kim Larsen. 2000. The impressive power of stopwatches. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’00), Catuscia Palamidessi (Ed.). Lecture Notes in Computer Science, Vol. 1877. Springer, Berlin, 138--152. DOI: http://dx.doi.org/10.1007/3-540-44618-4_12 Google ScholarDigital Library
- Kwang Ting Cheng and A. S. Krishnakumar. 1993. Automatic functional test generation using the extended finite state machine model. In Proceedings of the 30th International Design Automation Conference (DAC’93). ACM, New York, NY, 86--91. DOI: http://dx.doi.org/10.1145/157485.164585 Google ScholarDigital Library
- E. M. Clarke, E. A. Emerson, and A. P. Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8, 2 (1986), 244--263. DOI: http://dx.doi.org/10.1145/5397.5399 Google ScholarDigital Library
- Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA. Google ScholarDigital Library
- 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’07). IEEE, Piscataway, NJ, 398--405. DOI: http://dx.doi.org/10.1109/EFTA.2007.4416795Google Scholar
- Volker Diekert, Paul Gastin, and Antoine Petit. 1997. Removing ε-transitions in timed automata. In Proceedings of the 14th Annual Symposium on Theoretical Aspects of Computer Science (STACS’97), Rüdiger Reischuk and Michel Morvan (Eds.). Lecture Notes in Computer Science, Vol. 1200. Springer, Berlin, 583--594. DOI: http://dx.doi.org/10.1007/BFb0023491 Google ScholarDigital Library
- Cătălin Dima and Ruggero Lanotte. 2011. A study on shuffle, stopwatches and independently evolving clocks. Distributed Computing 25, 1 (2011), 5--33. DOI: http://dx.doi.org/10.1007/s00446-011-0148-2Google ScholarCross Ref
- Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, and Wang Yi. 2008. Timed automata patterns. IEEE Transactions on Software Engineering 34, 6 (November--December 2008), 844--859. DOI: http://dx.doi.org/10.1109/TSE.2008.52 Google ScholarDigital Library
- Herbert B. Enderton. 2001. A Mathematical Introduction to Logic (2nd ed.). Harcourt/Academic Press, San Diego, CA.Google Scholar
- Uli Fahrenberg, Kim Larsen, and Claus Thrane. 2010. Verification, performance analysis and controller synthesis for real-time systems. In Fundamentals of Software Engineering, Farhad Arbab and Marjan Sirjani (Eds.). Lecture Notes in Computer Science, Vol. 5961. Springer, Berlin, 34--61. DOI: http://dx.doi.org/10.1007/978-3-642-11623-0_2 Google ScholarDigital Library
- John B. Fraleigh. 1999. A First Course in Abstract Algebra (6th ed.). Addison-Wesley, Boston, MA.Google Scholar
- Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi. 2010. Modeling time in computing: A taxonomy and a comparative survey. Comput. Surveys 42, 2 (February 2010), 6:1--6:59. DOI: http://dx.doi.org/10.1145/1667062.1667063 Google ScholarDigital Library
- Stephen J. Garland and Nancy a Lynch. 1998. The IOA Langage and Toolset: Support for Designing, Analyzing, and Building Distributed Systems. Technical Report MIT/LCS/TR-762. MIT Laboratory for Computer Science.Google Scholar
- Rainer Gawlick, Roberto Segala, Jørgen Søgaard-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 Google ScholarDigital Library
- Rodolfo Gomez and Howard Bowman. 2007. Efficient detection of zeno runs in timed automata. In Proceedings of the 5th International Conference on the Formal Modeling and Analysis of Timed Systems (FORMATS’07), Jean-Francois Raskin and P.S. Thiagarajan (Eds.), Vol. 4763. Springer, Berlin, 195--210. DOI: http://dx.doi.org/10.1007/978-3-540-75454-1_15 Google ScholarDigital Library
- Jameleddine Hassine, Juergen Rilling, and Rachida Dssouli. 2007. Formal verification of use case maps with real time extensions. In Proceedings of the Conference on Design for Dependable Systems (SDL’07), Emmanuel Gaudin, Elie Najm, and Rick Reed (Eds.). Lecture Notes in Computer Science, Vol. 4745. Springer, Berlin, 225--241. DOI: http://dx.doi.org/10.1007/978-3-540-74984-4_14 Google ScholarDigital Library
- Jameleddine Hassine, Juergen Rilling, and Rachida Dssouli. 2010. An evaluation of timed scenario notations. Journal of Systems and Software 83, 2 (2010), 326--350. DOI: http://dx.doi.org/10.1016/j.jss.2009.09.014 Google ScholarDigital Library
- 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.Google Scholar
- T. 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’96), 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 Google ScholarDigital Library
- 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’92). IEEE, Piscataway, NJ, USA, 394--406. DOI: http://dx.doi.org/10.1109/LICS.1992.185551Google Scholar
- T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. 1994. Symbolic model checking for real-time systems. Information and Computation 111, 2 (1994), 193--244. DOI: http://dx.doi.org/10.1006/inco.1994.1045 Google ScholarDigital Library
- Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. 1998. What’s decidable about hybrid automata? J. Comput. System Sci. 57, 1 (1998), 94--124. DOI: http://dx.doi.org/10.1006/jcss.1998.1581 Google ScholarDigital Library
- Thomas Hune, Judi Romijn, Mariëelle Stoelinga, and Frits Vaandrager. 2001. Linear parametric model checking of timed automata. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), Tiziana Margaria and Wang Yi (Eds.). Lecture Notes in Computer Science, Vol. 2031. Springer, Berlin, 189--203. DOI: http://dx.doi.org/10.1007/3-540-45319-9_14 Google ScholarDigital Library
- Marcin Jurdziński 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 Google ScholarDigital Library
- 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’03). IEEE, Piscataway, NJ, 166--177. DOI: http://dx.doi.org/10.1109/REAL.2003.1253264 Google ScholarDigital Library
- Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager. 2010. The theory of timed I/O automata, Second Edition. Synthesis Lectures on Distributed Computing Theory 1, 1 (2010), 1--137. DOI: http://dx.doi.org/10.2200/S00310ED1V01Y201011DCT005Google ScholarCross Ref
- Christine Largouët, Marie-Odile Cordier, Yves-Marie Bozec, Yulong Zhao, and Guy Fontenelle. 2012. Use of timed automata and model-checking to explore scenarios on ecosystem models. Environmental Modelling & Software 30, 0 (2012), 123--138. DOI: http://dx.doi.org/10.1016/j.envsoft.2011.08.005 Google ScholarDigital Library
- François Laroussinie, Kim Larsen, and Carsten Weise. 1995. From timed automata to logic—and back. In Mathematical Foundations of Computer Science, Jirí Wiedermann and Petr Hájek (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_158Google Scholar
- François 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_27Google Scholar
- 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 Google ScholarDigital Library
- Kim G. Larsen and Yi Wang. 1997. Time-abstracted bisimulation: Implicit specifications and decidability. Information and Computation 134, 2 (1997), 75--101. DOI: http://dx.doi.org/10.1006/inco.1997.2623 Google ScholarDigital Library
- Huimin Lin. 1996. Symbolic transition graph with assignment. In CONCUR’96: Proceedings of the 7th International Conference on Concurrency Theory (CONCUR’96), Ugo Montanari and Vladimiro Sassone (Eds.), Vol. 1119. Springer, Berlin, 50--65. DOI: http://dx.doi.org/10.1007/3-540-61604-7_47 Google ScholarDigital Library
- 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 Google ScholarDigital Library
- N. Lynch and F. Vaandrager. 1995a. Forward and backward simulations. Part I: Untimed systems. Information and Computation 121, 2 (1995), 214--233. DOI: http://dx.doi.org/10.1006/inco.1995.1134 Google ScholarDigital Library
- Nancy Lynch and Frits Vaandrager. 1995b. Forward and Backward Simulations Part II: Timing Systems. Technical Report MIT-LCS-TM-458. MIT Laboratory for Computer Science. Google ScholarDigital Library
- Nancy Lynch and Frits Vaandrager. 1996a. Action transducers and timed automata. Formal Aspects of Computing 8, 5 (1996), 499--538. DOI: http://dx.doi.org/10.1007/BF01211907 Google ScholarCross Ref
- Nancy Lynch and Frits Vaandrager. 1996b. Forward and backward simulations: II. Timing-based systems. Information and Computation 128, 1 (1996), 1--25. DOI: http://dx.doi.org/10.1006/inco.1996.0060 Google ScholarDigital Library
- Oded Maler and Grégory Batt. 2008. Approximating continuous systems by timed automata. In Formal Methods in Systems Biology, Jasmin Fisher (Ed.). Lecture Notes in Computer Science, Vol. 5054. Springer, Berlin, 77--89. DOI: http://dx.doi.org/10.1007/978-3-540-68413-8_6 Google ScholarDigital Library
- Michael Merritt, Francesmary Modugno, and Mark Tuttle. 1991. Time-constrained automata. In Proceedings of the Conference on Concurrency Theory (CONCUR’91), 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 Google ScholarDigital Library
- R. Milner. 1989. Communication and Concurrency. Prentice-Hall, Upper Saddle River, NJ. Google ScholarDigital Library
- Georges Morbé, Florian Pigorsch, and Christoph Scholl. 2011. Fully symbolic model checking for timed automata. In Proceedings of the International Conference on Computer Aided Verification (CAV’11), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Lecture Notes in Computer Science, Vol. 6806. Springer, Berlin, 616--632. DOI: http://dx.doi.org/10.1007/978-3-642-22110-1_50 Google ScholarDigital Library
- Ernst-Rüdiger Olderog and Henning Dierks. 2008. Real-Time Systems: Formal Specification and Automatic Verification. Cambridge University Press, New York, NY. Google ScholarDigital Library
- Wojciech Penczek and Agata Półrola. 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_4Google Scholar
- A. Petrenko, S. Boroday, and R. Groz. 2004. Confirming configurations in EFSM testing. IEEE Transactions on Software Engineering 30, 1 (January 2004), 29--42. DOI: http://dx.doi.org/10.1109/TSE.2004.1265734 Google ScholarDigital Library
- Roberto Segala, Rainer Gawlick, Jørgen Søgaard-Andersen, and Nancy Lynch. 1998. Liveness in timed and untimed systems. Information and Computation 141, 2 (1998), 119--171. DOI: http://dx.doi.org/10.1006/inco.1997.2671 Google ScholarDigital Library
- A. C. Shaw. 1992. Communicating real-time state machines. IEEE Transactions on Software Engineering 18, 9 (September 1992), 805--816. DOI: http://dx.doi.org/10.1109/32.159840 Google ScholarDigital Library
- Christoffer Sloth and Rafael Wisniewski. 2011. Verification of continuous dynamical systems by timed automata. Formal Methods in System Design 39, 1 (August 2011), 1--36. DOI: http://dx.doi.org/10.1007/s10703-011-0118-0 Google ScholarDigital Library
- 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’95), Pierre Wolper (Ed.), Vol. 939. Springer, Berlin, 211--224. DOI: http://dx.doi.org/10.1007/3-540-60045-0_52 Google ScholarDigital Library
- Jan Springintveld, Frits Vaandrager, and Pedro R. D’Argenio. 2001. Testing timed automata. Theoretical Computer Science 254, 1--2 (2001), 225--257. DOI: http://dx.doi.org/10.1016/S0304-3975(99)00134-6 Google ScholarDigital Library
- 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’96), Ugo Montanari and Vladimiro Sassone (Eds.), Vol. 1119. Springer, Berlin, 546--562. DOI: http://dx.doi.org/10.1007/3-540-61604-7_75 Google ScholarDigital Library
- Stavros Tripakis. 2009. Checking timed Büchi automata emptiness on simulation graphs. ACM Transactions on Computational Logic 10, 3 (2009), 1--19. DOI: http://dx.doi.org/10.1145/1507244.1507245 Google ScholarDigital Library
- Stavros Tripakis and Sergio Yovine. 2001. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18, 1 (January 2001), 25--68. DOI: http://dx.doi.org/10.1023/A:1008734703554 Google ScholarDigital Library
- Farn Wang. 2003. Efficient verification of timed automata with BDD-like data-structures. In Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’03), Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, and Supratik Mukhopadhyay (Eds.), Vol. 2575. Springer, Berlin, 189--205. DOI: http://dx.doi.org/10.1007/3-540-36384-X_17 Google ScholarDigital Library
- Farn Wang. 2004a. Efficient Verification of timed automata with BDD-like data structures. International Journal on Software Tools for Technology Transfer 6, 1 (2004), 77--97. DOI: http://dx.doi.org/10.1007/s10009-003-0135-4 Google ScholarDigital Library
- Farn Wang. 2004b. Formal verification of timed systems: A survey and perspective. Proc. IEEE 92, 8 (2004), 1283--1307. DOI: http://dx.doi.org/10.1109/JPROC.2004.831197Google ScholarCross Ref
- Farn Wang. 2006. REDLIB for the formal verification of embedded systems. In Proceedings of the International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’06). IEEE Computer Society, Piscataway, NJ, 341--346. DOI: http://dx.doi.org/10.1109/ISoLA.2006.68 Google ScholarDigital Library
- 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.ecse410Google Scholar
- Farn Wang. 2008. Time-progress evaluation for dense-time automata with concave path conditions. In Automated Technology for Verification and Analysis, Sungdeok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan (Eds.). Lecture Notes in Computer Science, Vol. 5311. Springer, Berlin, 258--273. DOI: http://dx.doi.org/10.1007/978-3-540-88387-6_24 Google ScholarDigital Library
- Farn Wang, Geng-Dian Huang, and Fang Yu. 2006. TCTL inevitability analysis of dense-time systems: From theory to engineering. IEEE Transactions on Software Engineering 32, 7 (July 2006), 510--526. DOI: http://dx.doi.org/10.1109/TSE.2006.71 Google ScholarDigital Library
- Sergio Yovine. 1997. KRONOS: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer 1, 1 (12 1997), 123--133. DOI: http://dx.doi.org/10.1007/s100090050009Google ScholarDigital Library
- 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 Google ScholarDigital Library
- Dezhuang Zhang and Rance Cleaveland. 2005a. Fast generic model-checking or data-based systems. In Proceedings of Formal Techniques for Networked and Distributed Systems (FORTE’05), Farn Wang (Ed.). Lecture Notes in Computer Science, Vol. 3731. Springer, Berlin, 83--97. DOI: http://dx.doi.org/10.1007/11562436_8 Google ScholarDigital Library
- Dezhuang Zhang and Rance Cleaveland. 2005b. Fast on-the-fly parametric real-time model checking. In Proceedings of the 26th IEEE International Real-Time Systems Symposium (RTSS’05). IEEE Computer Society, Washington, DC, 157--166. DOI: http://dx.doi.org/10.1109/RTSS.2005.22 Google ScholarDigital Library
Index Terms
- A menagerie of timed automata
Recommendations
Interrupt Timed Automata: verification and expressiveness
We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single processor environment.
While the reachability problem is undecidable for ...
Alternating timed automata
A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages that is closed under boolean operations and which has an ...
Undecidable problems about timed automata
FORMATS'06: Proceedings of the 4th international conference on Formal Modeling and Analysis of Timed SystemsWe solve some decision problems for timed automata which were raised by S. Tripakis in [Tri04] and by E. Asarin in [Asa04]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a ...
Comments