Domain Axioms for a Family of Near-Semirings
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
- PDF / 468,098 Bytes
- 16 Pages / 430 x 660 pts Page_size
- 50 Downloads / 204 Views
2
D´epartement d’informatique et de g´enie logiciel, Universit´e Laval, Canada [email protected] Department of Computer Science, University of Sheffield, United Kingdom [email protected]
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.
1
Introduction
Variants of Kleene algebras provide the basic operations for modelling the dynamics of discrete systems. Choices between actions or processes are modelled through addition, sequential composition through multiplication, finite and infinite iteration via fixed points. Additive identities capture deadlock or abortion; silent or ineffective actions correspond to multiplicative identities. A main benefit of the approach is its suitability for first-order automated deduction in applications where model checking or interactive theorem proving is usually employed. Axiomatic variations are dictated by the semantics of application domains. Kleene algebras, for instance, capture partial program correctness under angelic choice [10] or trace models of reactive systems. Variants in which some axioms have been weakened admit predicate transformer models for total program correctness under demonic choice [16], expectation transformer models for probabilistic programs and protocols [11], and multirelational [7] or game-based models [8] for situations where angelic and demonic choices interact. Other variants of Kleene algebras provide algebraic semantics for parallel reactive systems modelled by action systems [3] or for basic process algebras [4]. A main source of variation is the interaction of choice with composition. For games and processes, for instance, a choice between the sequences xy and xz of actions x, y and z must be distinguished from a choice between y or z after execution of x, hence x(y + z) = xy + xz. Relation- or trace-based models, in contrast, require this distributivity law. Other applications might exclude that an infinite action x can be aborted after it has started, that is, x0 = 0. Again, this annihilation law certainly holds for binary relations. In many of these applications, axiomatising a domain operator is essential. For Kleene algebras, domain has been defined as a map into an embedded Boolean J. Meseguer and G. Ro¸su (Eds.): AMAST 2008, LNCS 5140, pp. 330–345, 2008. c Springer-Verlag Berlin Heidelberg 2008
Domain Axioms for a Family of Near-Semirings
331
algebra that models a state space [5]. In fact, it suffices to axiomatise domain on the semiring retract of the Kleene algebra. It turned out that this axiomatisation can essentially be reused
Data Loading...
