BRICS RS-00-27 Ésik & Kuich: Inductive^{∗}-Semirings BRICS

Basic Research in Computer Science

Inductive^{∗}-Semirings

Zoltán Ésik Werner Kuich BRICS Report Series RS-00-27 ISSN 0909-0878 October 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Zoltán Ésik & Werner Kuich.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/00/27/

Inductive ^{∗}-Semirings^{∗}

Z. Ésik^{†}

Dept. of Computer Science

University of Szeged Árpád tér 2 H-6720 Szeged Hungary

email: esik@inf.u-szeged.hu

W. Kuich^{‡}

Institut für Algebra und Computermathematik Technische Universität Wien Wiedner Hauptstraße 8–10 A-1040 Wien Austria email: kuich@tu-wien.ac.at

October 2000

Abstract

One of the most well-known induction principles in computer science is the fixed point induction rule, or least pre-fixed point rule. Inductive^{∗}- semirings are partially ordered semirings equipped with a star operation satisfying the fixed point equation and the fixed point induction rule for linear terms. Inductive^{∗}-semirings are extensions of continuous semirings and the Kleene algebras of Conway and Kozen.

We develop, in a systematic way, the rudiments of the theory of inductive ^{∗}-semirings in relation to automata, languages and power series. In particular, we prove that if S is an inductive ^{∗}-semiring, then so is the semiring of matrices S^{n×n}, for any integer n ≥ 0, and that if S is an inductive ^{∗}-semiring, then so is any semiring of power series S⟨ ⟨A^{∗}⟩ ⟩. As shown by Kozen, the dual of an inductive ^{∗}-semiring may not be inductive. In contrast, we show that the dual of an iteration semiring is an iteration semiring. Kuich proved a general Kleene theorem for continuous semirings, and Bloom and Ésik proved a Kleene theorem for all Conway semirings. Since any inductive ^{∗}-semiring is a Conway semiring and an iteration semiring, as we show, there results a Kleene theorem applicable to all inductive ^{∗}-semirings. We also describe the structure of the initial inductive ^{∗}-semiring and conjecture that any free inductive ∗-semiring may be given as a semiring of rational power series with coefficients in the initial inductive ^{∗}-semiring. We relate this conjecture to recent axiomatization results on the equational theory of the regular sets.

∗The results of this paper were presented at the 3rd International Colloquium on Words, Languages and Combinatorics, Kyoto, March 2000.

†Partially supported by grant no. T22423 from the National Foundation of Hungary for Scientific Research and the Austrian-Hungarian Bilateral Research and Development Fund, no. A-4/1999. The work reported in the paper was partially carried out during the first author’s visit at BRICS.

‡Partially supported by the Austrian-Hungarian Bilateral Research and Development Fund, no. A-4/1999.

1 Introduction

One of the most well-known induction principles used in computer science and in particular in semantics is the fixed point induction rule, see de Bakker and Scott [9] and Park [21]. Inductive ^{∗}-semirings are semirings equipped with a partial order satisfying the fixed point equation and the fixed point induction rule for linear terms. Inductive ^{∗}-semirings extend the notion of continuous semirings used by Goldstern [13], Sakarovitch [22] and Kuich [19] and the Kleene algebras of Conway [7] and Kozen [16, 17]. Also, every Blikle net [2] and quantale [15] is an inductive ^{∗}-semiring. Continuous semirings cannot be defined within first-order logic. In contrast, inductive semrings are defined by implications and thus form a quasi-variety. We provide, in a systematic way, the rudiments of a theory of inductive ^{∗}- semirings related to automata, languages and power series. In particular, we prove that if S is an inductive ^{∗}-semiring, then so is S^{n×n}, for any integer n ≥ 0. Also, we prove that if S is an inductive ^{∗}-semiring, then so is any semiring of power series S⟨ ⟨A^{∗}⟩ ⟩. Moreover, we prove that any inductive ^{∗}- semiring is a Conway semiring and an iteration semiring. As shown by Kozen [17], the dual of an inductive ^{∗}-semiring is not not always an inductive ^{∗}- semiring. In contrast, we prove that the dual of an iteration semiring is an iteration semiring. Kuich [19] proved a general Kleene theorem for continuous semirings. Bloom and Ésik [4, 6] define Conway semirings and prove a general Kleene theorem for all Conway semirings. Since any inductive ^{∗}-semiring is a Conway semiring and an iteration semiring, there results a Kleene theorem applicable to all inductive ^{∗}-semirings. We present a variation of this result which also applies to all Conway semirings and thus to all inductive ^{∗}-semirings. Our proof follows standard arguments, see, e.g., Conway [7], but we recall the main constructions in order to make the paper selfcontained. We also describe the structure of the initial inductive ^{∗}-semiring and conjecture that any free inductive ^{∗}-semiring may be characterized as a semiring of rational power series with coefficients in the initial inductive ^{∗}-semiring. We relate this conjecture to recent axiomatization results on the equational theory of the regular sets and rational power series, see [18, 16, 5, 10, 11]. In a companion paper, we plan to study semirings equipped with a partial order satsifying the fixed point equation and the fixed point induction rule for all algebraic terms. Some notation. For each integer n ≥ 0, we denote the set {1, …, n} by [n]. Thus, [0] is the empty set. If A is a set, we let A^{∗} denote the set of all words over A including the empty word ϵ. For each word w ∈ A^{∗}, |w| denotes the length of w.

2 Inductive ^{∗}-semirings and Conway semirings

In this section we define our main concept, inductive^{∗}-semirings, and establish some elementary properties of inductive^{∗}-semirings. We then prove that every inductive ^{∗}-semiring is a Conway semiring. Recall that a semiring is an algebra S = (S, +, ·, 0, 1) equipped with binary operations + (sum or addition) and · (product or multiplication) and constants 0 and 1 such that (S, +, 0) is a commutative monoid, (S, ·, 1) is a monoid and multiplication distributes over all finite sums, including the empty sum. Thus,

(a + b)c = ac + bc
c(a + b) = ca + cb
a · 0 = 0
0 · a = 0

hold for all a, b, c ∈ S. An ordered semiring^{1} is a semiring S equipped with a partial order ≤ such that the operations are monotonic. A morphism of semirings is a function that preserves the operations and constants. A morphism of ordered semirings also preserves the partial order. A ^{∗}-semiring is a semiring S equipped with a star operation ^{∗} : S → S. Morphisms of ^{∗}-semirings preserve the star operation.

Definition 2.1 An inductive ^{∗}-semiring is a ^{∗}-semiring which is also an ordered semiring and satisfies the fixed point inequation

aa^{∗} + 1 ≤ a^{∗}  (1)

and the fixed point induction rule

ax + b ≤ x ⇒ a^{∗}b ≤ x.  (2)

A morphism of inductive ^{∗}-semirings is an order preserving ^{∗}-semiring morphism.

Proposition 2.2 The fixed point equation

aa^{∗} + 1 = a^{∗}  (3)

holds in any inductive ^{∗}-semiring. Moreover, the star operation is monotonic.

1This notion of ordered semiring is more special than the one defined in [12].

Proof. Since the semiring operations are monotonic, (1) implies

a(aa^{∗} + 1) + 1 ≤ aa^{∗} + 1.

Thus, a^{∗} ≤ aa^{∗} + 1 by the fixed point induction rule. By (1) this proves (3). As for the second claim, suppose that a ≤ b in an inductive ^{∗}-semiring. Then ab^{∗} + 1 ≤ bb^{∗} + 1 = b^{∗}, so that a^{∗} ≤ b^{∗} by the fixed point induction rule. □

The main examples of inductive^{∗}-semirings can be derived from the continuous semirings defined below. Recall that a directed set in a partially ordered set P is a nonempty set D ⊆ P such that any two elements of D have an upper bound in D. We call P a complete partially ordered set, or cpo^{2}, for short, if P has a least element and least upper bounds sup D of all directed sets D ⊆ P. When P is a cpo, so is P^{n}, for any n ≥ 0. The order on P^{n} is the pointwise order. Suppose that P and Q are cpo’s. A function f : P → Q is called continuous if f preserves the sup of any directed set, i.e.,

f(sup D) = sup f(D),

for all directed sets D ⊆ P. It follows that any continuous function is monotonic.

Definition 2.3 A continuous semiring is an ordered semiring S which is a cpo with least element 0 and such that the sum and product operations are continuous. A morphism of continuous semirings is a continuous semiring morphism.

In a continuous semiring S, we may define the sum of any family of elements of S. Given a_{i} ∈ S, i ∈ I, we define

∑_{i∈I} a_{i} = sup_{F ⊆I, F finite} ∑_{i∈F} a_{i}.  (4)

It follows that any continuous semiring morphism preserves all sums.

Definition 2.4 Suppose that S is both a ^{∗}-semiring and a continuous semiring. We call S a continuous ^{∗}-semiring if the star operation on S is given by

a^{∗} = ∑_{n≥0} a^{n},

for all a ∈ S. A morphism of continuous ^{∗}-semirings is a ^{∗}-semiring morphism which is continuous.

2Cpo’s are called dcpo’s in [8].

It follows that the star operation is also continuous. Note that if S and S′ are continuous ^{∗}-semirings, then any continuous semiring morphism S → S′ automatically preserves the star operation. By the well-known fixed-point theorem for continuous functions, [8] Theorem 4.5, we have:

