{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:32Z","timestamp":1740108332971,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T00:00:00Z","timestamp":1649376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T00:00:00Z","timestamp":1649376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001773","name":"University of New South Wales","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001773","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2023,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with timeout transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.<\/jats:p>","DOI":"10.1007\/s00236-022-00417-1","type":"journal-article","created":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T13:04:23Z","timestamp":1649423063000},"page":"11-57","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reactive bisimulation semantics for a process algebra with timeouts"],"prefix":"10.1007","volume":"60","author":[{"given":"Rob","family":"van Glabbeek","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,4,8]]},"reference":[{"issue":"2","key":"417_CR1","doi-asserted-by":"publisher","first-page":"127","DOI":"10.3233\/FI-1986-9202","volume":"9","author":"JCM Baeten","year":"1986","unstructured":"Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Syntax and defining equations for an interrupt mechanism in process algebra. Fundam. Inform. 9(2), 127\u2013168 (1986). https:\/\/doi.org\/10.3233\/FI-1986-9202","journal-title":"Fundam. Inform."},{"key":"417_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624193","volume-title":"Process Algebra. Cambridge Tracts in Theoretical Computer Science","author":"JCM Baeten","year":"1990","unstructured":"Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1990). https:\/\/doi.org\/10.1017\/CBO9780511624193"},{"issue":"3\u20135","key":"417_CR3","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/s00236-019-00356-4","volume":"57","author":"B Bisping","year":"2020","unstructured":"Bisping, B., Nestmann, U., Peters, K.: Coupled similarity: the first 32 years. Acta Inform. 57(3\u20135), 439\u2013463 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00356-4","journal-title":"Acta Inform."},{"key":"417_CR4","unstructured":"Bouwman, M.S.: Liveness analysis in process algebra: simpler techniques to model mutex algorithms. Technical Report, Eindhoven University of Technology (2018). http:\/\/www.win.tue.nl\/~timw\/downloads\/bouwman_seminar.pdf"},{"issue":"3\u20135","key":"417_CR5","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00236-020-00371-w","volume":"57","author":"MS Bouwman","year":"2020","unstructured":"Bouwman, M.S., Luttik, B., Willemse, T.A.C.: Off-the-shelf automated analysis of liveness properties for just paths. Acta Inform. 57(3\u20135), 551\u2013590 (2020). https:\/\/doi.org\/10.1007\/s00236-020-00371-w","journal-title":"Acta Inform."},{"issue":"3","key":"417_CR6","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"SD Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560\u2013599 (1984). https:\/\/doi.org\/10.1145\/828.833","journal-title":"J. ACM"},{"issue":"6","key":"417_CR7","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/BF01211248","volume":"5","author":"J Davies","year":"1993","unstructured":"Davies, J., Schneider, S.: Recursion induction for real-time processes. Formal Aspects Comput. 5(6), 530\u2013553 (1993). https:\/\/doi.org\/10.1007\/BF01211248","journal-title":"Formal Aspects Comput."},{"key":"417_CR8","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R De Nicola","year":"1984","unstructured":"De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83\u2013133 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90113-0","journal-title":"Theor. Comput. Sci."},{"key":"417_CR9","doi-asserted-by":"publisher","unstructured":"Dyseryn, V., van Glabbeek, R.J., H\u00f6fner, P.: Analysing Mutual Exclusion using Process Algebra with Signals. In: Peters, K., Tini, S. (eds.). Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, Electronic Proceedings in Theoretical Computer Science, vol. 255. Open Publishing Association, pp. 18\u201334. https:\/\/doi.org\/10.4204\/EPTCS.255.2 (2017)","DOI":"10.4204\/EPTCS.255.2"},{"key":"417_CR10","doi-asserted-by":"publisher","unstructured":"Fokkink, W.J.: Introduction to Process Algebra. Texts in Theoretical Computer Science, An EATCS Series. Springer, Berlin (2000). https:\/\/doi.org\/10.1007\/978-3-662-04293-9","DOI":"10.1007\/978-3-662-04293-9"},{"key":"417_CR11","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In: Borzyszkowski, A.M., Soko\u0142owski, S. (eds.). Proceedings 18th International Symposium on Mathematical Foundations of Computer Science, MFCS \u201993, LNCS 711. Springer, pp. 473\u2013484 (1993). https:\/\/doi.org\/10.1007\/3-540-57182-5_39","DOI":"10.1007\/3-540-57182-5_39"},{"key":"417_CR12","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: The Linear Time\u2014Branching Time Spectrum II; The semantics of sequential systems with silent moves. In: Best, E. (ed.). Proceedings 4th International Conference on Concurrency Theory, CONCUR\u201993, LNCS 715. Springer, pp. 66\u201381 (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_6","DOI":"10.1007\/3-540-57208-2_6"},{"key":"417_CR13","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: On the expressiveness of ACP (extended abstract). In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.). Proceedings First Workshop on the Algebra of Communicating Processes, ACP\u201994, Workshops in Computing. Springer, pp. 188\u2013217 (1994). https:\/\/doi.org\/10.1007\/978-1-4471-2120-6_8","DOI":"10.1007\/978-1-4471-2120-6_8"},{"key":"417_CR14","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: The Linear Time\u2014Branching Time Spectrum I; The Semantics of Concrete, Sequential Processes. In: Bergstra, J.A., Ponse, A., S.A. Smolka, editors: Handbook of Process Algebra, chapter\u00a01, Elsevier, pp. 3\u201399 (2001). https:\/\/doi.org\/10.1016\/B978-044482830-9\/50019-9","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"key":"417_CR15","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.jlap.2004.03.007","volume":"60\u201361","author":"RJ van Glabbeek","year":"2004","unstructured":"van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. J. Logic Algebr. Program. 60\u201361, 229\u2013258 (2004). https:\/\/doi.org\/10.1016\/j.jlap.2004.03.007","journal-title":"J. Logic Algebr. Program."},{"key":"417_CR16","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: Lean and full congruence formats for recursion. In: Proceedings 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201917. IEEE Computer Society Press (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005142","DOI":"10.1109\/LICS.2017.8005142"},{"key":"417_CR17","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J.: Ensuring liveness properties of distributed systems: open problems. J. Log. Algebr. Methods Program. 109, 100480 (2019)","DOI":"10.1016\/j.jlamp.2019.100480"},{"issue":"2","key":"417_CR18","doi-asserted-by":"publisher","first-page":"11","DOI":"10.23638\/LMCS-17(2:11)2021","volume":"17","author":"RJ van Glabbeek","year":"2021","unstructured":"van Glabbeek, R.J.: Failure trace semantics for a process algebra with time-outs. Log. Methods Comput. Sci. 17(2), 11 (2021). https:\/\/doi.org\/10.23638\/LMCS-17(2:11)2021","journal-title":"Log. Methods Comput. Sci."},{"key":"417_CR19","unstructured":"van Glabbeek, R.J.: Modelling Mutual Exclusion in a Process Algebra with Time-outs. https:\/\/arxiv.org\/abs\/2106.12785 (2021)"},{"issue":"2\u20133","key":"417_CR20","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s00236-015-0221-6","volume":"52","author":"RJ van Glabbeek","year":"2015","unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: CCS: It\u2019s not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions. Acta Inform. 52(2\u20133), 175\u2013205 (2015)","journal-title":"Acta Inform."},{"issue":"4","key":"417_CR21","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/3329125","volume":"52","author":"RJ van Glabbeek","year":"2019","unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: Progress, justness and fairness. ACM Comput. Surv. 52(4), 69 (2019). https:\/\/doi.org\/10.1145\/3329125","journal-title":"ACM Comput. Surv."},{"key":"417_CR22","unstructured":"van Glabbeek, R.J., Middelburg, C.A.: On Infinite Guarded Recursive Specifications in Process Algebra (2020). http:\/\/arxiv.org\/abs\/2005.00746"},{"issue":"3","key":"417_CR23","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":"417_CR24","doi-asserted-by":"publisher","unstructured":"Grabmayer, C., Fokkink, W.J.: A complete proof system for 1-free regular expressions modulo bisimilarity. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.). Proceedings of 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201920. ACM, pp. 465\u2013478 (2020). https:\/\/doi.org\/10.1145\/3373718.3394744","DOI":"10.1145\/3373718.3394744"},{"key":"417_CR25","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(93)90111-6","volume":"118","author":"JF Groote","year":"1993","unstructured":"Groote, J.F.: Transition system specifications with negative premises. Theor. Comput. Sci. 118, 263\u2013299 (1993). https:\/\/doi.org\/10.1016\/0304-3975(93)90111-6","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"417_CR26","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/0890-5401(92)90013-6","volume":"100","author":"JF Groote","year":"1992","unstructured":"Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100(2), 202\u2013260 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90013-6","journal-title":"Inf. Comput."},{"issue":"1","key":"417_CR27","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"},{"key":"417_CR28","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"417_CR29","doi-asserted-by":"publisher","unstructured":"Liu, X., Yu, T.: Canonical solutions to recursive equations and completeness of equational axiomatisations. In: Konnov, I., Kovacs, L. (eds.). Proceedings 31st International Conference on Concurrency Theory (CONCUR 2020), Leibniz International Proceedings in Informatics (LIPIcs) 171, Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.35","DOI":"10.4230\/LIPIcs.CONCUR.2020.35"},{"issue":"2","key":"417_CR30","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.ic.2005.05.007","volume":"203","author":"M Lohrey","year":"2005","unstructured":"Lohrey, M., D\u2019Argenio, P.R., Hermanns, H.: Axiomatising divergence. Inf. Comput. 203(2), 115\u2013144 (2005). https:\/\/doi.org\/10.1016\/j.ic.2005.05.007","journal-title":"Inf. Comput."},{"key":"417_CR31","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/0022-0000(84)90023-0","volume":"28","author":"R Milner","year":"1984","unstructured":"Milner, R.: A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci. 28, 439\u2013466 (1984). https:\/\/doi.org\/10.1016\/0022-0000(84)90023-0","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"417_CR32","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0890-5401(89)90070-9","volume":"81","author":"R Milner","year":"1989","unstructured":"Milner, R.: A complete axiomatisation for observational congruence of finite-state behaviors. Inf. Comput. 81(2), 227\u2013247 (1989). https:\/\/doi.org\/10.1016\/0890-5401(89)90070-9","journal-title":"Inf. Comput."},{"key":"417_CR33","doi-asserted-by":"publisher","unstructured":"Milner, R.: Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (ed.). Handbook of Theoretical Computer Science, chapter\u00a019, Elsevier Science Publishers B.V. (North-Holland), pp. 1201\u20131242. Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer (1990). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"417_CR34","doi-asserted-by":"publisher","unstructured":"Olderog, E.-R.: Operational Petri net semantics for CCSP. In: Rozenberg, G. (ed.). Advances in Petri Nets 1987, LNCS 266. Springer, pp. 196\u2013223 (1987). https:\/\/doi.org\/10.1007\/3-540-18086-9_27","DOI":"10.1007\/3-540-18086-9_27"},{"key":"417_CR35","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/BF00268075","volume":"23","author":"E-R Olderog","year":"1986","unstructured":"Olderog, E.-R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes. Acta Inform. 23, 9\u201366 (1986). https:\/\/doi.org\/10.1007\/BF00268075","journal-title":"Acta Inform."},{"key":"417_CR36","doi-asserted-by":"publisher","unstructured":"Parrow, J., Sj\u00f6din, P.: Multiway synchronization verified with coupled simulation. In: Cleaveland, W.R. (ed.). Proceedings CONCUR 92, Stony Brook, NY, USA, LNCS 630. Springer, pp. 518\u2013533 (1992). https:\/\/doi.org\/10.1007\/BFb0084813","DOI":"10.1007\/BFb0084813"},{"key":"417_CR37","unstructured":"Pohlmann, M.: Reducing strong reactive bisimilarity to strong bisimilarity. Bachelor\u2019s thesis, TU Berlin. https:\/\/maxpohlmann.github.io\/Reducing-Reactive-to-Strong-Bisimilarity\/thesis.pdf (2021)"},{"key":"417_CR38","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"GM Reed","year":"1988","unstructured":"Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theor. Comput. Sci. 58, 249\u2013261 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90030-8","journal-title":"Theor. Comput. Sci."},{"key":"417_CR39","doi-asserted-by":"publisher","unstructured":"Vaandrager, F.W.: Expressiveness results for process algebras. In: de\u00a0Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.). Proceedings REX Workshop on Semantics: Foundations and Applications, Beekbergen, The Netherlands, 1992, LNCS 666. Springer, pp. 609\u2013638 (1993). https:\/\/doi.org\/10.1007\/3-540-56596-5_49","DOI":"10.1007\/3-540-56596-5_49"},{"issue":"2","key":"417_CR40","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/0890-5401(90)90048-M","volume":"85","author":"DJ Walker","year":"1990","unstructured":"Walker, D.J.: Bisimulation and divergence. Inf. Comput. 85(2), 202\u2013241 (1990). https:\/\/doi.org\/10.1016\/0890-5401(90)90048-M","journal-title":"Inf. Comput."},{"issue":"2","key":"417_CR41","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/bf01449999","volume":"65","author":"E Zermelo","year":"1908","unstructured":"Zermelo, E.: Untersuchungen \u00fcber die Grundlagen der Mengenlehre I. Math. Ann. 65(2), 261\u2013281 (1908). https:\/\/doi.org\/10.1007\/bf01449999","journal-title":"Math. Ann."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-022-00417-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-022-00417-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-022-00417-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,27]],"date-time":"2023-02-27T05:03:28Z","timestamp":1677474208000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-022-00417-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,8]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["417"],"URL":"https:\/\/doi.org\/10.1007\/s00236-022-00417-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2022,4,8]]},"assertion":[{"value":"5 May 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}