Kleene algebra with tests.
We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.
INTRODUCTION
Kleene algebras are algebraic structures with operators +, \Delta,   , 0, and 1 satisfying
certain axioms. They arise in various guises in many contexts: relational algebra
[Ng 1984; Tarski 1941], semantics and logics of programs [Kozen 1981; Pratt 1988],
automata and formal language theory [Kuich 1987; Kuich and Salomaa 1986], and
the design and analysis of algorithms [Aho et al. 1975; Iwano and Steiglitz 1990;
Kozen 1991]. Many authors have contributed to the development of Kleene algebra
[Anderaa 1965; Archangelsky 1992; Backhouse 1975; Bloom and '
Esik 1993; Boffa
1990; Cohen 1994a; Conway 1971; Gorshkov 1989; Kleene 1956; Kozen 1981; 1990;
Author's address: Computer Science Department, Cornell University, Ithaca, NY 14853-7501;
email: kozen@cs.cornell.edu.
The support of the National Science Foundation under grant CCR-9317320 is gratefully acknowledged

Permission to make digital/hard copy of all or part of this material without fee is granted
provided that the copies are not made or distributed for profit or commercial advantage, the
ACM copyright/server notice, the title of the publication, and its date appear, and notice is given
that copying is by permission of the Association for Computing Machinery, Inc. (ACM). To copy
otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific
permission and/or a fee.
c
1994; Krob 1991; Kuich and Salomaa 1986; Pratt 1990; Redko 1964; Sakarovitch
1987; Salomaa 1966].
In semantics and logics of programs, Kleene algebra forms an essential component
of Propositional Dynamic Logic (PDL) [Fischer and Ladner 1979], in which it is
mixed with Boolean algebra and modal logic to give a theoretically appealing and
practical system for reasoning about computation at the propositional level.
Syntactically, PDL is a two-sorted logic consisting of programs and propositions ,
defined by mutual induction. A test '? can be formed from any proposition ';
intuitively, '? acts as a guard that succeeds with no side effects in states satisfying
' and fails or aborts in states not satisfying '. Semantically, programs are modeled
as binary relations on a set of states, and '? is interpreted as the subset of the
identity relation consisting of all pairs (s; s) such that ' is true in state s.
From a practical point of view, many simple program manipulations, such as
loop unwinding and basic safety analysis, do not require the full power of PDL, but
can be carried out in a purely equational subsystem using the axioms of Kleene
algebra. However, tests are an essential ingredient, since they are needed to model
conventional programming constructs such as conditionals and while loops. We
define in Section 2 a variant of Kleene algebra, called Kleene algebra with tests, for
reasoning equationally with these constructs.
Cohen has studied Kleene algebra in the presence of extra Boolean and commutativity
conditions. He has given several practical examples of the use of Kleene
algebra in program verification, such as lazy caching [Cohen 1994b] and concurrency
control [Cohen 1994c]. He has also shown that Kleene algebra with extra
conditions of the form remains decidable [Cohen 1994a]. It can be shown using
a result of Berstel [1979] (see also Gibbons and Rytter [1986] and Kozen [1996])
that *-continuous Kleene algebra in the presence of extra commutativity conditions
of the form even for atomic p and q, is undecidable.
In Section 3 we give a complete equational proof of a classical folk theorem [Harel
1980; Mirkowska 1972] which states that every while program can be simulated by
another while program with at most one while loop. The approach we take is that
of Mirkowska [1972], who gives a set of local transformations that allow every while
program to be transformed systematically to one with at most one while loop. For
each such transformation, we give a purely equational proof of correctness. This
result illustrates the use of Kleene algebra with tests and commutativity conditions
in program equivalence proofs.
In Section 4.1, we observe that the universal Horn theory of the *-continuous
Kleene algebras is not recursively enumerable, therefore not finitely axiomatizable.
This follows from a construction of Berstel [1979] (see also Gibbons and Rytter
[1986]) and Lemma 7.1 of Kozen [1991]. This resolves an open question of Kozen
[1994].
2. KLEENE ALGEBRA
As defined in Kozen [1994], a Kleene algebra is an algebraic structure
satisfying (1)-(15) below. As usual, we omit the operator \Delta from expressions, writing
pq for p \Delta q. The order of precedence of the operators is
Kleene Algebra with Tests \Delta 3
should be parsed as )). The unary operator is defined by q
where - refers to the natural partial order on K:
Instead of (14) and (15), we might take the equivalent axioms
Axioms (1)-(11) say that the structure is an idempotent semiring under +, \Delta, 0,
and 1, and the remaining axioms (12)-(17) say essentially that   behaves like the
Kleene star operator of formal language theory or the reflexive transitive closure
operator of relational algebra. See Kozen [1994] for an introduction.
A Kleene algebra is said to be   -continuous if it satisfies the infinitary condition
r (18)
where
and where the supremum is with respect to the natural order -. We can think of
(18) as a conjunction of the infinitely many axioms pq and the
infinitary Horn formula
s:
In the presence of the other axioms, the *-continuity condition (18) implies (14)-
(17) and is strictly stronger in the sense that there exist Kleene algebras that are
not *-continuous [Kozen 1990].
All true identities between regular expressions, interpreted as regular sets of
strings, are derivable from the axioms of Kleene algebra [Kozen 1994]. In the au-
thor's experience, two of the most useful such identities for simplifying expressions
are
which we call the sliding and the denesting rules, respectively. For example, to
derive the identity (p   q)  reason equationally as follows:
(p   q)
2.1 Kleene Algebra with Tests
To accommodate tests, we introduce the following variant of Kleene algebra. A
Kleene algebra with tests is a two-sorted algebra
and is a unary operator defined only on B such that
is a Kleene algebra and
is a Boolean algebra. The elements of B are called tests. We reserve the letters
arbitrary elements of K and a; b; c; d; e for tests. In PDL, a test
would be written b?, but since we are using different symbols for tests we can omit
the ?.
The sequential composition operator \Delta acts as conjunction when applied to tests,
and the choice operator acts as disjunction. Intuitively, a test bc succeeds iff
both b and c succeed, and b + c succeeds iff either b or c succeeds.
It follows immediately from the definition that b - 1 for all b 2 B. It is tempting
to define tests in an arbitrary Kleene algebra to be the set fp 2 K 1g. This is
the approach taken by Cohen [1994a]. This approach is more restrictive than ours,
and we feel that it is less desirable for two important reasons:
(1) Although it makes sense in algebras of binary relations [Ng 1984; Tarski 1941],
it does not work in all Kleene algebras. For example, consider the (min,+)
Kleene algebra of the theory of algorithms (see Kozen [1991]), consisting of the
set fx 2 R j x - 0g [ f1g with operations min, +, x 7! 0, 1, and 0 for the
Kleene algebra operations +, \Delta,   , 0, and 1, respectively. In this algebra, p - 1
for all p, but the idempotence law fails, so the set fp 2 K does
not form a Boolean algebra. In our approach, every Kleene algebra extends
Kleene Algebra with Tests \Delta 5
trivially to a Kleene algebra with tests by taking the two-element Boolean
algebra f0; 1g. Of course, there are more interesting models as well.
(2) Even in algebras of binary relations, it forces us to consider all elements
as tests, including conditions that in practice would not normally be considered
testable. For example, there may be programs p whose input/output relations
have no side effects, i.e. p - 1, but the associated test succeeds iff p halts, which
in general is undecidable. We intend tests to be viewed as simple predicates
that are easily recognizable as such and that are immediately decidable in a
given state (and whose complements are therefore also immediately decidable).
Having an explicit Boolean subalgebra allows this.
2.2 While Programs
For the results of Section 3, we work with a Pascal-like programming language with
sequential composition p ; q, a conditional test if b then p else q, and a looping
construct while b do p. Programs built inductively from atomic programs and
tests using these constructs are called while programs. We take the sequential
composition operator to be of lower precedence than the conditional test or while
loop, parenthesizing with
while b do
should be parsed as
begin while b do p end ; q
and not
while b do begin
We occasionally omit the else clause of a conditional test. This can be considered
an abbreviation for a conditional test with the dummy else clause 1 (true).
These constructs are modeled in Kleene algebra with tests as follows:
if b then p else
if b then
while b do
See Kozen and Tiuryn [1990] for a discussion of the relation-theoretic semantics
of while programs and tests and a semantic justification of these definitions.
2.3 Commutativity Conditions
We will also be reasoning in the presence of commutativity conditions of the form
is an arbitrary element of the Kleene algebra and where b is a
test. The practical significance of these conditions will become apparent in Section
3. Intuitively, the execution of program p does not affect the value of b. It stands
to reason that if p does not affect b, then neither should it affect b. This is indeed
the case:
Lemma 2.3.1. In any Kleene algebra with tests, the following are equivalent:
Proof. By symmetry, it suffices to show the equivalence of (1) and (3). Assuming
(1), we have
Conversely, assuming (3), we have
therefore
Of course, any pair of tests commute, i.e., this is an axiom of Boolean
algebra.
We conclude this section with a pair of useful results that are fairly evident from
an intuitive point of view, but nevertheless require formal justification.
Lemma 2.3.2. In any Kleene algebra with tests, if
Note that it is not the case that bq  the left-hand side is 0
and the right-hand side is 1.
Proof. We prove the three inequalities
the equivalence of b(qb)   with these expressions follows from (19). For the first
inequality, it suffices by axiom (15) to show that b + (bq)   bq - (bq)   b. By Boolean
algebra and the commutativity assumption, we have
The second inequality follows from b - 1 and the monotonicity of the Kleene
algebra operators.
For the last inequality, it suffices by (14) to show
Note that in this last argument, we did not use the fact that b was a test.
Theorem 2.3.3. In any Kleene algebra, if p is generated by a set of elements
all of which commute with q, then p commutes with q.
Proof. Let p be an expression in the language of Kleene algebra, and assume
that all atomic subexpressions of p commute with q. The proof is by induction on
the structure of p. The basis and all inductive cases except for subexpressions of
the form r   are straightforward. For the inductive case we have by the
induction hypothesis that and we need to argue that qr  q. The
Kleene Algebra with Tests \Delta 7
inequality in one direction is given by the argument in the last paragraph in the
proof of Lemma 2.3.2, which uses (14), and in the other direction by a symmetric
argument using (15).
3. A FOLK THEOREM
In this section we give a purely equational proof, using Kleene algebra with tests
and commutativity conditions, of a classical result: every while program can be
simulated by a while program with at most one while loop, provided extra Boolean
variables are allowed. This theorem is the subject of a treatise on folk theorems by
Harel [1980], who notes that it is commonly but erroneously attributed to B-ohm
and Jacopini [1966] and who argues with some justification that it was known to
Kleene. The version as stated here is originally due to Mirkowska [1972], who gives
a set of local transformations that allow every while program to be transformed
systematically to one with at most one while loop. We consider a similar set of local
transformations and give a purely equational proof of correctness for each. This
result illustrates the use of Kleene algebra with tests and commutativity conditions
in program equivalence proofs.
It seems to be a commonly held belief that this result has no purely schematic
(i.e., propositional, uninterpreted) proof [Harel 1980]. The proofs of Hirose and
Oya [1972] and Mirkowska [1972], as reported in Harel [1980], use extra variables
to remember certain values at certain points in the program, either program counter
values or the values of tests. Since having to remember these values seems unavoid-
able, one might infer that the only recourse is to introduce extra variables, along
with an explicit assignment mechanism for assigning values to them. Thus, as the
argument goes, proofs of this theorem cannot be purely propositional.
We disagree with this conclusion. The only purpose of these extra variables is
to preserve values across computations. In our treatment, we only need to preserve
the values of certain tests b over certain computations p.
We can handle this purely equationally as follows. Suppose we need to preserve
the value of b across p. We introduce a new test c and commutativity condition
intuitively says that the computation of p does not affect the value
of c. Then we insert in an appropriate place the program s
new atomic program. Intuitively, we regard s as assigning the value of b to some
new Boolean variable that is tested in c, although there is no explicit mechanism
for doing this; s is just an uninterpreted atomic program symbol. However, the
in the language of while programs, if b then c
else c) insures that b and c have the same Boolean value just after execution of s.
3.1 An Example
To illustrate this technique, consider the simple program
else begin
If the value of b were preserved by p, then we could rewrite this program more
simply as
Formally, the assumption that the value of b is preserved by p takes the form of the
commutativity condition 2.3.1, we also have
in the language of Kleene algebra, the equivalence of (21) and (22) becomes the
equation
This identity can be established by simple equational reasoning:
bpr by the commutativity assumptions.
But what if b is not preserved by p? This situation seems to call for a Boolean
variable to remember the value of b across p and an explicit assignment mechanism
to set the value of the variable. However, our approach is much less drastic. We
introduce a new atomic test c and atomic program s along with the commutativity
condition intuitively modeling the idea that c tests a variable that is not
modified by p, and insert the program s
We can now give a purely equational proof of the equivalence of the two programs
else begin
and
using the axioms of Kleene algebra with tests and the commutativity condition
In fact, we can even do away with the atomic program s: if the two
programs are equivalent without the precomputation s, then they are certainly
equivalent with it.
Removing the leading s and expressing the two programs in the language of
Kleene algebra, the equivalence problem becomes
Using the distributive laws (8) and (9) and the laws of Boolean algebra, we can
simplify the left-hand side of (23) as follows:
The right-hand side of (23) simplifies in a similar fashion to the same expression:
Here the commutativity assumption is used in the second step.
Kleene Algebra with Tests \Delta 9
3.2 A Normal Form Theorem
A program is in normal form if it is of the form
do q (24)
where p and q are while free. The subprogram p is called the precomputation of
the normal form.
In our approach, the folk theorem takes the following form:
Theorem 3.2.1. Every while program, suitably augmented with finitely many
new subprograms of the form s bc, is equivalent to a while program in normal
form, reasoning in Kleene algebra with tests under certain commutativity assumptions
Theorem 3.2.1 is proved by induction on the structure of the program. Each
programming construct accounts for one case in the inductive proof. For each case,
we give a transformation that moves an inner while loop to the outside and an
equational proof of its correctness. The inductive construction is performed from
the inside out, i.e., smaller subprograms first.
In the statement of Theorem 3.2.1, we have been deliberately vague about where
to insert subprograms s ; bc+bc and what commutativity assumptions need
to be assumed. This will all be made explicit, but it is better done in the context
of the construction below.
3.3 Conditional
We first show how to deal with a conditional containing programs in normal form
in its then and else clauses. Consider the program
if b then begin
else begin
We introduce a new atomic program s and test c and assume that c commutes with
Under these assumptions, we show that the programs
if b then begin
else begin
and
if c then p 1 else
while do
if c then q 1 else q 2
are equivalent. Note that if the two programs in the then and else clauses of (25)
are in normal form, then (26) is in normal form. As argued in Section 3.1, we can
do away with the precomputation s.
Removing s and rewriting (25) in the language of Kleene algebra, we obtain
which reduces by distributivity and Boolean algebra to
Similarly, (26) becomes
The subexpression cd 1 of (28) is equivalent by propositional reasoning to
Here we have used the familiar propositional equivalence
and a De Morgan law. The other subexpressions of (28) can be simplified using
distributivity and Boolean algebra to obtain
Using distributivity, this can be broken up into the sum of four terms:
Under the commutativity assumptions, Lemma 2.3.2 implies that (31) and (32)
vanish; and for the remaining two terms (30) and (33), we have
The sum of these two terms is exactly (27).
3.4 Nested Loops
We next consider the case that is perhaps the most interesting: denesting two nested
while loops. This construction is particularly remarkable in that no commutativity
conditions (thus no extra variables) are needed; compare the corresponding transformations
of Hirose and Oya [1972] and Mirkowska [1972], as reported in Harel
[1980], which do use extra variables.
We show that the program
while b do begin
while c do q
Kleene Algebra with Tests \Delta 11
is equivalent to the program
if b then begin
do
if c then q else p
end.
This construction transforms a pair of nested while loops to a single while loop
inside a conditional test. No commutativity conditions are assumed in the proof.
After this transformation, the while loop can be taken outside the conditional
using the transformation of Section 3.3 (this part does require a commutativity
condition). A dummy normal form such as while 0 do 1 can be supplied for
the missing else clause. Note that if the program inside the block of
(34) is in normal form, then the resulting program will be in normal form.
Not surprisingly, the key property used in the proof is the denesting property
(20), which equates a regular expression of   -depth two with another of   -depth
one.
Translating to the language of Kleene algebra, (34) becomes
(bp(cq)   c)   b; (36)
and (35) becomes
The b in (37) is for the nonexistent else clause of the outermost conditional of (35).
The starred subexpression in (37) can be simplified using the basic laws of Kleene
and Boolean algebra:
(b
is equivalent to bc by a De Morgan Law. Making these transformations
to (37), we obtain
Unwinding the outer loop in (36) using (12) and distributing b over the resulting
sum, we obtain
Applying the sliding rule (19) to this expression gives
Now removing b, bp, and bc from this expression and (38), it suffices to show
But this is just an instance of the denesting rule (20).
Eliminating Postcomputations
We wish to show that a postcomputation occurring after a while loop can be
absorbed into the while loop. Consider a program of the form
while b do
We can assume without loss of generality that b, the test of the while loop, commutes
with the postcomputation q. If not, introduce a new test c that commutes
with q along with an atomic program s that intuitively sets the value of c to b, and
before the loop and in the loop after the body. We then claim that
the two programs
do begin
while c do begin
are equivalent. This allows us to replace (40) with (41), for which the commutativity
assumption holds.
For purposes of arguing that (40) and (41) are equivalent, we can omit all occurrences
of s. The leading occurrences can be omitted as argued in Section 3.1, and
the occurrences inside the while loops can be assumed to be part of p. The two
trailing occurrences of q can be omitted as well. After making these modifications
and writing the programs in the language of Kleene algebra, we need to show
Using the sliding rule (19) on both sides, this becomes
By distributivity and Boolean algebra, both sides reduce easily to (bcp)   bc.
Under the assumption that b and q commute, we show that (39) is equivalent to
the program
if b then q
else while b do begin
if b then q
end.
Note that if p and q are while free, then (42) consists of a program in normal
form inside a conditional, which can be transformed to normal form using the
construction of Section 3.3.
Written in the language of Kleene algebra, (39) becomes
(bp)   bq; (43)
and (42) becomes
Unwinding one iteration of (43) using (12) and distributing bq over the resulting
sum, we obtain
Kleene Algebra with Tests \Delta 13
Eliminating the term bq from both sides, it suffices to prove
Starting from the right-hand side, we have
sliding (19)
3.6 Composition
The composition of two programs in normal form
while b 1 do
while b 2 do q 2
can be transformed to a single program in normal form. We have actually already
done all the work needed to handle this case. First, we use the result of Section 3.5
to absorb the while-free program p 2 into the first while loop. We can also ignore
since it can be absorbed into the precomputation of the resulting normal form
when we are done. It therefore suffices to show how to transform a program
while b do
while c do q
to normal form, where p and q are while free.
As argued in Section 3.5, we can assume without loss of generality that the test
b commutes with the program q by introducing a new test if necessary. Since b also
commutes with c by Boolean algebra, by Theorem 2.3.3 we have that b commutes
with the entire second while loop. This allows us to use the transformation of
Section 3.5, absorbing the second while loop into the first. The resulting program
looks like
if b then while c do q
else while b do begin
if b then while c do q
end.
Here we have just substituted while c do q for q in (42). At this point we can
apply the transformation of Section 3.3 to the inner subprogram
if b then while c do q
using a dummy normal form for the omitted else clause, giving two nested loops
in the else clause of (47); then the transformation of Section 3.4 to the else clause
of (47); finally, the transformation of Section 3.3 to the entire resulting program,
yielding a program in normal form.
The transformations of Sections 3.3-3.6 give a systematic method for moving
while loops outside of any other programming construct. By applying these transformations
inductively from the innermost loops outward, we can transform any
program into a program in normal form.
None of these arguments needed an explicit assignment mechanism to Boolean
variables, but only a dummy program s which does something unspecified (and
which more often than not can be omitted in the actual proof) and a guard of the
that says that b and c somehow obtained the same Boolean value.
Of course, in a real implementation, s might assign the value of the test b to
some new Boolean variable that is tested in c, but this does not play a role in
equational proofs. The point is that it is not significant exactly how Boolean
values are preserved across computations, but rather that they can be preserved;
and for the purposes of formal verification, this fact is completely captured by a
commutativity assumption. Thus we are justified in our claim that we have given
a purely equational proof of Theorem 3.2.1.
4. RELATED RESULTS
4.1 Decidability and Undecidability
How difficult is reasoning in Kleene algebra under commutativity assumptions
qp? In other words, how hard is it to determine whether the universal Horn formula
holds in all Kleene algebras or in all *-continuous Kleene algebras, where
E is a finite set of equations of the form
It turns out that the problem is undecidable in general for *-continuous Kleene
algebras. However, for conditions of the form is a test, the problem
is PSPACE-complete for both Kleene algebras with tests and *-continuous
Kleene algebras with tests; thus it is no more difficult than reasoning without extra
conditions.
The undecidability result for general commutativity assumptions
continuous Kleene algebras follows from an undecidability result of Berstel [1979]
(see also Gibbons and Rytter [1986]) on regular sets over partially commutative
monoids and a result relating *-continuous Kleene algebras and regular sets [Kozen
1991, Lemma 7.1, p. 35]. A more direct proof has also been given by Cohen (private
communication, 1994); see Kozen [1996]. This reduction is not valid in the absence
of *-continuity for reasons explained below in Section 4.2.
The decidability result for conditions of the form pb = bp follows from the fact
that these conditions are equivalent to conditions of the form
Cohen [1994a] shows that Kleene algebra with conditions reduces efficiently
to Kleene algebra without conditions. In Kozen and Smith [1996], this result is
extended to Kleene algebra with tests. Thus reasoning in the presence of commutativity
conditions of the form used in Section 3 is no harder than reasoning without
extra conditions.
4.2 Finite Axiomatizability
Berstel's result establishes more than just undecidability. The constructions of
Berstel [1979] (see also Gibbons and Rytter [1986]) and Cohen (see Kozen [1996])
employ reductions from co-r.e. complete sets, namely the emptiness problem for
Kleene Algebra with Tests \Delta 15
Turing machines and the complement of Post's correspondence problem, respec-
tively. This implies that the universal Horn theory of the *-continuous Kleene
algebras is not recursively enumerable, therefore not finitely axiomatizable. In fact,
the theory is \Pi 1
1997]. The universal Horn theory of the Kleene
algebras is finitely axiomatizable (the axiomatization is given in Section 2); thus
the two theories do not coincide. This answers a question of Kozen [1994].
4.3 Completeness and Complexity
In Kozen and Smith [1996], we show that the equational theory of *-continuous
Kleene algebras with tests is complete over relational models and that it admits
consisting of sets of "guarded strings." These models
are analogous to the regular sets of strings over a finite alphabet for Kleene algebra
without tests. Using a technique based on Kozen [1994], it is also shown in Kozen
and Smith [1996] that the equational theories of Kleene algebras with tests and
*-continuous Kleene algebras with tests coincide. These results are analogous to
the completeness result of Kozen [1994] for Kleene algebras without tests.
These results imply that the equational theory of Kleene algebras with tests
reduces to PDL and is therefore decidable in at most exponential time. We have
shown by different methods that the problem is actually PSPACE-complete [Cohen
et al. 1996], thus no harder than the equational theory of Kleene algebras, which is
known to be PSPACE-complete [Stockmeyer and Meyer 1973].