Proposition 2.5 Any continuous ^{∗}-semiring is an inductive ^{∗}-semiring.

Some examples of continuous ^{∗}-semirings are:

1. The semiring P_{M} of all subsets of a multiplicative monoid M, equipped with the union and complex product operations and the partial order given by set inclusion.

2. For any set A, the semiring L_{A} of all languages in A^{∗}.

3. For any set A, the semiring Rel_{A} of all binary relations over A.

4. The semiring N_{∞} obtained by adding a top element to N, the ordered semiring of natural numbers {0, 1, 2, …} equipped with the usual sum and product operations.

5. Any finite ordered semiring, in particular the semiring k = {0, 1, …, k − 1}, for each integer k > 1. In this semiring, the sum and product operations and the partial order are the usual ones except that x + y is k − 1 if the usual sum is > k − 1, and similarly for xy. When k = 2, this semiring is also known as the Boolean semiring B.

6. Every Blikle net [2] or quantale [15].

Inductive ^{∗}-semirings other than continuous ^{∗}-semirings include the semirings R_{A} and CF_{A} of regular and context free languages in A^{∗}, and the Kleene algebras of Kozen [16] that we will call Kozen semirings below. For the existence of inductive ^{∗}-semirings that cannot be embedded in any continuous ∗-semiring see below.

Example 2.6 We give a generalization of an example of Kozen [17]. Suppose that (M, +, 0, ≤) is a commutative monoid equipped with a partial order ≤ such that 0 is the least element of M and such that M is a cpo, i.e., all directed sets have a supremum. Moreover, suppose that + is continuous. Let F_{M} denote the set of all strict additive and monotonic functions f : M → M, i.e., such that

f(a + b) = f(a) + f(b)
f(0) = 0
a ≤ b ⇒ f(a) ≤ f(b),

for all a, b ∈ A. When f, g ∈ F_{M}, define

(f + g)(a) = f(a) + g(a)
(f ∘ g)(a) = f(g(a))

for all a ∈ A. Moreover, let 0(a) = 0, 1(a) = a, all a ∈ A. Equipped with these operations and constants, and the pointwise partial order, F_{M} is an ordered semiring. By the Knaster-Tarski fixed point theorem [8], for each f ∈ F_{M} and a ∈ A, the monotonic function x ↦ f(x)+a, x ∈ M has a least pre-fixed point that we denote by f^{∗}(a). In fact, f^{∗}(a) is the “limit” of the sequence

f^{0}(a) = a
f^{α+1} = f(f^{α}(a)) + a
f^{α}(a) = sup_{β<α} f^{β}(a), α > 0 is a limit ordinal.

Using this, and the continuity of +, it follows easily that f^{∗} is a strict additive function. Since f^{∗} is also monotonic, there results a well-defined star operation on F_{M}. In fact, F_{M} is an inductive ^{∗}-semiring.

Suppose that S is a ^{∗}-semiring which is an ordered semiring. Below we will say that the weak fixed point induction rule holds in S if

ax + b = x ⇒ a^{∗}b ≤ x,

for all a, b and x in S.

Proposition 2.7 The following equations hold in an inductive semiring:

a^{∗}a + 1 = a^{∗}  (5)
(ab)^{∗} = 1 + a(ba)^{∗}b  (6)
(ab)^{∗}a = a(ba)^{∗}  (7)
(a + b)^{∗} = (a^{∗}b)^{∗}a^{∗}.  (8)

Proof. To prove (5), note that

a(a^{∗}a + 1) + 1 = (aa^{∗} + 1)a + 1
= a^{∗}a + 1,

so that

a^{∗} ≤ a^{∗}a + 1,  (9)

by the weak fixed point induction rule. But for all b,

aba(ba)^{∗} + a = a(ba(ba)^{∗} + 1)
= a(ba)^{∗}.

Thus,

(ab)^{∗}a ≤ a(ba)^{∗},  (10)

again by the weak fixed point induction rule. Taking b = 1 in (10), we have

a^{∗}a ≤ aa^{∗}.  (11)

By (9) and (11),

a^{∗} ≤ a^{∗}a + 1 ≤ aa^{∗} + 1 = a^{∗}.

Next we prove (6). Since

ab(a(ba)^{∗}b + 1) + 1 = a(ba(ba)^{∗} + 1)b + 1
= a(ba)^{∗}b + 1,

we have

(ab)^{∗} ≤ a(ba)^{∗}b + 1,  (12)

by the weak fixed point induction rule. But by (10) and (3),

a(ba)^{∗}b + 1 ≤ ab(ab)^{∗} + 1
= (ab)^{∗},

which together with (12) yields (6). We now prove (7).

(ab)^{∗}a = (a(ba)^{∗}b + 1)a
= a((ba)^{∗}ba + 1)
= a(ba)^{∗},

by (6) and (5). To prove (8), note that by (3), (6) and (7),

(a + b)(a^{∗}b)^{∗}a^{∗} + 1 = a(a^{∗}b)^{∗}a^{∗} + b(a^{∗}b)^{∗}a^{∗} + 1
= aa^{∗}(ba^{∗})^{∗} + (ba^{∗})^{∗}
= (aa^{∗} + 1)(ba^{∗})^{∗}
= a^{∗}(ba^{∗})^{∗}
= (a^{∗}b)^{∗}a^{∗}.

Thus,

(a + b)^{∗} ≤ (a^{∗}b)^{∗}a^{∗}.  (13)

For the reverse inequation, assume that

(a + b)x + 1 = x  (14)

for some x. Then,

ax + bx + 1 = x,

so that

a^{∗}(bx + 1) = a^{∗}bx + a^{∗} ≤ x,

by the weak fixed point induction rule. Now, by the fixed point induction rule,

(a^{∗}b)^{∗}a^{∗} ≤ x.

Thus, taking x = (a + b)^{∗} in (14), we have

(a^{∗}b)^{∗}a^{∗} ≤ (a + b)^{∗}.  (15)

Equation (8) now follows from (13) and (15). □

The ^{∗}- semirings satisfying (6) and (8) have a distinguishing name.

Definition 2.8 [4, 6, 12] A Conway semiring is a ^{∗}-semiring satisfying the sum star equation (8) and the product star equation (6). A morphism of Conway semirings is a ^{∗}-semiring morphism.

Note that the fixed point equation and all of the equations appearing in Proposition 2.7 hold in any Conway semiring. By the fixed point equation, also 0^{∗} = 1 in any Conway semiring. Only the weak fixed point induction rule was used in Proposition 2.7 to prove (6). This observation gives rise to the following definition.

Definition 2.9 A weak inductive ^{∗}-semiring is an ordered semiring which is also a ^{∗}-semiring and satisfies the fixed point equation (3), the sum star equation (8) and the weak fixed point induction rule. A morphism of weak inductive ^{∗}-semirings is an ordered semiring morphism which preserves the star operation.

Clearly, every inductive ^{∗}-semiring is a weak inductive ^{∗}-semiring.

Corollary 2.10 Any weak inductive ^{∗}-semiring is a Conway semiring. Any inductive ^{∗}-semiring is a Conway semiring with a monotonic star operation.

Proposition 2.11 The inequations

0 ≤ a
a ≤ a + b
∑_{i=0}^{n} a_{i} ≤ a^{∗}, n ≥ 0

hold in any weak inductive ^{∗}-semiring S.

Proof. Since

1 · a + 0 = a,

we have 0 = 1^{∗} · 0 ≤ a. Since the sum operation is monotonic, also

a = a + 0
≤ a + b,

for all a, b ∈ S. Since by repeated applications of the fixed point equation,

a^{∗} = a^{n+1}a^{∗} + ∑_{i=0}^{n} a^{i},

we have ∑_{i=0}^{n} a^{i} ≤ a^{∗}, for all n ≥ 0. □

Remark 2.12 Inductive ^{∗}-semirings are ordered algebraic structures in the usual universal algebraic sense, see [3, 23]. In fact, since inductive ^{∗}-semirings are defined by (in)equations and implications, they form a quasi-variety. Hence, the class of inductive ^{∗}-semirings is closed under the constructions of direct products, substructures, direct and inverse limits, etc. (When S and S′ are inductive ^{∗}-semirings, we say that S is a substructure of S′ if S ⊆ S′ and the operations and the partial order on S are the restrictions of the corresponding operations and the partial order on S′.) Similar closure properties are enjoyed by weak inductive ^{∗}-semirings.

3 Sum-ordered semirings

In any semiring S, we may define a relation ⪯ by a ⪯ b iff there is some c with a + c = b. This relation is a preorder preserved by the semiring operations.

Definition 3.1 An ordered semiring S is called sum-ordered [20] if the partial order ≤ given on S coincides with the above relation ⪯, i.e., when

a ≤ b ⇔ ∃c a + c = b,

for all a, b ∈ S.

Note that 0 ≤ a and hence a ≤ a+b hold for all a, b in a sum-ordered semiring S, so that 0 is the least element of S. Each of the continuous semirings P_{M}, L_{A}, R_{A}, Rel_{A}, N_{∞} and k is sum-ordered.

Proposition 3.2 Suppose that S, partially ordered by the relation ≤, is an ordered semiring. Then S, equipped with the relation ⪯, is a sum-ordered semiring iff 0 is least. Moreover, in this case, ⪯ is included in ≤.

