×

zbMATH — the first resource for mathematics

A menagerie of timed automata. (English) Zbl 1305.68113
ACM Comput. Surv. 46, No. 3, Article No. 40, 56 p. (2014); corrections ibid. 50, No. 3, Article No. 42, 8p. (2017).

MSC:
68Q45 Formal languages and automata
68-02 Research exposition (monographs, survey articles) pertaining to computer science
Keywords:
timed automata
Software:
REDLIB; Uppaal; CMC; Kronos
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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 · Zbl 1088.68023
[2] 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 · Zbl 1046.68574
[3] 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.113766 · Zbl 0769.68088
[4] 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 · Zbl 0783.68076
[5] 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 · Zbl 0765.68150
[6] 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 · Zbl 0803.68071
[7] 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 · Zbl 1310.68139
[8] 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 · Zbl 1078.68070
[9] 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_1 · Zbl 1105.68057
[10] 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 · Zbl 0974.68523
[11] 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. · Zbl 1169.68535
[12] Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA. · Zbl 1179.68076
[13] 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 · Zbl 1105.68350
[14] 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 · Zbl 1143.68430
[15] 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 · Zbl 1099.94523
[16] 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_3 · Zbl 1088.68119
[17] 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 · Zbl 0953.68565
[18] 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 · Zbl 1379.68216
[19] 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. · Zbl 0930.68077
[20] 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_13 · Zbl 1279.68196
[21] 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
[22] 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
[23] Patricia Bouyer. 2002. Timed Automata May Cause Some Troubles. Technical Report RS-02-35. BRICS-Aalborg University.
[24] 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 · Zbl 1035.68511
[25] 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 · Zbl 1273.68197
[26] 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 · Zbl 1347.68218
[27] 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 · Zbl 1117.68396
[28] 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 · Zbl 1216.68158
[29] 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 · Zbl 1070.68063
[30] 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 · Zbl 1176.68099
[31] Patricia Bouyer and François Laroussinie. 2010. Model Checking Timed Automata. ISTE, London, 111–140. DOI: http://dx.doi.org/10.1002/9780470611012.ch4
[32] 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 · Zbl 1175.68256
[33] 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
[34] H. Bowman and R. Gomez. 2006. How to stop time stopping. Formal Aspects of Computing 18, 4 (December 2006), 459–493. · Zbl 1105.68059
[35] 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 · Zbl 0999.68112
[36] 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
[37] 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 · Zbl 0591.68027
[38] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA.
[39] 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.4416795
[40] 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
[41] 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-2 · Zbl 1277.68179
[42] 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
[43] Herbert B. Enderton. 2001. A Mathematical Introduction to Logic (2nd ed.). Harcourt/Academic Press, San Diego, CA. · Zbl 0992.03001
[44] 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 · Zbl 1274.68185
[45] John B. Fraleigh. 1999. A First Course in Abstract Algebra (6th ed.). Addison-Wesley, Boston, MA. · Zbl 1060.00001
[46] 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 · Zbl 1260.68004
[47] 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.
[48] 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 · Zbl 0917.68152
[49] 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 · Zbl 1141.68435
[50] 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 · Zbl 05304363
[51] 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
[52] 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.
[53] 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
[54] 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.185551 · Zbl 0806.68080
[55] 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 · Zbl 0806.68080
[56] 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 · Zbl 0920.68091
[57] 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 · Zbl 0978.68094
[58] 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 · Zbl 1171.68528
[59] 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
[60] 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/S00310ED1V01Y201011DCT005 · Zbl 1226.68004
[61] 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
[62] 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_158 · Zbl 1193.03069
[63] 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_27
[64] 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 · Zbl 0887.68068
[65] 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 · Zbl 0887.68068
[66] 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
[67] 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 · Zbl 0856.68103
[68] 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 · Zbl 0834.68123
[69] 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. · Zbl 0834.68123
[70] 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 · Zbl 0860.68072
[71] 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 · Zbl 0856.68103
[72] 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 · Zbl 1374.68262
[73] 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
[74] R. Milner. 1989. Communication and Concurrency. Prentice-Hall, Upper Saddle River, NJ. · Zbl 0683.68008
[75] 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 · Zbl 05940748
[76] Ernst-Rüdiger Olderog and Henning Dierks. 2008. Real-Time Systems: Formal Specification and Automatic Verification. Cambridge University Press, New York, NY. · Zbl 1161.68030
[77] 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_4 · Zbl 1094.68067
[78] 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 · Zbl 05113125
[79] 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 · Zbl 0917.68152
[80] 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 · Zbl 05114391
[81] 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 · Zbl 1233.68158
[82] 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
[83] 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 · Zbl 0972.68104
[84] 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
[85] 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 · Zbl 1352.68165
[86] 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 · Zbl 0971.68096
[87] 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 · Zbl 1022.68586
[88] 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 · Zbl 02243233
[89] 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.831197
[90] 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
[91] 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
[92] 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 · Zbl 1183.68384
[93] 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 · Zbl 05341834
[94] 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/s100090050009 · Zbl 1060.68606
[95] 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
[96] 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 · Zbl 1169.68523
[97] 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 · Zbl 1169.68523
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.