ACKNOWLEDGMENTS

Thanks to Ernie Cohen, Neal Glew, David Gries, David Harel, Greg Morrisett,
Vaughan Pratt, Fred B. Schneider, Frederick Smith, Dave Walker, and the anonymous
referees for valuable comments. I am indebted to Ernie Cohen for his kind
permission to include a previously unpublished result in an earlier version of this
article [Kozen 1996, Theorem 4].



--R

The Design and Analysis of Computer Algorithms.
On the algebra of regular expressions.
A new finite complete solvable quasiequational calculus for algebra of regular languages.
Closure algorithms and the star-height problem of regular languages

Transductions and Context-free Languages

Une remarque sur les syst'emes complets d'identit'es rationnelles.

Hypotheses in Kleene algebra.
Lazy caching.

The complexity of Kleene algebra with tests.

Regular Algebra and Finite Machines.
Propositional dynamic logic of regular programs.

On the decidability of some problems about rational subsets of free partially commutative monoids.
Rational data structures and their applications.
On folk theorems.
General theory of flowcharts.
A semiring on convex polygons and zero-sum cycle prob- lems
Representation of events in nerve nets and finite automata.
On induction vs.
On Kleene algebras and closed semirings.

The Design and Analysis of Algorithms.
A completeness theorem for Kleene algebras and the algebra of regular events.
Kleene algebra with tests and commutativity conditions.
On the complexity of reasoning in Kleene algebra.
Kleene algebra with tests: Completeness and decidabil- ity
Logics of programs.
A complete system of B-rational identities
The Kleene and Parikh theorem in complete semirings.

