{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:02:01Z","timestamp":1768341721888,"version":"3.49.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states; then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_8","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"161-183","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Bisimulation Learning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8180-0904","authenticated-orcid":false,"given":"Mirco","family":"Giacobbe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7406-3440","authenticated-orcid":false,"given":"Yannik","family":"Schnitzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"8_CR1","unstructured":"Abate, A., Edwards, A., Giacobbe, M.: Neural abstractions. In: NeurIPS (2022)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Stochastic omega-regular verification and control with supermartingales. In: CAV. LNCS. Springer (2024)","DOI":"10.1007\/978-3-031-65633-0_18"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Ashok, P., Jackermeier, M., Jagtap, P., Kret\u00ednsk\u00fd, J., Weininger, M., Zamani, M.: dtcontrol: decision tree learning algorithms for controller representation. In: HSCC, pp. 17:1\u201317:7. ACM (2020)","DOI":"10.1145\/3365365.3382220"},{"key":"8_CR4","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"issue":"6A","key":"8_CR5","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_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: TACAS (2). LNCS, vol. 13994, pp. 495\u2013522. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","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"},{"key":"8_CR8","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":"8_CR9","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_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0023733","volume-title":"Computer-Aided Verification","author":"A Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 197\u2013203. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023733"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-28756-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Bozga","year":"2012","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Deciding conditional termination. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 252\u2013266. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_18"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","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"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-319-89960-2_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Br\u00e1zdil","year":"2018","unstructured":"Br\u00e1zdil, T., Chatterjee, K., K\u0159et\u00ednsk\u00fd, J., Toman, V.: Strategy representation by decision trees in\u00a0reactive\u00a0synthesis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 385\u2013407. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_21"},{"key":"8_CR14","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."},{"key":"8_CR15","doi-asserted-by":"crossref","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)","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","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"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"8_CR18","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\/1190215.1190257"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 328\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_32"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"2","key":"8_CR21","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_CR22","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: ESEC\/SIGSOFT FSE, pp. 633\u2013645. ACM (2022)","DOI":"10.1145\/3554332"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-71493-4_20","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2007","unstructured":"Girard, A.: Approximately bisimilar finite abstractions of stable linear systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 231\u2013244. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71493-4_20"},{"issue":"5\u20136","key":"8_CR24","doi-asserted-by":"publisher","first-page":"568","DOI":"10.3166\/ejc.17.568-578","volume":"17","author":"A Girard","year":"2011","unstructured":"Girard, A., Pappas, G.J.: Approximate bisimulation: A bridge between computer science and control theory. Eur. J. Control. 17(5\u20136), 568\u2013578 (2011)","journal-title":"Eur. J. Control."},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"RJ Glabbeek","year":"1993","unstructured":"Glabbeek, R.J.: The linear time \u2014 Branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66\u201381. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_6"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An O(mlogn) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. 18(2), 13:1\u201313:34 (2017)","DOI":"10.1145\/3060140"},{"issue":"1\/2","key":"8_CR27","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S0019-9958(85)80014-0","volume":"66","author":"O Grumberg","year":"1985","unstructured":"Grumberg, O., Francez, N., Makowsky, J.A., de Roever, W.P.: A proof rule for fair termination of guarded commands. Inf. Control 66(1\/2), 83\u2013102 (1985)","journal-title":"Inf. Control"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Heizmann, M., et al.: Ultimate automizer and the commuhash normal form - (competition contribution). In: TACAS (2). LNCS, vol. 13994, pp. 577\u2013581. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_39","DOI":"10.1007\/978-3-031-30820-8_39"},{"issue":"1","key":"8_CR29","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_CR30","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\/982962.964021"},{"key":"8_CR31","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"},{"issue":"1","key":"8_CR32","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."},{"key":"8_CR33","unstructured":"Lamport, L.: What good is temporal logic? In: IFIP Congress, pp. 657\u2013668. North-Holland\/IFIP (1983)"},{"key":"8_CR34","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_CR35","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_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/3-540-58179-0_71","volume-title":"Computer Aided Verification","author":"I Lee","year":"1994","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"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-90636-8_7","volume-title":"Formal Aspects of Component Software","author":"J Martens","year":"2021","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"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol.\u00a092. Springer (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"8_CR39","unstructured":"Milner, R.: Communication and concurrency. PHI Series in computer science. Prentice Hall (1989)"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-61604-7_56","volume-title":"CONCUR \u201996: Concurrency Theory","author":"F Moller","year":"1996","unstructured":"Moller, F.: Infinite results. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 195\u2013216. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_56"},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","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"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Murali, V., Trivedi, A., Zamani, M.: Closure certificates. In: HSCC, pp. 10:1\u201310:11. ACM (2024)","DOI":"10.1145\/3641513.3650120"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"KS Namjoshi","year":"1997","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 284\u2013296. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0058037"},{"issue":"2","key":"8_CR44","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"RD Nicola","year":"1995","unstructured":"Nicola, R.D., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Sharma, R.: Termination proofs from tests. In: ESEC\/SIGSOFT FSE, pp. 246\u2013256. ACM (2013)","DOI":"10.1145\/2491411.2491413"},{"issue":"6","key":"8_CR46","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."},{"issue":"12","key":"8_CR47","doi-asserted-by":"publisher","first-page":"2035","DOI":"10.1016\/j.automatica.2003.07.003","volume":"39","author":"GJ Pappas","year":"2003","unstructured":"Pappas, G.J.: Bisimilar linear systems. Autom. 39(12), 2035\u20132047 (2003)","journal-title":"Autom."},{"key":"8_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). https:\/\/doi.org\/10.1007\/BFb0017309"},{"key":"8_CR49","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_CR50","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\/1168918.1168907"},{"key":"8_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-319-10936-7_19","volume-title":"Static Analysis","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 302\u2013318. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10936-7_19"},{"issue":"1\u20132","key":"8_CR52","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"MY Vardi","year":"1991","unstructured":"Vardi, M.Y.: Verification of concurrent programs: The automata-theoretic framework. Ann. Pure Appl. Log. 51(1\u20132), 79\u201398 (1991)","journal-title":"Ann. Pure Appl. Log."},{"key":"8_CR53","doi-asserted-by":"crossref","unstructured":"Walker, D.J.: Bisimulations and divergence. In: LICS, pp. 186\u2013192. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5117"},{"issue":"12","key":"8_CR54","doi-asserted-by":"publisher","first-page":"3135","DOI":"10.1109\/TAC.2014.2351652","volume":"59","author":"M Zamani","year":"2014","unstructured":"Zamani, M., Esfahani, P.M., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans. Autom. Control 59(12), 3135\u20133150 (2014)","journal-title":"IEEE Trans. Autom. Control"}],"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-65633-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:14:44Z","timestamp":1732479284000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}