A decidability result for the model checking of infinite-state systems. (English) Zbl 1279.68226
Summary: We present a decidability result for the model checking of a certain class of properties that can be conveniently expressed as ground formulae of a first-order temporal fragment. The decidability result is obtained by importing into the context of model-checking problems some techniques developed for the combination of decision procedures for the satisfiability of constraints. The general decidability result is then specialized for checking properties of particular interest, such as liveness and safety, and, for the latter case, a more optimized algorithm has been proposed.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B25 | Decidability of theories and sets of sentences |
Software:
NuSMVReferences:
| [1] | Abadi, M.: The power of temporal proofs. Theor. Comp. Sci. 65(1), 35–83 (1989) · Zbl 0669.03010 · doi:10.1016/0304-3975(89)90138-2 |
| [2] | Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of the 11th IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 313–321. IEEE Computer Society, New Brunswick, NJ, USA (1996) |
| [3] | Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Van Maaren, H., Biere, A., Heule, M., Walsh, T. (eds.) The Handbook of Satisfiability, vol. II, chap. 26, pp. 887–925. IOS Press, Amsterdam, The Netherlands (2009) |
| [4] | Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Computer Science, vol. 4130, pp. 513–527. Springer, Seattle, WA, USA (2006) · Zbl 1222.03011 |
| [5] | Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, A.E., Sistla, A.P. (eds.) Proceedings of the 12th International Conference on Computer Aided Verification (CAV 2000). Lecture Notes in Computer Science, vol. 1855, pp. 403–418. Springer, Chicago, IL, USA (2000) · Zbl 0974.68118 |
| [6] | Bräuner, T., Ghilardi, S.: First-order modal logic. In: van Benthem, J., Blackburn, P., Wolter, F. (eds.) Handbook of Modal Logic, pp. 549–620. Elsevier, Amsterdam (2007) |
| [7] | Chang, C.-C., Keisler, J.H.: Model Theory, 3rd edn. North Holland, Amsterdam, The Netherlands (1990) |
| [8] | Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002). Lecture Notes in Computer Science, vol. 2404, pp. 359–364. Springer, Copenhagen, Denmark (2002) · Zbl 1010.68766 |
| [9] | Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999) |
| [10] | D’Agostino, G., Hollenberg, M.: Logical questions concerning the {\(\mu\)}-calculus: interpolation, Lyndon and Los-Tarski. J. Symb. Log. 65(1), 310–332 (2000) · Zbl 0982.03011 · doi:10.2307/2586539 |
| [11] | Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Towards a model-checker for counter systems. In: Graf, S., Zhang, W. (eds.) Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006). Lecture Notes in Computer Science, vol. 4218, pp. 493–507. Springer, Beijing, ROC (2006) · Zbl 1161.68563 |
| [12] | Demri, S.: Linear-time temporal logics with Presburger constraints: an overview. J. Appl. Non-Class. Log. 16(3–4), 311–347 (2006) · Zbl 1186.03036 · doi:10.3166/jancl.16.311-347 |
| [13] | de Moura, L.M., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) Proceedings of the 18th International Conference on Automated Deduction (CADE 2002). Lecture Notes in Computer Science, vol. 2392, pp. 438–455. Springer, Copenhagen, Denmark (2002) · Zbl 1072.68602 |
| [14] | Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical logic. In: Undergraduate Texts in Mathematics, 2nd edn. Springer, New York (1994) · Zbl 0795.03001 |
| [15] | Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3–4), 221–249 (2004) · Zbl 1069.03008 · doi:10.1007/s10817-004-6241-5 |
| [16] | Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. In: Pfenning, F. (ed.) Proceedings of the 21st Conference on Automated Deduction (CADE 2007). Lecture Notes in Computer Science, vol. 4603, pp. 362–378. Springer, Bremen, Germany (2007) · Zbl 1213.68378 |
| [17] | Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. Rapporto Interno DSI 313-07, Università degli Studi di Milano, Milano, Italy (2007) · Zbl 1213.68378 |
| [18] | Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Noetherianity and combination problems. In: Konev, B., Wolter, F. (eds.) Proceedings of the 6th International Workshop on Frontiers of Combining Systems (FroCoS 2007). Lecture Notes in Computer Science, vol. 4720, pp. 206–220. Springer, Liverpool, UK (2007) · Zbl 1148.03010 |
| [19] | Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Trans. Comput. Log. 9(2), 1–54 (2008) · doi:10.1145/1342991.1342992 |
| [20] | Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer Aided Verification (CAV 1997). Lecture Notes in Computer Science, vol. 1254, pp. 72–83. Springer, Haifa, Israel (1997) |
| [21] | Hodges, W.: Model theory. In: Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press, Cambridge, UK (1993) · Zbl 0789.03031 |
| [22] | Kröger, F.: On the interpretability of arithmetic in temporal logic. Theor. Comp. Sci. 73(1), 47–60 (1990) · Zbl 0703.03004 · doi:10.1016/0304-3975(90)90161-A |
| [23] | Maidl, M.: A unifying model checking approach for safety properties of parameterized systems. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer Aided Verification (CAV 2001). Lecture Notes in Computer Science, vol. 2102, pp. 311–323. Springer, Paris, France (2001) · Zbl 0991.68047 |
| [24] | Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995) · Zbl 0844.68079 |
| [25] | McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005). Lecture Notes in Computer Science, vol. 3440, pp. 1–12. Springer, Edinburgh, UK (2005) · Zbl 1087.68597 |
| [26] | Merz, S.: Decidability and incompleteness results for first-order temporal logics of linear time. J. Appl. Non-Class. Log. 2(2), 139–156 (1992) · Zbl 0790.03019 · doi:10.1080/11663081.1992.10510779 |
| [27] | Minsky, M.L.: Recursive unsolvability of Post’s problem of ”tag” and other topics in the theory of Turing machines. Ann. Math. 74(3), 437–455 (1961) · Zbl 0105.00802 · doi:10.2307/1970290 |
| [28] | Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079 |
| [29] | Nicolini, E.: Combined decision procedures for constraint satisfiability. Ph.D. thesis, Dipartimento di Matematica, Università degli Studi di Milano, Milano, Italy (2007) |
| [30] | Pitts, A.M.: On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log. 57(1), 33–52 (1992) · Zbl 0763.03009 · doi:10.2307/2275175 |
| [31] | Plaisted, D.A.: A decision procedure for combination of propositional temporal logic and other specialized theories. J. Autom. Reason. 2(2), 171–190 (1986) · Zbl 0635.03026 · doi:10.1007/BF02432150 |
| [32] | Rybina, T., Voronkov, A.: A logical reconstruction of reachability. In: Broy, M., Zamulin, A.V. (eds.) 5th International Andrei Ershov Memorial Conference (PSI 2003). Lecture Notes in Computer Science, vol. 2890, pp. 222–237. Springer, Akademgorodok, Novosibirsk, Russia (2003) · Zbl 1254.68153 |
| [33] | Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Form. Methods Syst. Des. 15(1), 49–74 (1999) · doi:10.1023/A:1008791913551 |
| [34] | Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Computer Science, vol. 4130, pp. 235–250. Springer, Seattle, WA, USA (2006) · Zbl 1222.03018 |
| [35] | Szalas, A.: Concerning the semantic consequence relation in first-order temporal logic. Theor. Comp. Sci. 47(3), 329–334 (1986) · Zbl 0622.03012 · doi:10.1016/0304-3975(86)90157-X |
| [36] | Szalas, A., Holenderski, L.: Incompleteness of first-order temporal logic with until. Theor. Comp. Sci. 57, 317–325 (1988) · Zbl 0677.03013 · doi:10.1016/0304-3975(88)90045-X |
| [37] | Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K. (eds.) Proceedings of the 1st International Workshop on Frontiers of Combining Systems (FroCoS 1996), Applied Logic, pp. 103–120. Kluwer, Munich, Germany (1996) · Zbl 0893.03001 |
| [38] | Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comp. Sci. 290(1), 291–353 (2003) · Zbl 1018.68033 · doi:10.1016/S0304-3975(01)00332-2 |
| [39] | Visser, A.: Uniform interpolation and layered bisimulation. In: Hájek, P. (ed.) Proceedings of Gödel96: Logical Foundations of Mathematics, Computer Science, and Physics. Lecture Notes Logic, vol. 6, , pp. 139–164. Springer, Brno, Czech Republic (1996) · Zbl 0854.03026 |
| [40] | Zucchelli, D.: Combination methods for software verification. Ph.D. thesis, Università degli Studi di Milano and Université Henri Poincaré - Nancy 1, Milano, Italy (2007) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
