{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:59:12Z","timestamp":1743141552556,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031617157"},{"type":"electronic","value":"9783031617164"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-61716-4_12","type":"book-chapter","created":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:47:52Z","timestamp":1716954472000},"page":"188-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Minimal Depth Distinguishing Formulas Without Until for\u00a0Branching Bisimulation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4797-7735","authenticated-orcid":false,"given":"Jan","family":"Martens","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2196-6587","authenticated-orcid":false,"given":"Jan Friso","family":"Groote","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,5,22]]},"reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(96)00034-8","volume":"58","author":"AA Basten","year":"1996","unstructured":"Basten, A.A.: Branching bisimilarity is an equivalence indeed! Inf. Process. Lett. 58(3), 141\u2013147 (1996). https:\/\/doi.org\/10.1016\/0020-0190(96)00034-8","journal-title":"Inf. Process. Lett."},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Bradfield, J.C., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3, pp. 721\u2013756. North-Holland (2007). https:\/\/doi.org\/10.1016\/s1570-2464(07)80015-2","DOI":"10.1016\/s1570-2464(07)80015-2"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/BFb0023750","volume-title":"Computer-Aided Verification","author":"R Cleveland","year":"1991","unstructured":"Cleveland, R.: On automatically explaining bisimulation inequivalence. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 364\u2013372. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023750"},{"issue":"2","key":"12_CR5","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). https:\/\/doi.org\/10.1145\/201019.201032","journal-title":"J. ACM"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/11804192_10","volume-title":"Formal Methods for Components and Objects","author":"W Fokkink","year":"2006","unstructured":"Fokkink, W., van Glabbeek, R., de Wind, P.: Divide and congruence: from decomposition of modalities to preservation of branching bisimulation. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 195\u2013218. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_10"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-031-15629-8_14","volume-title":"A Journey from Process Algebra via Timed Automata to Model Learning","author":"JH Geuvers","year":"2022","unstructured":"Geuvers, J.H.: Apartness and distinguishing formulas in Hennessy-Milner logic. In: Jansen, N., Stoelinga, M., van den Bos, P. (eds.) A Journey from Process Algebra via Timed Automata to Model Learning. Lecture Notes in Computer Science, vol. 13560, pp. 266\u2013282. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15629-8_14"},{"key":"12_CR8","unstructured":"Geuvers, J.H., Golov, A.: Directed branching bisimulation via apartness and positive logic. arXiv preprint arXiv:2210.07380 (2022)"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Geuvers, J.H., Jacobs, B.: Relating apartness and bisimulation. Log. 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":"12_CR10","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3\u201399. North-Holland\/Elsevier (2001). https:\/\/doi.org\/10.1016\/b978-044482830-9\/50019-9","DOI":"10.1016\/b978-044482830-9\/50019-9"},{"issue":"3","key":"12_CR11","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). https:\/\/doi.org\/10.1145\/233551.233556","journal-title":"J. ACM"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.J.: An phO(phmlogphn) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. 18(2), 13:1\u201313:34 (2017). https:\/\/doi.org\/10.1145\/3060140","DOI":"10.1145\/3060140"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press (2014). https:\/\/mitpress.mit.edu\/books\/modeling-and-analysis-communicating-systems","DOI":"10.7551\/mitpress\/9946.001.0001"},{"key":"12_CR14","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":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-45237-7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DN Jansen","year":"2020","unstructured":"Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.: An O(m\u00a0log\u00a0n) algorithm for branching bisimilarity on labelled transition systems. In: TACAS 2020. LNCS, vol. 12079, pp. 3\u201320. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_1"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/3-540-55179-4_3","volume-title":"Computer Aided Verification","author":"H Korver","year":"1992","unstructured":"Korver, H.: Computing distinguishing formulas for branching bisimulation. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 13\u201323. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55179-4_3"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Martens, J.J.M., Groote, J.F.: Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable. In: P\u00e9rez, G.A., Raskin, J.-F. (eds.) Proceedings of Conference on Concurrency Theory, (CONCUR 2023). LIPIcs, vol. 279, pp. 32:1\u201332:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2023.32","DOI":"10.4230\/LIPIcs.CONCUR.2023.32"},{"issue":"3","key":"12_CR18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255\u2013281 (2003). https:\/\/doi.org\/10.1016\/S0167-6423(02)00094-1","journal-title":"Sci. Comput. Program."},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Milner, R.: 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"}],"container-title":["Lecture Notes in Computer Science","Logics and Type Systems in Theory and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61716-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:49:24Z","timestamp":1716954564000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61716-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031617157","9783031617164"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61716-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"22 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}