×

zbMATH — the first resource for mathematics

Model checking real-time systems. (English) Zbl 1392.68235
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 1001-1046 (2018).
Summary: This chapter surveys timed automata as a formalism for model checking real-time systems. We begin with introducing the model, as an extension of finite-state automata with real-valued variables for measuring time. We then present the main model-checking results in this framework, and give a hint about some recent extensions (namely weighted timed automata and timed games).
For the entire collection see [Zbl 1390.68001].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 1. Abdeddaïm, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272-300 (2006) · Zbl 1088.68023
[2] 2. Abdeddaïm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 478-492. Springer, Heidelberg (2001) · Zbl 0991.68507
[3] 3. Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J.-P., Stevens, P. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2280, pp. 113-126. Springer, Heidelberg (2002) · Zbl 1043.68510
[4] 4. Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 3580, pp. 1089-1101. Springer, Heidelberg (2005) · Zbl 1085.68078
[5] 5. Allamigeon, X., Gaubert, S., Goubault, É.: Inferring min and max invariants using max-plus polyhedra. In: Alpuente, M., Vidal, G. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 5079, pp. 189-204. Springer, Heidelberg (2008) · Zbl 1149.68346
[6] 6. Altisen, K., Gößler, G., Pnueli, A., Sifakis, J., Tripakis, S., Yovine, S.: A framework for scheduler synthesis. In: Symposium on Real-Time Systems (RTSS), pp. 154-163. IEEE, Piscataway (1999)
[7] 7. Alur, R.: Techniques for automatic verification of real-time systems. PhD thesis, Stanford University (1991)
[8] 8. Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 3142, pp. 122-133. Springer, Heidelberg (2004) · Zbl 1098.68061
[9] 9. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2-34 (1993) · Zbl 0783.68076
[10] 10. Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 836, pp. 162-177. Springer, Heidelberg (1994)
[11] 11. Alur, R., Courcoubetis, C., Henzinger, T.A.: Computing accumulated delays in real time systems. Form. Methods Syst. Des. 11(2), 137-155 (1997)
[12] 12. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems (HSCC). LNCS, vol. 736, pp. 209-229. Springer, Heidelberg (1993)
[13] 13. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183-235 (1994) · Zbl 0803.68071
[14] 14. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116-146 (1996) · Zbl 0882.68021
[15] 15. Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. In: Dill, D.L. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 818, pp. 1-13. Springer, Heidelberg (1994) · Zbl 0912.68132
[16] 16. Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211(1-2), 253-273 (1999) · Zbl 0912.68132
[17] 17. Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35-77 (1993) · Zbl 0791.68103
[18] 18. Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181-203 (1994) · Zbl 0807.68065
[19] 19. Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) Symposium on the Theory of Computing (STOC), pp. 592-601. ACM, New York (1993) · Zbl 1310.68139
[20] 20. Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Domenica Di Benedetto, M., Sangiovani-Vincentelli, A.L. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol. 2034, pp. 49-62. Springer, Heidelberg (2001) · Zbl 0991.93076
[21] 21. Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times—a tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2280, pp. 460-464. Springer, Heidelberg (2002) · Zbl 1043.68513
[22] 22. Archer, M., Heitmeyer, C.L., Riccobene, E.: Using TAME to prove invariants of automata models: two case studies. In: Per, M., Heimdahl, E. (eds.) Workshop on Formal Methods in Software Practice (FMSP), pp. 25-36. ACM, New York (2000)
[23] 23. Arnold, A., Nivat, M.: The metric space of infinite trees. Algebraic and topological properties. Fundam. Inform. 3(4), 445-476 (1980) · Zbl 0453.68021
[24] 24. Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-structures for the verification of timed automata. In: Maler, O. (ed.) International Workshop on Hybrid and Real-Time Systems (HART). LNCS, vol. 1201, pp. 346-360. Springer, Heidelberg (1997)
[25] 25. Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F., van Schuppen, J.H. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol. 1569, pp. 19-30. Springer, Heidelberg (1999) · Zbl 0952.93064
[26] 26. Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems II (HSCC). LNCS, vol. 999, pp. 1-20. Springer, Heidelberg (1995)
[27] 27. Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1466, pp. 470-484. Springer, Heidelberg (1998) · Zbl 0933.94045
[28] 28. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Albers, S., Alberto, M., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 5557, pp. 43-54. Springer, Heidelberg (2009) · Zbl 1248.68284
[29] 29. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2619, pp. 254-270. Springer, Heidelberg (2003) · Zbl 1031.68076
[30] 30. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone-based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 312-326. Springer, Heidelberg (2004) · Zbl 1126.68453
[31] 31. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8(3), 204-215 (2006) · Zbl 1126.68453
[32] 32. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in Uppaal. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 174-188. Springer, Heidelberg (2001) · Zbl 0978.68541
[33] 33. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Domenica Di Benedetto, M., Sangiovani-Vincentelli, A.L. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol. 2034, pp. 147-161. Springer, Heidelberg (2001) · Zbl 0991.68037
[34] 34. Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 341-353. Springer, Heidelberg (1999) · Zbl 1046.68577
[35] 35. Behrmann, G., Larsen, K.G., Pelánek, R.: To store or not to store. In: Hunt, W.A. Jr, Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 433-445. Springer, Heidelberg (2003) · Zbl 1278.68155
[36] 36. Ben Salah, R., Bozga, M., Maler, O.: On interleaving in timed automata. In: Baier, C., Hermanns, H. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 4137, pp. 465-476. Springer, Heidelberg (2006) · Zbl 1151.68457
[37] 37. Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1466, pp. 485-500. Springer, Heidelberg (1998)
[38] 38. Bengtsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) International Conference on Formal Engineering Methods (ICFEM). LNCS, vol. 2885, pp. 491-503. Springer, Heidelberg (2003)
[39] 39. Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 2098, pp. 87-124. Springer, Heidelberg (2004) · Zbl 1088.68119
[40] 40. Bérard, B., Diekert, V., Gastin, P., Petit, A.: Characterization of the expressive power of silent transitions in timed automata. Fundam. Inform. 36(2-3), 145-182 (1998) · Zbl 0930.68077
[41] 41. Bérard, B., Dufour, C.: Timed automata and additive clock constraints. Inf. Process. Lett. 75(1-2), 1-7 (2000)
[42] 42. Bérard, B., Gastin, P., Petit, A.: Timed automata with non-observable actions: expressive power and refinement. In: Puech, C., Reischuk, R. (eds.) Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 1046, pp. 257-268. Springer, Heidelberg (1996) · Zbl 1379.68216
[43] 43. Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Mason, R.E.A. (ed.) IFIP World Computer Congress (WCC), pp. 41-46. North-Holland/IFIP, Amsterdam (1983)
[44] 44. Beyer, D., Lewerentz, C., Noack, A.: Rabbit: a tool for BDD-based verification of real-time systems. In: Hunt, W.A. Jr, Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 122-125. Springer, Heidelberg (2003)
[45] 45. Bøgholm, T., Kragh-Hansen, H., Olsen, P., Thomsen, B., Larsen, K.G.: Model-based schedulability analysis of safety critical hard real-time Java programs. In: Bollella, G., Locke, C.D. (eds.) International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES), vol. 343, pp. 106-114. ACM, New York (2008)
[46] 46. Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) International Symposium on Compositionality: The Significant Difference (COMPOS). LNCS, vol. 1536, pp. 103-129. Springer, Heidelberg (1998)
[47] 47. Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: Symposium on Real-Time Systems (RTSS), pp. 25-35. IEEE, Piscataway (1997)
[48] 48. Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 2607, pp. 620-631. Springer, Heidelberg (2003)
[49] 49. Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188-194 (2006) · Zbl 1187.68291
[50] 50. Bouyer, P., Brinksma, E., Larsen, K.G.: Staying alive as cheaply as possible. Form. Methods Syst. Des. 32(1), 2-23 (2008) · Zbl 1135.93352
[51] 51. Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Kamal, L., Mahajan, M. (eds.) Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol. 3328, pp. 148-160. Springer, Heidelberg (2004) · Zbl 1117.68396
[52] 52. Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97-116 (2010) · Zbl 1209.03010
[53] 53. Bouyer, P., Dufour, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2-3), 291-345 (2004) · Zbl 1070.68063
[54] 54. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed automata with observers under energy constraints. In: Johansson, K.H., Yi, W. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC), pp. 61-70. ACM, New York (2010) · Zbl 1361.68135
[55] 55. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol. 5215, pp. 33-47. Springer, Heidelberg (2008) · Zbl 1171.68524
[56] 56. Bouyer, P., Haddad, S., Reynier, P.-A.: Undecidability results for timed automata with silent transitions. Fundam. Inform. 92(1-2), 1-25 (2009) · Zbl 1176.68099
[57] 57. Bouyer, P., Larsen, K.G., Markey, N.: Model checking one-clock priced timed automata. Log. Methods Comput. Sci. 4(2), 1-28 (2008) · Zbl 1149.68401
[58] 58. Bouyer, P., Larsen, K.G., Markey, N.: Lower-bound constrained runs in weighted timed automata. In: Int. Conf. on Quantitative Evaluation of Systems (QEST), pp. 128-137. IEEE, Piscataway (2012)
[59] 59. Bouyer, P., Larsen, K.G., Markey, N., Rasmussen, J.I.: Almost optimal strategies in one-clock priced timed automata. In: Arun-Kumar, S., Garg, N. (eds.) Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol. 4337, pp. 345-356. Springer, Heidelberg (2006) · Zbl 1177.68142
[60] 60. Bozga, M., Jianmin, H., Maler, O., Yovine, S.: Verification of asynchronous circuits using timed automata. In: Asarin, E., Maler, O., Yovine, S. (eds.) Workshop on Theory and Practice of Timed Systems (TPTS). Electronic Notes in Theoretical Computer Science, vol. 65, pp. 47-59. Elsevier, Amsterdam (2002) · Zbl 1270.68164
[61] 61. Brekling, A.W., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Log. Algebraic Program. 77(1-2), 1-19 (2008) · Zbl 1151.68339
[62] 62. Brenguier, R.: Nash equilibria in concurrent games—application to timed games. PhD thesis, Lab. Spécification & Vérification, ENS Cachan, France (2012)
[63] 63. Brihaye, T., Bruyère, V., Raskin, J.-F.: Model-checking for weighted timed automata. In: Lakhnech, Y., Yovine, S. (eds.) Joint Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol. 3253, pp. 277-292. Springer, Heidelberg (2004) · Zbl 1109.68512
[64] 64. Brihaye, T., Bruyère, V., Raskin, J.-F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol. 3829, pp. 49-64. Springer, Heidelberg (2005) · Zbl 1175.68241
[65] 65. Brihaye, T., Henzinger, T.A., Prabhu, V.S., Raskin, J.-F.: Minimum-time reachability in timed games. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 4596, pp. 825-837. Springer, Heidelberg (2007) · Zbl 1171.68526
[66] 66. Brihaye, T., Laroussinie, F., Markey, N., Oreiby, G.: Timed concurrent game structures. In: Caires, L., Vasconcelos, V.T. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 4703, pp. 445-459. Springer, Heidelberg (2007) · Zbl 1151.68510
[67] 67. Brzozowski, J.A., Seger, C.-J.H.: Advances in asynchronous circuit theory part II: bounded inertial delay models, MOS circuits, design techniques. Bull. Eur. Assoc. Theor. Comput. Sci. 43, 199-263 (1991) · Zbl 0747.94024
[68] 68. Byg, J., Jørgensen, K.Y., Srba, J.: TAPAAL: editor, simulator and verifier of timed-arc Petri nets. In: Liu, Z., Ravn, A.P. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 5799, pp. 84-89. Springer, Heidelberg (2009)
[69] 69. Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 3653, pp. 66-80. Springer, Heidelberg (2005) · Zbl 1134.68382
[70] 70. Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, K., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 4762, pp. 192-206. Springer, Heidelberg (2007) · Zbl 1141.68428
[71] 71. Cassez, F., Jensen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers—an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol. 5469, pp. 90-104. Springer, Heidelberg (2009) · Zbl 1237.93058
[72] 72. Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1877, pp. 138-152. Springer, Heidelberg (2000) · Zbl 0999.68112
[73] 73. Čerāns, K.: Decidability of bisimulation equivalences for parallel timer processes. In: von Bochmann, G., Probst, D.K. (eds.) Intl. Workshop on Computer-Aided Verification (CAV). LNCS, vol. 663, pp. 302-315. Springer, Heidelberg (1993)
[74] 74. Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) Int. Conf. on Embedded Software (EMSOFT). LNCS, vol. 2855, pp. 117-133. Springer, Heidelberg (2003)
[75] 75. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244-263 (1986) · Zbl 0591.68027
[76] 76. Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some progress in satisfiability checking for difference logic. In: Lakhnech, Y., Yovine, S. (eds.) Joint Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol. 3253, pp. 263-276. Springer, Heidelberg (2004) · Zbl 1109.68513
[77] 77. Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) International Conference on Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 4121, pp. 170-183. Springer, Heidelberg (2006) · Zbl 1187.68537
[78] 78. David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of Herschel-Planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) International Symposium on Leveraging Applications of Formal Methods (ISoLA). LNCS, vol. 7610, pp. 293-307. Springer, Heidelberg (2012)
[79] 79. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6806, pp. 349-355. Springer, Heidelberg (2011)
[80] 80. David, A., Larsen, K.G., Rasmussen, J.I., Skou, A.: Model-based design for embedded systems. In: Nicolescu, G., Mosterman, P.J. (eds.) Model-Based Design for Embedded Systems. Computational Analysis, Synthesis, and Design of Dynamic Systems. CRC Press, Boca Raton (2009)
[81] 81. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1384, pp. 313-329. Springer, Heidelberg (1998)
[82] 82. de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 2761, pp. 142-156. Springer, Heidelberg (2003) · Zbl 1262.68141
[83] 83. De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Form. Methods Syst. Des. 33(1-3), 45-84 (2008) · Zbl 1165.68392
[84] 84. Dembinski, P., Janowska, A., Janowski, P., Penczek, W., Pólrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: Verics: a tool for verifying timed automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2619, pp. 278-283. Springer, Heidelberg (2003) · Zbl 1031.68546
[85] 85. Dierks, H.: PLC-automata: a new class of implementable real-time automata. Theor. Comput. Sci. 253(1), 61-93 (2001) · Zbl 0954.68085
[86] 86. Dierks, H.: Finding optimal plans for domains with continuous effects with UPPAAL Cora. In: ICAPS Workshop on Verification and Validation of Model-Based Planning and Schedulin Systems (VV&PS) (2005)
[87] 87. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) International Workshop on Automatic Verification Methods for Finite State Systems (AVMFSS). LNCS, vol. 407, pp. 197-212. Springer, Heidelberg (1990)
[88] 88. Ehlers, R., Fass, D., Gerke, M., Peter, H.-J.: Fully symbolic timed model checking using constraint matrix diagrams. In: Symposium on Real-Time Systems (RTSS), pp. 360-371. IEEE, Piscataway (2010)
[89] 89. Faella, M., La Torre, S., Murano, A.: Dense real-time games. In: Symp. on Logic in Computer Science (LICS), pp. 167-176. IEEE, Piscataway (2002) · Zbl 1057.68057
[90] 90. Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2), 301-317 (2006) · Zbl 1088.68087
[91] 91. Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyzing time Petri nets. In: Etessami, K., Rajamani, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 418-423. Springer, Heidelberg (2005) · Zbl 1081.68618
[92] 92. Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) International Workshop on Hybrid and Real-Time Systems (HART). LNCS, vol. 1201, pp. 331-345. Springer, Heidelberg (1997)
[93] 93. Hansen, M.R., Madsen, J., Brekling, A.W.: Semantics and verification of a language for modelling hardware architectures. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Zhou Chaochen on the Occasion of Their 70th Birthdays. LNCS, vol. 4700, pp. 300-319. Springer, Heidelberg (2007) · Zbl 1151.68480
[94] 94. Hansen, T.D., Ibsen-Jensen, R., Miltersen, P.B.: A faster algorithm for solving one-clock priced timed games. In: D’Argenio, P.R., Melgratt, H.C. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 8052, pp. 531-545. Springer, Heidelberg (2013) · Zbl 1390.68387
[95] 95. Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modelling and analysis of an audio/video protocol: an industrial case study using Uppaal. In: Symposium on Real-Time Systems (RTSS), pp. 2-13. IEEE, Piscataway (1997)
[96] 96. Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) Int. Workshop on Formal Modelling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol. 2791. Springer, Heidelberg (2003) · Zbl 1099.68657
[97] 97. Hendriks, M., van den Nieuwelaar, B., Vaandrager, F.: Model checker aided design of a controller for a wafer scanner. Int. J. Softw. Tools Technol. Transf. 8(6), 633-647 (2006)
[98] 98. Henzinger, T.A.: The theory of hybrid automata. In: Symp. on Logic in Computer Science (LICS), pp. 278-292. IEEE, Piscataway (1996) · Zbl 0959.68073
[99] 99. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A user guide to HyTech. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1019, pp. 41-71. Springer, Heidelberg (1995)
[100] 100. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What is decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94-124 (1998) · Zbl 0920.68091
[101] 101. Henzinger, T.A., Kopke, P.W., Wong-Toi, H.: The expressive power of clocks. In: Fülöp, Z., Gecseg, F. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 944, pp. 417-428. Springer, Heidelberg (1995) · Zbl 1412.68131
[102] 102. Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 623, pp. 545-558. Springer, Heidelberg (1992)
[103] 103. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real time systems. Inf. Comput. 111(2), 193-244 (1994) · Zbl 0806.68080
[104] 104. Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 1443, pp. 580-591. Springer, Heidelberg (1998)
[105] 105. Herrmann, P.: Timed automata and recognizability. Inf. Process. Lett. 65(6), 313-318 (1998) · Zbl 0925.68275
[106] 106. Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Log. Algebraic Program. 52-53, 183-220 (2002) · Zbl 1008.68069
[107] 107. Hüttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Symposium on Logical Foundations of Computer Science. LNCS, vol. 363, pp. 163-180. Springer, Heidelberg (1989) · Zbl 0683.03014
[108] 108. Igna, G., Kannan, V., Yang, Y., Basten, T., Geilen, M.C.W., Vaandrager, F., Voorhoeve, M., de Smet, S., Somers, L.J.: Formal modeling and scheduling of datapaths of digital document printers. In: Cassez, F., Jard, C. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol. 5215, pp. 170-187. Springer, Heidelberg (2008)
[109] 109. Jaghoori, M.M., de Boer, F.S., Chothia, T., Sirjani, M.: Schedulability of asynchronous real-time concurrent objects. J. Log. Algebraic Program. 78(5), 402-416 (2009) · Zbl 1188.68085
[110] 110. Jensen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using UPPAAL Tiga. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol. 4763, pp. 227-240. Springer, Heidelberg (2007)
[111] 111. Jørgensen, K.Y., Larsen, K.G., Srba, J.: Time-darts: a data structure for verification of closed timed automata. In: Conference on Systems Software Verification (SSV). Electronic Proceedings in Theoretical Computer Science, vol. 102, pp. 141-155 (2012)
[112] 112. Julliand, J., Mountassir, H., Oudot, É.: VeSTA: a tool to verify the correct integration of a component in a composite timed system. In: Butler, M.J., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) International Conference on Formal Engineering Methods (ICFEM). LNCS, vol. 4789, pp. 116-135. Springer, Heidelberg (2007)
[113] 113. Klimoš, M., Larsen, K.G., Štefaňák, F., Thaarup, J.: Nash equilibria in concurrent priced games. In: Dediu, A.H., Martín-Vide, C. (eds.) Intl. Conf. on Language and Automata Theory and Applications (LATA). LNCS, vol. 7183, pp. 363-376. Springer, Heidelberg (2012) · Zbl 1351.68182
[114] 114. Kupferschmid, S., Dräger, K., Hoffmann, J., Finkbeiner, B., Dierks, H., Podelski, A., Behrmann, G.: Uppaal/DMC—abstraction-based heuristics for directed model checking. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 679-682. Springer, Heidelberg (2007)
[115] 115. Kupferschmid, S., Hoffmann, J., Larsen, K.G.: Fast directed model checking via Russian doll abstraction. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963, pp. 203-217. Springer, Heidelberg (2008) · Zbl 1134.68412
[116] 116. Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster than Uppaal? In: Gupta, A., Malik, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5123, pp. 552-555. Springer, Heidelberg (2008)
[117] 117. La Torre, S., Napoli, M.: A decidable dense branching-time temporal logic. In: Kapoor, S., Prasad, S. (eds.) Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol. 1974, pp. 139-150. Springer, Heidelberg (2000) · Zbl 1044.03012
[118] 118. La Torre, S., Napoli, M.: Timed tree automata with an application to temporal logic. Acta Inform. 38(2), 89-116 (2001) · Zbl 1033.68065
[119] 119. Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 493-505. Springer, Heidelberg (2001) · Zbl 0991.68536
[120] 120. Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: Symposium on Real-Time Systems (RTSS), pp. 14-24. IEEE, Piscataway (1997)
[121] 121. Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nord. J. Comput. 6(3), 271-298 (1999) · Zbl 0937.68086
[122] 122. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1-2), 134-152 (1997) · Zbl 1060.68577
[123] 123. Larsen, K.G., Rasmussen, J.I.: Optimal conditional reachability for multi-priced timed automata. Theor. Comput. Sci. 390(2-3), 197-213 (2008) · Zbl 1134.68029
[124] 124. Lasota, S., Walukiewicz, I.: Alternating timed automata. ACM Trans. Comput. Log. 9(2), 10:1-10:27 (2008) · Zbl 1367.68172
[125] 125. Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 296-311. Springer, Heidelberg (2004) · Zbl 1126.68458
[126] 126. Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci. 345(1), 27-59 (2005) · Zbl 1079.68052
[127] 127. Mader, A., Wupper, H.: Timed automaton models for simple programmable logic controllers. In: Euromicro Conference on Real-Time Systems (ECRTS), pp. 106-113. IEEE, Piscataway (1999)
[128] 128. Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: Mayr, E.W., Puech, C. (eds.) Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 900, pp. 229-242. Springer, Heidelberg (1995) · Zbl 1379.68227
[129] 129. Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N., Krogh, B.H. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol. 1790, pp. 296-310. Springer, Heidelberg (2000) · Zbl 0992.93050
[130] 130. Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989) · Zbl 0683.68008
[131] 131. Minea, M.: Partial order reduction for model checking of timed automata. In: Baeten, J.C.M., Mauw, S. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1664, pp. 431-446. Springer, Heidelberg (1999) · Zbl 0939.68085
[132] 132. Møller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: Flum, J., Rodríguez-Artalejo, M. (eds.) International Workshop on Computer Science Logic (CSL). LNCS, vol. 1862, pp. 111-125. Springer, Heidelberg (1999) · Zbl 0944.68040
[133] 133. Ouaknine, J., Rabinovich, A., Worrell, J.: Time-bounded verification. In: Bravetti, M., Zavattaro, G. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 5710, pp. 496-510. Springer, Heidelberg (2009) · Zbl 1254.68151
[134] 134. Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: closing a decidability gap. In: Symp. on Logic in Computer Science (LICS), pp. 54-63. IEEE, Piscataway (2004)
[135] 135. Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Symp. on Logic in Computer Science (LICS), pp. 188-197. IEEE, Piscataway (2005)
[136] 136. Ouaknine, J., Worrell, J.: On metric temporal logic and faulty Turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) International Conference on Foundations of Software Science and Computation Structure (FoSSaCS. LNCS, vol. 3921, pp. 217-230. Springer, Heidelberg (2006) · Zbl 1180.03021
[137] 137. Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Log. Methods Comput. Sci. 3(1), 1-27 (2007) · Zbl 1128.03008
[138] 138. Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-Conference on Theoretical Computer Science (TCS). LNCS, vol. 104, pp. 167-183. Springer, Heidelberg (1981)
[139] 139. Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol. 1486, pp. 210-227. Springer, Heidelberg (1998)
[140] 140. Raskin, J.-F., Schobbens, P.-Y.: The logic of event-clocks: decidability, complexity and expressiveness. J. Autom. Lang. Comb. 4(3), 247-286 (1999) · Zbl 0978.03015
[141] 141. Roux, O.F., Rusu, V.: Deciding time-bounded properties for ELECTRE reactive programs with stopwatch automata. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems II (HSCC). LNCS, vol. 999, pp. 405-416. Springer, Heidelberg (1995)
[142] 142. Rutkowski, M.: Two-player reachability-price games on single-clock timed automata. In: Workshop on Quantitative Aspects of Programming Languages (QAPL). Electronic Proceedings in Theoretical Computer Science, vol. 57 (2011)
[143] 143. Sankur, O.: Robustness in timed automata: analysis, synthesis, implementation. PhD thesis, Lab. Spécification & Vérification, ENS Cachan, France (2013) · Zbl 1407.68282
[144] 144. Schuts, M., Zhu, Y., Heidarian, F., Vaandrager, F.: Modelling clock synchronization in the Chess gMAC WSN protocol. In: Andova, S., McIver, A.K., D’Argenio, P.R., Cuijpers, P.J.L., Markovski, J., Morgan, C.C., Núñez, M. (eds.) Workshop on Quantitative Formal Methods: Theory and Applications (QFM). Electronic Proceedings in Theoretical Computer Science, vol. 13, pp. 41-54 (2009)
[145] 145. Tapken, J., Dierks, H.: MOBY/PLC—graphical development of PLC-automata. In: Ravn, A.P., Rischel, H. (eds.) Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol. 1486, pp. 311-314. Springer, Heidelberg (1998)
[146] 146. Tripakis, S.: Description and schedulability analysis of the software architecture of an automated vehicle control system. In: Sangiovani-Vincentelli, A.L., Sifakis, J. (eds.) Int. Conf. on Embedded Software (EMSOFT). LNCS, vol. 2491, pp. 123-137. Springer, Heidelberg (2002) · Zbl 1027.68960
[147] 147. Tripakis, S.: Checking timed Büchi automata emptiness on simulation graphs. ACM Trans. Comput. Log. 10(3), 15:1-15:19 (2009) · Zbl 1352.68165
[148] 148. Tripakis, S., Altisen, K.: On-the-fly controller synthesis for discrete and dense-time systems. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) World Congress on Formal Methods (FM). LNCS, vol. 1708, pp. 233-252. Springer, Heidelberg (1999) · Zbl 1037.93522
[149] 149. Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Des. 18(1), 25-68 (2001) · Zbl 0971.68096
[150] 150. Tripakis, S., Yovine, S.: Timing analysis and code generation of vehicle control software using Taxys. In: Havelund, K., Roşu, G. (eds.) International Workshop on Runtime Verification (RV). Electronic Notes in Theoretical Computer Science, vol. 55, pp. 277-286. Elsevier, Amsterdam (2001)
[151] 151. Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed Büchi automata emptiness efficiently. Form. Methods Syst. Des. 26(3), 267-292 (2005) · Zbl 1085.68083
[152] 152. Wang, F.: Model-checking distributed real-time systems with states, events, and multiple fairness assumptions. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) International Conference on Algebraic Methodology and Software Technology (AMAST). LNCS, vol. 3116, pp. 553-567. Springer, Heidelberg (2004) · Zbl 1108.68530
[153] 153. Wang, F.: Efficient model-checking of dense-time systems with time-convexity analysis. Theor. Comput. Sci. 467, 89-108 (2013) · Zbl 1279.68222
[154] 154. Wang, F., Huang, G.-D., Yu, F.: TCTL inevitability analysis of dense-time systems: from theory to engineering. IEEE Trans. Softw. Eng. 32(7), 510-526 (2006)
[155] 155. Wang, F., Yao, L.-W., Yang, Y.-L.: Efficient verification of distributed real-time systems with broadcasting behaviors. Real-Time Syst. 47(4), 285-318 (2011) · Zbl 1230.68155
[156] 156. Waszniowski, L., Hanzálek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39-65 (2008) · Zbl 1133.68381
[157] 157. Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Hogrefe, D., Leue, S. (eds.) Intl. Conf. on Formal Description Techniques (FORTE). IFIP Conference Proceedings, vol. 6, pp. 243-258. Chapman & Hall, London (1995)
[158] 158. Yovine, S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1(1-2), 123-133 (1997) · Zbl 1060.68606
[159] 159. Zennou, S., Yguel, M., Niebert, Peter: ELSE: a new symbolic state generator for timed automata. In: Larsen, K.G., Niebert, P. (eds.) Int. Workshop on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol. 2791, pp. 273-280. Springer, Heidelberg (2003)
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.