Algorithmic logic and its applications.
Relation algebras with transitive closure.

Action logic and pure induction.
On defining relations for the algebra of regular events.
Kleene's theorem revisited: A formal path from Kleene to Chomsky.
In Trends
Two complete axiom systems for the algebra of regular events.
Word problems requiring exponential time.
On the calculus of relations.
revised November
--TR
The Kleene and the Parikh theorem in complete semirings
Kleene''s theorem revisited
On the decidability of some problems about rational subsets of free partially commutative monoids
On Kleene algebras and closed semirings
Dynamic algebras as a well-behaved fragment of relation algebras
A semiring on convex polygons and zero-sum cycle problems
Action logic and pure induction
Logics of programs
The design and analysis of algorithms
Complete systems of <inline-equation> <f> <sc>B</sc></f> </inline-equation>-rational identities
A completeness theorem for Kleene algebras and the algebra of regular events
Two Complete Axiom Systems for the Algebra of Regular Events
On folk theorems
Flow diagrams, turing machines and languages with only two formation rules
Semirings, Automata and Languages
Kleene Algebra withTests and Commutativity Conditions
Kleene Algebra with Tests
On Induction vs. *-Continuity
On the Complexity of Reasoning in Kleene Algebra
Word problems requiring exponential time(Preliminary Report)
The Complexity of Kleene Algebra with Tests

