Abstract
PREG Axiomatizer is a tool used for proving strong bisimilarity between ground terms consisting of operations in the GSOS format extended with predicates. It automatically derives sound and ground-complete axiomatizations using a technique proposed by the authors of this paper. These axiomatizations are provided as input to the Maude system, which, in turn, is used as a reduction engine for provided ground terms. These terms are bisimilar if and only if their normal forms obtained in this fashion are equal. The motivation of this tool is the optimized handling of equivalence checking between complex ground terms within automated provers and checkers.
The authors have been been partially supported by the projects “New Developments in Operational Semantics” (nr. 080039021) and “Meta-theory of Algebraic Process Theories” (nr. 100014021) of the Icelandic Fund for Research. Eugen-Ioan Goriac is supported by the doctoral grant “Extending and Axiomatizing Structural Operational Semantics: Theory and Tools” (nr. 110294-0061) of the Icelandic Fund for Research.
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.: Deriving complete inference systems for a class of GSOS languages generation regular behaviours. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 449–464. Springer, Heidelberg (1994)
Aceto, L., Bloom, B., Vaandrager, F.: Turning SOS rules into equations. Inf. Comput. 111, 1–52 (1994), http://portal.acm.org/citation.cfm?id=184662.184663
Aceto, L., Caltais, G., Goriac, E.I., Ingólfsdóttir, A.: Axiomatizing GSOS with predicates (2011), http://ru.is/faculty/luca/PAPERS/extending_GSOS_with_predicates.pdf
Aceto, L., Cimini, M., Ingólfsdóttir, A., Mousavi, M., Reniers, M.A.: SOS rule formats for zero and unit elements. Theoretical Computer Science (to appear, 2011)
Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press, Cambridge (2010)
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge University Press, New York (1990)
Baeten, J.C.M., de Vink, E.P.: Axiomatizing GSOS with termination. J. Log. Algebr. Program. 60-61, 323–351 (2004)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42, 232–268 (1995), http://doi.acm.org/10.1145/200836.200876
Bosscher, D.J.B.: Term rewriting properties of SOS axiomatisations. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 425–439. Springer, Heidelberg (1994), http://portal.acm.org/citation.cfm?id=645868.668513
Chalub, F., Braga, C.: Maude MSOS Tool. Electron. Notes Theor. Comput. Sci. 176, 133–146 (2007), http://portal.acm.org/citation.cfm?id=1279349.1279455
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)
Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1989)
Mousavi, M.R., Reniers, M.A.: Prototyping SOS meta-theory in Maude. Electron. Notes Theor. Comput. Sci. 156, 135–150 (2006), http://dx.doi.org/10.1016/j.entcs.2005.09.030
Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60-61, 17–139 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Caltais, G., Goriac, EI., Ingolfsdottir, A. (2011). PREG Axiomatizer – A Ground Bisimilarity Checker for GSOS with Predicates. In: Corradini, A., Klin, B., Cîrstea, C. (eds) Algebra and Coalgebra in Computer Science. CALCO 2011. Lecture Notes in Computer Science, vol 6859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22944-2_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-22944-2_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22943-5
Online ISBN: 978-3-642-22944-2
eBook Packages: Computer ScienceComputer Science (R0)