{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:01Z","timestamp":1740123361097,"version":"3.37.3"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,2,3]],"date-time":"2018-02-03T00:00:00Z","timestamp":1517616000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000943","name":"Commonwealth Scientific and Industrial Research Organisation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000943","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-018-9450-z","type":"journal-article","created":{"date-parts":[[2018,2,3]],"date-time":"2018-02-03T02:55:56Z","timestamp":1517626556000},"page":"485-520","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formally Verified Algorithms for Upper-Bounding State Space Diameters"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8244-518X","authenticated-orcid":false,"given":"Mohammad","family":"Abdulaziz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"Gretton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,2,3]]},"reference":[{"key":"9450_CR1","doi-asserted-by":"crossref","unstructured":"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\u2013391. SIAM (2016)","DOI":"10.1137\/1.9781611974331.ch28"},{"key":"9450_CR2","unstructured":"Abdulaziz, M., Gretton, C., Norrish, M.: Mechanising theoretical upper bounds in planning. In: Workshop on Knowledge Engineering for Planning and Scheduling (2014)"},{"key":"9450_CR3","doi-asserted-by":"crossref","unstructured":"Abdulaziz, M., Gretton, C., Norrish, M.: Verified over-approximation of the diameter of propositionally factored transition systems. In: Interactive Theorem Proving, pp. 1\u201316. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-22102-1_1"},{"key":"9450_CR4","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1609\/icaps.v27i1.13837"},{"issue":"4","key":"9450_CR5","doi-asserted-by":"publisher","first-page":"1167","DOI":"10.1137\/S0097539796303421","volume":"28","author":"D Aingworth","year":"1999","unstructured":"Aingworth, D., Chekuri, C., Indyk, P., Motwani, R.: Fast estimation of diameter and shortest paths (without matrix multiplication). SIAM J. Comput. 28(4), 1167\u20131181 (1999)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"9450_CR6","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1006\/jcss.1997.1388","volume":"54","author":"N Alon","year":"1997","unstructured":"Alon, N., Galil, Z., Margalit, O.: On the exponent of the all pairs shortest path problem. J. Comput. Syst. Sci. 54(2), 255\u2013262 (1997)","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"9450_CR7","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/210332.210337","volume":"42","author":"N Alon","year":"1995","unstructured":"Alon, N., Yuster, R., Zwick, U.: Color-coding. J. ACM (JACM) 42(4), 844\u2013856 (1995)","journal-title":"J. ACM (JACM)"},{"key":"9450_CR8","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Computer Aided Verification, pp. 151\u2013165. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_12"},{"key":"9450_CR9","doi-asserted-by":"crossref","unstructured":"Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: Compositionality: The Significant Difference, pp. 81\u2013102. Springer, Berlin (1998)","DOI":"10.21236\/ADA339195"},{"key":"9450_CR10","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"9450_CR11","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, pp. 193\u2013207 (1999)","DOI":"10.21236\/ADA360973"},{"issue":"6","key":"9450_CR12","doi-asserted-by":"publisher","first-page":"1395","DOI":"10.1137\/S0097539702416761","volume":"32","author":"A Bj\u00f6rklund","year":"2003","unstructured":"Bj\u00f6rklund, A., Husfeldt, T.: Finding a path of superlogarithmic length. SIAM J. Comput. 32(6), 1395\u20131402 (2003)","journal-title":"SIAM J. Comput."},{"key":"9450_CR13","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rklund, A., Husfeldt, T., Khanna, S.: Approximating longest directed paths and cycles. In: International Colloquium on Automata, Languages, and Programming, pp. 222\u2013233. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27836-8_21"},{"key":"9450_CR14","doi-asserted-by":"publisher","unstructured":"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\u2013146 (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"9450_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013164. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.27"},{"key":"9450_CR16","doi-asserted-by":"crossref","unstructured":"Case, M.L., Mony, H., Baumgartner, J., Kanzelman, R.: Enhanced verification by temporal decomposition. In: FMCAD 2009, pp. 17\u201324. Austin (2009)","DOI":"10.1109\/FMCAD.2009.5351146"},{"issue":"5","key":"9450_CR17","doi-asserted-by":"publisher","first-page":"2075","DOI":"10.1137\/08071990X","volume":"39","author":"TM Chan","year":"2010","unstructured":"Chan, T.M.: More algorithms for all-pairs shortest paths in weighted graphs. SIAM J. Comput. 39(5), 2075\u20132089 (2010)","journal-title":"SIAM J. Comput."},{"key":"9450_CR18","doi-asserted-by":"crossref","unstructured":"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\u20131052. Society for Industrial and Applied Mathematics (2014)","DOI":"10.1137\/1.9781611973402.78"},{"key":"9450_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Informatics, pp. 176\u2013194. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44577-3_12"},{"issue":"11","key":"9450_CR20","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Turing lecture: model checking-algorithmic verification and debugging. Commun. ACM 52(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"issue":"5","key":"9450_CR21","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"9450_CR22","doi-asserted-by":"crossref","unstructured":"Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively formalizing automata theory. In: Proof, Language, and Interaction, pp. 213\u2013238 (2000)","DOI":"10.7551\/mitpress\/5641.003.0014"},{"issue":"1","key":"9450_CR23","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.jctb.2004.11.005","volume":"94","author":"P Dankelmann","year":"2005","unstructured":"Dankelmann, P.: The diameter of directed graphs. J. Comb. Theory Ser. B 94(1), 183\u2013186 (2005)","journal-title":"J. Comb. Theory Ser. B"},{"issue":"4","key":"9450_CR24","doi-asserted-by":"publisher","first-page":"1355","DOI":"10.1016\/j.disc.2015.11.021","volume":"339","author":"P Dankelmann","year":"2016","unstructured":"Dankelmann, P., Dorfling, M.: Diameter and maximum degree in Eulerian digraphs. Discrete Math. 339(4), 1355\u20131361 (2016)","journal-title":"Discrete Math."},{"issue":"1","key":"9450_CR25","doi-asserted-by":"crossref","first-page":"R157","DOI":"10.37236\/429","volume":"17","author":"P Dankelmann","year":"2010","unstructured":"Dankelmann, P., Volkmann, L.: The diameter of almost Eulerian digraphs. Electron. J. Comb. 17(1), R157 (2010)","journal-title":"Electron. J. Comb."},{"key":"9450_CR26","doi-asserted-by":"crossref","unstructured":"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\u201397. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-03545-1_6"},{"issue":"1","key":"9450_CR27","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0095-8956(89)90066-X","volume":"47","author":"P Erd\u0151s","year":"1989","unstructured":"Erd\u0151s, P., Pach, J., Pollack, R., Tuza, Z.: Radius, diameter, and minimum degree. J. Comb. Theory Ser. B 47(1), 73\u201379 (1989)","journal-title":"J. Comb. Theory Ser. B"},{"key":"9450_CR28","doi-asserted-by":"crossref","unstructured":"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\u2013478. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"issue":"3\u20134","key":"9450_CR29","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"RE Fikes","year":"1971","unstructured":"Fikes, R.E., Nilsson, N.J.: Strips: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3\u20134), 189\u2013208 (1971)","journal-title":"Artif. Intell."},{"issue":"3","key":"9450_CR30","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10703-011-0115-3","volume":"39","author":"E Filiot","year":"2011","unstructured":"Filiot, E., Jin, N., Raskin, J.F.: Antichains and compositional algorithms for LTL synthesis. Formal Methods Syst. Des. 39(3), 261\u2013296 (2011)","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"9450_CR31","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1137\/0205006","volume":"5","author":"ML Fredman","year":"1976","unstructured":"Fredman, M.L.: New bounds on the complexity of the shortest path problem. SIAM J. Comput. 5(1), 83\u201389 (1976)","journal-title":"SIAM J. Comput."},{"key":"9450_CR32","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10462-007-9049-y","volume":"26","author":"M Helmert","year":"2006","unstructured":"Helmert, M.: The fast downward planning system. J. Artif. Intell. Res. 26, 191\u2013246 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"9450_CR33","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"9450_CR34","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359\u2013363 (1992)"},{"issue":"2","key":"9450_CR35","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0004-3702(94)90069-8","volume":"68","author":"CA Knoblock","year":"1994","unstructured":"Knoblock, C.A.: Automatically generating abstractions for planning. Artif. Intell. 68(2), 243\u2013302 (1994)","journal-title":"Artif. Intell."},{"issue":"6","key":"9450_CR36","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/BF01158390","volume":"41","author":"A Knyazev","year":"1987","unstructured":"Knyazev, A.: Diameters of pseudosymmetric graphs. Math. Notes 41(6), 473\u2013482 (1987)","journal-title":"Math. Notes"},{"issue":"1","key":"9450_CR37","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.entcs.2005.07.021","volume":"144","author":"D Kroening","year":"2006","unstructured":"Kroening, D.: Computing over-approximations with bounded model checking. Electron. Notes Theor. Comput. Sci. 144(1), 79\u201392 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9450_CR38","doi-asserted-by":"crossref","unstructured":"Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: Computer Aided Verification, pp. 557\u2013572. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_44"},{"key":"9450_CR39","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: VMCAI, pp. 298\u2013309 (2003)","DOI":"10.1007\/3-540-36384-X_24"},{"key":"9450_CR40","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking. In: Symbolic Model Checking, pp. 25\u201360. Springer, Berlin (1993)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"issue":"3","key":"9450_CR41","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1307\/mmj\/1028999370","volume":"12","author":"JW Moon","year":"1965","unstructured":"Moon, J.W., et al.: On the diameter of a graph. Mich. Math. J. 12(3), 349\u2013351 (1965)","journal-title":"Mich. Math. J."},{"key":"9450_CR42","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/11921240_1"},{"issue":"1","key":"9450_CR43","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/S0893-9659(04)90003-1","volume":"17","author":"PM Pardalos","year":"2004","unstructured":"Pardalos, P.M., Migdalas, A.: A note on the complexity of longest path problems related to graph coloring. Appl. Math. Lett. 17(1), 13\u201315 (2004)","journal-title":"Appl. Math. Lett."},{"key":"9450_CR44","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: A formalisation of finite automata using hereditarily finite sets. In: International Conference on Automated Deduction, pp. 231\u2013245. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21401-6_15"},{"issue":"1","key":"9450_CR45","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0890-5401(02)93175-5","volume":"178","author":"A Pnueli","year":"2002","unstructured":"Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The small model property: How small can it be? Inf. Comput. 178(1), 279\u2013293 (2002)","journal-title":"Inf. Comput."},{"key":"9450_CR46","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.artint.2012.08.001","volume":"193","author":"J Rintanen","year":"2012","unstructured":"Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45\u201386 (2012)","journal-title":"Artif. Intell."},{"key":"9450_CR47","unstructured":"Rintanen, J., Gretton, C.O.: Computing upper bounds on lengths of transition sequences. In: International Joint Conference on Artificial Intelligence (2013)"},{"key":"9450_CR48","doi-asserted-by":"crossref","unstructured":"Robinson, N., Gretton, C., Pham, D.N., Sattar, A.: SAT-based parallel planning using a split representation of actions. In: ICAPS (2009)","DOI":"10.1609\/icaps.v19i1.13368"},{"key":"9450_CR49","doi-asserted-by":"crossref","unstructured":"Roditty, L., Vassilevska\u00a0Williams, 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\u2013524. ACM (2013)","DOI":"10.1145\/2488608.2488673"},{"key":"9450_CR50","doi-asserted-by":"crossref","unstructured":"Schimpf, A., Merz, S., Smaus, J.G.: Construction of B\u00fcchi automata for LTL model checking verified in Isabelle\/HOL. In: International Conference on Theorem Proving in Higher Order Logics, pp. 424\u2013439. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03359-9_29"},{"key":"9450_CR51","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, 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\u2013125 (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"9450_CR52","doi-asserted-by":"crossref","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Theorem Proving in Higher Order Logics, LNCS, vol. 5170, pp. 28\u201332. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71067-7_6"},{"issue":"5","key":"9450_CR53","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1002\/jgt.3190160505","volume":"16","author":"J Soares","year":"1992","unstructured":"Soares, J.: Maximum diameter of regular digraphs. J. Graph Theory 16(5), 437\u2013450 (1992)","journal-title":"J. Graph Theory"},{"key":"9450_CR54","doi-asserted-by":"crossref","unstructured":"Sprenger, C.: A verified model checker for the modal $$\\mu $$ \u03bc -calculus in Coq. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 167\u2013183. Springer, Berlin (1998)","DOI":"10.1007\/BFb0054171"},{"key":"9450_CR55","unstructured":"Williams, B.C., Nayak, P.P.: A reactive planner for a model-based executive. In: International Joint Conference on Artificial Intelligence, pp. 1178\u20131185. Morgan Kaufmann Publishers, Los Altos (1997)"},{"key":"9450_CR56","doi-asserted-by":"crossref","unstructured":"Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill\u2013Nerode theorem based on regular expressions (proof pearl). In: International Conference on Interactive Theorem Proving, pp. 341\u2013356. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22863-6_25"},{"key":"9450_CR57","unstructured":"Yuster, R.: Computing the Diameter Polynomially Faster Than APSP. arXiv preprint arXiv:1011.6181 (2010)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9450-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9450-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9450-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T23:09:22Z","timestamp":1719788962000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9450-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,3]]},"references-count":57,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9450"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9450-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,2,3]]},"assertion":[{"value":"1 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 January 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 February 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}