Abstract
This paper offers a meta-theorem for languages with a Structural Operational Semantics (SOS) in the style of Plotkin. Namely, it proposes a generic rule format for SOS guaranteeing that certain constants act as left- or right-unit elements for a set of binary operators. We show the generality of our format by applying it to a wide range of operators from the literature on process calculi.
The work of Aceto and Ingolfsdottir has been partially supported by the projects “The Equational Logic of Parallel Processes” (nr. 060013021), and “New Developments in Operational Semantics” (nr. 080039021) of the Icelandic Research Fund. The first author dedicates the paper to the memory of his mother, Imelde Diomede Aceto, who passed away a year ago.
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
Preview
Unable to display preview. Download preview PDF.
References
Aceto, L., Birgisson, A., Ingolfsdottir, A., Mousavi, M.R., Reniers, M.A.: Rule Formats for Determinism and Idempotence. In: FSEN 2009. LNCS, vol. 5961. Springer, Heidelberg (to appear, 2010)
Aceto, L., Fokkink, W.J., Verhoef, C.: Structural Operational Semantics. In: Handbook of Process Algebra, ch. 3, pp. 197–292. Elsevier, Amsterdam (2001)
Aceto, L., Ingolfsdottir, A., Mousavi, M.R., Reniers, M.A.: A Rule Format for Unit Elements. Tech. Rep. CSR-0913, Eindhoven University of Technology (2009)
Baeten, J.C.M., Bergstra, J.: Mode Transfer in Process Algebra. Tech. Rep. CSR-0001, Eindhoven University of Technology (2000)
Bergstra, J.A., Klop, J.W.: Fixedpoint Semantics in Process Algebra. Tech. Rep. IW 206/82, Center for Mathematics, Amsterdam (1982)
Cranen, S., Mousavi, M.R., Reniers, M.A.: A Rule Format for Associativity. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 447–461. Springer, Heidelberg (2008)
van Glabbeek, R.J.: The Linear Time - Branching Time Apectrum I. In: Handbook of Process Algebra, ch. 1, pp. 3–100. Elsevier, Amsterdam (2001)
Hennessy, M., Milner, R.: Algebraic Laws for Non-Determinism and Concurrency. J. ACM 32(1), 137–161 (1985)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Mousavi, M.R., Reniers, M.A., Groote, J.F.: A Syntactic Commutativity Format for SOS. IPL 93, 217–223 (2005)
Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS Formats and Meta-Theory: 20 Years after. TCS 373(3), 238–272 (2007)
Plotkin, G.D.: A Structural Approach to Operational Semantics. JLAP 60-61, 17–140 (2004)
Plotkin, G.D.: A Powerdomain for Countable Non-Determinism (extended abstract). In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 418–428. Springer, Heidelberg (1982)
Verhoef, C.: A Congruence Theorem for Structured Operational Semantics with Predicates and Negative Premises. Nordic Journal of Computing 2(2), 274–302 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Ingolfsdottir, A., Mousavi, M., Reniers, M.A. (2010). A Rule Format for Unit Elements. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds) SOFSEM 2010: Theory and Practice of Computer Science. SOFSEM 2010. Lecture Notes in Computer Science, vol 5901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11266-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-11266-9_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11265-2
Online ISBN: 978-3-642-11266-9
eBook Packages: Computer ScienceComputer Science (R0)