Proof. We only need to show that when 0 is least in S, then ⪯ is antisymmetric. But suppose that a ⪯ b and b ⪯ a. Then there exists some c with a + c = b. Thus, since 0 ≤ c and the sum operation is monotonic, we have a ≤ a + c = b. In the same way, b ≤ a. But ≤ is antisymmetric, so that a = b. □

Thus, by Proposition 2.11, if S is a (weak) inductive ^{∗}-semiring, then S, equipped with the relation ⪯ is a sum-ordered semiring.

Proposition 3.3 Suppose that S and S′ are ordered semirings and h is a semiring morphism S → S′. If S is sum-ordered and 0 is the least element of S′, then h is an ordered semiring morphism.

Proof. If a ≤ b in S, then there is some c with a + c = b. Thus, h(a) + h(c) = h(b), so that h(a) ⪯ h(b) in S′. But since 0 is the least element of S′, we have h(a) ≤ h(b). □

Proposition 3.4 Suppose that S is a ^{∗}-semiring which is a sum-ordered semiring. Then S is an inductive ^{∗}-semiring iff S satisfies the fixed point (in)equation and the weak fixed point induction rule. Thus, S is an inductive ∗-semiring iff S is a weak inductive ^{∗}-semiring.

Proof. We only need to show that if S satisfies the weak fixed point induction rule, then S also satisfies the fixed point induction rule. So suppose that ax + b ≤ x, for some a, b, x ∈ S. Then, since S is sum-ordered, there exists c ∈ S with ax + (b + c) = x. Hence, a^{∗}b + a^{∗}c = a^{∗}(b + c) ≤ x, so that a^{∗}b ≤ x.

□

We end this section by presenting an inductive ^{∗}-semiring S which, equipped with the sum-order, is not inductive. Let N denote the natural numbers. Suppose that M = N ∪ {a, b, c} is equipped with the the usual + operation on N, and

