Reactive bisimulation semantics for a process algebra with timeouts. (English) Zbl 1539.68202
Summary: 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.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q55 | Semantics in the theory of computing |
References:
| [1] | Baeten, JCM; Bergstra, JA; Klop, JW, Syntax and defining equations for an interrupt mechanism in process algebra, Fundam. Inform., 9, 2, 127-168 (1986) · Zbl 0617.68027 · doi:10.3233/FI-1986-9202 |
| [2] | Baeten, JCM; Weijland, WP, Process Algebra. Cambridge Tracts in Theoretical Computer Science (1990), Cambridge: Cambridge University Press, Cambridge · Zbl 0716.68002 · doi:10.1017/CBO9780511624193 |
| [3] | Bisping, B.; Nestmann, U.; Peters, K., Coupled similarity: the first 32 years, Acta Inform., 57, 3-5, 439-463 (2020) · Zbl 1476.68166 · doi:10.1007/s00236-019-00356-4 |
| [4] | 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 |
| [5] | Bouwman, MS; Luttik, B.; Willemse, TAC, Off-the-shelf automated analysis of liveness properties for just paths, Acta Inform., 57, 3-5, 551-590 (2020) · Zbl 1443.68109 · doi:10.1007/s00236-020-00371-w |
| [6] | Brookes, SD; Hoare, CAR; Roscoe, AW, A theory of communicating sequential processes, J. ACM, 31, 3, 560-599 (1984) · Zbl 0628.68025 · doi:10.1145/828.833 |
| [7] | Davies, J.; Schneider, S., Recursion induction for real-time processes, Formal Aspects Comput., 5, 6, 530-553 (1993) · Zbl 0806.68073 · doi:10.1007/BF01211248 |
| [8] | De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theor. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518 · doi:10.1016/0304-3975(84)90113-0 |
| [9] | Dyseryn, V., van Glabbeek, R.J., Höfner, 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-34. doi:10.4204/EPTCS.255.2 (2017) · Zbl 1483.68227 |
| [10] | Fokkink, W.J.: Introduction to Process Algebra. Texts in Theoretical Computer Science, An EATCS Series. Springer, Berlin (2000). doi:10.1007/978-3-662-04293-9 · Zbl 0941.68087 |
| [11] | van Glabbeek, R.J.: A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In: Borzyszkowski, A.M., Sokołowski, S. (eds.). Proceedings 18th International Symposium on Mathematical Foundations of Computer Science, MFCS ’93, LNCS 711. Springer, pp. 473-484 (1993). doi:10.1007/3-540-57182-5_39 |
| [12] | van Glabbeek, R.J.: The Linear Time—Branching Time Spectrum II; The semantics of sequential systems with silent moves. In: Best, E. (ed.). Proceedings 4th International Conference on Concurrency Theory, CONCUR’93, LNCS 715. Springer, pp. 66-81 (1993). doi:10.1007/3-540-57208-2_6 |
| [13] | 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’94, Workshops in Computing. Springer, pp. 188-217 (1994). doi:10.1007/978-1-4471-2120-6_8 |
| [14] | van Glabbeek, R.J.: The Linear Time—Branching Time Spectrum I; The Semantics of Concrete, Sequential Processes. In: Bergstra, J.A., Ponse, A., S.A. Smolka, editors: Handbook of Process Algebra, chapter 1, Elsevier, pp. 3-99 (2001). doi:10.1016/B978-044482830-9/50019-9 · Zbl 1035.68073 |
| [15] | van Glabbeek, RJ, The meaning of negative premises in transition system specifications II, J. Logic Algebr. Program., 60-61, 229-258 (2004) · Zbl 1072.68075 · doi:10.1016/j.jlap.2004.03.007 |
| [16] | van Glabbeek, R.J.: Lean and full congruence formats for recursion. In: Proceedings 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’17. IEEE Computer Society Press (2017). doi:10.1109/LICS.2017.8005142 |
| [17] | van Glabbeek, R.J.: Ensuring liveness properties of distributed systems: open problems. J. Log. Algebr. Methods Program. 109, 100480 (2019) · Zbl 1435.68216 |
| [18] | van Glabbeek, RJ, Failure trace semantics for a process algebra with time-outs, Log. Methods Comput. Sci., 17, 2, 11 (2021) · Zbl 1535.68172 · doi:10.23638/LMCS-17(2:11)2021 |
| [19] | van Glabbeek, R.J.: Modelling Mutual Exclusion in a Process Algebra with Time-outs. https://arxiv.org/abs/2106.12785 (2021) · Zbl 1535.68172 |
| [20] | van Glabbeek, RJ; Höfner, P., CCS: It’s not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions, Acta Inform., 52, 2-3, 175-205 (2015) · Zbl 1327.68171 · doi:10.1007/s00236-015-0221-6 |
| [21] | van Glabbeek, RJ; Höfner, P., Progress, justness and fairness, ACM Comput. Surv., 52, 4, 69 (2019) · doi:10.1145/3329125 |
| [22] | van Glabbeek, R.J., Middelburg, C.A.: On Infinite Guarded Recursive Specifications in Process Algebra (2020). http://arxiv.org/abs/2005.00746 |
| [23] | van Glabbeek, RJ; Weijland, WP, Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600 (1996) · Zbl 0882.68085 · doi:10.1145/233551.233556 |
| [24] | 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’20. ACM, pp. 465-478 (2020). doi:10.1145/3373718.3394744 · Zbl 1502.68192 |
| [25] | Groote, JF, Transition system specifications with negative premises, Theor. Comput. Sci., 118, 263-299 (1993) · Zbl 0778.68057 · doi:10.1016/0304-3975(93)90111-6 |
| [26] | Groote, JF; Vaandrager, FW, Structured operational semantics and bisimulation as a congruence, Inf. Comput., 100, 2, 202-260 (1992) · Zbl 0752.68053 · doi:10.1016/0890-5401(92)90013-6 |
| [27] | Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021 · doi:10.1145/2455.2460 |
| [28] | Hoare, CAR, Communicating Sequential Processes (1985), Englewood Cliffs: Prentice Hall, Englewood Cliffs · Zbl 0637.68007 |
| [29] | 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ür Informatik (2020). doi:10.4230/LIPIcs.CONCUR.2020.35 · Zbl 07559491 |
| [30] | Lohrey, M.; D’Argenio, PR; Hermanns, H., Axiomatising divergence, Inf. Comput., 203, 2, 115-144 (2005) · Zbl 1110.68086 · doi:10.1016/j.ic.2005.05.007 |
| [31] | Milner, R., A complete inference system for a class of regular behaviours, J. Comput. Syst. Sci., 28, 439-466 (1984) · Zbl 0562.68065 · doi:10.1016/0022-0000(84)90023-0 |
| [32] | Milner, R., A complete axiomatisation for observational congruence of finite-state behaviors, Inf. Comput., 81, 2, 227-247 (1989) · Zbl 0688.68050 · doi:10.1016/0890-5401(89)90070-9 |
| [33] | Milner, R.: Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (ed.). Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201-1242. 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). doi:10.1007/3-540-10235-3 |
| [34] | Olderog, E.-R.: Operational Petri net semantics for CCSP. In: Rozenberg, G. (ed.). Advances in Petri Nets 1987, LNCS 266. Springer, pp. 196-223 (1987). doi:10.1007/3-540-18086-9_27 · Zbl 0636.68072 |
| [35] | Olderog, E-R; Hoare, CAR, Specification-oriented semantics for communicating processes, Acta Inform., 23, 9-66 (1986) · Zbl 0569.68019 · doi:10.1007/BF00268075 |
| [36] | Parrow, J., Sjödin, P.: Multiway synchronization verified with coupled simulation. In: Cleaveland, W.R. (ed.). Proceedings CONCUR 92, Stony Brook, NY, USA, LNCS 630. Springer, pp. 518-533 (1992). doi:10.1007/BFb0084813 |
| [37] | Pohlmann, M.: Reducing strong reactive bisimilarity to strong bisimilarity. Bachelor’s thesis, TU Berlin. https://maxpohlmann.github.io/Reducing-Reactive-to-Strong-Bisimilarity/thesis.pdf (2021) |
| [38] | Reed, GM; Roscoe, AW, A timed model for communicating sequential processes, Theor. Comput. Sci., 58, 249-261 (1988) · Zbl 0655.68031 · doi:10.1016/0304-3975(88)90030-8 |
| [39] | Vaandrager, F.W.: Expressiveness results for process algebras. In: de Bakker, 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-638 (1993). doi:10.1007/3-540-56596-5_49 |
| [40] | Walker, DJ, Bisimulation and divergence, Inf. Comput., 85, 2, 202-241 (1990) · Zbl 0713.68036 · doi:10.1016/0890-5401(90)90048-M |
| [41] | Zermelo, E., Untersuchungen über die Grundlagen der Mengenlehre I, Math. Ann., 65, 2, 261-281 (1908) · JFM 39.0097.03 · doi:10.1007/bf01449999 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
