{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:24:26Z","timestamp":1742912666486,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377051"},{"type":"electronic","value":"9783031377068"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We characterize all common notions of behavioral equivalence by <jats:italic>one<\/jats:italic> 6-dimensional energy game, where energies bound capabilities of an attacker trying to tell processes apart. The defender-winning initial credits exhaustively determine which preorders and equivalences from the (strong) linear-time\u2013branching-time spectrum relate processes.<\/jats:p><jats:p>The time complexity is exponential, which is optimal due to trace equivalence being covered. This complexity improves drastically on our previous approach for deciding groups of equivalences where exponential sets of distinguishing HML formulas are constructed on top of a super-exponential reachability game. In experiments using the VLTS benchmarks, the algorithm performs on par with the best similarity algorithm.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_5","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"85-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Process Equivalence Problems as\u00a0Energy Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0637-0171","authenticated-orcid":false,"given":"Benjamin","family":"Bisping","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1093\/logcom\/exm062","volume":"18","author":"PA Abdulla","year":"2008","unstructured":"Abdulla, P.A., Bouajjani, A., D\u2019orso, J.: Monotonic and downward closed games. J. Log. Comput. 18(1), 153\u2013169 (2008). https:\/\/doi.org\/10.1093\/logcom\/exm062","journal-title":"J. Log. Comput."},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-642-40184-8_9","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 106\u2013120. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_9"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification, chap. Modelling mutual exclusion algorithms, pp. 142\u2013158. Cambridge University Press (2007). https:\/\/doi.org\/10.1017\/CBO9780511814105.008","DOI":"10.1017\/CBO9780511814105.008"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Bisping, B.: Linear-time-branching-time spectroscope v0.3.0 (2023). https:\/\/doi.org\/10.5281\/zenodo.7870252, archived on Zenodo","DOI":"10.5281\/zenodo.7870252"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Bisping, B.: Process equivalence problems as energy games. Tech. rep., Technische Universit\u00e4t Berlin (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.08904","DOI":"10.48550\/arXiv.2303.08904"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Bisping, B., Jansen, D.N.: Linear-time\u2013branching-time spectroscopy accounting for silent steps (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.17671","DOI":"10.48550\/arXiv.2305.17671"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Bisping, B., Jansen, D.N., Nestmann, U.: Deciding all behavioral equivalences at once: a game for linear-time-branching-time spectroscopy. Logical Methods Comput. Sci. 18(3) (2022). https:\/\/doi.org\/10.46298\/lmcs-18(3:19)2022","DOI":"10.46298\/lmcs-18(3:19)2022"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-030-17462-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Bisping","year":"2019","unstructured":"Bisping, B., Nestmann, U.: Computing coupled similarity. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 244\u2013261. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_14"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-72016-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Bisping","year":"2021","unstructured":"Bisping, B., Nestmann, U.: A game for linear-time\u2013branching-time spectroscopy. In: TACAS 2021. LNCS, vol. 12651, pp. 3\u201319. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_1"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14162-1_40","volume-title":"Automata, Languages and Programming","author":"T Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil, T., Jan\u010dar, P., Ku\u010dera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478\u2013489. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_40"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-15349-5_7","volume-title":"Reachability Problems","author":"J Chaloupka","year":"2010","unstructured":"Chaloupka, J.: Z-reachability problem for games on 2-dimensional vector addition systems with states is in P. In: Ku\u010dera, A., Potapov, I. (eds.) RP 2010. LNCS, vol. 6227, pp. 104\u2013119. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15349-5_7"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-89330-1_8","volume-title":"Programming Languages and Systems","author":"X Chen","year":"2008","unstructured":"Chen, X., Deng, Y.: Game characterizations of process equivalences. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 107\u2013121. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89330-1_8"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Logical Methods Comput. Sci. 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:12)2019","DOI":"10.23638\/LMCS-15(1:12)2019"},{"issue":"2","key":"5_CR14","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BF01768705","volume":"8","author":"A Ehrenfeucht","year":"1979","unstructured":"Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. J. Game Theory 8(2), 109\u2013113 (1979). https:\/\/doi.org\/10.1007\/BF01768705","journal-title":"Int. J. Game Theory"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-23283-1_9","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2011","author":"U Fahrenberg","year":"2011","unstructured":"Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy games in multiweighted automata. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 95\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23283-1_9"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Filiot, E., Hamel-de le Court, E.: Two-player boundedness counter games. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 243, pp. 21:1\u201321:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.21","DOI":"10.4230\/LIPIcs.CONCUR.2022.21"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-540-27813-9_19","volume-title":"Computer Aided Verification","author":"C Fournet","year":"2004","unstructured":"Fournet, C., Hoare, T., Rajamani, S.K., Rehof, J.: Stuck-free conformance. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 242\u2013254. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_19"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Garavel, H.: The VLTS benchmark suite (2017). https:\/\/doi.org\/10.18709\/perscido.2017.11.ds100, jointly created by CWI\/SEN2 and INRIA\/VASY as a CADP resource","DOI":"10.18709\/perscido.2017.11.ds100"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Garavel, H., Lang, F.: Equivalence checking 40 years after: A review of bisimulation tools. In: Jansen, N., Stoelinga, M., van den Bos, P. (eds.) A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, pp. 213\u2013265. Springer Nature Switzerland, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15629-8_13","DOI":"10.1007\/978-3-031-15629-8_13"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Geuvers, H., Jacobs, B.: Relating apartness and bisimulation. Logical Methods Comput. Sci. 17(3) (2021). https:\/\/doi.org\/10.46298\/LMCS-17(3:15)2021","DOI":"10.46298\/LMCS-17(3:15)2021"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0039066","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"RJ Glabbeek","year":"1990","unstructured":"Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278\u2013297. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039066"},{"key":"5_CR22","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":"5_CR23","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: The linear time-branching time spectrum I: The semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, chap. 1, pp. 3\u201399. Elsevier, Amsterdam (2001). https:\/\/doi.org\/10.1016\/B978-044482830-9\/50019-9","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-10003-2_79","volume-title":"Automata, Languages and Programming","author":"M Hennessy","year":"1980","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299\u2013309. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10003-2_79"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Horne, R., Mauw, S.: Discovering ePassport Vulnerabilities using Bisimilarity. Logical Methods Comput. Sci. 17(2) (2021). https:\/\/doi.org\/10.23638\/LMCS-17(2:24)2021","DOI":"10.23638\/LMCS-17(2:24)2021"},{"issue":"3","key":"5_CR26","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0097-3165(72)90063-5","volume":"13","author":"JB Kruskal","year":"1972","unstructured":"Kruskal, J.B.: The theory of well-quasi-ordering: A frequently discovered concept. J. Combinatorial Theory, Ser. A 13(3), 297\u2013305 (1972). https:\/\/doi.org\/10.1016\/0097-3165(72)90063-5","journal-title":"J. Combinatorial Theory, Ser. A"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Shamash Halevy, N.: Energy games with resource-bounded environments. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 243, pp. 19:1\u201319:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.19","DOI":"10.4230\/LIPIcs.CONCUR.2022.19"},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12, 115\u2013116 (1981). https:\/\/doi.org\/10.1016\/0020-0190(81)90106-X","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"5_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2009.06.002","volume":"208","author":"F Ranzato","year":"2010","unstructured":"Ranzato, F., Tapparo, F.: An efficient simulation algorithm based on abstract interpretation. Inf. Comput. 208(1), 1\u201322 (2010). https:\/\/doi.org\/10.1016\/j.ic.2009.06.002","journal-title":"Inf. Comput."},{"key":"5_CR30","unstructured":"Reichert, J.: Reachability games with counters: Decidability and algorithms. Theses, \u00c9cole normale sup\u00e9rieure de Cachan - ENS Cachan (2015). https:\/\/tel.archives-ouvertes.fr\/tel-01314414"},{"issue":"3","key":"5_CR31","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.jlap.2008.10.002","volume":"78","author":"AW Roscoe","year":"2009","unstructured":"Roscoe, A.W.: Revivals, stuckness and the hierarchy of CSP models. J. Logic Algebraic Program. 78(3), 163\u2013190 (2009). https:\/\/doi.org\/10.1016\/j.jlap.2008.10.002","journal-title":"J. Logic Algebraic Program."},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-61474-5_61","volume-title":"Computer Aided Verification","author":"SK Shukla","year":"1996","unstructured":"Shukla, S.K., Hunt, H.B., Rosenkrantz, D.J.: HORNSAT, model checking, verification and games. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 99\u2013110. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_61"},{"key":"5_CR33","unstructured":"Stirling, C.: Modal and temporal logics for processes. Department of Computer Science, University of Edinburgh, Tech. rep. (1993)"},{"key":"5_CR34","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/j.ic.2015.03.001","volume":"241","author":"Y Velner","year":"2015","unstructured":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A., Raskin, J.F.: The complexity of multi-mean-payoff and multi-energy games. Inf. Comput. 241, 177\u2013196 (2015). https:\/\/doi.org\/10.1016\/j.ic.2015.03.001","journal-title":"Inf. Comput."}],"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-37706-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:03:28Z","timestamp":1704452608000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}