x + y = \{ \begin{matrix}a & if x ∈ N and y = a, or x = a and y ∈ N \\ b & if x ∈ N and y = b, or x = b and y ∈ N \\ c & otherwise. \end{matrix}

Let ≤ be the usual partial order on N, and let n ≤ a ≤ b ≤ c, all n ∈ N, and of course a ≤ a, b ≤ b and c ≤ c. Let S denote the semiring of all strict additive and monotonic functions on M as defined in Example 2.6. As shown above, S, equipped with the pointwise partial order can be turned into an inductive ∗-semiring. But the same semiring S, equipped with the sum-order, has no appropriate star operation. Indeed, when f is the function f(n) = n + 1 and f(x) = x for x ∉ N, then, with respect to the sum-order, there is no least x with f(x) = x.

Problem 3.1 Does there exist a weak inductive ^{∗}-semiring with a nonmonotonic star operation? Does there exist a weak inductive ^{∗}-semiring with a monotonic star operation which is not an inductive ^{∗}-semiring?

4 Idempotent inductive ^{∗}-semirings

A semiring S is called idempotent if 1 + 1 = 1 holds in S. It then follows that a + a = a, for all a ∈ S.

Proposition 4.1 Suppose that S is an idempotent ordered semiring. The following conditions are equivalent.

1. 0 is the least element of S, i.e., 0 ≤ a holds for all a in S.

2. For all a, b ∈ S, a ≤ a + b.

3. For all a, b ∈ S, a ≤ b iff a + b = b.

4. S is sum-ordered.

Proof. It is clear that the first condition implies the second and that the last condition implies the first. In fact, the first two conditions are equivalent in any ordered semiring. Suppose that the second condition holds. If a ≤ b then a + b ≤ b + b = b ≤ a + b, so that a + b = b. Conversely, if a + b = b, then a ≤ b, since a ≤ a + b. Thus the second condition implies the third. Finally, if the third condition holds then a ≤ b iff there is some c with a + c = b. It follows that S is sum-ordered. □

Corollary 4.2 Suppose that S and S′ are ordered semirings such that S is idempotent and 0 is least in both S and S′. Then any semiring morphism S → S′ is an ordered semiring morphism.

Corollary 4.3 An ordered idempotent semiring S equipped with a star operation is an inductive ^{∗}-semiring iff S satisfies the fixed point (in)equation and the weak fixed point induction rule. Hence S is an inductive semiring iff S is a weak inductive ^{∗}-semiring.

Proposition 4.4 Any idempotent inductive ^{∗}-semiring S satisfies the equation

1^{∗} = 1.

Proof. Since 1 + 1 = 1, 1^{∗} ≤ 1. On the other hand, 1 ≤ 1^{∗} + 1 = 1^{∗}. □

5 Matrices

If S is a Conway semiring, then for each n ≥ 0, the semiring S^{n×n} of all n × n matrices over S may be turned into a Conway semiring. In fact, our definition of the star operation on S^{n×n} applies to any ^{∗}-semiring.

Definition 5.1 Suppose that S is a ^{∗}-semiring. We define the star M^{∗} of an n × n matrix M in S^{n×n} by induction on n.

• If n = 0, M^{∗} is the unique 0 × 0 matrix.

• If n = 1, M = [a], for some a ∈ S. We define M^{∗} = [a^{∗}].

• If n > 1, write

M = [ \begin{matrix}a & b \\ c & d \end{matrix} ]

where a is (n − 1) × (n − 1) and d is 1 × 1. We define

M^{∗} = [ \begin{matrix}α & β \\ γ & δ \end{matrix} ]  (16)

where

α = (a + bd^{∗}c)^{∗}  (17)
β = αbd^{∗}  (18)
γ = δca^{∗}  (19)
δ = (d + ca^{∗}b)^{∗}.  (20)

The following result is implicit in [7].

Theorem 5.2 [7] If S is a Conway semiring, then so is S^{n×n}, for any n ≥ 0. Moreover, for each matrix M ∈ S^{n×n}, and for each way of writing M as

M = [ \begin{matrix}a & b \\ c & d \end{matrix} ]

where a and d are square matrices, it holds that

M^{∗} = [ \begin{matrix}α & β \\ γ & δ \end{matrix} ]

where α, β, γ and δ are given as above.

In fact, the collection of all n×m matrices, for n, m ≥ 0 form a Conway theory [6]. (In [4, 6], Theorem 5.2 is derived from a general result that holds for all Conway theories.) We now give a characterization of Conway semirings.

Theorem 5.3 The following conditions are equivalent for a ^{∗}-semiring S.

1. S is a Conway semiring.

2. S^{2×2} satisfies the fixed point equation.

3. For each n ≥ 0, S^{n×n} satisfies the fixed point equation.

Proof. It is clear that the last condition implies the second. Moreover, by the previous theorem, the first condition implies (the second and) the third. Thus, we are left to show that the second condition implies the first. So suppose that the fixed point equation holds in S^{2×2}, i.e.,

[ \begin{matrix}a & b \\ c & d \end{matrix} ] [ \begin{matrix}a & b \\ c & d \end{matrix} ]^{∗} + [ \begin{matrix}1 & 0 \\ 0 & 1 \end{matrix} ] = [ \begin{matrix}a & b \\ c & d \end{matrix} ]^{∗}

for all a, b, c, d ∈ S. Thus, using the definition of the star operation,

a(a + bd^{∗}c)^{∗} + b(d + ca^{∗}b)^{∗}ca^{∗} + 1 = (a + bd^{∗}c)^{∗}  (21)
a(a + bd^{∗}c)^{∗}bd^{∗} + b(d + ca^{∗}b)^{∗} = (a + bd^{∗}c)^{∗}bd^{∗}.  (22)

Letting b = 0 (and c = d = 0, say) in (21) we obtain aa^{∗} + 1 = a^{∗}, so that the fixed point equation holds in S. In particular, 0^{∗} = 1. Thus, letting a = d = 0, (21) gives b(cb)^{∗}c + 1 = (bc)^{∗}. Also, letting a = 0 and b = 1,

(22) gives (d + c)^{∗} = (d^{∗}c)^{∗}d^{∗}. Hence, both the product star and sum star equations hold in S proving that S is a Conway semiring. □

The above argument actually gives the following results:

Corollary 5.4 A ^{∗}-semiring S is a Conway semiring iff for some n > 1, S^{n×n} satisfies the fixed point equation.

Corollary 5.5 A ^{∗}-semiring S is a Conway semiring iff the fixed point equation holds in S^{2×2} for all lower or upper triangular matrices.

When S is a partially ordered semiring, then, equipped with the pointwise order, so is S^{n×n}, for any integer n ≥ 0.

Theorem 5.6 Suppose that S is an inductive ^{∗}-semiring. Then for each n ≥ 0, S^{n×n} is also an inductive ^{∗}-semiring.

Proof. We have already proved that any inductive semiring is a Conway semiring. Hence, the fixed point equation holds in S^{n×n}, for all n ≥ 0. As for the fixed point induction rule, we prove by induction on n that if a ∈ S^{n×n}, b, ξ ∈ S^{n×m} with aξ + b ≤ ξ, then a^{∗}b ≤ ξ. Our argument is essentially the same as the proof of Theorem 4 in Chapter 3 of Conway [7]. The case n = 0 is trivial and the case n = 1 holds by assumption. Supposing n > 1, write

a = [ \begin{matrix}a_{1} & a_{2} \\ a_{3} & a_{4} \end{matrix} ]
b = [ \begin{matrix}b_{1} \\ b_{2} \end{matrix} ]
ξ = [ \begin{matrix}ξ_{1} \\ ξ_{2} \end{matrix} ]

where a_{1} is (n − 1) × (n − 1), b_{1} and ξ_{1} are (n − 1) × m, etc. Since aξ + b ≤ b, we have

a_{1}ξ_{1} + a_{2}ξ_{2} + b_{1} ≤ ξ_{1}
a_{3}ξ_{1} + a_{4}ξ_{2} + b_{2} ≤ ξ_{2}.

By the induction assumption,

a_{1}^{∗}(a_{2}ξ_{2} + b_{1}) ≤ ξ_{1},

so that

a_{3}a_{1}^{∗}a_{2}ξ_{2} + a_{3}a_{1}^{∗}b_{1} ≤ a_{3}ξ_{1}

and

(a_{4} + a_{3}a_{1}^{∗}a_{2})ξ_{2} + (a_{3}a_{1}^{∗}b_{1} + b_{2}) ≤ ξ_{2}.

Thus,

(a_{4} + a_{3}a_{1}^{∗}a_{2})^{∗}(a_{3}a_{1}^{∗}b_{1} + b_{2}) ≤ ξ_{2},  (23)

since the fixed point induction rule holds in S. In the same way,

(a_{1} + a_{2}a_{4}^{∗}a_{3})^{∗}(a_{2}a_{4}^{∗}b_{2} + b_{1}) ≤ ξ_{1}.  (24)

But

a^{∗} = [ \begin{matrix}(a_{1} + a_{2}a_{4}^{∗}a_{3})^{∗} & (a_{1} + a_{2}a_{4}^{∗}a_{3})^{∗}a_{2}a_{4}^{∗} \\ (a_{4} + a_{3}a_{1}^{∗}a_{2})^{∗}a_{3}a_{1}^{∗} & (a_{4} + a_{3}a_{1}^{∗}a_{2})^{∗} \end{matrix} ]

so that (23) and (24) amount to a^{∗}b ≤ ξ. □

Remark 5.7 Theorem 5.6 may be viewed as an instance of the well-known rule found independently by Bekić [1] and de Bakker and Scott [9] to compute “simultaneous least pre-fixed points” of continuous functions.

Problem 5.1 Suppose that S is a weak inductive ^{∗}-semiring. Are the matrix semirings S^{n×n} weak inductive semirings?

6 Iteration semirings

Iteration semirings were originally defined in [4]. Here we recall the definition given in [10]. Suppose that G is a finite group of order n, say G = {g_{1}, …, g_{n}}. For each g_{i}, let a_{g_{i}} be a variable associated with g_{i}. The n × n matrix M_{G} is defined by

(M_{G})_{i,j} = a_{g_{i}^{−1}g_{j}}, i, j ∈ [n].

Thus, each row of M_{G} is a permutation of the first row, and similarly for columns. In particular, for each i ∈ [n], let π_{g_{i}} denote the n × n permutation matrix corresponding to the permutation of G induced by left multiplication with g_{i}. Thus, for any r, s ∈ [n], (π_{g_{i}})_{r,s} = 1 iff g_{s} = g_{i}g_{r}.

Lemma 6.1 [18]

π_{g_{i}}M_{G}π_{g_{i}}^{−1} = M_{G},

for all i ∈ [n].

Let α_{n} denote the 1 × n matrix whose first component is 1 and whose other components are 0, and let δ_{n} denote the n × 1 matrix whose components are all 1.

Definition 6.2 Conway [7] The group-equation associated with G is

α_{n}M_{G}^{∗}δ_{n} = (a_{g_{1}} + … + a_{g_{n}})^{∗}.

We will use the group-equations only in Conway semirings. In such semirings, it is irrelevant in what order the elements of the group G are listed. This follows from the following fact.

Lemma 6.3 The permutation equation holds in all Conway semirings S:

(πMπ^{−1})^{∗} = πM^{∗}π^{−1},

for all π, M ∈ S^{n×n} such that π is a permutation matrix with inverse π^{−1}.

Proof. Since S^{n×n} is a Conway semiring, by the product star and dual fixed point equations we have

(πMπ^{−1})^{∗} = π(Mπ^{−1}π)^{∗}Mπ^{−1} + 1
= πM^{∗}Mπ^{−1} + 1
= π(M^{∗}M + 1)π^{−1}
= πM^{∗}π^{−1}.

See also [7, 4]. □

Definition 6.4 [4, 6] An iteration semiring is a Conway semiring satisfying the group-equations for all finite groups. A morphism of iteration semirings is a ^{∗}-semiring morphism.

Theorem 6.5 Any inductive ^{∗}-semiring is an iteration semiring.

Proof. Suppose that S is an inductive ^{∗}-semiring. By Corollary 2.10, S is a Conway semiring. Thus we only need to establish the group-equations. So let G = {g_{1}, …, g_{n}} denote a group of order n, and let a_{g_{1}}, …, a_{g_{n}} be some elements of S associated with the group elements. Define a = a_{g_{1}} + … + a_{g_{n}}. Since each row of M_{G} is a permutation of the a_{g_{i}}, we have that

M_{G}δ_{n} = δ_{n}a,  (25)

i.e., each row of M_{G} sums up to a. Thus,

M_{G}(δ_{n}a^{∗}) + δ_{n} = δ_{n}(aa^{∗} + 1)
= δ_{n}aa^{∗}
= δ_{n}a^{∗},

so that M_{G}^{∗}δ_{n} ≤ δ_{n}a^{∗} and

α_{n}M_{G}^{∗}δ_{n} ≤ a^{∗}

by the weak fixed point induction rule. As for the reverse inequality, note that each row of M_{G}^{∗} is a permutation of the first row. This follows since for each i ∈ [n], M_{G} = π_{g_{i}}M_{G}π_{g_{i}}^{−1}, by Lemma 6.1. Thus, M_{G}^{∗} = π_{g_{i}}M_{G}^{∗}π_{g_{i}}^{−1}, by the permutation equation. Thus,

M_{G}^{∗}δ_{n} = δ_{n}α_{n}M_{G}^{∗}δ_{n}.  (26)

Thus, by (25) and (26),

a(α_{n}M_{G}^{∗}δ_{n}) + 1 = α_{n}δ_{n}aα_{n}M_{G}^{∗}δ_{n} + α_{n}δ_{n}
= α_{n}M_{G}δ_{n}α_{n}M_{G}^{∗}δ_{n} + α_{n}δ_{n}
= α_{n}M_{G}M_{G}^{∗}δ_{n} + α_{n}δ_{n}
= α_{n}(M_{G}M_{G}^{∗} + 1)δ_{n}
= α_{n}M_{G}^{∗}δ_{n}.

The weak fixed point induction rule gives

a^{∗} ≤ α_{n}M_{G}^{∗}δ_{n}.
□

Remark 6.6 It is shown in [18, 10] that whenever S is an iteration semiring, then so is S^{n×n}, for each n ≥ 0. In fact, the algebraic theory of matrices over an iteration semiring is an iteration theory, see [10].

7 Duality

The opposite or dual S^{op} of a ^{∗}-semiring S is equipped with the same operations and constants as S except for multiplication, which is the reverse of the multiplication in S. When S is ordered, so is S^{op} equipped with the same partial order. Note that (S^{op})^{op} = S.

Proposition 7.1 A ^{∗}-semiring S is a Conway semiring iff S^{op} is a Conway semiring.

Proof. Suppose that S is a Conway semiring. It is clear that the product star equation (6) holds in S^{op}. As for the sum star equation, note that in S,

(a + b)^{∗} = (a^{∗}b)^{∗}a^{∗}
= a^{∗}(ba^{∗})^{∗},

by the product star equation. It follows that the sum star equation holds in S^{op}. □

When M is an n × m matrix over a semiring S, define M^{op} to be the m × n matrix with M_{ij}^{op} = M_{ji}, for all i ∈ [m] and j ∈ [n]. Note that when S is a ∗-semiring, then both S^{n×n} and (S^{op})^{n×n} are ^{∗}-semirings, for any n ≥ 0.

Theorem 7.2 Suppose that S is a Conway semiring. Then the Conway semirings (S^{n×n})^{op} and (S^{op})^{n×n} are isomorphic.

Proof. It is clear that the map M ↦ M^{op} preserves the sum operation and the constants 0 and 1. To complete the proof that this map is the required isomorphism, we need to show that

(MN)^{op} = N^{op} ∘ M^{op}  (27)
(M^{∗})^{op} = (M^{op})^{⊗}  (28)

hold for all M, N ∈ S^{n×n}, where ∘ and ^{⊗} denote the product and star operations in (S^{op})^{n×n}. We leave the verification of (27) to the reader. The proof of (28) is by induction on n. The cases n = 0, 1 are clear. When n > 1, let us partition M into four block matrices

M = [ \begin{matrix}a & b \\ c & d \end{matrix} ]

as above. Then

M^{op} = [ \begin{matrix}a^{op} & c^{op} \\ b^{op} & d^{op} \end{matrix} ]

Recall that

M^{∗} = [ \begin{matrix}α & β \\ γ & δ \end{matrix} ]

where α, β, γ, δ are defined as in (17) – (20). Let

(M^{op})^{⊗} = [ \begin{matrix}α′ & γ′ \\ β′ & δ′ \end{matrix} ]

We need to prove that α^{op} = α′, β^{op} = β′, etc. But, by using the induction assumption,

α^{op} = ((a + bd^{∗}c)^{∗})^{op}
= ((a + bd^{∗}c)^{op})^{⊗}
= (a^{op} + c^{op} ∘ (d^{∗})^{op} ∘ b^{op})^{⊗}
= (a^{op} + c^{op} ∘ (d^{op})^{⊗} ∘ b^{op})^{⊗}
= α′.

Also, using the Conway semiring equation

u^{∗}z(x + yu^{∗}z)^{∗} = u^{∗}z(x^{∗}yu^{∗}z)^{∗}x^{∗}
= (u^{∗}zx^{∗}y)^{∗}u^{∗}zx^{∗}
= (u + zx^{∗}y)^{∗}zx^{∗},

it follows that

β^{op} = (αbd^{∗})^{op}
= (d^{∗})^{op} ∘ b^{op} ∘ α^{op}
= (d^{⊗})^{op} ∘ b^{op} ∘ α′
= (d^{⊗})^{op} ∘ b^{op} ∘ (a^{op} + c^{op} ∘ (d^{op})^{⊗} ∘ b^{op})^{⊗}
= (d + b^{op} ∘ (a^{op})^{⊗} ∘ c^{op})^{⊗} ∘ b^{op} ∘ (a^{op})^{⊗}
= β′.

The proofs of the other equations are similar. Note that the Conway identities (8) and (6) were needed only in the proof of (33). □

The dual t^{op} of a ^{∗}-semiring term t is defined by induction on the structure of t.

• If t is a variable or one of the constants 0, 1, then t^{op} = t.

• If t = t_{1} + t_{2} then t^{op} = t_{1}^{op} + t_{2}^{op}.

• If t = t_{1}t_{2} then t^{op} = t_{2}^{op}t_{1}^{op}.

• If t = t_{1}^{∗} then t^{op} = (t_{1}^{op})^{∗}.

Thus, (t^{op})^{op} = t. The dual of an equation t_{1} = t_{2} is the equation t_{1}^{op} = t_{2}^{op}, and the dual of an implication t_{1} = s_{1} ∧ … ∧ t_{n} = s_{n} ⇒ t = s is t_{1}^{op} = s_{1}^{op} ∧ … ∧ t_{n}^{op} = s_{n}^{op} ⇒ t^{op} = s^{op}. The dual of an inequation t ≤ s or implication t_{1} ≤ s_{1} ∧ … ∧ t_{n} ≤ s_{n} ⇒ t ≤ s is defined in the same way. Note that the dual fixed point equation (5) is indeed the dual of the fixed point equation (3), and the dual fixed point induction rule

xa + b ≤ x ⇒ ba^{∗} ≤ x  (29)

is the dual of (2). Moreover, the product star equation is self dual in that its dual is equivalent to the product star equation. The dual of the sum star equation is the equation (a + b)^{∗} = a^{∗}(ba^{∗})^{∗} mentioned above.

Proposition 7.3 The dual of an (in)equation or implication holds in a ^{∗}- semiring S iff it holds S^{op}.

Corollary 7.4 An equation (or implication) holds in all Conway semirings iff so does its dual.

Below we will consider term matrices. The sum and product operations on term matrices are defined in the usual way. The star of a term matrix is defined by the matrix formula (16). When M is an n × p term matrix, we define M^{op} to be the p × n matrix such that (M^{op})_{ij} = (M_{ji})^{op}, for all i ∈ [p] and j ∈ [n]. If M and M′ are n × p term matrices and S is a ^{∗}-semiring, we say that the equation M = M′ holds in S if each equation M_{ij} = M′_{ij} does, for any i ∈ [n], j ∈ [p]. The dual of the equation M = M′ is the equation M^{op} = M^{′op}. Clearly, any ^{∗}-semiring satisfies the equations

(M + N)^{op} = M^{op} + N^{op}  (30)
(MN)^{op} = N^{op}M^{op}  (31)
(M^{op})^{op} = M  (32)

for any term matrices M, N of appropriate size. By Theorem 7.2, we also have

Corollary 7.5 Any Conway semiring satisfies the equations

(M^{∗})^{op} = (M^{op})^{∗},  (33)

for any term matrices M, N of appropriate size.

Recall that the group-equation associated with a finite group G = {g_{1}, …, g_{n}} of order n is the equation

α_{n} · M_{G}^{∗} · δ_{n} = (a_{g_{1}} + … + a_{g_{n}})^{∗},

where (M_{G})_{ij} = a_{g_{i}^{−1}g_{j}}, for all i, j ∈ [n], α_{n} is the n-dimensional row vector whose first component is 1 and whose other components are 0, and δ_{n} is the n-dimensional column vector whose components are all 1. Below, without loss of generality we will assume that g_{1} is the unit of G.

Lemma 7.6 In Conway semirings, the group-equation associated with a finite group G is equivalent to the equation

δ_{n}^{op} · M_{G}^{∗} · α_{n}^{op} = (a_{g_{1}} + … + a_{g_{n}})^{∗}.

Proof. Note that the meaning of this equation is that the sum of the entries of the first column of M_{G}^{∗} is (a_{g_{1}} + … + a_{g_{n}})^{∗}. By Lemma 6.1 and the permutation equation, the equation

π_{g_{i}} · M_{G}^{∗} · π_{g_{i}}^{op} = M_{G}^{∗}

holds in all Conway semirings for each i ∈ [n]. Thus, if we let t_{g_{1}}, …, t_{g_{n}} denote the terms in the first row of M_{G}^{∗}, then under the Conway semiring equations, for each i ∈ [n] the ith row is t_{g_{i}^{−1}g_{1}}, …, t_{g_{i}^{−1}g_{n}}. Hence, under the Conway semiring equations, there is a bijective correspondence between the entries of the first row and the entries of the first column of M_{G}^{∗}. □

The matrix N_{G} = M_{G}(a_{g_{1}^{−1}}, …, a_{g_{n}^{−1}}) is obtained form M_{G} by substituting a_{g_{i}^{−1}} for a_{g_{i}}, for all i ∈ [n].

Corollary 7.7 In Conway semirings, the equation associated with a finite group G of order n is equivalent to the equation

δ_{n}^{op} · N_{G}^{∗} · α_{n}^{op} = (a_{g_{1}} + … + a_{g_{n}})^{∗}.

Note that for each i, j ∈ [n], the (i, j)th entry of N_{G} is a_{g_{j}^{−1}g_{i}}. Thus,

Lemma 7.8 The matrices M_{G}^{op} and N_{G} are equal.

Thus, by Corollary 7.5, we have

Lemma 7.9 The equation

(M_{G}^{∗})^{op} = N_{G}^{∗}

holds in all Conway semirings.

Proposition 7.10 If the group-equation associated with a finite group G of order n holds in a Conway semiring S, then so does its dual.

Proof. Using the above notation, the dual of the equation associated with G is

δ_{n}^{op} · (M_{G}^{∗})^{op} · α_{n}^{op} = (a_{g_{1}} + … + a_{g_{n}})^{∗}.

By Lemma 7.9, this equation holds in S iff the equation

δ_{n}^{op} · N_{G}^{∗} · α_{n}^{op} = (a_{g_{1}} + … + a_{g_{n}})^{∗}

holds. But by Corollary 7.7, in Conway semirings this equation is equivalent to the group-equation associated with G. □

Corollary 7.11 Any iteration semiring satisfies the dual of any group-- equation. A ^{∗}-semiring is an iteration semiring iff its dual is an iteration semiring.

Corollary 7.12 An equation holds in all iteration semirings iff so does its dual.

We have seen that the dual of a Conway or iteration semiring is also a Conway or iteration semiring. As pointed out by Kozen, the corresponding fact does not hold for inductive ^{∗}-semirings.

Proposition 7.13 Kozen [17] There exists an idempotent inductive^{∗}-semiring S such that S^{op} is not an inductive ^{∗}-semiring.

In fact, as shown by Kozen, when A is an infinite set and M is P (A), the power set of A equipped with the union operation and the subset order, then the dual of the inductive ^{∗}-semiring F_{M} constructed in Example 2.6 is not an inductive ^{∗}-semiring. Such a semiring cannot be embedded in any continuous ∗-semiring.

Definition 7.14 A symmetric inductive^{∗}-semiring is an inductive^{∗}-semiring which satisfies the dual fixed point induction rule (29). A morphism of symmetric inductive ^{∗}-semirings is an inductive ^{∗}-semiring morphism.

Proposition 7.15 An inductive ^{∗}-semiring S is a symmetric inductive ^{∗}- semiring iff S^{op} is also an inductive ^{∗}-semiring.

Proof. By Proposition 2.7, the dual of the fixed point equation (5) holds in any inductive ^{∗}-semiring. □

Proposition 7.16 Any continuous ^{∗}-semiring is a symmetric inductive ^{∗}- semiring.

Proof. Is S is a continuous ^{∗}-semiring, then so is S^{op}. □

Proposition 7.17 If S is a symmetric inductive semiring, then so is S^{n×n}, for each n ≥ 0.

Proof. By Theorem 5.6, both S^{n×n} and (S^{op})^{n×n} are inductive ^{∗}-semirings. But by Theorem 7.2, (S^{op})^{n×n} is isomorphic to (S^{n×n})^{op}. □

We end this section with a definition.

Definition 7.18 A Kozen semiring is an idempotent symmetric inductive ^{∗}- semiring. A morphism of Kozen semirings is an inductive semiring morphism.

Kozen semirings are called Kleene algebras in [16]. Examples of Kozen semirings are the semirings ℙ_{M}, 𝕃_{A}, ℝ_{A}, ℂ𝔽_{A}, ℝ⋖_{A} and the Boolean semiring 𝔹. In fact, any idempotent continuous ^{∗}-semiring is a Kozen semiring.

8 Power series

Suppose that S is a semiring and A is a set. Recall that a formal power series over A with coefficients in S is a function

r : A^{∗} → S,

usually denoted

r = ∑_{u∈A^{∗}}(r, u)u,

where (r, u) is just r(u), the value of function r on the word u. Here, A^{∗} denotes the free monoid of all words over A including the empty word ϵ. Equipped with the operations of pointwise sum and Cauchy product, power series form a semiring S⟨ ⟨A^{∗}⟩ ⟩. The neutral elements are the series 0 whose coefficients are all zero, and the series 1 such that the coefficient of the empty word ϵ is 1 and the other coefficients are 0. (In a similar fashion, every element of S can be identified with a power series.) When S is partially ordered, we may turn S⟨ ⟨A^{∗}⟩ ⟩ into a partially ordered semiring by the pointwise order.

Definition 8.1 Suppose that S is a ^{∗}-semiring. For each s ∈ S⟨ ⟨A^{∗}⟩ ⟩, we define

(s^{∗}, ϵ) = (s, ϵ)^{∗}
(s^{∗}, u) = (s, ϵ)^{∗} ∑_{vw=u, v≠ϵ}(s, v)(s^{∗}, w),

for all u ∈ A^{∗}, u ≠ ϵ.

This defines a star operation on S⟨ ⟨A^{∗}⟩ ⟩.

Remark 8.2 It is easy to see by induction on the length of the word u that

(s^{∗}, u) = ∑_{u_{1}...u_{n}=u, u_{i}≠ϵ}(s, ϵ)^{∗}(s, u_{1})(s, ϵ)^{∗} … (s, u_{n})(s, ϵ)^{∗}.

It then follows that

(s, u^{∗}) = ( ∑_{wv=u, v≠ϵ}(s^{∗}, w)(s, v))(s, ϵ)^{∗},

for all u ≠ ϵ.

Theorem 8.3 [4, 6] If S is a Conway semiring, or an iteration semiring, then so is S⟨ ⟨A^{∗}⟩ ⟩.

Theorem 8.4 If S is an inductive ^{∗}-semiring, then so is S⟨ ⟨A^{∗}⟩ ⟩.

Proof. First we show that the fixed point equation holds, i.e.,

(ss^{∗} + 1, u) = (s^{∗}, u),

for all s ∈ S⟨ ⟨A^{∗}⟩ ⟩ and u ∈ A^{∗}. When u = ϵ, we have

(ss^{∗} + 1, ϵ) = (s, ϵ)(s^{∗}, ϵ) + 1
= (s, ϵ)(s, ϵ)^{∗} + 1
= (s, ϵ)^{∗}
= (s^{∗}, ϵ),

since the fixed point equation holds in S. Suppose now that u ≠ ϵ. Then, again using the fixed point equation in S,

(ss^{∗} + 1, u) = (s, ϵ)(s^{∗}, u) + ∑_{vw=u, v≠ϵ}(s, v)(s^{∗}, w)
= (s, ϵ)[(s, ϵ)^{∗} ∑_{vw=u, v≠ϵ}(s, v)(s^{∗}, w)] + ∑_{vw=u, v≠ϵ}(s, v)(s^{∗}, w)
= ((s, ϵ)(s, ϵ)^{∗} + 1) ∑_{vw=u, v≠ϵ}(s, v)(s^{∗}, w)
= (s, ϵ)^{∗} ∑_{vw=u, v≠ϵ}(s, v)(s^{∗}, w)
= (s^{∗}, u).

We now prove that the fixed point induction rule holds in S⟨ ⟨A^{∗}⟩ ⟩. So suppose that r, s, ξ ∈ S⟨ ⟨A^{∗}⟩ ⟩ such that

rξ + s ≤ ξ.  (34)

We must prove that r^{∗}s ≤ ξ, i.e., that (r^{∗}s, u) ≤ (ξ, u), for all words u ∈ A^{∗}. When u = ϵ, (34) gives

(r, ϵ)(ξ, ϵ) + (s, ϵ) ≤ (ξ, ϵ).

Since the fixed point induction rule holds in S, we have (r^{∗}s, ϵ) = (r, ϵ)^{∗}(s, ϵ) ≤ (ξ, ϵ). Assume that u ≠ ϵ. Then by (34),

(r, ϵ)(ξ, u) + ∑_{vw=u, v≠ϵ}(r, v)(ξ, w) + (s, u) ≤ (ξ, u).  (35)

By induction,

(r^{∗}s, w) ≤ (ξ, w),  (36)

for all w with |w| < |u|. By (35) and (36),

(r, ϵ)(ξ, u) + ∑_{vw=u, v≠ϵ}(r, v)(r^{∗}s, w) + (s, u) ≤ (ξ, u),

so that

(r, ϵ)^{∗}( ∑_{vw=u, v≠ϵ}(r, v)(r^{∗}s, w) + (s, u)) ≤ (ξ, u),

by the fixed point induction rule. Thus, by Lemma 8.5 below, (r^{∗}s, u) ≤ (ξ, u).

□

Lemma 8.5 For all u ∈ A^{∗},

(r, ϵ)^{∗}( ∑_{vw=u, v≠ϵ}(r, v)(r^{∗}s, w) + (s, u)) = (r^{∗}s, u).

Proof. Let us denote by suf(u) the set of all suffixes of u, i.e., the set of all z ∈ A^{∗} such that z′z = u for some uniquely defined z′. Below we will denote z′ by u/z. Then,

(r, ϵ)^{∗}( ∑_{vw=u, v≠ϵ}(r, v)(r^{∗}s, w) + (s, u))

= (r, ϵ)^{∗}( ∑_{vwz=u, v≠ϵ}(r, v)(r^{∗}, w)(s, z) + (s, u))
= ∑_{z∈suf(u),z≠u}(r, ϵ)^{∗}( ∑_{vw=u/z, v≠ϵ}(r, v)(r^{∗}, w)(s, z)) + (r, ϵ)^{∗}(s, u)
= ∑_{z∈suf(u),z≠u}(r^{∗}, u/z)(s, z) + (r^{∗}, ϵ)(s, u)
= ∑_{z∈suf(u)}(r^{∗}, u/z)(s, z)
= ∑_{vz=u}(r^{∗}, v)(s, z)
= (r^{∗}s, u).
□

Remark 8.6 A certain converse of Theorem 8.4 holds also. Suppose that S is an inductive ^{∗}-semiring. Then S⟨ ⟨A^{∗}⟩ ⟩ is an ordered semiring. We have proved that each linear function ξ ↦ rξ + s over S⟨ ⟨A^{∗}⟩ ⟩ has a least pre-fixed point solution, viz. s^{∗}r. Thus, if S⟨ ⟨A^{∗}⟩ ⟩ is turned into an inductive ^{∗}-semiring, by any definition of srtar, then that star operation is the same as the one given in Definition 8.1.

Problem 8.1 Does Theorem 8.4 hold for weak inductive ^{∗}-semirings?

We now consider power series with coefficients in the dual semiring.

Proposition 8.7 Suppose that S is a ^{∗}-semiring and A is a set. Then the ∗-semirings (S⟨ ⟨A^{∗}⟩ ⟩)^{op} and S^{op}⟨ ⟨A^{∗}⟩ ⟩ are isomorphic.

Proof. For each s ∈ S⟨ ⟨A^{∗}⟩ ⟩, define the power series s^{op} by

(s^{op}, u) = (s, u^{op}), u ∈ A^{∗},

where u^{op} is the word u written in the reverse order. The reader will have no difficulty to check that the function s ↦ s^{op} is a semiring isomorphism (S⟨ ⟨A^{∗}⟩ ⟩)^{op} → S^{op}⟨ ⟨A^{∗}⟩ ⟩. The fact that the star operation is preserved follows using Remark 8.2. Denoting the star operation in S^{op}⟨ ⟨A^{∗}⟩ ⟩ by ^{⊗} (and the product operation by ∘), we have ((s^{∗})^{op}, ϵ) = (s, ϵ)^{∗} = ((s^{op})^{⊗}, ϵ), for all s ∈ S⟨ ⟨A^{∗}⟩ ⟩. For nonempty words u,

((s^{∗})^{op}, u) = (s, ϵ)^{∗} ∑_{vw=u^{op}, v≠ϵ}(s, v)(s^{∗}, w)
= ( ∑_{wv=u^{op}, v≠ϵ}(s^{∗}, w)(s, v))(s, ϵ)^{∗}
= ( ∑_{vw=u, v≠ϵ}(s^{∗}, w^{op})(s, v^{op}))(s, ϵ)^{∗}
= (s^{op}, ϵ)^{∗} ∘ ( ∑_{vw=u, v≠ϵ}(s^{op}, v) ∘ ((s^{op}),^{⊗} w))
= ((s^{op})^{⊗}, u).
□

Corollary 8.8 If S is a symmetric inductive ^{∗}-semiring, then so is any semiring S⟨ ⟨A^{∗}⟩ ⟩ of power series.

Proof. This follows from Theorem 8.4 and Proposition 8.7. □

Remark 8.9 Suppose that S is a (symmetric) inductive ^{∗}-semmiring. Then the star operation is uniquely determined by the semiring structure and the partial order. Thus, when S⟨ ⟨A^{∗}⟩ ⟩ is ordered by the pointwise order, the star operation given above is the only one turning S⟨ ⟨A^{∗}⟩ ⟩ into an inductive ^{∗}-semiring.

9 A Kleene theorem for inductive ^{∗}-semirings

Definition 9.1 Suppose that S is a ^{∗}-semiring and A ⊆ S. A mechanism [7] over A is a triple D = (α, M, β), where α ∈ {0, 1}^{1×n}, β ∈ {0, 1}^{n×1} and M ∈ (A ∪ {0, 1})^{n×n}, for some n ≥ 0. The behaviour of D is

|D| = αM^{∗}β.

Mechanisms are called presentations in [6].

Definition 9.2 A Kleene semiring^{3} is a ^{∗}-semiring S such that for all A ⊆ S, the following two sets are equal:

1. ℝ⅁≈(A), the sub ^{∗}-semiring generated by A.

2. ℝ(A), the set of all behaviours over A.

Remark 9.3 For any ^{∗}-semiring S and A ⊆ S, we have ℝ(A) ⊆ ℝ⅁≈(A), by the definition of the star operation on matrices. Thus S is a Kleene semiring iff ℝ⅁≈(A) ⊆ ℝ(A) holds for all A ⊆ S.

Suppose that A ⊆ S, where S is a ^{∗}-semiring. For each a ∈ A, let

D_{a} = ([ 1 0 ] , [ \begin{matrix}0 & a \\ 0 & 0 \end{matrix} ] , [ \begin{matrix}0 \\ 1 \end{matrix} ]) .

Moreover, let

D_{0} = ([0], [0], [0])
D_{1} = ([1], [0], [1]).

Then |D_{0}| = 0, and if 0^{∗} = 1 holds in S, |D_{a}| = a and |D_{1}| = 1, so that A ∪ {0, 1} ⊆ ℝ(A).

Theorem 9.4 Every Conway semiring is a Kleene semiring.

Proof. Suppose that S is a Conway semiring and A ⊆ S. Since 0^{∗} = 1 holds in S, we have A∪{0, 1} ⊆ ℝ(A). Thus, we only need to show that ℝ(A) is closed under the sum, product and star operations. Following the proof of Theorem 8 in Chapter 3 of Conway [7], define

D = (α, M, β)
D′ = (α′, M′, β′)

Define

D + D′ = ([ α α′ ] , [ \begin{matrix}M & 0 \\ 0 & M′ \end{matrix} ] , [ \begin{matrix}β \\ β′ \end{matrix} ])
D · D′ = ([ α 0 ] , [ \begin{matrix}M & βα′ \\ 0 & M′ \end{matrix} ] , [ \begin{matrix}0 \\ β′ \end{matrix} ])
D^{∗} = ([ 1 0 ] , [ \begin{matrix}0 & α \\ β & M \end{matrix} ] , [ \begin{matrix}1 \\ 0 \end{matrix} ])

3Sakarovitch [22] defines a Kleene semiring as a ^{∗}-semiring which can be embedded in a continuous semiring.

Then we have

|D + D′| = |D| + |D′|
|D · D′| = |D| · |D′|
|D^{∗}| = |D|^{∗}.
□

Corollary 9.5 Every inductive ^{∗}-semiring is a Kleene semiring.

For a version of Theorem 9.4, which also holds in all Conway semirings, see [4] or [6]. Suppose that S is a^{∗}-semiring and A is a set. We may identify any letter a ∈ A with the power series r_{a} such that (r_{a}, a) = 1 and (r_{a}, u) = 0, for all words u ∈ A^{∗}, u ≠ a. We let S^{rat}⟨ ⟨A^{∗}⟩ ⟩ denote the set ℝ⅁≈(A). Note that S^{rat}⟨ ⟨A^{∗}⟩ ⟩ is a ∗-semiring, and when S is ordered, also an ordered semiring. Since equations and implications are preserved by substructures, we have

Proposition 9.6 If S is a Conway semiring or an iteration semiring, then so is S^{rat}⟨ ⟨A^{∗}⟩ ⟩, for all A ⊆ S. If S is an inductive ^{∗}-semiring, then so is any S^{rat}⟨ ⟨A^{∗}⟩ ⟩.

10 Free inductive ^{∗}-semirings

Since inductive ^{∗}-semirings form a quasi-variety of ordered algebras, all free inductive^{∗}-semirings exist. In this section we provide an explicit description of the initial inductive ^{∗}-semiring. In particular, we prove that the continuous ^{∗}- semiring ℕ_{∞}, obtained by adjoining a top element to the semiring ℕ of natural numbers, is initial in the class of inductive ^{∗}-semirings. We then conjecture that for any set A, the rational power series in ℕ_{∞}⟨ ⟨A^{∗}⟩ ⟩ form the free inductive ∗-semiring on the set A. Since any inductive ^{∗}-semiring is an iteration semiring, the initial inductive ∗-semiring is a quotient of the initial iteration semiring. The structure of the initial iteration semiring I_{0} was described in [4, 6]. Its elements are

0, 1, 2, …, 1^{∗}, (1^{∗})^{2}, …, 1^{∗∗}.

The operations are the expected ones, so that x + y and xy have their usual meaning for all x, y ∈ {0, 1, …}, and

x + y = max{x, y}

xy = \{ \begin{matrix}0 & if x = 0 or y = 0 \\ max\{x, y\} & if x ∈ \{1, 2, …\} or y ∈ \{1, 2, …\} \\ (1^{∗})^{m+n} & if x = (1^{∗})^{m}, y = (1^{∗})^{n} \\ 1^{∗∗} & if x, y ≠ 0 and (x = 1^{∗∗} or y = 1^{∗∗}), \end{matrix}

if x or y is in the set {1^{∗}, (1^{∗})^{2}, …, 1^{∗∗}}. The star operation is defined so that 0^{∗} = 1, the star of 1 is the element 1^{∗}, and x^{∗} = 1^{∗∗} for all x ≠ 0, 1. Of course, the operation max refers to the linear order corresponding to the above sequencing of the elements of I_{0}. Note that this order is just the sum-order on I_{0}. But I_{0} is not an inductive ^{∗}-semiring, since

2 · 1^{∗} + 1 = 1^{∗} + 1^{∗} + 1
= 1^{∗} + 1
= 1^{∗},

yet 2^{∗} = 1^{∗∗} ≰ 1^{∗}. To turn I_{0} into an inductive ^{∗}-semiring, we need to identify 1^{∗} and 1^{∗∗} and hence to collapse all elements in the set {1^{∗}, (1^{∗})^{2}, …, 1^{∗∗}}. The resulting ^{∗}-semiring is isomorphic to ℕ_{∞}.

Theorem 10.1 The continuous ^{∗}-semiring ℕ_{∞}, equipped with the natural star operation, is initial in the class of inductive ^{∗}-semirings.

Proof. We have already noted that ℕ_{∞} is an inductive ^{∗}-semiring. By the above argument, ℕ_{∞} is initial in the class of all iteration semirings satisfying 1^{∗} = 1^{∗∗}. But any inductive ^{∗}-semiring S satisfies this equation, so that there is a unique ^{∗}-semiring morphism ℕ_{∞} → S. Since the order on ℕ_{∞} is the sum-order, this morphism preserves the order. □

Corollary 10.2 Any inductive ^{∗}-semiring is an iteration semiring satisfying 1^{∗} = 1^{∗∗}.

In fact, every complete (or countably complete) semiring is an iteration semiring satisfying 1^{∗} = 1^{∗∗}, as shown in [4, 6]. (The fact that any complete semiring is a Conway semiring was established in [19] and [14].) Such a semiring S has a sum operation ∑_{i∈I} s_{i}, defined for all families s_{i} ∈ S, i ∈ I which extends the binary sum operation and such that summation is associative and product distributes over all sums. For any complete semiring S and s ∈ S, we define s^{∗} = ∑_{n≥0} s^{n}. Equipped with the sum operation defined in (4), every continuous semiring is complete. On the other hand, there exist complete sum-ordered semirings which are not inductive. For one example, consider the semiring R_{∞}^{+} of nonnegative real numbers with a top element ∞ adjoined, equipped with the sum operation

∑_{i∈I} r_{i} = \{ \begin{matrix}∞ & if r_{i} ≠ 0 for an infinite number of i′s, \\ & or ∃i r_{i} = ∞ \\ the usual sum & otherwise \end{matrix}

and multiplication

r_{1}r_{2} = \{ \begin{matrix}∞ & if r_{1}, r_{2} ≠ 0 and ∞ ∈ \{r_{1}, r_{2}\} \\ the usual sum & otherwise. \end{matrix}

In this semiring we have (1/2)^{∗} = ∞, but the least solution of the equation x = x/2 + 1 is 2.

Remark 10.3 The semiring ℕ_{∞} is also initial in the class of weak inductive ∗-semirings, and in the class of all continuous ^{∗}-semirings.

Conjecture 10.4 For any set A, the semiring ℕ_{∞}^{rat}⟨ ⟨A^{∗}⟩ ⟩ is the free inductive ∗-semiring on A.

Since any inductive ^{∗}-semiring is an iteration semiring, this conjecture is implied by the following:

Conjecture 10.5 For any set A, the (unordered reduct of the) ^{∗}-semiring ℕ_{∞}^{rat}⟨ ⟨A^{∗}⟩ ⟩ is the free iteration semiring on A satisfying the equation 1^{∗} = 1^{∗∗}.

If Conjectures 10.4 and 10.5 hold, then we also have:

Conjecture 10.6 An equation holds in all inductive ^{∗}-semirings iff it holds in all iteration semirings satisfying 1^{∗} = 1^{∗∗}.

The “Boolean versions” of all of the above three conjectures are known to hold.

Theorem 10.7 [18] For each set A, the semiring 𝔹^{rat}⟨ ⟨A^{∗}⟩ ⟩ is freely generated by A in the class of all iteration semirings satisfying 1^{∗} = 1.

See also [10]. Since 𝔹^{rat}⟨ ⟨A^{∗}⟩ ⟩ is an inductive ^{∗}-semiring, and in fact a Kozen semiring, we also have

Corollary 10.8 For each set A, the semiring 𝔹^{rat}⟨ ⟨A^{∗}⟩ ⟩ is freely generated by A in the class of all idempotent inductive ^{∗}-semirings.

Corollary 10.9 [16] For each set A, the semiring 𝔹^{rat}⟨ ⟨A^{∗}⟩ ⟩ is freely generated by A in the class of all Kozen semirings.

A generalization of Corollary 10.8 has been obtained in [11].

Theorem 10.10 For any set A and for each natural number k > 1, the semiring ℸ^{rat}⟨ ⟨A^{∗}⟩ ⟩ is freely generated by the set A in the class of all symmetric inductive ^{∗}-semirings satisfying the equation k − 1 = k.

Of course, in the above equation, k denotes the k-fold sum of 1 with itself.

Conjecture 10.11 For any integer k > 1, the semiring ℸ^{rat}⟨ ⟨A^{∗}⟩ ⟩ is the free iteration semiring on the set A satisfying the equation k − 1 = 1^{∗}. Moreover, ℸ^{rat}⟨ ⟨A^{∗}⟩ ⟩ is the free inductive ^{∗}- semiring on the set A satisfying the equation k − 1 = k.

11 Summary

We have studied in detail the relation between 5 classes of ^{∗}-semirings. In decreasing order of generality, these are Conway semirings, iteration semirings, inductive ^{∗}-semirings, symmetric inductive ^{∗}-semirings and continuous ∗-semirings. Except for continuous ^{∗}-semirings, each class can be axiomatized within first order logic. Conway semirings and iteration semirings form two varieties of ^{∗}-semirings, and inductive ^{∗}-semirings and symmetric inductive ^{∗}-semirings form two finitely axiomatizable quasi-varieties of ordered ^{∗}- semirings. In contrast with Conway semirings, ^{∗}-semirings do not have a finite basis for their identities. In addition to the iteration semiring identities, any iteration ^{∗}-semiring satisfies equation 1^{∗} = 1^{∗∗}. We have conjectured that the variety of ^{∗}-semirings generated by the (unordered reducts of) inductive, symmetric inductive, or continuous ^{∗}-semirings is exactly the subvariety of iteration ^{∗}-semirings defined by the equation 1^{∗} = 1^{∗∗}. The free continuous ∗-semiring on a set A may be described as the power series semiring ℕ_{∞}⟨ ⟨A^{∗}⟩ ⟩ (equipped with the pointwise order). We have conjectured that in each of the classes of iteration ^{∗}-semirings satisfying 1^{∗} = 1^{∗∗}, inductive ^{∗}-semirings and symmetric inductive ^{∗}-semirings, the free ^{∗}-semirings can be described as the semirings ℕ_{∞}^{rat}⟨ ⟨A^{∗}⟩ ⟩ of rational power series in ℕ_{∞}⟨ ⟨A^{∗}⟩ ⟩, equipped with the ponitwise order where appropriate. The above conjectures may be seen as natural extensions of some of Conway’s conjectures [7] regarding the axiomatization of the regular sets, confirmed in Krob [18]. (For an extension of Krob’s result in another direction, see Ésik [10].) The results of Krob [18] and those given in Kozen [16] and Ésik and Kuich [11] provide ample evidence for these conjectures.

Continuous^{∗}-semirings, Conway semirings and iteration^{∗}-semirings have been known to be closed for several constructions including matrix semirings, duals, and power series. In this paper, we have established the same closure properties of symmetric inductive ^{∗}-semirings. Inductive ^{∗}-semirings are closed for matrices and power series, but not for duals. From these facts, we have derived a general Kleene theorem applicable to all inductive ^{∗}-semirings.

References

[1] H. Bekic̆. Definable operations in general algebras, and the theory of automata and flowcharts, Technical Report, IBM Laboratory, Vienna, 1969.

[2] A.J. Blikle. Nets: complete lattices with composition. Bull. Acad. Polon. Sci. Ser. Math. Astronom. Phys., 19:1123–1127, 1971.

[3] S.L. Bloom. Varieties of ordered algebras. J. Computer System Sciences, 45:200–212,1976.

[4] S.L. Bloom and Z. Ésik. Matrix and matricial iteration theories, Part I, Journal of Computer and System Sciences. 46:381–408, 1993.

[5] S.L. Bloom and Z. Ésik. Equational axioms for regular sets. Mathematical Structures in Computer Science, 3:1–24, 1993.

[6] S.L. Bloom and Z. Ésik. Iteration Theories: the Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer–Verlag, 1993.

[7] J.C. Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971.

[8] B.A. Davey and H.A. Priestly. Introduction to Lattices and Order. Cambridge University Press, 1990.

[9] J.W. de Bakker and D. Scott. A theory of programs. IBM, Vienna, 1969.

[10] Z. Ésik. Group axioms for iteration. Information and Computation, 148:131–180, 1999.

[11] Z. Ésik and W. Kuich. A generalization of Kozen’s axiomatization of the equational theory of regular sets. To appear.

[12] J.S. Golan. The Theory of Semirings with Applications in Computer Science. Longman Scientific and Technical, 1993.

[13] M. Goldstern. Vervollständigung von Halbringen. Diploma Thesis, Technical University of Vienna, 1985.

[14] U. Hebish. The Kleene theorem in countably complete semirings. Bayreuther Mathematische Schriften, 31:55-66, 1990.

[15] R. Kimmo. Quantales and Their Applications. Longman Scientific and Technical, 1990.

[16] D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In Proc. IEEE Symposium on Logic in Computer Science, pages 214–225, 1991.

[17] D. Kozen. On Kleene algebras and closed semirings. In Proc. MFCS ’90, LNCS 452, pages 26–47, Springer–Verlag, 1990.

[18] D. Krob. Complete systems of B-rational identities. Theoretical Computer Science, 89:207–343, 1991.

[19] W. Kuich. The Kleene and Parikh theorem in complete semirings. In Proc. ICALP’87, LNCS 267, pages 212–225, Springer-Verlag, 1987.

[20] E.G. Manes and M.A. Arbib. Algebraic Approaches to Program Semantics, Springer, 1986.

[21] D.M.R. Park. Fixpoint induction and proofs of program properties. In Machine Intelligence 5, D. Michie and B. Meltzer, Eds., pages 59–78, Edinburgh Univ. Press, 1970.

[22] J. Sakarovitch. Kleene’s theorem revisited. In: LNCS 281, pages 39–50, 1987.

[23] W. Wechler. Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science, Vol. 25. Springer-Verlag, 1992.

Recent BRICS Report Series Publications

RS-00-27 ZoltánÉsik and Werner Kuich. Inductive^{∗}-Semirings. October 2000. 34 pp.

RS-00-26 František Čapkovič. Modelling and Control of Discrete Event Dynamic Systems. October 2000. 58 pp.

RS-00-25 Zoltán Ésik. Continuous Additive Algebras and Injective Simulations of Synchronization Trees. September 2000. 41 pp.

RS-00-24 Claus Brabrand and Michael I. Schwartzbach. Growing Languages with Metamorphic Syntax Macros. September 2000.

RS-00-23 Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characteristic Formulae for Timed Automata. September 2000. 23 pp.

RS-00-22 Thomas S. Hune and Anders B. Sandholm. Using Automata in Control Synthesis — A Case Study. September 2000. 20 pp. Appears in Maibaum, editor, Fundamental Approaches to Software Engineering: First International Conference, FASE ’00 Proceedings, LNCS 1783, 2000, pages 349–362.

RS-00-21 M. Oliver Möller and Rajeev Alur. Heuristics for Hierarchical Partitioning with Application to Model Checking. August 2000. 30 pp.

RS-00-20 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. 2-Nested Simulation is not Finitely Equationally Axiomatizable. August 2000. 13 pp.

RS-00-19 Vinodchandran N. Variyam. A Note on NP ∩ coNP/poly. August 2000. 7 pp.

RS-00-18 Federico Crazzolara and Glynn Winskel. Language, Semantics, and Methods for Cryptographic Protocols. August 2000. ii+42 pp.

RS-00-17 Thomas S. Hune. Modeling a Language for Embedded Systems in Timed Automata. August 2000. 26 pp. Earlier version entitled Modelling a Real-Time Language appeared in Gnesi and Latella, editors, Fourth International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS ’99 Proceedings of the FLoC Workshop, 1999, pages 259–282.