# A completeness theorem for Kleene algebras and the algebra of regular events

@article{Kozen1991ACT, title={A completeness theorem for Kleene algebras and the algebra of regular events}, author={Dexter Kozen}, journal={[1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science}, year={1991}, pages={214-225} }

A finitary axiomatization of the algebra of regular events involving only equations and equational implications that is sound for all interpretations over Kleene algebras is given. Axioms for Kleene algebra are presented, and some basic consequences are derived. Matrices over a Kleene algebra are considered. The notion of an automaton over an arbitrary Kleen algebra is defined and used to derive the classical results of the theory of finite automata as a result of the axioms. The completeness… Expand

#### Topics from this paper

#### 42 Citations

The Complexity of Kleene Algebra with Tests

- Mathematics
- 1996

Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety… Expand

Sound and Complete Axiomatizations of Coalgebraic Language Equivalence

- Mathematics, Computer Science
- TOCL
- 2013

This article investigates under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalized powerset construction that determinizes coalgebras. Expand

Modal Kleene Algebra and Partial Correctness

- Computer Science, Mathematics
- AMAST
- 2004

Modal Kleene algebra provides a unifying semantics for various program calculi and enhances efficient cross-theory reasoning in this class, often in a very concise state-free style. Expand

The Algebra of Finite State Processes

- Mathematics
- 1995

This thesis is concerned with the algebraic theory of finite state processes. The processes we focus on are those given by a signature with prefix, summation and recursion, considered modulo strong… Expand

Equational Properties of Kleene Algebras of Relations with Conversion

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 1995

A set of equational axioms for the variety generated by all algebras of binary relations with operations of union, composition, conversion and reflexive-transitive closure and neutral elements 0 and 1 are described. Expand

Equational Axioms of Test Algebra

- Mathematics, Computer Science
- CSL
- 1997

It is shown that the Kleene algebra component cannot be replaced by a finite set of test algebra equations, so a finite equational axiomatization relative to Kleenegebra is achieved. Expand

Kleene modules and linear languages

- Mathematics, Computer Science
- J. Log. Algebraic Methods Program.
- 2006

The simultaneous linear fixed-point operator μ on languages can be reduced to iteration * on R and the scalar product :. Expand

Omega Algebra, Demonic Refinement Algebra and Commands

- Computer Science, Mathematics
- RelMiCS
- 2006

It is shown that the convergence operator can be defined explicitly in terms of infinite iteration and domain if and only if domain coinduction for infinite iteration holds. Expand

An Infinitary Sequent System for the Equational Theory of *-continuous Action Lattices

- Mathematics, Computer Science
- Fundam. Informaticae
- 2007

The cut-elimination theorem is proved and it is shown that ACT$_ω$ is $Π^0_1$, whence, by a result of Buszkowski [1], it is complete. Expand

The Algebraic Approach I: The Algebraization of the Chomsky Hierarchy

- Computer Science, Mathematics
- RelMiCS
- 2008

This work embodying the Chomsky hierarchy, itself, within an infinite complete lattice of algebras that ranges from dioids to quantales, and includes many of the forms of KleeneAlgebra that have been considered in the literature. Expand