--CTR
Hubie Chen , Riccardo Pucella, A coalgebraic approach to Kleene algebra with tests, Theoretical Computer Science, v.327 n.1-2, p.23-44, 25 October 2004
Dexter Kozen, Some results in dynamic model theory, Science of Computer Programming, v.51 n.1-2, p.3-22, May 2004
Riccardo Pucella, Logical verification and equational verification, ACM SIGACT News, v.36 n.2, June 2005
Klaus-Dieter Schewe , Bernhard Thalheim, Conceptual modelling of web information systems, Data & Knowledge Engineering, v.54 n.2, p.147-188, August 2005
Dexter Kozen , Jerzy Tiuryn, Substructural logic and partial correctness, ACM Transactions on Computational Logic (TOCL), v.4 n.3, p.355-378, July
Therrezinha Fernandes , Jules Desharnais, Describing data flow analysis techniques with Kleene algebra, Science of Computer Programming, v.65 n.2, p.173-194, March, 2007
Sorin Lerner , Todd Millstein , Erika Rice , Craig Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, ACM SIGPLAN Notices, v.40 n.1, p.364-377, January 2005
Dexter Kozen, On Hoare logic and Kleene algebra with tests, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.60-76, July 2000
Bernhard Mller , Georg Struth, Algebras of modal operators and partial correctness, Theoretical Computer Science, v.351 n.2, p.221-239, 21 February 2006
Klaus-Dieter Schewe , Bernhard Thalheim , Aleksander Binemann-Zdanowicz , Roland Kaschek , Thomas Kuss , Bernd Tschiedel, A Conceptual View of Web-Based E-Learning Systems, Education and Information Technologies, v.10 n.1-2, p.83-110, January   2005
J. von Wright, Towards a refinement algebra, Science of Computer Programming, v.51 n.1-2, p.23-45, May 2004
Bernhard Mller, Kleene getting lazy, Science of Computer Programming, v.65 n.2, p.195-214, March, 2007
Maarten Marx, Conditional XPath, ACM Transactions on Database Systems (TODS), v.30 n.4, p.929-959, December 2005
Jules Desharnais , Bernhard Mller , Georg Struth, Kleene algebra with domain, ACM Transactions on Computational Logic (TOCL), v.7 n.4, p.798-833, October 2006
Klaus-Dieter Schewe , Bernhard Thalheim, Personalisation of web information systems - A term rewriting approach, Data & Knowledge Engineering, v.62 n.1, p.101-117, July, 2007
Fairouz Tchier, Demonic fixed points, Acta Cybernetica, v.17 n.3, p.533-555, January 2006
kleene algebra;dynamic logic;specification