{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:54:18Z","timestamp":1743087258568,"version":"3.40.3"},"publisher-location":"Cham","reference-count":98,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_13","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"272-291","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Simulation Relations and\u00a0Applications in\u00a0Formal Methods"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5953-3384","authenticated-orcid":false,"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3658-1065","authenticated-orcid":false,"given":"Christian","family":"Schilling","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5551-6547","authenticated-orcid":false,"given":"Ji\u0159\u00ed","family":"Srba","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90224-P","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Hol\u00edk, L., Kaati, L., Vojnar, T.: A uniform (bi-)simulation-based framework for reducing tree automata. Electron. Notes Theor. Comput. Sci. 251, 27\u201348 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.08.026","DOI":"10.1016\/j.entcs.2009.08.026"},{"key":"13_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems: Modelling","author":"L Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling. Cambridge University Press, Specification and Verification (2007)"},{"key":"13_CR4","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. 52, pp. 100\u2013172. Cambridge University Press (2012)","DOI":"10.1017\/CBO9780511792588.004"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid Systems. LNCS, vol. 736, pp. 209\u2013229. Springer, Cham (1992). https:\/\/doi.org\/10.1007\/3-540-57318-6_30","DOI":"10.1007\/3-540-57318-6_30"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: ICALP, LNCS, vol. 443, pp. 322\u2013335. Springer, Cham (1990). https:\/\/doi.org\/10.1007\/BFb0032042","DOI":"10.1007\/BFb0032042"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010--8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC. pp. 202\u2013211. ACM (2004). https:\/\/doi.org\/10.1145\/1007352.1007390","DOI":"10.1145\/1007352.1007390"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Andersen, J.R., et al.: CAAL: concurrency workbench, Aalborg edition. In: ICTAC. LNCS, vol. 9399, pp. 573\u2013582. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_33","DOI":"10.1007\/978-3-319-25150-9_33"},{"key":"13_CR10","first-page":"94","volume":"95","author":"A Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94\u2013129 (2008)","journal-title":"Bull. EATCS"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: Complexity of decision problems for mixed and modal specifications. In: FOSSACS. LNCS, vol. 4962, pp. 112\u2013126. Springer, Cham (2008). https:\/\/doi.org\/10.1007\/978-3-540-78499-9_9","DOI":"10.1007\/978-3-540-78499-9_9"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: EXPTIME-complete decision problems for modal and mixed specifications. ENTCS 242(1), 19\u201333 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.06.011","DOI":"10.1016\/j.entcs.2009.06.011"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems. LNCS, vol. 999, pp. 1\u201320. Springer, Cham (1994). https:\/\/doi.org\/10.1007\/3-540-60472-3_1","DOI":"10.1007\/3-540-60472-3_1"},{"key":"13_CR14","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Bauer, S.S., Juhl, L., Larsen, K.G., Srba, J., Legay, A.: A logic for accumulated-weight reasoning on multiweighted modal automata. In: TASE, pp. 77\u201384. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/TASE.2012.9","DOI":"10.1109\/TASE.2012.9"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Benes, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Srba, J.: On determinism in modal transition systems. Theor. Comput. Sci. 410(41), 4026\u20134043 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.009","DOI":"10.1016\/j.tcs.2009.06.009"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., M\u00f8ller, M.H., Srba, J.: Parametric modal transition systems. In: ATVA. LNCS, vol. 6996, pp. 275\u2013289. Springer, Cham (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_20","DOI":"10.1007\/978-3-642-24372-1_20"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Srba, J.: Checking thorough refinement on modal transition systems is EXPTIME-complete. In: ICTAC. LNCS, vol. 5684, pp. 112\u2013126. Springer, Cham (2009). https:\/\/doi.org\/10.1007\/978-3-642-03466-4_7","DOI":"10.1007\/978-3-642-03466-4_7"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Bouajjani, A., Loiseaux, C., Sifakis, J.: Property preserving simulations. In: CAV. LNCS, vol. 663, pp. 260\u2013273. Springer, Cham (1992). https:\/\/doi.org\/10.1007\/3-540-56496-9_21","DOI":"10.1007\/3-540-56496-9_21"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Bloom, B., Paige, R.: Transformational design and implementation of a new efficient solution to the ready simulation problem. Sci. Comput. Program. 24(3), 189\u2013220 (1995). https:\/\/doi.org\/10.1016\/0167-6423(95)00003-B","DOI":"10.1016\/0167-6423(95)00003-B"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Fernandez, J., 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","DOI":"10.1007\/BFb0023733"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.): Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS \u201995, Aarhus, Denmark, 19\u201320 May 1995, Proceedings, LNCS, vol. 1019. Springer, Cham (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0","DOI":"10.1007\/3-540-60630-0"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: TACAS. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Handbook of Process Algebra, pp. 545\u2013623. North-Holland\/Elsevier (2001). https:\/\/doi.org\/10.1016\/b978-044482830-9\/50027-8","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Bustan, D., Grumberg, O.: Simulation based minimization. In: CADE. LNCS, vol. 1831, pp. 255\u2013270. Springer, Cham (2000). https:\/\/doi.org\/10.1007\/10721959_20","DOI":"10.1007\/10721959_20"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Calzolai, F., Nicola, R.D., Loreti, M., Tiezzi, F.: TAPAs: a tool for the analysis of process algebras. Trans. Petri Nets Other Model. Concurr. 1, 54\u201370 (2008). https:\/\/doi.org\/10.1007\/978-3-540-89287-8_4","DOI":"10.1007\/978-3-540-89287-8_4"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR. LNCS, vol. 3653, pp. 66\u201380. Springer, Cham (2005). https:\/\/doi.org\/10.1007\/11539452_9","DOI":"10.1007\/11539452_9"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Cerans, K.: Decidability of bisimulation equivalences for parallel timer processes. In: CAV. LNCS, vol. 663, pp. 302\u2013315. Springer, Cham (1992). https:\/\/doi.org\/10.1007\/3-540-56496-9_24","DOI":"10.1007\/3-540-56496-9_24"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification - theory and tools. In: CAV. LNCS, vol. 697, pp. 253\u2013267. Springer, Cham (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_21","DOI":"10.1007\/3-540-56922-7_21"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994). https:\/\/doi.org\/10.1145\/186025.186051","DOI":"10.1145\/186025.186051"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench. In: Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 24\u201337. Springer, Cham (1989). https:\/\/doi.org\/10.1007\/3-540-52148-8_3","DOI":"10.1007\/3-540-52148-8_3"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36\u201372 (1993). https:\/\/doi.org\/10.1145\/151646.151648","DOI":"10.1145\/151646.151648"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: CAV. LNCS, vol. 1102, pp. 394\u2013397. Springer, Cham (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_87","DOI":"10.1007\/3-540-61474-5_87"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Clemente, L.: B\u00fcchi automata can have smaller quotients. In: ICALP. LNCS, vol. 6756, pp. 258\u2013270. Springer, Cham (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_20","DOI":"10.1007\/978-3-642-22012-8_20"},{"key":"13_CR35","unstructured":"Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Log. Methods Comput. Sci. 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:12)2019"},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253\u2013291 (1997). https:\/\/doi.org\/10.1145\/244795.244800","DOI":"10.1145\/244795.244800"},{"key":"13_CR37","doi-asserted-by":"crossref","unstructured":"Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Handbook of Model Checking, pp. 385\u2013419. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_13","DOI":"10.1007\/978-3-319-10575-8_13"},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: ECDAR: an environment for compositional design and analysis of real time systems. In: ATVA. LNCS, vol. 6252, pp. 365\u2013370. Springer, Cham (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_29","DOI":"10.1007\/978-3-642-15643-4_29"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: CAV. LNCS, vol. 575, pp. 255\u2013265. Springer, Cham (1991). https:\/\/doi.org\/10.1007\/3-540-55179-4_25","DOI":"10.1007\/3-540-55179-4_25"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"Enevoldsen, S., Larsen, K.G., Mariegaard, A., Srba, J.: Dependency graphs with applications to verification. Int. J. Softw. Tools Technol. Transf. 22(5), 635\u2013654 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00578-9","DOI":"10.1007\/s10009-020-00578-9"},{"key":"13_CR41","doi-asserted-by":"crossref","unstructured":"Etessami, K.: A hierarchy of polynomial-time computable simulations for automata. In: CONCUR. LNCS, vol. 2421, pp. 131\u2013144. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/3-540-45694-5_10","DOI":"10.1007\/3-540-45694-5_10"},{"key":"13_CR42","doi-asserted-by":"crossref","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: CONCUR. LNCS, vol. 1877, pp. 153\u2013167. Springer, Cham (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_13","DOI":"10.1007\/3-540-44618-4_13"},{"key":"13_CR43","doi-asserted-by":"crossref","unstructured":"Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SIAM J. Comput. 34(5), 1159\u20131175 (2005). https:\/\/doi.org\/10.1137\/S0097539703420675","DOI":"10.1137\/S0097539703420675"},{"key":"13_CR44","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89\u2013107 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0244-z","DOI":"10.1007\/s10009-012-0244-z"},{"key":"13_CR45","unstructured":"Gauwin, O., Muscholl, A., Raskin, M.: Minimization of visibly pushdown automata is NP-complete. Log. Methods Comput. Sci. 16(1) (2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:14)2020"},{"key":"13_CR46","doi-asserted-by":"crossref","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: Coarsest partition problems. J. Autom. Reason. 31(1), 73\u2013103 (2003). https:\/\/doi.org\/10.1023\/A:1027328830731","DOI":"10.1023\/A:1027328830731"},{"key":"13_CR47","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3 - A modern refinement checker for CSP. In: TACAS. LNCS, vol. 8413, pp. 187\u2013201. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"13_CR48","doi-asserted-by":"crossref","unstructured":"Girard, A., Julius, A.A., Pappas, G.J.: Approximate simulation relations for hybrid systems. Discret. Event Dyn. Syst. 18(2), 163\u2013179 (2008). https:\/\/doi.org\/10.1007\/s10626-007-0029-9","DOI":"10.1007\/s10626-007-0029-9"},{"key":"13_CR49","doi-asserted-by":"crossref","unstructured":"Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control. 52(5), 782\u2013798 (2007). https:\/\/doi.org\/10.1109\/TAC.2007.895849","DOI":"10.1109\/TAC.2007.895849"},{"key":"13_CR50","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843\u2013871 (1994). https:\/\/doi.org\/10.1145\/177492.177725","DOI":"10.1145\/177492.177725"},{"key":"13_CR51","doi-asserted-by":"crossref","unstructured":"Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: CAV. LNCS, vol. 2404, pp. 610\u2013624. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_51","DOI":"10.1007\/3-540-45657-0_51"},{"key":"13_CR52","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Schilling, C., Tischner, D.: Minimization of visibly pushdown automata using partial Max-SAT. In: TACAS. LNCS, vol. 10205, pp. 461\u2013478 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_27","DOI":"10.1007\/978-3-662-54577-5_27"},{"key":"13_CR53","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: Hybrid automata with finite bisimulations. In: ICALP. LNCS, vol. 944, pp. 324\u2013335. Springer, Cham (1995). https:\/\/doi.org\/10.1007\/3-540-60084-1_85","DOI":"10.1007\/3-540-60084-1_85"},{"key":"13_CR54","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS. pp. 278\u2013292. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561342","DOI":"10.1109\/LICS.1996.561342"},{"key":"13_CR55","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.: HYTECH: the Cornell HYbrid TECHnology tool. In: Hybrid Systems. LNCS, vol. 999, pp. 265\u2013293. Springer, Cham (1994). https:\/\/doi.org\/10.1007\/3-540-60472-3_14","DOI":"10.1007\/3-540-60472-3_14"},{"key":"13_CR56","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control. 43(4), 540\u2013554 (1998). https:\/\/doi.org\/10.1109\/9.664156","DOI":"10.1109\/9.664156"},{"key":"13_CR57","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W.: State equivalences for rectangular hybrid automata. In: CONCUR. LNCS, vol. 1119, pp. 530\u2013545. Springer, Cham (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_74","DOI":"10.1007\/3-540-61604-7_74"},{"key":"13_CR58","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998). https:\/\/doi.org\/10.1006\/jcss.1998.1581","DOI":"10.1006\/jcss.1998.1581"},{"key":"13_CR59","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.K.: Fair simulation. Inf. Comput. 173(1), 64\u201381 (2002). https:\/\/doi.org\/10.1006\/inco.2001.3085","DOI":"10.1006\/inco.2001.3085"},{"key":"13_CR60","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K., Tasiran, S.: An assume-guarantee rule for checking simulation. ACM Trans. Program. Lang. Syst. 24(1), 51\u201364 (2002). https:\/\/doi.org\/10.1145\/509705.509707","DOI":"10.1145\/509705.509707"},{"key":"13_CR61","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Rajamani, S.K.: Fair bisimulation. In: TACAS. LNCS, vol. 1785, pp. 299\u2013314. Springer, Cham (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_21","DOI":"10.1007\/3-540-46419-0_21"},{"key":"13_CR62","unstructured":"Hojati, R.: A BDD-Based Environment for Formal Verification of Hardware Systems. Ph.D. thesis, EECS Department, University of California, Berkeley (1996). https:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/1996\/3052.html"},{"key":"13_CR63","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations, pp. 189\u2013196. Academic Press (1971). https:\/\/doi.org\/10.1016\/B978-0-12-417750-5.50022-1","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"13_CR64","doi-asserted-by":"crossref","unstructured":"Jan\u010dar, P., Srba, J.: Undecidability of bisimilarity by defender\u2019s forcing. J. ACM 55(1), 1\u201326 (2008). https:\/\/doi.org\/10.1145\/1326554.1326559","DOI":"10.1145\/1326554.1326559"},{"key":"13_CR65","doi-asserted-by":"crossref","unstructured":"Jiang, T., Ravikumar, B.: Minimal NFA problems are hard. SIAM J. Comput. 22(6), 1117\u20131141 (1993). https:\/\/doi.org\/10.1137\/0222067","DOI":"10.1137\/0222067"},{"key":"13_CR66","doi-asserted-by":"crossref","unstructured":"Julius, A.A., D\u2019Innocenzo, A., Benedetto, M.D.D., Pappas, G.J.: Approximate equivalence and synchronization of metric transition systems. Syst. Control. Lett. 58(2), 94\u2013101 (2009). https:\/\/doi.org\/10.1016\/j.sysconle.2008.09.001","DOI":"10.1016\/j.sysconle.2008.09.001"},{"key":"13_CR67","doi-asserted-by":"crossref","unstructured":"Juvekar, S., Piterman, N.: Minimizing generalized B\u00fcchi automata. In: CAV. LNCS, vol. 4144, pp. 45\u201358. Springer, Cham (2006). https:\/\/doi.org\/10.1007\/11817963_7","DOI":"10.1007\/11817963_7"},{"key":"13_CR68","doi-asserted-by":"crossref","unstructured":"Kucera, A., Mayr, R.: Why is simulation harder than bisimulation? In: CONCUR. LNCS, vol. 2421, pp. 594\u2013610. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/3-540-45694-5_39","DOI":"10.1007\/3-540-45694-5_39"},{"key":"13_CR69","unstructured":"Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. Chic. J. Theor. Comput. Sci. 1998 (1998). https:\/\/cjtcs.cs.uchicago.edu\/articles\/1998\/2\/contents.html"},{"key":"13_CR70","doi-asserted-by":"crossref","unstructured":"Ku\u010dera, A., Jan\u010dar, P.: Equivalence-checking with infinite-state systems: Techniques and results. In: SOFSEM. LNCS, vol. 2540, pp. 41\u201373. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/3-540-36137-5_3","DOI":"10.1007\/3-540-36137-5_3"},{"key":"13_CR71","doi-asserted-by":"crossref","unstructured":"Lanotte, R., Tini, S.: Taylor approximation for hybrid systems. Inf. Comput. 205(11), 1575\u20131607 (2007), https:\/\/doi.org\/10.1016\/j.ic.2007.05.004","DOI":"10.1016\/j.ic.2007.05.004"},{"key":"13_CR72","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic - and back. In: MFCS. LNCS, vol. 969, pp. 529\u2013539. Springer, Cham (1995). https:\/\/doi.org\/10.1007\/3-540-60246-1_158","DOI":"10.1007\/3-540-60246-1_158"},{"key":"13_CR73","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: On modal refinement and consistency. In: CONCUR. LNCS, vol. 4703, pp. 105\u2013119. Springer, Cham (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_8","DOI":"10.1007\/978-3-540-74407-8_8"},{"key":"13_CR74","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"13_CR75","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/LICS.1988.5119","DOI":"10.1109\/LICS.1988.5119"},{"key":"13_CR76","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Yi, W.: Time abstracted bisimulation: Implicit specifications and decidability. In: MFPS. LNCS, vol. 802, pp. 160\u2013176. Springer, Cham (1993). https:\/\/doi.org\/10.1007\/3-540-58027-1_8","DOI":"10.1007\/3-540-58027-1_8"},{"key":"13_CR77","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: STOC, pp. 264\u2013274. ACM (1992). https:\/\/doi.org\/10.1145\/129712.129738","DOI":"10.1145\/129712.129738"},{"key":"13_CR78","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137\u2013151. ACM (1987). https:\/\/doi.org\/10.1145\/41840.41852","DOI":"10.1145\/41840.41852"},{"key":"13_CR79","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Zamani, M.: Approximately bisimilar symbolic models for digital control systems. In: CAV. LNCS, vol. 7358, pp. 362\u2013377. Springer, Cham (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_28","DOI":"10.1007\/978-3-642-31424-7_28"},{"key":"13_CR80","doi-asserted-by":"crossref","unstructured":"Mayr, R.: Process rewrite systems. Inf. Comput. 156(1\u20132), 264\u2013286 (2000). https:\/\/doi.org\/10.1006\/inco.1999.2826","DOI":"10.1006\/inco.1999.2826"},{"key":"13_CR81","doi-asserted-by":"crossref","unstructured":"Mayr, R., Clemente, L.: Advanced automata minimization. In: POPL, pp. 63\u201374. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429079","DOI":"10.1145\/2480359.2429079"},{"key":"13_CR82","doi-asserted-by":"crossref","unstructured":"Mazala, R.: Infinite games. In: Automata, Logics, and Infinite Games: a Guide to Current Research. LNCS, vol. 2500, pp. 23\u201342. Springer, Cham (2001). https:\/\/doi.org\/10.1007\/3-540-36387-4_2","DOI":"10.1007\/3-540-36387-4_2"},{"key":"13_CR83","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: IJCAI, pp. 481\u2013489 (1971). https:\/\/ijcai.org\/Proceedings\/71\/Papers\/044.pdf"},{"key":"13_CR84","doi-asserted-by":"crossref","unstructured":"Moller, F.: Infinite results. In: CONCUR. LNCS, vol. 1119, pp. 195\u2013216. Springer, Cham (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_56","DOI":"10.1007\/3-540-61604-7_56"},{"key":"13_CR85","doi-asserted-by":"crossref","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987). https:\/\/doi.org\/10.1137\/0216062","DOI":"10.1137\/0216062"},{"key":"13_CR86","doi-asserted-by":"crossref","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Theoretical Computer Science. LNCS, vol. 104, pp. 167\u2013183. Springer, Cham (1981). https:\/\/doi.org\/10.1007\/BFb0017309","DOI":"10.1007\/BFb0017309"},{"key":"13_CR87","doi-asserted-by":"crossref","unstructured":"Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Autom. 44(10), 2508\u20132516 (2008). https:\/\/doi.org\/10.1016\/j.automatica.2008.02.021","DOI":"10.1016\/j.automatica.2008.02.021"},{"key":"13_CR88","doi-asserted-by":"crossref","unstructured":"Rauch Henzinger, M., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: FOCS, pp. 453\u2013462. IEEE Computer Society (1995). https:\/\/doi.org\/10.1109\/SFCS.1995.492576","DOI":"10.1109\/SFCS.1995.492576"},{"key":"13_CR89","unstructured":"Schewe, S.: Beyond hyper-minimisation\u2013minimising DBAs and DPAs is NP-complete. In: FSTTCS. LIPIcs, vol. 8, pp. 400\u2013411. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2010). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2010.400"},{"key":"13_CR90","doi-asserted-by":"crossref","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: CAV. LNCS, vol. 1855, pp. 248\u2013263. Springer, Cham (2000). https:\/\/doi.org\/10.1007\/10722167_21","DOI":"10.1007\/10722167_21"},{"key":"13_CR91","doi-asserted-by":"crossref","unstructured":"Srba, J.: Roadmap of infinite results. In: Current Trends in Theoretical Computer Science: The Challenge of the New Century, vol. 2, pp. 337\u2013350. World Scientific (2004)","DOI":"10.1142\/9789812562494_0054"},{"key":"13_CR92","doi-asserted-by":"crossref","unstructured":"Srba, J.: Beyond language equivalence on visibly pushdown automata. Log. Methods Comput. Sci. 5(1) (2009). https:\/\/arxiv.org\/abs\/0901.2068","DOI":"10.2168\/LMCS-5(1:2)2009"},{"key":"13_CR93","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Local model checking games. In: CONCUR. LNCS, vol. 962, pp. 1\u201311. Springer, Cham (1995). https:\/\/doi.org\/10.1007\/3-540-60218-6_1","DOI":"10.1007\/3-540-60218-6_1"},{"key":"13_CR94","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: STOC, pp. 1\u20139. ACM (1973). https:\/\/doi.org\/10.1145\/800125.804029","DOI":"10.1145\/800125.804029"},{"key":"13_CR95","doi-asserted-by":"crossref","unstructured":"Thomas, W.: On the Ehrenfeucht-Fra\u00efss\u00e9 game in theoretical computer science. In: TAPSOFT. LNCS, vol. 668, pp. 559\u2013568. Springer, Cham (1993). https:\/\/doi.org\/10.1007\/3-540-56610-4_89","DOI":"10.1007\/3-540-56610-4_89"},{"key":"13_CR96","doi-asserted-by":"crossref","unstructured":"Tiwari, A.: Abstractions for hybrid systems. Formal Methods Syst. Des. 32(1), 57\u201383 (2008). https:\/\/doi.org\/10.1007\/s10703-007-0044-3","DOI":"10.1007\/s10703-007-0044-3"},{"key":"13_CR97","unstructured":"Urabe, N., Hasuo, I.: Fair simulation for nondeterministic and probabilistic B\u00fcchi automata: a coalgebraic perspective. Log. Methods Comput. Sci. 13(3) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(3:20)2017"},{"key":"13_CR98","doi-asserted-by":"crossref","unstructured":"Yi, W.: CCS + time = an interleaving model for real time systems. In: ICALP. LNCS, vol. 510, pp. 217\u2013228. Springer, Cham (1991). https:\/\/doi.org\/10.1007\/3-540-54233-7_136","DOI":"10.1007\/3-540-54233-7_136"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:07:51Z","timestamp":1672358871000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":98,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}