Abstract
In the field of structural operational semantics (SOS), there have been several proposals both for syntactic rule formats guaranteeing the validity of algebraic laws, and for algorithms for automatically generating ground-complete axiomatizations. However, there has been no synergy between these two types of results. This paper takes the first steps in marrying these two areas of research in the meta-theory of SOS and shows that taking algebraic laws into account in the mechanical generation of axiomatizations results in simpler axiomatizations. The proposed theory is applied to a paradigmatic example from the literature, showing that, in this case, the generated axiomatization coincides with a classic hand-crafted one.
The first three authors have been partially supported by the project ‘Meta-theory of Algebraic Process Theories’ (nr. 100014021) of the Icelandic Research Fund. Eugen-Ioan Goriac is also funded by the project ‘Extending and Axiomatizing Structural Operational Semantics: Theory and Tools’ (nr. 1102940061) of the Icelandic Research Fund.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aceto, L., Bloom, B., Vaandrager, F.W.: Turning SOS rules into equations. Information and Computation 111, 1–52 (1994)
Aceto, L., Caltais, G., Goriac, E.-I., Ingolfsdottir, A.: PREG Axiomatizer - a ground bisimilarity checker for GSOS with predicates. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 378–385. Springer, Heidelberg (2011)
Aceto, L., Fokkink, W., Ingólfsdóttir, A., Luttik, B.: Finite equational bases in process algebra: Results and open questions. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes... (Klop Festschrift). LNCS, vol. 3838, pp. 338–367. Springer, Heidelberg (2005)
Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 3, pp. 197–292. Elsevier Science, Dordrecht (2001)
Aceto, L., Ingolfsdottir, A., Mousavi, M., Reniers, M.A.: Algebraic properties for free! Bulletin of the European Association for Theoretical Computer Science 99, 81–104 (2009)
Baeten, J., Basten, T., Reniers, M.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press (2009)
Baeten, J.J., de Vink, E.P.: Axiomatizing GSOS with termination. Journal of Logic and Algebraic Programming 60-61, 323–351 (2004)
Bergstra, J.A., Klop, J.W.: Fixedpoint semantics in process algebra. Technical Report IW 206/82, Center for Mathematics, Amsterdam, The Netherlands (1982)
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control 60(1-3), 109–137 (1984)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. Journal of the ACM 42(1), 232–268 (1995)
Bosscher, D.: Term rewriting properties of SOS axiomatisations. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 425–439. Springer, Heidelberg (1994)
van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 1, pp. 3–100. Elsevier Science, Dordrecht (2001)
Hennessy, M., Milner, A.R.: Algebraic laws for non-determinism and concurrency. Journal of the ACM 32(1), 137–161 (1985)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Milner, A.R.: Communication and Concurrency. Prentice-Hall (1989)
Mousavi, M., Reniers, M., Groote, J.F.: A syntactic commutativity format for SOS. Information Processing Letters 93, 217–223 (2005)
Mousavi, M., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theoretical Computer Science 373, 238–272 (2007)
Park, D.M.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Progamming 60, 17–139 (2004)
Ulidowski, I.: Finite axiom systems for testing preorder and De Simone process languages. Theoretical Computer Science 239(1), 97–139 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Goriac, EI., Ingolfsdottir, A., Mousavi, M.R., Reniers, M.A. (2013). Exploiting Algebraic Laws to Improve Mechanized Axiomatizations. In: Heckel, R., Milius, S. (eds) Algebra and Coalgebra in Computer Science. CALCO 2013. Lecture Notes in Computer Science, vol 8089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40206-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-40206-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40205-0
Online ISBN: 978-3-642-40206-7
eBook Packages: Computer ScienceComputer Science (R0)