{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:24:12Z","timestamp":1760142252205,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":72,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986840"},{"type":"electronic","value":"9783031986857"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We introduce a bisimulation learning algorithm for non-deterministic transition systems. We generalise bisimulation learning to systems with bounded branching and extend its applicability to model checking branching-time temporal logic, while previously it was limited to deterministic systems and model checking linear-time properties. Our method computes a finite stutter-insensitive bisimulation quotient of the system under analysis, represented as a decision tree. We adapt the proof rule for well-founded bisimulations to an iterative procedure that trains candidate decision trees from sample transitions of the system, and checks their validity over the entire transition relation using SMT solving. This results in a new technology for model checking CTL* without the next-time operator. Our technique is sound, entirely automated, and yields abstractions that are succinct and effective for formal verification and system diagnostics. We demonstrate the efficacy of our method on diverse benchmarks comprising concurrent software, communication protocols and robotic scenarios. Our method performs comparably to mature tools in the special case of LTL model checking, and outperforms the state of the art in CTL and CTL* model checking for systems with very large and countably infinite state space.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_8","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:31:35Z","timestamp":1753155095000},"page":"161-184","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Branching Bisimulation Learning"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"given":"Mirco","family":"Giacobbe","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Micheletti","sequence":"additional","affiliation":[]},{"given":"Yannik","family":"Schnitzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 270\u2013288. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A., Giacobbe, M., Micheletti, C., Schnitzer, Y.: Branching bisimulation learning (technical report). CoRR abs\/2504.12246 (2025)","DOI":"10.1007\/978-3-031-98685-7_8"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Abate, A., Giacobbe, M., Roy, D., Schnitzer, Y.: Model checking and strategy synthesis with abstractions and certificates. In: Principles of Verification (2). Lecture Notes in Computer Science, vol. 15261, pp. 360\u2013391. Springer (2024)","DOI":"10.1007\/978-3-031-75775-4_16"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Abate, A., Giacobbe, M., Schnitzer, Y.: Bisimulation learning. In: CAV (3). Lecture Notes in Computer Science, vol. 14683, pp. 161\u2013183. Springer (2024)","DOI":"10.1007\/978-3-031-65633-0_8"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Srba, J.: The algorithmics of bisimilarity. In: Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science, vol.\u00a052, pp. 100\u2013172. Cambridge University Press (2012)","DOI":"10.1017\/CBO9780511792588.004"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 536\u2013550. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44685-0_36","DOI":"10.1007\/3-540-44685-0_36"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp.\u00a01\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"8_CR8","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"issue":"6A","key":"8_CR9","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1007\/BF03180566","volume":"4","author":"JL Balc\u00e1zar","year":"1992","unstructured":"Balc\u00e1zar, J.L., Gabarr\u00f3, J., Santha, M.: Deciding bisimilarity is P-complete. Formal Aspects Comput. 4(6A), 638\u2013648 (1992)","journal-title":"Formal Aspects Comput."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1267\u20131329. IOS Press (2021)","DOI":"10.3233\/FAIA201017"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869\u2013882. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_61","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Efficient CTL verification via horn constraints solving. In: HCVS@ETAPS. EPTCS, vol.\u00a0219, pp. 1\u201314 (2016)","DOI":"10.4204\/EPTCS.219.1"},{"issue":"5\u20136","key":"8_CR13","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.S., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT@IJCAR. EPiC Series in Computing, vol.\u00a020, pp. 3\u201311. EasyChair (2012)","DOI":"10.29007\/1l7f"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105\u2013125. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_8","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 589\u2013606. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_34","DOI":"10.1007\/978-3-662-54577-5_34"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Herrera, C., Steiner, W.: Verification of fault-tolerant clock synchronization algorithms. In: ARCH@CPSWeek. EPiC Series in Computing, vol.\u00a043, pp. 36\u201341. EasyChair (2016)","DOI":"10.29007\/hq8s"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Fernandez, J., Halbwachs, N.: Minimal model generation. In: CAV. Lecture Notes in Computer Science, vol.\u00a0531, pp. 197\u2013203. Springer (1990)","DOI":"10.1007\/BFb0023733"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_22","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115\u2013131 (1988)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$\\hat{2}$$0 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Carelli, M., Grumberg, O.: CTL* verification and synthesis using existential horn clauses. In: ATVA (2). Lecture Notes in Computer Science, vol. 15055, pp. 177\u2013197. Springer (2024)","DOI":"10.1007\/978-3-031-78750-8_9"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuXmv Symbolic Model Checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs. Lecture Notes in Computer Science, vol.\u00a0131, pp. 52\u201371. Springer (1981)","DOI":"10.1007\/BFb0025774"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV. Lecture Notes in Computer Science, vol.\u00a01855, pp. 154\u2013169. Springer (2000)","DOI":"10.1007\/10722167_15"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: POPL, pp. 265\u2013276. ACM (2007)","DOI":"10.1145\/1190216.1190257"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: On Automation of CTL* verification for infinite-state systems. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 13\u201329. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_2","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 87\u2013101. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_8","DOI":"10.1007\/11547662_8"},{"issue":"1","key":"8_CR32","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M Dam","year":"1994","unstructured":"Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theor. Comput. Sci. 126(1), 77\u201396 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"8_CR33","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R De Nicola","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"issue":"2","key":"8_CR34","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10009-017-0468-z","volume":"20","author":"T van Dijk","year":"2018","unstructured":"van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. Int. J. Softw. Tools Technol. Transf. 20(2), 157\u2013177 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cNot Never\u201d revisited: on branching versus linear time. In: POPL, pp. 127\u2013140. ACM Press (1983)","DOI":"10.1145\/567067.567081"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Ermis, E., Nutz, A., Dietsch, D., Hoenicke, J., Podelski, A.: Ultimate Kojak. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 421\u2013423. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_36","DOI":"10.1007\/978-3-642-54862-8_36"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Fernandez, J.-C., Mounier, L.: A tool set for deciding behavioral equivalences. In: Baeten, J., Groote, J.F. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 23\u201342. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54430-5_78","DOI":"10.1007\/3-540-54430-5_78"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Garcia-Contreras, I., K., H.G.V., Shoham, S., Gurfinkel, A.: Fast approximations of quantifier elimination. In: CAV (2). Lecture Notes in Computer Science, vol. 13965, pp. 64\u201386. Springer (2023)","DOI":"10.1007\/978-3-031-37703-7_4"},{"issue":"3","key":"8_CR39","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ van Glabbeek","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996)","journal-title":"J. ACM"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV. Lecture Notes in Computer Science, vol.\u00a01254, pp. 72\u201383. Springer (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An $$O(m\\log n)$$ algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. 18(2), 13:1\u201313:34 (2017)","DOI":"10.1145\/3060140"},{"key":"8_CR42","doi-asserted-by":"publisher","unstructured":"Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626\u2013638. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032063","DOI":"10.1007\/BFb0032063"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A.: Program verification with constrained horn clauses (invited paper). In: CAV (1). Lecture Notes in Computer Science, vol. 13371, pp. 19\u201329. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Heizmann, M., et al.: Ultimate automizer and the commuhash normal form - (competition contribution). In: TACAS (2). Lecture Notes in Computer Science, vol. 13994, pp. 577\u2013581. Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_39"},{"issue":"1","key":"8_CR45","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/964001.964021"},{"key":"8_CR47","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/503272.503279"},{"key":"8_CR48","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An $${n \\log n}$$ algorithm for minimizing states in a finite automaton. In: Kohavi, Z., Paz, A. (eds.) Theory of Machines and Computations, pp. 189\u2013196. Academic Press (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"8_CR49","unstructured":"Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.: A simpler $$O(m \\log n)$$ algorithm for branching bisimilarity on labelled transition systems. CoRR abs\/1909.10824 (2019)"},{"key":"8_CR50","doi-asserted-by":"publisher","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"issue":"1","key":"8_CR51","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"issue":"2\u20133","key":"8_CR52","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.tcs.2004.09.023","volume":"331","author":"Y Kesten","year":"2005","unstructured":"Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theor. Comput. Sci. 331(2\u20133), 397\u2013428 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR53","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. In: ICALP. Lecture Notes in Computer Science, vol.\u00a0140, pp. 348\u2013359. Springer (1982)","DOI":"10.1007\/BFb0012782"},{"key":"8_CR54","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series, Springer (2016)","DOI":"10.1007\/978-3-662-50497-0"},{"key":"8_CR55","unstructured":"Lamport, L.: What good is temporal logic? In: IFIP Congress. pp. 657\u2013668. North-Holland\/IFIP (1983)"},{"key":"8_CR56","doi-asserted-by":"crossref","unstructured":"Lamport, L., Melliar-Smith, P.M.: Byzantine clock synchronization. In: PODC, pp. 68\u201374. ACM (1984)","DOI":"10.1145\/800222.806737"},{"key":"8_CR57","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: STOC, pp. 264\u2013274. ACM (1992)","DOI":"10.1145\/129712.129738"},{"key":"8_CR58","doi-asserted-by":"publisher","unstructured":"Lee, I., Rajasekaran, S.: A parallel algorithm for relational coarsest partition problems and its implementation. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 404\u2013414. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_71","DOI":"10.1007\/3-540-58179-0_71"},{"key":"8_CR59","doi-asserted-by":"crossref","unstructured":"Manolios, P., Namjoshi, K.S., Summers, R.: Linking theorem proving and model-checking with well-founded bisimulation. In: CAV. Lecture Notes in Computer Science, vol.\u00a01633, pp. 369\u2013379. Springer (1999)","DOI":"10.1007\/3-540-48683-6_32"},{"key":"8_CR60","doi-asserted-by":"publisher","unstructured":"Martens, J., Groote, J.F., van den Haak, L., Hijma, P., Wijs, A.: A linear parallel algorithm to compute bisimulation and relational coarsest partitions. In: Sala\u00fcn, G., Wijs, A. (eds.) FACS 2021. LNCS, vol. 13077, pp. 115\u2013133. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90636-8_7","DOI":"10.1007\/978-3-030-90636-8_7"},{"key":"8_CR61","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"8_CR62","doi-asserted-by":"publisher","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"8_CR63","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"8_CR64","doi-asserted-by":"publisher","unstructured":"Mumme, M., Ciardo, G.: A fully symbolic bisimulation algorithm. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 218\u2013230. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24288-5_19","DOI":"10.1007\/978-3-642-24288-5_19"},{"key":"8_CR65","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: FSTTCS. Lecture Notes in Computer Science, vol.\u00a01346, pp. 284\u2013296. Springer (1997)","DOI":"10.1007\/BFb0058037"},{"issue":"1 &2","key":"8_CR66","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(95)00136-0","volume":"163","author":"D Niwinski","year":"1996","unstructured":"Niwinski, D., Walukiewicz, I.: Games for the mu-calculus. Theor. Comput. Sci. 163(1 &2), 99\u2013116 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"8_CR67","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"key":"8_CR68","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS. pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR69","doi-asserted-by":"publisher","unstructured":"Prabhakar, P., Soto, M.G.: Counterexample guided abstraction refinement for stability analysis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 495\u2013512. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_27","DOI":"10.1007\/978-3-319-41528-4_27"},{"key":"8_CR70","doi-asserted-by":"crossref","unstructured":"S, S.P., Fedyukovich, G., Madhukar, K., D\u2019Souza, D.: Specification synthesis with constrained horn clauses. In: PLDI. pp. 1203\u20131217. ACM (2021)","DOI":"10.1145\/3453483.3454104"},{"key":"8_CR71","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"8_CR72","doi-asserted-by":"crossref","unstructured":"T\u00f3th, T., Hajdu, A., V\u00f6r\u00f6s, A., Micskei, Z., Majzik, I.: Theta: a framework for abstraction refinement-based model checking. In: FMCAD, pp. 176\u2013179 (2017)","DOI":"10.23919\/FMCAD.2017.8102257"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:55:09Z","timestamp":1760086509000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}