Exploiting Algebraic Laws to Improve Mechanized AxiomatizationsShow others and affiliations
2013 (English)In: Algebra and Coalgebra in Computer Science: 5th International Conference, Calco 2013, Warsaw, Poland, September 2013, Proceedings, Berlin: Springer Berlin/Heidelberg, 2013, p. 36-50Conference paper, Published paper (Refereed)
Abstract [en]
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. © 2013 Springer-Verlag Berlin Heidelberg.
Place, publisher, year, edition, pages
Berlin: Springer Berlin/Heidelberg, 2013. p. 36-50
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8089
Keywords [en]
Process Algebra, Structural Operational Semantics, Bisimulation, Ground Complete Axiomatization, Algebraic Properties, Rule Formats
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:hh:diva-22060DOI: 10.1007/978-3-642-40206-7_5Scopus ID: 2-s2.0-84885981989Libris ID: 14699888ISBN: 9783642402067 ISBN: 9783642402050 OAI: oai:DiVA.org:hh-22060DiVA, id: diva2:619611
Conference
CALCO 2013, The 5th Conference on Algebra and Coalgebra in Computer Science, Warsaw, Poland, September 3-6, 2013
Projects
Meta-theory of Algebraic Process TheoriesExtending and Axiomatizing Structural Operational Semantics: Theory and Tools
Funder
eLLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications2013-05-062013-05-062018-01-11Bibliographically approved