Abstract
Communication with value passing has received ample attention in process theory. Value passing through a sequential composition has received much less attention. In recent work, we found that sequential value passing is the essential ingredient to prove the analogue of the classical theorem of the equivalence of pushdown automata and context-free grammars in a setting of interactive processes and bisimulation. Subsequently, we found that the treatment of sequential value passing in the process setting can be simplified considerably. We report on this simplification here, and find another application of sequential value passing, viz. a Kleene theorem for processes.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Aceto, L., Fokkink, W.J., Verhoef, C.: Structural operational semantics. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 197–292. North-Holland/Elsevier (2001). https://doi.org/10.1016/b978-044482830-9/50021-7
Baeten, J.C.M., Corradini, F., Grabmayer, C.A.: A characterization of regular expressions under bisimulation. J. ACM 54(2), 6–28 (2007). https://doi.org/10.1145/1219092.1219094
Baeten, J.C.M., Bergstra, J.A.: Process algebra with propositional signals. Theor. Comput. Sci. 177(2), 381–405 (1997). https://doi.org/10.1016/S0304-3975(96)00253-8
Baeten, J.C.M., Carissimo, C., Luttik, B.: Pushdown automata and context-free grammars in bisimulation semantics. Logical Methods Comput. Sci. 19, 15:1–15.32 (2023). https://doi.org/10.46298/LMCS-19(1:15)2023
Baeten, J.C.M., Luttik, B., Muller, T., van Tilburg, P.: Expressiveness modulo bisimilarity of regular expressions with parallel composition. Math. Struct. Comput. Sci. 26(6), 933–968 (2016). https://doi.org/10.1017/S0960129514000309
Baeten, J.C.M., Luttik, B., Yang, F.: Sequential composition in the presence of intermediate termination (extended abstract). In: Peters, K., Tini, S. (eds.) Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, EXPRESS/SOS 2017, Berlin, Germany, 4 September 2017. EPTCS, vol. 255, pp. 1–17 (2017). https://doi.org/10.4204/EPTCS.255.1. http://arxiv.org/abs/1709.00049
Baeten, J.C.M., Verhoef, C.: A congruence theorem for structured operational semantics with predicates. In: Best, E. (ed.) CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, 23–26 August 1993, Proceedings. Lecture Notes in Computer Science, vol. 715, pp. 477–492. Springer (1993). https://doi.org/10.1007/3-540-57208-2_33
Baeten, J.C., Basten, T., Reniers, M.: Process Algebra: Equational Theories of Communicating Processes, vol. 50. Cambridge university press, Cambridge (2010). https://doi.org/10.1017/CBO9781139195003
Belder, A., Luttik, B., Baeten, J.: Sequencing and intermediate acceptance: axiomatisation and decidability of bisimilarity. In: Roggenbach, M., Sokolova, A. (eds.) 8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019. Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.CALCO.2019.11
Bergstra, J.A., Fokkink, W., Ponse, A.: Chapter 5 - process algebra with recursive operations. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 333–389. Elsevier Science, Amsterdam (2001). https://doi.org/10.1016/B978-044482830-9/50023-0
Bloom, B.: When is partial trace equivalence adequate? Formal Aspects Comput. 6(3), 317–338 (1994). https://doi.org/10.1007/BF01215409
Bol, R.N., Groote, J.F.: The meaning of negative premises in transition system specifications. J. ACM 43(5), 863–914 (1996). https://doi.org/10.1145/234752.234756
Garavel, H.: Nested-unit petri nets: a structural means to increase efficiency and scalability of verification on elementary nets. In: Devillers, R.R., Valmari, A. (eds.) Application and Theory of Petri Nets and Concurrency - 36th International Conference, PETRI NETS 2015, Brussels, Belgium, 21–26 June 2015, Proceedings. Lecture Notes in Computer Science, vol. 9115, pp. 179–199. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-319-19488-2_9
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996). https://doi.org/10.1145/233551.233556
van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. J. Log. Algebr. Program. 60–61, 229–258 (2004). https://doi.org/10.1016/j.jlap.2004.03.007
Grabmayer, C., Fokkink, W.J.: A complete proof system for 1-free regular expressions modulo bisimilarity. CoRR abs/2004.12740 (2020). https://arxiv.org/abs/2004.12740
Groote, J.F.: Transition system specifications with negative premises. Theor. Comput. Sci. 118(2), 263–299 (1993). https://doi.org/10.1016/0304-3975(93)90111-6
Groote, J.F., Ponse, A.: Process algebra with guards: combining hoare logic with process algebra. Formal Aspects Comput. 6(2), 115–164 (1994). https://doi.org/10.1007/BF01221097
Hennessy, M.: Value-passing in process algebras. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 31–31. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039048
Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Automata Studies, pp. 3–41 (1956)
Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997). https://doi.org/10.1145/256167.256195
Luttik, B.: Divergence-preserving branching bisimilarity. In: Dardha, O., Rot, J. (eds.) Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020, and 17th Workshop on Structural Operational Semantics, Online, 31 August 2020. EPTCS, vol. 322, pp. 3–11 (2020). https://doi.org/10.4204/EPTCS.322.2
Milner, R.: A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci. 28(3), 439–466 (1984). https://doi.org/10.1016/0022-0000(84)90023-0
Verhoef, C.: A congruence theorem for structured operational semantics with predicates and negative premises. Nord. J. Comput. 2(2), 274–302 (1995)
Visser, E., Benaissa, Z.: A core language for rewriting. In: Kirchner, C., Kirchner, H. (eds.) 1998 International Workshop on Rewriting Logic and its Applications, WRLA 1998, Abbaye des Prémontrés at Pont-à-Mousson, France, September 1998. Electronic Notes in Theoretical Computer Science, vol. 15, pp. 422–441. Elsevier (1998). https://doi.org/10.1016/S1571-0661(05)80027-1
Acknowledgements
We are grateful to the two anonymous reviewers for their careful reviews; their comments and suggestions led to improvements in the presentation.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Baeten, J.C.M., Luttik, B. (2024). Sequential Value Passing Yields a Kleene Theorem for Processes. In: Capretta, V., Krebbers, R., Wiedijk, F. (eds) Logics and Type Systems in Theory and Practice. Lecture Notes in Computer Science, vol 14560. Springer, Cham. https://doi.org/10.1007/978-3-031-61716-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-031-61716-4_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-61715-7
Online ISBN: 978-3-031-61716-4
eBook Packages: Computer ScienceComputer Science (R0)