Skip to main content
SpringerLink
Log in
Book cover

Handbook of Model Checking pp 1111–1147Cite as

Symbolic Model Checking in Non-Boolean Domains

  • Chapter
  • First Online:

  • 9494 Accesses

Abstract

We consider symbolic model checking as a general procedure to compute fixed points on general lattices. We show that this view provides a unified approach for formal reasoning about systems that is applicable to many different classes of systems and properties. Our unified view is based on the notion of region algebras together with appropriate generalizations of the modal \(\mu\)-calculus. We show applications of our general approach to problems in infinite-state verification, reactive synthesis, and the analysis of probabilistic systems.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Symp. on Logic in Computer Science (LICS), pp. 313–321. IEEE, Piscataway (1996)

    Google Scholar 

  2. de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R., Lugiez, D. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 2761, pp. 102–126. Springer, Heidelberg (2003)

    Google Scholar 

  3. de Alfaro, L., Faella, M., Henzinger, T., 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 

  4. de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theor. Comput. Sci. 345(1), 139–170 (2005)

    Article  MathSciNet  Google Scholar 

  5. de Alfaro, L., Henzinger, T.: Concurrent omega-regular games. In: Symp. on Logic in Computer Science (LICS), pp. 141–154. IEEE, Piscataway (2000)

    Google Scholar 

  6. de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 564–575. IEEE, Piscataway (1998)

    Google Scholar 

  7. de Alfaro, L., Henzinger, T., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: Symp. on Logic in Computer Science (LICS), pp. 279–290. IEEE, Piscataway (2001)

    Google Scholar 

  8. de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: Larsen, K.G., Nielsen, M. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 2154, pp. 536–550 (2001)

    Google Scholar 

  9. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)

    Article  MathSciNet  Google Scholar 

  10. de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Log. Methods Comput. Sci. 4(3) (2008)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  12. Alur, R., Henzinger, T., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  13. Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P., Nerode, A., Kohn, W., Sastry, S. (eds.) Hybrid Systems (II). LNCS, vol. 999, pp. 1–20. Springer, Heidelberg (1995)

    MATH  Google Scholar 

  14. Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)

    Article  MathSciNet  Google Scholar 

  15. Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. 10(5), 401–424 (2008)

    Article  Google Scholar 

  16. Basu, S.: New results on quantifier elimination over real closed fields and applications to constraint databases. J. ACM 46(4), 537–555 (1999)

    Article  MathSciNet  Google Scholar 

  17. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K., Lime, D.: UPPAAL-Tiga: time for playing games! In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Bhat, G., Cleaveland, R.: Efficient local model-checking for fragments of the modal \(\mu\)-calculus. In: Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1055, pp. 107–126. Springer, Heidelberg (1996)

    Google Scholar 

  19. Bloem, R., Chatterjee, K., Henzinger, T., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911–938 (2012)

    Article  MathSciNet  Google Scholar 

  21. Bodík, R., Chandra, S., Galenson, J., Kimelman, D., Tung, N., Barman, S., Rodarmor, C.: Programming with angelic nondeterminism. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 339–352. ACM, New York (2010)

    MATH  Google Scholar 

  22. Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  23. Boigelot, B.: Domain-specific regular acceleration. Int. J. Softw. Tools Technol. Transf. 14(2), 193–206 (2012)

    Article  Google Scholar 

  24. Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 2083. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  25. Bouajjani, A., Habermehl, P., Holík, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) Implementation and Applications of Automata (CIAA). LNCS, vol. 5148, pp. 57–67. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  26. Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855. Springer, Heidelberg (2000)

    Google Scholar 

  27. Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404. Springer, Heidelberg (2002)

    Google Scholar 

  28. Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003)

    Google Scholar 

  29. Bradfield, J.: The modal \(\mu\)-calculus alternation hierarchy is strict. Theor. Comput. Sci. 195(2), 133–153 (1998)

    Article  MathSciNet  Google Scholar 

  30. van Breugel, F., Worrel, J.: Towards quantitative verification of probabilistic systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) Intl. Colloquium on Automata, Languages and Programming. LNCS, vol. 2076, pp. 421–432. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  31. Bryant, R.: Graph-based algorithms for Boolean function manipulation. Trans. Comput. C-35(8), 677–691 (1986)

    Article  Google Scholar 

  32. Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite systems using Presburger arithmetic. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 400–411. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  33. Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  Google Scholar 

  34. Bustan, D., Kupferman, O., Vardi, M.: A measured collapse of the modal \(\mu\)-calculus. In: Diekert, V., Habib, M. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 2996, pp. 522–533. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  35. Cassez, F., David, A., Fleury, E., Larsen, K., 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 

  36. Chandra, S., Torlak, E., Barman, S., Bodík, R.: Angelic debugging. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Intl. Conf. on Software Engineering (ICSE), pp. 121–130. ACM, New York (2011)

    Google Scholar 

  37. Chatterjee, K., de Alfaro, L., Henzinger, T.: The complexity of quantitative concurrent parity games. In: Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 678–687. ACM, New York (2006)

    Google Scholar 

  38. Chatterjee, K., de Alfaro, L., Henzinger, T.: Qualitative concurrent parity games. Trans. Comput. Log. 12(4), 28 (2011)

    MathSciNet  MATH  Google Scholar 

  39. Chatterjee, K., Doyen, L., Henzinger, T.: Quantitative languages. Trans. Comput. Log. 11(4), 23:1–23:38 (2010)

    MathSciNet  MATH  Google Scholar 

  40. Chatterjee, K., Henzinger, T.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 107–138. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  41. Chatterjee, K., Henzinger, T.: A survey of stochastic \(\omega\)-regular games. J. Comput. Syst. Sci. 78(2), 394–413 (2012)

    Article  MathSciNet  Google Scholar 

  42. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Symp. on Principles of Programming Languages (POPL). ACM, New York (1977)

    MATH  Google Scholar 

  43. Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) Programming Language Implementation and Logic Programming (PLILP). LNCS, vol. 631. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  44. Dam, M.: CTL∗ and ECTL∗ as fragments of the modal \(\mu\)-calculus. Theor. Comput. Sci. 126, 77–96 (1994)

    Article  Google Scholar 

  45. De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  46. De Wulf, M., Doyen, L., Maquet, N., Raskin, J.F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. 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. 63–77. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  47. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1664, pp. 258–273. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  48. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Symp. on Logic in Computer Science (LICS), pp. 413–422. IEEE, Piscataway (2002)

    Google Scholar 

  49. Dickson, L.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. Math. 35, 413–422 (1913)

    Article  MathSciNet  Google Scholar 

  50. Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  51. Doyen, L., Raskin, J.F.: Antichains for the automata-based approach to model-checking. Log. Methods Comput. Sci. 1, 5 (2009)

    MathSciNet  MATH  Google Scholar 

  52. Doyen, L., Raskin, J.F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6015, pp. 2–22. Springer, Heidelberg (2010)

    Google Scholar 

  53. Emerson, E., Jutla, C.: Tree automata, mu-calculus and determinacy. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 368–377. IEEE, Piscataway (1991)

    Google Scholar 

  54. Emerson, E., Lei, C.: Efficient model checking in fragments of the propositional \(\mu\)-calculus. In: Symp. on Logic in Computer Science (LICS), pp. 267–278. IEEE, Piscataway (1986)

    Google Scholar 

  55. Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electron. Notes Theor. Comput. Sci. 220(3), 61–77 (2008)

    Article  Google Scholar 

  56. Filiot, E., Jin, N., Raskin, J.F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  57. Filiot, E., Jin, N., Raskin, J.F.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261–296 (2011)

    Article  Google Scholar 

  58. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere. Tech. Rep. LSV-98-4, Laboratoire Spécification et Vérification (1998)

    Google Scholar 

  59. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008)

    Article  MathSciNet  Google Scholar 

  60. Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Hall, M.W., Padua, D.A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 62–73. ACM, New York (2011)

    Google Scholar 

  61. Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Lewis, H.R., Simons, B.B., Burkhard, W.A., Landweber, L.H. (eds.) Annual Symp. on the Theory of Computing, pp. 60–65. ACM, New York (1982)

    Google Scholar 

  62. Henzinger, T., Ho, P.H., Wong-Toi, H.: HyTech: the next generation. In: Real-Time Systems Symposium (RTSS), pp. 56–65. IEEE, Piscataway (1995)

    Google Scholar 

  63. Henzinger, T., Horowitz, B., Majumdar, R.: Rectangular hybrid games. In: Baeten, J., Mauw, S. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1664, pp. 320–335. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  64. Henzinger, T., Kupferman, O., Qadeer, S.: From prehistoric to postmodern symbolic model checking. In: Hu, A., Vardi, M. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1427, pp. 195–206. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  65. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)

    Article  MathSciNet  Google Scholar 

  66. Henzinger, T.A., Majumdar, R., Raskin, J.F.: A classification of symbolic transition systems. Trans. Comput. Log. 6(1), 1–32 (2005)

    Article  MathSciNet  Google Scholar 

  67. Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.A.: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 258–262. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  68. Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441–460 (2012)

    Article  MathSciNet  Google Scholar 

  69. Kechris, A.: Classical Descriptive Set Theory. Springer, Heidelberg (1994)

    MATH  Google Scholar 

  70. Könighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Bjesse, P., Slobodová, A. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 91–100. FMCAD, Austin (2011)

    Google Scholar 

  71. Kozen, D.: Results on the propositional \(\mu\)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983)

    Article  MathSciNet  Google Scholar 

  72. Kress-Gazit, H., Wongpiromsarn, T., Topcu, U.: Correct, reactive robot control from abstraction and temporal logic specifications. Robot. Autom. Mag. 18(3), 65–74 (2011)

    Article  Google Scholar 

  73. Kristoffer, S., Frederiksen, S., Miltersen, P.: Approximating the value of a concurrent reachability game in the polynomial time hierarchy. In: Cai, L., Cheng, S.W., Lam, T. (eds.) Intl. Symposium on Algorithms and Computation (ISAAC). LNCS, vol. 8283, pp. 457–467. Springer, Heidelberg (2013)

    Google Scholar 

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

    Article  Google Scholar 

  75. Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)

    MATH  Google Scholar 

  76. Martin, D.: Borel determinacy. Ann. Math. 102, 363–371 (1975)

    Article  MathSciNet  Google Scholar 

  77. Martin, D.: The determinacy of Blackwell games. J. Symb. Log. 63(4), 1565–1581 (1998)

    Article  MathSciNet  Google Scholar 

  78. McMillan, K.: Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic, Norwell (1993)

    Book  Google Scholar 

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

    MATH  Google Scholar 

  80. Miné, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31–100 (2006)

    Article  Google Scholar 

  81. von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1947)

    MATH  Google Scholar 

  82. Owen, G.: Game Theory. Academic Press, Cambridge (1995)

    MATH  Google Scholar 

  83. Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 46–57. IEEE, Piscataway (1977)

    Google Scholar 

  84. Reisig, W.: Petri Nets: An Introduction. Springer, Heidelberg (1985)

    Book  Google Scholar 

  85. Solar-Lezama, A., Rabbah, R., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Sarkar, V., Hall, M.W. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 281–294. ACM, New York (2005)

    Google Scholar 

  86. Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Intl. Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404–415. ACM, New York (2006)

    Chapter  Google Scholar 

  87. Srivastava, S., Gulwani, S., Foster, J.: From program verification to program synthesis. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 313–326. ACM, New York (2010)

    Google Scholar 

  88. Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, Massachusetts Institute of Technology (1974)

    Google Scholar 

  89. Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. Elsevier, Amsterdam (1990)

    Google Scholar 

  90. Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)

    Google Scholar 

  91. Vardi, M.: Automatic verification of probabilistic concurrent finite-state systems. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 327–338. IEEE, Piscataway (1985)

    Google Scholar 

  92. Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)

    Article  MathSciNet  Google Scholar 

  93. Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints (extended abstract). In: Mycroft, A. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 983. Springer, Heidelberg (1995)

    Google Scholar 

  94. Wong-Toi, H.: The synthesis of controllers for linear hybrid automata. In: Decision and Control, pp. 4607–4612. IEEE, Piscataway (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

  2. Université libre de Bruxelles, Brussels, Belgium

    Jean-François Raskin

Authors
  1. Rupak Majumdar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-François Raskin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rupak Majumdar .

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

Majumdar, R., Raskin, JF. (2018). Symbolic Model Checking in Non-Boolean Domains. 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_31

Download citation

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

  • 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