Symbolic model checking in non-Boolean domains. (English) Zbl 1392.68259

Majumdar, Rupak; Raskin, Jean-François

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). 1111-1147 (2018).

Summary: 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.
For the entire collection see [Zbl 1390.68001].

MSC:

68Q60

Specification and verification (program logics, model checking, etc.)

Software:

Acacia+; PHAVer; HyTech; UPPAAL TIGA; PPL; Antichains; Uppaal; FAST

References:

[1]	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)
[2]	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) · Zbl 1274.68209
[3]	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) · Zbl 1262.68141
[4]	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) · Zbl 1079.68062
[5]	5. de Alfaro, L., Henzinger, T.: Concurrent omega-regular games. In: Symp. on Logic in Computer Science (LICS), pp. 141-154. IEEE, Piscataway (2000)
[6]	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) · Zbl 1154.91306
[7]	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)
[8]	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) · Zbl 1006.68095
[9]	9. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374-397 (2004) · Zbl 1093.91001
[10]	10. de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Log. Methods Comput. Sci. 4(3) (2008) · Zbl 1147.68056
[11]	11. Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183-235 (1994) · Zbl 0803.68071
[12]	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) · Zbl 1070.68524
[13]	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)
[14]	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)
[15]	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)
[16]	16. Basu, S.: New results on quantifier elimination over real closed fields and applications to constraint databases. J. ACM 46(4), 537-555 (1999) · Zbl 1065.03507
[17]	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)
[18]	18. Bhat, G., Cleaveland, R.: Efficient local model-checking for fragments of the modal
[19]	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) · Zbl 1242.68151
[20]	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) · Zbl 1247.68050
[21]	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) · Zbl 1312.68053
[22]	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)
[23]	23. Boigelot, B.: Domain-specific regular acceleration. Int. J. Softw. Tools Technol. Transf. 14(2), 193-206 (2012)
[24]	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) · Zbl 0988.03022
[25]	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) · Zbl 1172.68493
[26]	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) · Zbl 0974.68118
[27]	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) · Zbl 1010.68085
[28]	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)
[29]	29. Bradfield, J.: The modal · Zbl 0915.03017
[30]	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) · Zbl 0986.68093
[31]	31. Bryant, R.: Graph-based algorithms for Boolean function manipulation. Trans. Comput. C-35(8), 677-691 (1986) · Zbl 0593.94022
[32]	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)
[33]	33. Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: · Zbl 0753.68066
[34]	34. Bustan, D., Kupferman, O., Vardi, M.: A measured collapse of the modal · Zbl 1122.68470
[35]	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) · Zbl 1134.68382
[36]	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)
[37]	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) · Zbl 1192.68430
[38]	38. Chatterjee, K., de Alfaro, L., Henzinger, T.: Qualitative concurrent parity games. Trans. Comput. Log. 12(4), 28 (2011) · Zbl 1351.68179
[39]	39. Chatterjee, K., Doyen, L., Henzinger, T.: Quantitative languages. Trans. Comput. Log. 11(4), 23:1-23:38 (2010) · Zbl 1351.68155
[40]	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) · Zbl 1143.68042
[41]	41. Chatterjee, K., Henzinger, T.: A survey of stochastic · Zbl 1237.91036
[42]	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) · Zbl 1149.68389
[43]	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) · Zbl 0776.68024
[44]	44. Dam, M.: CTL\^{}{∗} and ECTL\^{}{∗} as fragments of the modal · Zbl 0798.03018
[45]	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) · Zbl 1188.68171
[46]	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) · Zbl 1134.68404
[47]	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) · Zbl 0939.68081
[48]	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)
[49]	49. Dickson, L.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. Math. 35, 413-422 (1913) · JFM 44.0220.02
[50]	50. Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976) · Zbl 0368.68005
[51]	51. Doyen, L., Raskin, J.F.: Antichains for the automata-based approach to model-checking. Log. Methods Comput. Sci. 1, 5 (2009) · Zbl 1164.68021
[52]	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) · Zbl 1284.68348
[53]	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)
[54]	54. Emerson, E., Lei, C.: Efficient model checking in fragments of the propositional
[55]	55. Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electron. Notes Theor. Comput. Sci. 220(3), 61-77 (2008) · Zbl 1286.68313
[56]	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) · Zbl 1242.68158
[57]	57. Filiot, E., Jin, N., Raskin, J.F.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261-296 (2011) · Zbl 1258.03046
[58]	58. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere. Tech. Rep. LSV-98-4, Laboratoire Spécification et Vérification (1998) · Zbl 0973.68170
[59]	59. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263-279 (2008)
[60]	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)
[61]	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)
[62]	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)
[63]	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) · Zbl 0937.91005
[64]	64. Henzinger, T., Kupferman, O., Qadeer, S.: From \(pre\)historic to \(post\)modern 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) · Zbl 1074.68036
[65]	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) · Zbl 0920.68091
[66]	66. Henzinger, T.A., Majumdar, R., Raskin, J.F.: A classification of symbolic transition systems. Trans. Comput. Log. 6(1), 1-32 (2005) · Zbl 1367.68193
[67]	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)
[68]	68. Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441-460 (2012) · Zbl 1263.68112
[69]	69. Kechris, A.: Classical Descriptive Set Theory. Springer, Heidelberg (1994) · Zbl 0805.54035
[70]	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)
[71]	71. Kozen, D.: Results on the propositional · Zbl 0553.03007
[72]	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)
[73]	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) · Zbl 1406.68040
[74]	74. 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
[75]	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) · Zbl 1379.68227
[76]	76. Martin, D.: Borel determinacy. Ann. Math. 102, 363-371 (1975) · Zbl 0336.02049
[77]	77. Martin, D.: The determinacy of Blackwell games. J. Symb. Log. 63(4), 1565-1581 (1998) · Zbl 0926.03071
[78]	78. McMillan, K.: Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic, Norwell (1993)
[79]	79. Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989) · Zbl 0683.68008
[80]	80. Miné, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31-100 (2006) · Zbl 1105.68069
[81]	81. von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1947) · Zbl 1241.91002
[82]	82. Owen, G.: Game Theory. Academic Press, Cambridge (1995) · Zbl 1284.91004
[83]	83. Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 46-57. IEEE, Piscataway (1977)
[84]	84. Reisig, W.: Petri Nets: An Introduction. Springer, Heidelberg (1985) · Zbl 0555.68033
[85]	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)
[86]	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)
[87]	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) · Zbl 1312.68068
[88]	88. Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, Massachusetts Institute of Technology (1974)
[89]	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) · Zbl 0900.68316
[90]	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) · Zbl 1379.68233
[91]	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)
[92]	92. Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1-37 (1994) · Zbl 0827.03009
[93]	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)
[94]	94. Wong-Toi, H.: The synthesis of controllers for linear hybrid automata. In: Decision and Control, pp. 4607-4612. IEEE, Piscataway (1997)