{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:30Z","timestamp":1740108330883,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3-5","license":[{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100016378","name":"Technische Universit\u00e4t Dortmund","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100016378","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we prove that Hennessy\u2013Milner Logic (HML), despite its structural limitations, is sufficiently expressive to specify an initial property <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varphi _0$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msub><mml:mi>\u03c6<\/mml:mi><mml:mn>0<\/mml:mn><\/mml:msub><\/mml:math><\/jats:alternatives><\/jats:inline-formula> and a characteristic invariant <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\upchi _{_I}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msub><mml:mi>\u03c7<\/mml:mi><mml:msub><mml:mrow\/><mml:mi>I<\/mml:mi><\/mml:msub><\/mml:msub><\/mml:math><\/jats:alternatives><\/jats:inline-formula> for an arbitrary finite-state process <jats:italic>P<\/jats:italic> such that <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varphi _0 \\wedge \\mathbf{AG }(\\upchi _{_I})$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msub><mml:mi>\u03c6<\/mml:mi><mml:mn>0<\/mml:mn><\/mml:msub><mml:mo>\u2227<\/mml:mo><mml:mi>AG<\/mml:mi><mml:mrow><mml:mo>(<\/mml:mo><mml:msub><mml:mi>\u03c7<\/mml:mi><mml:msub><mml:mrow\/><mml:mi>I<\/mml:mi><\/mml:msub><\/mml:msub><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula> is a characteristic formula for <jats:italic>P<\/jats:italic>. This means that a process <jats:italic>Q<\/jats:italic>, even if infinite state, is bisimulation equivalent to <jats:italic>P<\/jats:italic> iff <jats:inline-formula><jats:alternatives><jats:tex-math>$$Q \\models \\varphi _0 \\wedge \\mathbf{AG }(\\upchi _{_I})$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>Q<\/mml:mi><mml:mo>\u22a7<\/mml:mo><mml:msub><mml:mi>\u03c6<\/mml:mi><mml:mn>0<\/mml:mn><\/mml:msub><mml:mo>\u2227<\/mml:mo><mml:mi>AG<\/mml:mi><mml:mrow><mml:mo>(<\/mml:mo><mml:msub><mml:mi>\u03c7<\/mml:mi><mml:msub><mml:mrow\/><mml:mi>I<\/mml:mi><\/mml:msub><\/mml:msub><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. It follows, in particular, that it is sufficient to check an HML formula for each state of a finite-state process to verify that it is bisimulation equivalent to <jats:italic>P<\/jats:italic>. In addition, more complex systems such as context-free processes can be checked for bisimulation equivalence with <jats:italic>P<\/jats:italic> using corresponding model checking algorithms. Our characteristic invariant is based on so called class-distinguishing formulas that identify bisimulation equivalence classes in <jats:italic>P<\/jats:italic> and which are expressed in HML. We extend Kanellakis and Smolka\u2019s partition refinement algorithm for bisimulation checking in order to generate concise class-distinguishing formulas for finite-state processes.<\/jats:p>","DOI":"10.1007\/s00236-020-00376-5","type":"journal-article","created":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T15:04:01Z","timestamp":1588777441000},"page":"671-687","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Characteristic invariants in Hennessy\u2013Milner logic"],"prefix":"10.1007","volume":"57","author":[{"given":"Marc","family":"Jasper","sequence":"first","affiliation":[]},{"given":"Maximilian","family":"Schl\u00fcter","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,5,6]]},"reference":[{"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.\u00a03, pp. 721\u2013756. North-Holland (2007). https:\/\/doi.org\/10.1016\/s1570-2464(07)80015-2","key":"376_CR1","DOI":"10.1016\/s1570-2464(07)80015-2"},{"doi-asserted-by":"publisher","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing Kripke structures in temporal logic. In: Ehrig, H., Kowalski, R.A., Levi, G., Montanari, U. (eds.) TAPSOFT\u201987: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23\u201327, 1987, Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP\u201987), Lecture Notes in Computer Science, vol. 249, pp. 256\u2013270. Springer (1987). https:\/\/doi.org\/10.1007\/3-540-17660-8_60","key":"376_CR2","DOI":"10.1007\/3-540-17660-8_60"},{"doi-asserted-by":"publisher","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 545\u2013623. Elsevier Science, Amsterdam (2001). https:\/\/doi.org\/10.1016\/B978-044482830-9\/50027-8. http:\/\/www.sciencedirect.com\/science\/article\/pii\/B9780444828309500278","key":"376_CR3","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"doi-asserted-by":"publisher","unstructured":"Burkart, O., Caucal, D., Steffen, B.: Bisimulation collapse and the process taxonomy. In: Montanari, U., Sassone, V. (eds.) CONCUR \u201996, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26\u201329, 1996, Proceedings, Lecture Notes in Computer Science, vol. 1119, pp. 247\u2013262. Springer (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_59","key":"376_CR4","DOI":"10.1007\/3-540-61604-7_59"},{"key":"376_CR5","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"CONCUR \u201992","author":"O Burkart","year":"1992","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W. (ed.) CONCUR \u201992, pp. 123\u2013137. Springer, Berlin Heidelberg, Berlin, Heidelberg (1992)"},{"doi-asserted-by":"publisher","unstructured":"Burkart, O., Steffen, B.: Pushdown Processes: Parallel Composition and Model Checking, pp. 98\u2013113. Springer Berlin Heidelberg, Berlin, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0015001","key":"376_CR6","DOI":"10.1007\/BFb0015001"},{"key":"376_CR7","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Automata, Languages and Programming","author":"O Burkart","year":"1997","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Automata, Languages and Programming, pp. 419\u2013429. Springer, Berlin Heidelberg, Berlin, Heidelberg (1997)"},{"doi-asserted-by":"publisher","unstructured":"Fischer, N., van Glabbeek, R.: Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours. J. Logical Algebraic Methods Program. 102, 64\u2013102 (2019). https:\/\/doi.org\/10.1016\/j.jlamp.2018.09.006. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S2352220817302201","key":"376_CR8","DOI":"10.1016\/j.jlamp.2018.09.006"},{"doi-asserted-by":"publisher","unstructured":"Floyd, R.W.: Assigning Meanings to Programs, pp. 65\u201381. Springer Netherlands, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","key":"376_CR9","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"376_CR10","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-45077-1_38","volume-title":"Fundamentals of Computation Theory","author":"W Fokkink","year":"2003","unstructured":"Fokkink, W., van Glabbeek, R., de Wind, P.: Compositionality of Hennessy\u2013Milner logic through structural operational semantics. In: Lingas, A., Nilsson, B.J. (eds.) Fundamentals of Computation Theory, pp. 412\u2013422. Springer, Berlin Heidelberg, Berlin, Heidelberg (2003)"},{"doi-asserted-by":"publisher","unstructured":"Fokkink, W., van Glabbeek, R., de Wind, P.: Compositionality of Hennessy\u2013Milner logic by structural operational semantics. Theor. Comput. Sci. 354(3), 421\u2013440 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2005.11.035. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397505008819","key":"376_CR11","DOI":"10.1016\/j.tcs.2005.11.035"},{"key":"376_CR12","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.) Formal Methods for Components and Objects, pp. 195\u2013218. Springer, Berlin Heidelberg, Berlin, Heidelberg (2006)"},{"doi-asserted-by":"publisher","unstructured":"Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. In: Paredaens, J. (ed.) Automata, Languages and Programming, 11th Colloquium, Antwerp, Belgium, July 16\u201320, 1984, Proceedings, Lecture Notes in Computer Science, vol. 172, pp. 222\u2013234. Springer (1984). https:\/\/doi.org\/10.1007\/3-540-13345-3_20","key":"376_CR13","DOI":"10.1007\/3-540-13345-3_20"},{"issue":"1\u20133","key":"376_CR14","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/S0019-9958(86)80038-9","volume":"68","author":"S Graf","year":"1986","unstructured":"Graf, S., Sifakis, J.: A logic for the description of non-deterministic programs and their properties. Inf. Control 68(1\u20133), 254\u2013270 (1986). https:\/\/doi.org\/10.1016\/S0019-9958(86)80038-9","journal-title":"Inf. Control"},{"issue":"1\u20133","key":"376_CR15","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/S0019-9958(86)80031-6","volume":"68","author":"S Graf","year":"1986","unstructured":"Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. Inf. Control 68(1\u20133), 125\u2013145 (1986). https:\/\/doi.org\/10.1016\/S0019-9958(86)80031-6","journal-title":"Inf. Control"},{"issue":"2","key":"376_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1142\/S0129054199000125","volume":"10","author":"M Habib","year":"1999","unstructured":"Habib, M., Paul, C., Viennot, L.: Partition refinement techniques: an interesting algorithmic tool kit. Int. J. Found. Comput. Sci. 10(2), 147\u2013170 (1999). https:\/\/doi.org\/10.1142\/S0129054199000125","journal-title":"Int. J. Found. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de\u00a0Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherlands, July 14\u201318, 1980, Proceedings, Lecture Notes in Computer Science, vol.\u00a085, pp. 299\u2013309. Springer (1980). https:\/\/doi.org\/10.1007\/3-540-10003-2_79","key":"376_CR17","DOI":"10.1007\/3-540-10003-2_79"},{"issue":"1","key":"376_CR18","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). https:\/\/doi.org\/10.1145\/2455.2460","journal-title":"J. ACM"},{"doi-asserted-by":"publisher","unstructured":"Hopcroft, J.: An n log n algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations, pp. 189\u2013196. Elsevier (1971). https:\/\/doi.org\/10.1016\/B978-0-12-417750-5.50022-1. http:\/\/www.sciencedirect.com\/science\/article\/pii\/B9780124177505500221","key":"376_CR19","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"doi-asserted-by":"publisher","unstructured":"Jancar, P., Kucera, A., Mayr, R.: Deciding bisimulation-like equivalences with finite-state processes. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) Automata, Languages and Programming, 25th International Colloquium, ICALP\u201998, Aalborg, Denmark, July 13\u201317, 1998, Proceedings, Lecture Notes in Computer Science, vol. 1443, pp. 200\u2013211. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0055053","key":"376_CR20","DOI":"10.1007\/BFb0055053"},{"doi-asserted-by":"publisher","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. In: Probert, R.L., Lynch, N.A., Santoro, N. (eds.) Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 17\u201319, 1983, pp. 228\u2013240. ACM (1983). https:\/\/doi.org\/10.1145\/800221.806724","key":"376_CR21","DOI":"10.1145\/800221.806724"},{"issue":"3","key":"376_CR22","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1017\/S1471068406002651","volume":"6","author":"A Kucera","year":"2006","unstructured":"Kucera, A., Jancar, P.: Equivalence-checking on infinite-state systems: techniques and results. TPLP 6(3), 227\u2013264 (2006). https:\/\/doi.org\/10.1017\/S1471068406002651","journal-title":"TPLP"},{"doi-asserted-by":"publisher","unstructured":"Kucera, A., Mayr, R.: On the complexity of semantic equivalences for pushdown automata and BPA. In: Diks, K., Rytter, W. (eds.) Mathematical Foundations of Computer Science 2002, 27th International Symposium, MFCS 2002, Warsaw, Poland, August 26\u201330, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2420, pp. 433\u2013445. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45687-2_36","key":"376_CR23","DOI":"10.1007\/3-540-45687-2_36"},{"issue":"2\u20133","key":"376_CR24","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/j.tcs.2006.01.021","volume":"358","author":"A Kucera","year":"2006","unstructured":"Kucera, A., Schnoebelen, P.: A general approach to comparing infinite-state systems with their finite-state specifications. Theor. Comput. Sci. 358(2\u20133), 315\u2013333 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.01.021","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Mayr, R.: Decidability of model checking with the temporal logic EF. Theor. Comput. Sci. 256(1), 31\u201362 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00101-8. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397500001018. ISS","key":"376_CR25","DOI":"10.1016\/S0304-3975(00)00101-8"},{"doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.\u00a092. Springer (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","key":"376_CR26","DOI":"10.1007\/3-540-10235-3"},{"key":"376_CR27","series-title":"PHI Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)"},{"doi-asserted-by":"publisher","unstructured":"Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11\u201315, 1989, Proceedings, Lecture Notes in Computer Science, vol. 372, pp. 723\u2013732. Springer (1989). https:\/\/doi.org\/10.1007\/BFb0035794","key":"376_CR28","DOI":"10.1007\/BFb0035794"},{"key":"376_CR29","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"CONCUR \u201995: Concurrency Theory","author":"B Steffen","year":"1995","unstructured":"Steffen, B., Cla\u00dfen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR \u201995: Concurrency Theory, pp. 72\u201387. Springer, Berlin Heidelberg, Berlin, Heidelberg (1995)"},{"issue":"1","key":"376_CR30","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B Steffen","year":"1994","unstructured":"Steffen, B., Ing\u00f3lfsd\u00f3ttir, A.: Characteristic formulas for processes with divergence. Inf. Comput. 110(1), 149\u2013163 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1028","journal-title":"Inf. Comput."},{"doi-asserted-by":"publisher","unstructured":"Steffen, B., Isberner, M., Jasper, M.: Playing with abstraction and representation. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi, pp. 191\u2013213. Springer International Publishing (2016). https:\/\/doi.org\/10.1007\/978-3-319-27810-0_10","key":"376_CR31","DOI":"10.1007\/978-3-319-27810-0_10"},{"key":"376_CR32","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/3-540-57182-5_39","volume-title":"Mathematical Foundations of Computer Science 1993","author":"R van Glabbeek","year":"1993","unstructured":"van Glabbeek, R.: A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In: Borzyszkowski, A.M., Soko\u0142owski, S. (eds.) Mathematical Foundations of Computer Science 1993, pp. 473\u2013484. Springer, Berlin Heidelberg, Berlin, Heidelberg (1993)"},{"key":"376_CR33","first-page":"66","volume-title":"CONCUR\u201993","author":"R van Glabbeek","year":"1993","unstructured":"van Glabbeek, R.: The linear time\u2014branching time spectrum ii. In: Best, E. (ed.) CONCUR\u201993, pp. 66\u201381. Springer, Berlin Heidelberg, Berlin, Heidelberg (1993)"},{"unstructured":"van Glabbeek, R.: What is branching time semantics and why to use it? In: Nielsen, M. (ed.) The Concurrency Column, Bulletin of the EATCS 53, pp. 190\u2013198 (1994)","key":"376_CR34"},{"doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.: The linear time\u2014branching time spectrum i. The semantics of concrete, sequential processes. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 3\u201399. Elsevier Science, Amsterdam (2001). https:\/\/doi.org\/10.1016\/B978-044482830-9\/50019-9. http:\/\/www.sciencedirect.com\/science\/article\/pii\/B9780444828309500199","key":"376_CR35","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.: A Characterisation of Weak Bisimulation Congruence, pp. 26\u201339. Springer Berlin Heidelberg, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11601548_4","key":"376_CR36","DOI":"10.1007\/11601548_4"},{"doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.: On cool congruence formats for weak bisimulations. Theor. Comput. Sci. 412(28), 3283\u20133302 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.02.036. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397511001605","key":"376_CR37","DOI":"10.1016\/j.tcs.2011.02.036"},{"issue":"4","key":"376_CR38","doi-asserted-by":"publisher","first-page":"371","DOI":"10.3233\/FI-2009-109","volume":"93","author":"R van Glabbeek","year":"2009","unstructured":"van Glabbeek, R., Luttik, B., Tr\u010dka, N.: Branching bisimilarity with explicit divergence. Fundamenta Informaticae 93(4), 371\u2013392 (2009)","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"publisher","unstructured":"van Glabbeek, R., Smolka, S., Steffen, B.: Reactive, generative, and stratified models of probabilistic processes. Inf Comput 121(1), 59\u201380 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1123. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540185711236","key":"376_CR39","DOI":"10.1006\/inco.1995.1123"},{"issue":"3","key":"376_CR40","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R van Glabbeek","year":"1996","unstructured":"van Glabbeek, R., 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"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00376-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00376-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00376-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,5]],"date-time":"2021-05-05T23:27:26Z","timestamp":1620257246000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00376-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,6]]},"references-count":40,"journal-issue":{"issue":"3-5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["376"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00376-5","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2020,5,6]]},"assertion":[{"value":"15 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}