Abstract
Axioms for domain operations in several variants of Kleene algebras and their semiring reducts are presented. They provide abstract enabledness conditions for algebras designed for the verification and refinement of action systems, probabilistic protocols, basic processes and games. The axiomatisations are simpler, more uniform and more flexible than previous attempts; they are especially suited for automated deduction. This is further demonstrated through the automated verification of some classical refinement laws for action systems.
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
Prover9 and Mace4, http://www.cs.unm.edu/~mccune/prover9
Back, R.J.R., von Wright, J.: Reasoning algebraically about loops. Acta Informatica 36(4), 295–334 (1999)
Bergstra, J.A., Fokkink, W.J., Ponse, A.: Process algebra with recursive operations. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 333–389. Elsevier, Amsterdam (2001)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM TOCL 7(4), 798–833 (2006)
Desharnais, J., Struth, G.: Domain semirings revisited. Technical Report CS-08-01, Department of Computer Science, University of Sheffield (2008); Accepted for Mathematics of Program Construction (MPC) (2008)
Furusawa, H., Tsumagari, N., Nishizawa, K.: A non-probabilistic model of probabilistic Kleene algebra. In: Berghammer, R., Möller, B., Struth, G. (eds.) Relations and Kleene Algebra in Computer Science. LNCS, vol. 4988, pp. 110–122. Springer, Heidelberg (2008)
Goranko, V.: The basic algebra of game equivalences. Studia Logica 75, 221–238 (2003)
Höfner, P., Struth, G.: Can refinement be automated? ENTCS 201, 197–222 (2007)
Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM TOCL 1(1), 60–76 (2000)
McIver, A.K., Gonzalia, C., Cohen, E., Morgan, C.C.: Using probabilistic Kleene algebra pKA for protocol verification. J. Logic and Algebraic Programming 76(1), 90–111 (2008)
Meinicke, L., Solin, K.: Refinement algebra for probabilistic programs. ENTCS 201, 177–195 (2007)
Möller, B.: Kleene getting lazy. Sc. Computer Programming 65(2), 195–214 (2007)
Pilz, G.: Near-Rings: The Theory and Its Application. North-Holland, Amsterdam (1983)
Solin, K., von Wright, J.: Refinement algebra with operators for enabledness and termination. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 397–415. Springer, Heidelberg (2006)
von Wright, J.: Towards a refinement algebra. Sc. Computer Programming 51(1-2), 23–45 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Desharnais, J., Struth, G. (2008). Domain Axioms for a Family of Near-Semirings. In: Meseguer, J., Roşu, G. (eds) Algebraic Methodology and Software Technology. AMAST 2008. Lecture Notes in Computer Science, vol 5140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79980-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-79980-1_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79979-5
Online ISBN: 978-3-540-79980-1
eBook Packages: Computer ScienceComputer Science (R0)