×

zbMATH — the first resource for mathematics

Formally verified algorithms for upper-bounding state space diameters. (English) Zbl 06921422
Summary: A completeness threshold is required to guarantee the completeness of planning as satisfiability, and bounded model checking of safety properties. We investigate completeness thresholds related to the diameter of the underlying transition system. A valid threshold, the diameter is the maximum element in the set of lengths of all shortest paths between pairs of states. The diameter is not calculated exactly in our setting, where the transition system is succinctly described using a (propositionally) factored representation. Rather, an upper bound on the diameter is calculated compositionally, by bounding the diameters of small abstract subsystems, and then composing those. We describe our formal verification in HOL4 of compositional algorithms for computing a relatively tight upper bound on the system diameter. Existing compositional algorithms are characterised in terms of the problem structures they exploit, including acyclicity in state-variable dependencies, and acyclicity in the state space. Such algorithms are further distinguished by: (1) whether the bound calculated for abstractions is the diameter, sublist diameter or recurrence diameter, and (2) the “direction” of traversal of the compositional structure, either top-down or bottom-up. As a supplement, we publish our library – now over 14k lines – of HOL4 proof scripts about transition systems. That shall be of use to future related mechanisation efforts, and is carefully designed for compatibility with hybrid systems.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abboud, A., Williams, V.V., Wang, J.: Approximation and fixed parameter subquadratic algorithms for radius and diameter in sparse graphs. In: Proceedings of the Twenty-Seventh Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 377-391. SIAM (2016) · Zbl 1410.68392
[2] Abdulaziz, M., Gretton, C., Norrish, M.: Mechanising theoretical upper bounds in planning. In: Workshop on Knowledge Engineering for Planning and Scheduling (2014)
[3] Abdulaziz, M., Gretton, C., Norrish, M.: Verified over-approximation of the diameter of propositionally factored transition systems. In: Interactive Theorem Proving, pp. 1-16. Springer, Berlin (2015) · Zbl 06481852
[4] Abdulaziz, M., Gretton, C., Norrish, M.: A state space acyclicity property for exponentially tighter plan length bounds. In: International Conference on Automated Planning and Scheduling (ICAPS). AAAI (2017)
[5] Aingworth, D; Chekuri, C; Indyk, P; Motwani, R, Fast estimation of diameter and shortest paths (without matrix multiplication), SIAM J. Comput., 28, 1167-1181, (1999) · Zbl 0926.68093
[6] Alon, N; Galil, Z; Margalit, O, On the exponent of the all pairs shortest path problem, J. Comput. Syst. Sci., 54, 255-262, (1997) · Zbl 0877.68090
[7] Alon, N; Yuster, R; Zwick, U, Color-coding, J. ACM (JACM), 42, 844-856, (1995) · Zbl 0885.68116
[8] Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Computer Aided Verification, pp. 151-165. Springer, Berlin (2002) · Zbl 1010.68514
[9] Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: Compositionality: The Significant Difference, pp. 81-102. Springer, Berlin (1998)
[10] Biere, A; Cimatti, A; Clarke, EM; Strichman, O; Zhu, Y, Bounded model checking, Adv. Comput., 58, 117-148, (2003)
[11] Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, pp. 193-207 (1999)
[12] Björklund, A; Husfeldt, T, Finding a path of superlogarithmic length, SIAM J. Comput., 32, 1395-1402, (2003) · Zbl 1041.68066
[13] Björklund, A., Husfeldt, T., Khanna, S.: Approximating longest directed paths and cycles. In: International Colloquium on Automata, Languages, and Programming, pp. 222-233. Springer, Berlin (2004) · Zbl 1098.68094
[14] Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Interactive Theorem Proving, First International Conference, ITP 2010, pp. 131-146 (2010). https://doi.org/10.1007/978-3-642-14052-5_11 · Zbl 1291.68326
[15] Bundala, D., Ouaknine, J., Worrell, J.: On the magnitude of completeness thresholds in bounded model checking. In: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, pp. 155-164. IEEE Computer Society (2012) · Zbl 1360.68579
[16] Case, M.L., Mony, H., Baumgartner, J., Kanzelman, R.: Enhanced verification by temporal decomposition. In: FMCAD 2009, pp. 17-24. Austin (2009)
[17] Chan, TM, More algorithms for all-pairs shortest paths in weighted graphs, SIAM J. Comput., 39, 2075-2089, (2010) · Zbl 1207.68436
[18] Chechik, S., Larkin, D.H., Roditty, L., Schoenebeck, G., Tarjan, R.E., Williams, V.V.: Better approximation algorithms for the graph diameter. In: Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 1041-1052. Society for Industrial and Applied Mathematics (2014)
[19] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Informatics, pp. 176-194. Springer, Berlin (2001)
[20] Clarke, EM; Emerson, EA; Sifakis, J, Turing lecture: model checking-algorithmic verification and debugging, Commun. ACM, 52, 74-84, (2009)
[21] Clarke, EM; Grumberg, O; Long, DE, Model checking and abstraction, ACM Trans. Program. Lang. Syst. (TOPLAS), 16, 1512-1542, (1994)
[22] Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively formalizing automata theory. In: Proof, Language, and Interaction, pp. 213-238 (2000) · Zbl 0698.05045
[23] Dankelmann, P, The diameter of directed graphs, J. Comb. Theory Ser. B, 94, 183-186, (2005) · Zbl 1064.05050
[24] Dankelmann, P; Dorfling, M, Diameter and maximum degree in Eulerian digraphs, Discrete Math., 339, 1355-1361, (2016) · Zbl 1329.05126
[25] Dankelmann, P; Volkmann, L, The diameter of almost Eulerian digraphs, Electron. J. Comb., 17, r157, (2010) · Zbl 1204.05042
[26] Doczkal, C., Kaiser, J.O., Smolka, G.: A constructive theory of regular languages in Coq. In: International Conference on Certified Programs and Proofs, pp. 82-97. Springer, Berlin (2013) · Zbl 1426.68143
[27] Erdős, P; Pach, J; Pollack, R; Tuza, Z, Radius, diameter, and minimum degree, J. Comb. Theory Ser. B, 47, 73-79, (1989) · Zbl 0686.05029
[28] Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable LTL model checker. In: International Conference on Computer Aided Verification, pp. 463-478. Springer, Berlin (2013) · Zbl 1258.03046
[29] Fikes, RE; Nilsson, NJ, Strips: a new approach to the application of theorem proving to problem solving, Artif. Intell., 2, 189-208, (1971) · Zbl 0234.68036
[30] Filiot, E; Jin, N; Raskin, JF, Antichains and compositional algorithms for LTL synthesis, Formal Methods Syst. Des., 39, 261-296, (2011) · Zbl 1258.03046
[31] Fredman, ML, New bounds on the complexity of the shortest path problem, SIAM J. Comput., 5, 83-89, (1976) · Zbl 0326.68027
[32] Helmert, M, The fast downward planning system, J. Artif. Intell. Res., 26, 191-246, (2006) · Zbl 1182.68245
[33] Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)
[34] Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359-363 (1992) · Zbl 1329.05126
[35] Knoblock, CA, Automatically generating abstractions for planning, Artif. Intell., 68, 243-302, (1994) · Zbl 0942.68712
[36] Knyazev, A, Diameters of pseudosymmetric graphs, Math. Notes, 41, 473-482, (1987) · Zbl 0698.05045
[37] Kroening, D, Computing over-approximations with bounded model checking, Electron. Notes Theor. Comput. Sci., 144, 79-92, (2006) · Zbl 1272.68264
[38] Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: Computer Aided Verification, pp. 557-572. Springer, Berlin (2011) · Zbl 1360.68592
[39] Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: VMCAI, pp. 298-309 (2003) · Zbl 1022.68579
[40] McMillan, K.L.: Symbolic model checking. In: Symbolic Model Checking, pp. 25-60. Springer, Berlin (1993)
[41] Moon, JW; etal., On the diameter of a graph, Mich. Math. J., 12, 349-351, (1965) · Zbl 0134.19603
[42] Nipkow, T.: Verifying a hotel key card system. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) Theoretical Aspects of Computing (ICTAC 2006), Lecture Notes in Computer Science, vol. 4281. Springer, Berlin (2006). Invited paper · Zbl 1168.68542
[43] Pardalos, PM; Migdalas, A, A note on the complexity of longest path problems related to graph coloring, Appl. Math. Lett., 17, 13-15, (2004) · Zbl 1039.05036
[44] Paulson, L.C.: A formalisation of finite automata using hereditarily finite sets. In: International Conference on Automated Deduction, pp. 231-245. Springer, Berlin (2015) · Zbl 06515509
[45] Pnueli, A; Rodeh, Y; Strichman, O; Siegel, M, The small model property: how small can it be?, Inf. Comput., 178, 279-293, (2002) · Zbl 1012.03040
[46] Rintanen, J, Planning as satisfiability: heuristics, Artif. Intell., 193, 45-86, (2012) · Zbl 1270.68276
[47] Rintanen, J., Gretton, C.O.: Computing upper bounds on lengths of transition sequences. In: International Joint Conference on Artificial Intelligence (2013)
[48] Robinson, N., Gretton, C., Pham, D.N., Sattar, A.: SAT-based parallel planning using a split representation of actions. In: ICAPS (2009)
[49] Roditty, L., Vassilevska Williams, V.: Fast approximation algorithms for the diameter and radius of sparse graphs. In: Proceedings of the Forty-Fifth Annual ACM Symposium on Theory of Computing, pp. 515-524. ACM (2013) · Zbl 1293.05184
[50] Schimpf, A., Merz, S., Smaus, J.G.: Construction of Büchi automata for LTL model checking verified in Isabelle/HOL. In: International Conference on Theorem Proving in Higher Order Logics, pp. 424-439. Springer, Berlin (2009) · Zbl 1252.68196
[51] Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Proceedings, pp. 108-125 (2000). https://doi.org/10.1007/3-540-40922-X_8 · Zbl 0885.68116
[52] Slind, K., Norrish, M.: A brief overview of HOL4. In: Theorem Proving in Higher Order Logics, LNCS, vol. 5170, pp. 28-32. Springer, Berlin (2008) · Zbl 1165.68474
[53] Soares, J, Maximum diameter of regular digraphs, J. Graph Theory, 16, 437-450, (1992) · Zbl 0768.05048
[54] Sprenger, C.: A verified model checker for the modal \(μ \)-calculus in Coq. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 167-183. Springer, Berlin (1998)
[55] Williams, B.C., Nayak, P.P.: A reactive planner for a model-based executive. In: International Joint Conference on Artificial Intelligence, pp. 1178-1185. Morgan Kaufmann Publishers, Los Altos (1997)
[56] Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl). In: International Conference on Interactive Theorem Proving, pp. 341-356. Springer, Berlin (2011) · Zbl 1342.68306
[57] Yuster, R.: Computing the Diameter Polynomially Faster Than APSP. arXiv preprint arXiv:1011.6181 (2010)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.