Skip to main content
SpringerLink
Log in

Model Checking Real-Time Systems

  • Chapter
  • First Online:
Handbook of Model Checking

Abstract

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).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdeddaïm, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272–300 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  7. Alur, R.: Techniques for automatic verification of real-time systems. PhD thesis, Stanford University (1991)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  9. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  11. Alur, R., Courcoubetis, C., Henzinger, T.A.: Computing accumulated delays in real time systems. Form. Methods Syst. Des. 11(2), 137–155 (1997)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  13. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  14. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  17. Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  18. Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–203 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  23. Arnold, A., Nivat, M.: The metric space of infinite trees. Algebraic and topological properties. Fundam. Inform. 3(4), 445–476 (1980)

    MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  41. Bérard, B., Dufour, C.: Timed automata and additive clock constraints. Inf. Process. Lett. 75(1–2), 1–7 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  49. Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188–194 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  50. Bouyer, P., Brinksma, E., Larsen, K.G.: Staying alive as cheaply as possible. Form. Methods Syst. Des. 32(1), 2–23 (2008)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  52. Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97–116 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  53. Bouyer, P., Dufour, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2–3), 291–345 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  56. Bouyer, P., Haddad, S., Reynier, P.-A.: Undecidability results for timed automata with silent transitions. Fundam. Inform. 92(1–2), 1–25 (2009)

    MathSciNet  MATH  Google Scholar 

  57. Bouyer, P., Larsen, K.G., Markey, N.: Model checking one-clock priced timed automata. Log. Methods Comput. Sci. 4(2), 1–28 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  62. Brenguier, R.: Nash equilibria in concurrent games—application to timed games. PhD thesis, Lab. Spécification & Vérification, ENS Cachan, France (2012)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  85. Dierks, H.: PLC-automata: a new class of implementable real-time automata. Theor. Comput. Sci. 253(1), 61–93 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Article  Google Scholar 

  98. Henzinger, T.A.: The theory of hybrid automata. In: Symp. on Logic in Computer Science (LICS), pp. 278–292. IEEE, Piscataway (1996)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  103. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real time systems. Inf. Comput. 111(2), 193–244 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  105. Herrmann, P.: Timed automata and recognizability. Inf. Process. Lett. 65(6), 313–318 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  118. La Torre, S., Napoli, M.: Timed tree automata with an application to temporal logic. Acta Inform. 38(2), 89–116 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  121. Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nord. J. Comput. 6(3), 271–298 (1999)

    MathSciNet  MATH  Google Scholar 

  122. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)

    Article  MATH  Google Scholar 

  123. Larsen, K.G., Rasmussen, J.I.: Optimal conditional reachability for multi-priced timed automata. Theor. Comput. Sci. 390(2–3), 197–213 (2008)

    Article  MATH  Google Scholar 

  124. Lasota, S., Walukiewicz, I.: Alternating timed automata. ACM Trans. Comput. Log. 9(2), 10:1–10:27 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  130. Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  143. Sankur, O.: Robustness in timed automata: analysis, synthesis, implementation. PhD thesis, Lab. Spécification & Vérification, ENS Cachan, France (2013)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  147. Tripakis, S.: Checking timed Büchi automata emptiness on simulation graphs. ACM Trans. Comput. Log. 10(3), 15:1–15:19 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  149. Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Des. 18(1), 25–68 (2001)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  151. Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed Büchi automata emptiness efficiently. Form. Methods Syst. Des. 26(3), 267–292 (2005)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  153. Wang, F.: Efficient model-checking of dense-time systems with time-convexity analysis. Theor. Comput. Sci. 467, 89–108 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  156. Waszniowski, L., Hanzálek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39–65 (2008)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  158. Yovine, S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1(1–2), 123–133 (1997)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, CNRS & ENS Paris-Saclay, Cachan, France

    Patricia Bouyer & Nicolas Markey

  2. IRISA, CNRS & INRIA & Univ. Rennes 1, Rennes, France

    Nicolas Markey

  3. École Polytechnique, Palaiseau, France

    Uli Fahrenberg

  4. Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen

  5. University of Oxford, Oxford, UK

    Joël Ouaknine & James Worrell

  6. Max Planck Institute for Software Systems, Saarbrücken, Germany

    Joël Ouaknine

Authors
  1. Patricia Bouyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Uli Fahrenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Nicolas Markey
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Joël Ouaknine
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. James Worrell
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nicolas Markey .

Editor information

Editors and Affiliations

  1. FORE Systems University Professor of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    Edmund M. Clarke

  2. Institute of Science and Technology Austria (IST), Klosterneuburg, Austria

    Thomas A. Henzinger

  3. Arbeitsbereich Formal Methods in Systems Engineering, Technische Universität Wien, Wien, Austria

    Helmut Veith

  4. Institut f. Angewandte Informationsverarbeitung und Kommunikationstechnologie (IAIK), Technische Universität Graz, Graz, Austria

    Roderick Bloem

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J. (2018). Model Checking Real-Time Systems. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10575-8_29

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10574-1

  • Online ISBN: 978-3-319-10575-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation