Completeness and Incompleteness of Synchronous Kleene Algebra

TL;DR

This paper investigates the completeness of Synchronous Kleene algebra (SKA), identifies its limitations, and proposes an alternative axiomatization that is both sound and complete with respect to language semantics.

Contribution

It demonstrates the incompleteness of existing SKA axioms and introduces a new set of axioms based on Salomaa's regular language axiomatization.

Findings

Identified a counterexample showing SKA axioms are incomplete.

Proposed an alternative axiomatization for SKA.

Proved the new axioms are sound and complete.

Abstract

Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics.

Equations

$$K\cdot L=\{uv:u\in K,v\in L\}$$

$$e+(f+g)=(e+f)+g$$

$$e\cdot 1=e=1\cdot e$$

$$e^{\ast }=1+e\cdot e^{\ast }=1+e^{\ast }\cdot e$$

$${\mathcal{T}}_{\mathsf{KA}}\ni e,f::=0|1|a\in \Sigma |e+f|e\cdot f|e^{\ast }$$

$$[[0{]]}_{\mathsf{KA}}=\varnothing$$

$$[[1{]]}_{\mathsf{KA}}=\{\epsilon \}$$

$$(M\cdot x)(q)=\sum _{e\in Q}M(q,e)\cdot x(e)$$

$$\ell (x)=\{\epsilon :o(x)=1\}\cup \bigcup _{x^{\prime }\in d(x,a)}\{a\}\cdot \ell (x^{\prime })$$

$$e\times (f+g)=e\times f+e\times g$$

$$(\alpha \cdot e)\times (\beta \cdot f)=(\alpha \times \beta )\cdot (e\times f)$$

$${\mathcal{T}}_{\mathsf{SL}}\ni e,f::=a\in \Sigma |e\times f$$

$${\mathcal{T}}_{\mathsf{SKA}}\ni e,f::=0|1|a\in {\mathcal{T}}_{\mathsf{SL}}|e+f|e\cdot f|e\times f|e^{\ast }$$

$$K\times L=\{u\times v:u\in K,v\in L\}$$

$$\small\begin{array}[]{@{}l@{\hspace{.5cm}}l@{\hspace{.5cm}}l@{}}\llbracket 0\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\emptyset\quad\llbracket 1\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\{\varepsilon\}\hfil\hskip 14.22636pt&\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\{\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}\}\quad\forall a\in\mathcal{T}_{\mathsf{SL}}\hfil\hskip 14.22636pt&\llbracket e^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}^{*}\\[3.87498pt] \llbracket e\cdot f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\cdot\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\hfil\hskip 14.22636pt&\llbracket e+f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}+\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\hfil\hskip 14.22636pt&\llbracket e\times f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\times\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\end{array}$$

$$\begin{array}[]{rll}K+L&=\left\{\begin{array}[]{l}\dagger\\[2.84526pt] K\cup L\end{array}\right.&\begin{array}[]{l}K=\dagger\vee L=\dagger\\[2.84526pt] \text{otherwise}\end{array}\\[14.22636pt] K\cdot L&=\left\{\begin{array}[]{l}\emptyset\\[2.84526pt] \dagger\\[2.84526pt] \{u\cdot v:u\in K,v\in L\}\end{array}\right.&\begin{array}[]{l}K=\emptyset\vee L=\emptyset\\[2.84526pt] K=\dagger\vee L=\dagger\\[2.84526pt] \text{otherwise}\end{array}\\[22.76219pt] K\times L&=\left\{\begin{array}[]{l}\emptyset\\[2.84526pt] \dagger\\[2.84526pt] \{u\times v:u\in K,v\in L\}\end{array}\right.&\begin{array}[]{l}K=\emptyset\vee L=\emptyset\\[2.84526pt] K=\dagger\vee L=\dagger\vee K,L\text{ infinite}\\[2.84526pt] \text{otherwise}\end{array}\\[22.76219pt] K^{*}&=\left\{\begin{array}[]{l}\dagger\\[2.84526pt] \bigcup_{n\in\mathbb{N}}K^{n}\end{array}\right.&\begin{array}[]{l}K=\dagger\\[2.84526pt] \text{otherwise}\end{array}\end{array}$$

$$(A\cdot K)\times (A\cdot L)=(A\times A)\cdot (K\times L)$$

$$e+(f+g)=(e+f)+g$$

$$e\cdot 1=e=1\cdot e$$

$$e^{\ast }=1+e\cdot e^{\ast }=1+e^{\ast }\cdot e$$

$${(e+1)}^{\ast }=e^{\ast }$$

$$H(0)=0$$

$$H(1)=1$$

$${\mathcal{T}}_{{\mathsf{F}}_1}\ni e,f::=0|1|a\in \Sigma |e+f|e\cdot f|e^{\ast }|H(e)$$

$$[[H(e){]]}_{{\mathsf{F}}_1}=[[e{]]}_{{\mathsf{F}}_1}\cap \{\epsilon \}$$

$$e\times (f+g)=e\times f+e\times g$$

$$(\alpha \cdot e)\times (\beta \cdot f)=(\alpha \times \beta )\cdot (e\times f)$$

$${\mathcal{T}}_{{\mathsf{SF}}_1}\ni e,f::=0|1|a\in {\mathcal{T}}_{\mathsf{SL}}|e+f|e\cdot f|e\times f|e^{\ast }|H(e)$$

$$[[H(e){]]}_{{\mathsf{SF}}_1}=[[e{]]}_{{\mathsf{SF}}_1}\cap \{\epsilon \}$$

$${\alpha }^{\ast }\times {\alpha }^{\ast }$$

$${\equiv }_{{\mathsf{SF}}_1}1+\alpha \cdot {\alpha }^{\ast }+(\alpha \times \alpha )\cdot ({\alpha }^{\ast }\times {\alpha }^{\ast }){\equiv }_{{\mathsf{SF}}_1}{\alpha }^{\ast }+\alpha \cdot ({\alpha }^{\ast }\times {\alpha }^{\ast })$$

$$o(0)$$

$$o(1)$$

$$\delta (0,A)$$

$$\delta (H(e),A)$$

$$\delta (a,A)$$

Full text

1 Introduction

Kleene algebra (KA) is applied in various contexts, such as relational algebra and automata theory. An important use of KA is as a logic of programs. This is because the axioms of KA correspond well to properties expected of sequential program composition, and hence they provide a logic for reasoning about control flow of sequential programs presented as Kleene algebra expressions. Regular languages then provide a canonical semantics for programs expressed in Kleene algebra, due to a tight connection between regular languages and the axioms of KA: an equation is provable using the Kleene algebra axioms if and only if the corresponding regular languages coincide [5, 19, 16].

In [22], Prisacariu proposes an extension of Kleene algebra, called synchronous Kleene algebra (SKA). The aim was to introduce an algebra useful for studying not only sequential programs but also synchronous concurrent programs. Here, synchrony is understood as in Milner’s SCCS [21], i.e., each program executes a single action instantaneously at each discrete time step. Hence, the synchrony paradigm assumes that basic actions execute in one unit of time and that at each time step, all components capable of acting will do so. This model permits a synchronous product operator, which yields a program that, at each time step, executes some combination of the actions put forth by the operand programs.

This new operator is governed by various expected axioms such as associativity and commutativity. Another axiom describes the interaction between the synchronous product and the sequential product, capturing the intended lock-step behaviour. Crucially, the axioms do not entail certain equations that relate the Kleene star (used to describe loops) and the synchronous product.

The contributions of this paper are twofold. First, we show that the lack of connection between the Kleene star and the synchronous product is problematic. In particular, we exploit this fact to devise a countermodel that violates a semantically valid equation, thus showing that the SKA axioms are incomplete w.r.t. the language semantics. This invalidates the completeness result in [22].

The second and main contribution of this paper is a sound and complete characterisation of the equational theory of SKA in terms of a generalisation of regular languages. The key difference with [22] is the shift from least fixpoint axioms in the style of Kozen [16] to a unique fixpoint axiom in the style of Salomaa [24]. In the completeness proof, we give a reduction to the completeness result of Salomaa via a normal form for SKA expressions. As a by-product, we get a proof of the correctness of the partial derivatives for SKA provided in [7].

This paper is organised as follows. In Section 2 we discuss the necessary preliminaries. In Section 3 we discuss SKA as presented in [22]. Next, in Section 4, we demonstrate why SKA is incomplete, and in Section 5 go on to provide a new set of axioms, which we call $\mathsf{SF}_{1}$. The latter section also includes basic results about the partial derivatives for SKA from [7]. In Section 6 we provide an algebraic characterisation of $\mathsf{SF}_{1}$-terms; this characterisation is used in Section 7, where we prove completeness of $\mathsf{SF}_{1}$ w.r.t. to its language model. In Section 8 we consider related work and conclude by discussing directions for future work in Section 9. For the sake of readability, some of the proofs appear in the appendix.

2 Preliminaries

Throughout this paper, we write $2$ for the two-element set $\{0,1\}$.

Languages

Throughout the paper we fix a finite alphabet $\Sigma$. A word formed over $\Sigma$ is a finite sequence of symbols from $\Sigma$. The empty word is denoted by $\varepsilon$. We write $\Sigma^{*}$ for the set of all words over $\Sigma$. Concatenation of words $u,v\in\Sigma^{*}$ is denoted by $uv\in\Sigma^{*}$. A language is a set of words. For $K,L\subseteq\Sigma^{*}$, we define

[TABLE]

where $K^{0}=\{\varepsilon\}$ and $K^{n+1}=K\cdot K^{n}$.

Kleene Algebra

We define a Kleene algebra [16] as a tuple $(A,+,\cdot,^{*},0,1)$ where $A$ is a set, ∗ is a unary operator, $+$ and $\cdot$ are binary operators and [math] and $1$ are constants. Moreover, for all $e,f,g\in A$ the following axioms are satisfied:

[TABLE]

Additionally, we write $e\leq f$ as a shorthand for $e+f=f$, and require that the least fixpoint axioms [16] hold, which stipulate that for $e,f,g\in A$ we have {mathpar} e + f ⋅g ≤g ⟹f^* ⋅e ≤g e + f ⋅g ≤f ⟹e ⋅g^* ≤f

The set of regular expressions, denoted $\mathcal{T}_{\mathsf{KA}}$, is described by the grammar:

[TABLE]

Regular expressions can be interpreted in terms of languages. This is done by defining $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{KA}}:\mathcal{T}_{\mathsf{KA}}\rightarrow\mathcal{P}(\Sigma^{*})$ inductively, as follows.

[TABLE]

A language $L$ is called regular if and only if $L=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{KA}}$ for some $e\in\mathcal{T}_{\mathsf{KA}}$.

We write $\equiv_{\scriptscriptstyle\mathsf{KA}}$ for the smallest congruence on $\mathcal{T}_{\mathsf{KA}}$ induced by the Kleene algebra axioms — e.g., for all $e\in\mathcal{T}_{\mathsf{KA}}$, we have $1+e\cdot e^{*}\equiv_{\scriptscriptstyle\mathsf{KA}}e^{*}$. Intuitively, $e\equiv_{\scriptscriptstyle\mathsf{KA}}f$ means that the regular expressions $e$ and $f$ can be proved equivalent according to the axioms of Kleene algebra. A pivotal result in the study of Kleene algebras tells us that $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{KA}}$ characterises $\equiv_{\scriptscriptstyle\mathsf{KA}}$, in the following sense:

Theorem 2.1 (Soundness and Completeness of KA [16])

For all $e,f\in\mathcal{T}_{\mathsf{KA}}$, we have that $e\equiv_{\scriptscriptstyle\mathsf{KA}}f$ if and only if $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{KA}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{KA}}$.

Remark 1

The above can be generalised, as follows. Let $\mathcal{K}=(A,+,\cdot,^{*},0,1)$ be a KA, and let $\sigma:\Sigma\to A$. Then for all $e,f\in\mathcal{T}_{\mathsf{KA}}$ such that $e\equiv_{\scriptscriptstyle\mathsf{KA}}f$, interpreting $e$ and $f$ according to $\sigma$ in $\mathcal{K}$ yields the same result. For instance, since ${(a^{*})}^{*}\equiv_{\scriptscriptstyle\mathsf{KA}}a^{*}$, we know that for any element $e$ of any KA $\mathcal{K}$, we have that ${(e^{*})}^{*}=e$.

Linear Systems

Let $Q$ be a finite set. A $Q$-vector is a function $x:Q\rightarrow\mathcal{T}_{\mathsf{KA}}$. A $Q$-matrix is a function $M:Q\times Q\rightarrow\mathcal{T}_{\mathsf{KA}}$. Let $x$ and $y$ be $Q$-vectors. Addition is defined pointwise, setting $(x+y)(q)=x(q)+y(q)$. Multiplication by a $Q$-matrix $M$ is given by

[TABLE]

When $x(q)\equiv_{\scriptscriptstyle\mathsf{KA}}y(q)$ for all $q\in Q$, we write $x\equiv_{\scriptscriptstyle\mathsf{KA}}y$.

Definition 1

A $Q$-linear system is a pair $(M,x)$ with $M$ a $Q$-matrix and $x$ a $Q$-vector. A solution to $(M,x)$ in KA is a $Q$-vector $y$ such that $M\cdot y+x\equiv_{\scriptscriptstyle\mathsf{KA}}y$.

Non-deterministic finite automata

A non-deterministic automaton (NDA) over an alphabet $\Sigma$ is a triple $(X,o,d)$ where $o\colon X\rightarrow 2$ is called the termination function and $d\colon X\times\Sigma\rightarrow X$ called the continuation function. If $X$ is finite, $(X,o,d)$ is referred to as a non-deterministic finite automaton (NFA).

The semantics of an NDA $(X,o,d)$ can be characterised recursively as the unique map $\ell:X\to\mathcal{P}(\Sigma^{*})$ such that

[TABLE]

This coincides with the standard definition of language acceptance.

3 Synchronous Kleene Algebra

Synchronous Kleene algebra extends Kleene algebra with an additional operator denoted $\times$, which we refer to as the synchronous product [22].

Definition 2 (Synchronous Kleene Algebra)

A synchronous KA (SKA) is a tuple $(A,S,+,\cdot,^{*},\times,0,1)$ such that $(A,+,\cdot,^{*},0,1)$ is a Kleene algebra and $\times$ is a binary operator on $A$, with $S\subseteq A$ closed under $\times$ and $(S,\times)$ a semilattice. Furthermore, the following hold for all $e,f,g\in A$ and $\alpha,\beta\in S$:

[TABLE]

Note that [math] and $1$ need not be elements of $S$. The semilattice terms, denoted $\mathcal{T}_{\mathsf{SL}}$, are given by the following grammar.

[TABLE]

The synchronous regular terms, denoted $\mathcal{T}_{\mathsf{SKA}}$, are given by the grammar:

[TABLE]

Thus we have $\mathcal{T}_{\mathsf{SL}}\subseteq\mathcal{T}_{\mathsf{SKA}}$. We then define $\equiv_{\scriptscriptstyle\mathsf{SKA}}$ as the smallest congruence on $\mathcal{T}_{\mathsf{SKA}}$ satisfying the axioms of $\mathsf{SKA}$ . Here, $\mathcal{T}_{\mathsf{SL}}$ plays the role of the semilattice; for instance, for $a\in\mathcal{T}_{\mathsf{SL}}$ we have that $a\times a\equiv_{\scriptscriptstyle\mathsf{SKA}}a$.

Remark 2

In [22], $\times$ is declared to be idempotent on the generators of the semilattice, whereas in our definition it holds for semilattice elements in general. This does not change anything, as the axiom $a\times a=a$ for generators together with commutativity and associativity results in idempotence on the semilattice. We present SKA as in 2 to prevent a meta-definition of a third sort (namely the semilattice generated by $\Sigma$) present in the signature of the algebra. We have also left out the second distributivity and unit axioms that follow immediately from the ones presented and commutativity.

3.1 A Language Model for SKA

Similar to Kleene algebra, there is a language model for SKA [22].

Words over $\mathcal{P}(\Sigma)\setminus\{\emptyset\}=\mathcal{P}_{n}(\Sigma)$ are called synchronous strings, and sets of synchronous strings are called synchronous languages. The standard language operations (sum, concatenation, Kleene closure) are also defined on synchronous languages. The synchronous product of synchronous languages $K,L$ is given by:

[TABLE]

where we define $\times$ inductively for $u,v\in{(\mathcal{P}_{n}(\Sigma))}^{*}$ and $x,y\in\mathcal{P}_{n}(\Sigma)$, as follows: {mathpar} u×ε= u = ε×u and (x⋅u)×( y⋅v) = (x∪y)⋅(u×v)

To define the language semantics for all elements in $\mathcal{T}_{\mathsf{SKA}}$, we first give an interpretation of elements in $\mathcal{T}_{\mathsf{SL}}$ in terms of non-empty finite subsets of $\Sigma$.

Definition 3

For $a\in\Sigma$ and $e,f\in\mathcal{T}_{\mathsf{SL}}$, define $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SL}}:\mathcal{T}_{\mathsf{SL}}\rightarrow\mathcal{P}_{n}(\Sigma)$ by {mathpar} ⟦a⟧$\mathsf{SL}$={a} ⟦e×f⟧$\mathsf{SL}$ = ⟦e⟧$\mathsf{SL}$∪⟦f⟧$\mathsf{SL}$

Denote the smallest congruence on $\mathcal{T}_{\mathsf{SL}}$ with respect to idempotence, associativity and commutativity of $\times$ with $\equiv_{\scriptscriptstyle\mathsf{SL}}$. It is not hard to show that $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SL}}$ characterises $\equiv_{\scriptscriptstyle\mathsf{SL}}$, in the following sense.

Lemma 1 (Soundness and Completeness of SL)

For all $e,f\in\mathcal{T}_{\mathsf{SL}}$, we have $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SL}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SL}}$ if and only if $e\equiv_{\scriptscriptstyle\mathsf{SL}}f$.

The semantics of synchronous regular terms is given in terms of a mapping to synchronous languages: $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SKA}}:\mathcal{T}_{\mathsf{SKA}}\rightarrow\mathcal{P}({(\mathcal{P}_{n}(\Sigma))}^{*})$. We have:

[TABLE]

A synchronous language $L$ is called regular when $L=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$ for some $e\in\mathcal{T}_{\mathsf{SKA}}$.

Let $S=\{\{x\}:x\in\mathcal{P}_{n}(\Sigma)\}$, that is to say, $S$ is the set of synchronous languages consisting of a single word, whose single letter is in turn a subset of $\Sigma$. Furthermore, let $\mathcal{L}_{\Sigma}$ denote the set of synchronous languages over $\Sigma$. It is straightforward to prove that $\mathcal{L}_{\Sigma}$ together with $S$ is closed under the SKA operations and satisfies the SKA axioms [22]; more precisely, we have:

Lemma 2 ()

The structure $(\mathcal{L}_{\Sigma},S,+,\cdot,^{*},\times,\emptyset,\{\varepsilon\})$ is an SKA, that is, synchronous languages over $\Sigma$ form an SKA.

As a consequence of 2, we obtain soundness of the SKA axioms with respect to the language model based on synchronous regular languages:

Lemma 3 (Soundness of SKA)

For all $e,f\in\mathcal{T}_{\mathsf{SKA}}$, we have that $e\equiv_{\scriptscriptstyle\mathsf{SKA}}f$ implies $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$.

Remark 3

The above generalises almost analogously to 1. Let $\mathcal{M}$ be an SKA with semilattice $S$, and let $\sigma:\Sigma\to S$ be a function. Then for all $e,f\in\mathcal{T}_{\mathsf{SKA}}$ such that $e\equiv_{\scriptscriptstyle\mathsf{SKA}}f$, if we interpret $e$ in $\mathcal{M}$ according to $\sigma$, then we should get the same result as when we interpret $f$ in $\mathcal{M}$ according to $\sigma$.

In other words, when $e\equiv_{\scriptscriptstyle\mathsf{SKA}}f$ holds, it follows that $e=f$ is a valid equation in every SKA, provided that the symbols from $\Sigma$ are interpreted as elements of the semilattice. It is not hard to show that this claim does not hold when symbols from $\Sigma$ can be interpreted as elements of the carrier at large.

4 Incompleteness of SKA

We now prove incompleteness of the SKA axioms as presented in [22]. Fix alphabet $\mathcal{A}=\{a\}$. First, note that the language model of SKA has the following property.

Lemma 4 ()

For $\alpha\in\mathcal{T}_{\mathsf{SL}}$, we have $\llbracket\alpha^{*}\times\alpha^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket\alpha^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$.

If $\equiv_{\scriptscriptstyle\mathsf{SKA}}$ were complete w.r.t. $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$, then the above implies that $a^{*}\times a^{*}\equiv_{\scriptscriptstyle\mathsf{SKA}}a^{*}$ holds. In this section, we present a countermodel where all the axioms of SKA are true, but $\alpha^{*}\times\alpha^{*}=\alpha^{*}$ does not hold for any $\alpha\in S$. This shows that $a^{*}\times a^{*}\not\equiv_{\scriptscriptstyle\mathsf{SKA}}a^{*}$; consequently, $\equiv_{\scriptscriptstyle\mathsf{SKA}}$ cannot be complete w.r.t. $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$.

Countermodel for SKA

We define our countermodel as follows. For the semilattice, let $S=\{\{\{s\}\}\}$, the set containing the synchronous language $\{\{s\}\}$. We denote the set of all synchronous languages over alphabet $\{s\}$ with $\mathcal{L}_{s}$; the carrier of our model is formed by $\mathcal{L}_{s}\cup\{\dagger\}$, where $\dagger$ is a symbol not found in $\mathcal{L}_{s}$. The symbol $\dagger$ exists only in the model, and not in the algebraic theory. It remains to define the SKA operators on this carrier, which we do as follows.

Definition 4

An element of $\mathcal{L}_{s}\cup\{\dagger\}$ is said to be infinite when it is an infinite language. For $K,L\in\mathcal{L}_{s}\cup\{\dagger\}$, define the SKA operators as follows:

[TABLE]

where $u\times v$ for $u\in K$ and $v\in L$ and $K^{n}$ is as defined in Section 3. Here, the cases are given in order of priority — e.g., if $K=\emptyset$ and $L=\dagger$, then $K\cdot L=\emptyset$.

The intuition behind this model is that SKA has no axioms that relate to the synchronous execution of starred expressions, such as in $\alpha^{*}\times\alpha^{*}$, nor can such a relation be derived from the axioms, meaning that a model has some leeway in defining the outcome in such cases. Since the language of a starred expression is generally infinite, we choose $\times$ such that it diverges to the extra element $\dagger$ when given infinite languages as input; for the rest of the operators, the behaviour on $\dagger$ is chosen to comply with the axioms.

First, we verify that our operators satisfy the SKA axioms.

Lemma 5 ()

$\mathcal{M}=(\mathcal{L}_{s}\cup\{\dagger\},\{\{\{s\}\}\},+,\cdot,^{*},\times,\emptyset,\{\varepsilon\})$* with the operators as defined in 4 forms an SKA.*

Proof

For the sake of brevity, we validate one of the least fixpoint axioms and the synchrony axiom; the other axioms are treated in the appendix.

Let $K,L,J\in\mathcal{L}_{s}\cup\{\dagger\}$. We verify that $K+L\cdot J\leq J\implies L^{*}\cdot K\leq J$. Assume that $K+L\cdot J\leq J$. If $J=\dagger$, then the result follows by definition of $\leq$ and our choice of $+$. Otherwise, if $J\in\mathcal{L}_{s}$, we distinguish two cases. If $L=\dagger$, then $J$ must be $\emptyset$ (otherwise $J=\dagger$); hence $K=\emptyset$, and the claim holds. Lastly, if $L\in\mathcal{L}_{s}$, then $K\in\mathcal{L}_{s}$. In this case, all of the operands are languages, and thus the proof goes through as it does for KA.

For the synchrony axiom, we need only check

[TABLE]

for $A=\{\{s\}\}$ as that is the only element in $S$. Let $K,L\in\mathcal{L}_{s}\cup\{\dagger\}$. If either $K$ or $L$ is $\emptyset$, both sides of the equation reduce to $\emptyset$. Otherwise, if $K$ or $L$ is $\dagger$, then both sides of the equation reduce to $\dagger$. If $K$ and $L$ are both infinite then $A\cdot K$ and $A\cdot L$ are infinite and the claim follows. In all the remaining cases where $K$ and $L$ are elements of $\mathcal{L}_{s}$ and at most one of them is infinite, the proof goes through as it does for synchronous regular languages (3). ∎

This leads us to the following theorem:

Theorem 4.1

The axioms of SKA presented in 2 are incomplete. That is, there exist $e,f\in\mathcal{T}_{\mathsf{SKA}}$ such that $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$ but $e\not\equiv_{\scriptscriptstyle\mathsf{SKA}}f$.

Proof

Take $a\in\mathcal{A}$. We know from 4 that $\llbracket a^{*}\times a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$. Now suppose $a^{*}\times a^{*}\equiv_{\scriptscriptstyle\mathsf{SKA}}a^{*}$. As our countermodel is an SKA that means in particular that ${\{\{s\}\}}^{*}\times{\{\{s\}\}}^{*}={\{\{s\}\}}^{*}$ should hold (c.f. 3). However, in this model we can calculate that ${\{\{s\}\}}^{*}\times{\{\{s\}\}}^{*}=\dagger\neq{\{\{s\}\}}^{*}$. Hence, we have a contradiction. Thus $a^{*}\times a^{*}\not\equiv_{\scriptscriptstyle\mathsf{SKA}}a^{*}$, rendering SKA incomplete.∎

5 A new axiomatisation

We now create an alternative algebraic formalism, which we call $\mathsf{SF}_{1}$, and prove that its axioms are sound and complete w.r.t the model of synchronous regular languages. Whereas the definition of SKA relies on Kleene algebras (with least fixpoint axioms) as presented by Kozen [16], the definition of $\mathsf{SF}_{1}$ builds on $\mathsf{F}_{1}$-algebras (with a unique fixpoint axiom) as presented by Salomaa [24]. The axioms of Salomaa are strictly stronger than Kozen’s [struthfoster], and we will see that the unique fixpoint axiom allows us to derive a connection between the synchronous product and the Kleene star, even though this connection is not represented in an axiom directly (see 7).

Definition 5

An $\mathsf{F}_{1}$-algebra [24] is a tuple $(A,+,\cdot,^{*},0,1,H)$ where $A$ is a set, ∗ is a unary operator, $+$ and $\cdot$ are binary operators and [math] and $1$ are constants, and such that for all $e,f,g\in A$ the following axioms are satisfied:

[TABLE]

Additionally, the loop tightening and unique fixpoint axiom hold:

[TABLE]

Lastly, we have the following axioms for $H$:

[TABLE]

In [24], an $e\in A$ with $H(e)=1$ is said to have the empty word property, which will be reflected in the semantic interpretation of $H(e)$ stated below.

The set of $\mathsf{F}_{1}$-expressions, denoted $\mathcal{T}_{\mathsf{F}_{1}}$, is described by:

[TABLE]

We can interpret $\mathsf{F}_{1}$-expressions in terms of languages through $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}:\mathcal{T}_{\mathsf{F}_{1}}\to\mathcal{P}(\Sigma^{*})$, defined analogously to $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{KA}}$, where furthermore for $e\in\mathcal{T}_{\mathsf{F}_{1}}$ we have

[TABLE]

We write $\equiv_{\scriptscriptstyle\mathsf{F}_{1}}$ for the smallest congruence on $\mathcal{T}_{\mathsf{F}_{1}}$ induced by the $\mathsf{F}_{1}$-axioms. Additionally, we require that for $a\in\Sigma$, we have $H(a)\equiv_{\scriptscriptstyle\mathsf{F}_{1}}0$. A characterisation similar to Theorem 2.1 can then be established as follows111Unlike [24], we include $H$ in the syntax; one can prove that for any $e\in\mathcal{T}_{\mathsf{F}_{1}}$ it holds that $H(e)\equiv 0$ or $H(e)\equiv 1$, and hence any occurence of $H$ can be removed from $e$. This is what allows us to apply the completeness result from op. cit. here.:

Theorem 5.1 (Soundness and Completeness of $\mathsf{F}_{1}$ [24])

For all $e,f\in\mathcal{T}_{\mathsf{F}_{1}}$, we have that $e\equiv_{\scriptscriptstyle\mathsf{F}_{1}}f$ if and only if $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$.

Remark 4

Kozen [16] noted that the above does not generalise along the same lines as in 1. In particular, the axiom $H(a)\equiv_{\scriptscriptstyle\mathsf{SKA}}0$ is not stable under substitution; for instance, if we interpret $H(a)$ according to the valuation $a\mapsto\{\epsilon\}$ in the $\mathsf{F}_{1}$-algebra of languages, then we obtain $\{\epsilon\}$, whereas [math] is interpreted as $\emptyset$.

Definition 6

A synchronous $\mathsf{F}_{1}$-algebra ($\mathsf{SF}_{1}$-algebra for short) is a tuple $(A,S,+,\cdot,^{*},0,1,H)$, such that $(A,+,\cdot,^{*},0,1,H)$ is an $\mathsf{F}_{1}$-algebra and $\times$ is a binary operator on $A$, with $S\subseteq A$ closed under $\times$ and $(S,\times)$ a semilattice. Furthermore, the following hold for all $e,f,g\in A$ and $\alpha,\beta\in S$:

[TABLE]

Moreover, $H$ is compatible with $\times$ as well, i.e., for $e,f\in A$ we have that $H(e\times f)=H(e)\times H(f)$. Lastly, for $\alpha\in S$ we require that $H(\alpha)=0$.

Remark 5

The countermodel from Section 4 cannot be extended to a model of $\mathsf{SF}_{1}$. To see this, note that we have $H(\{\{s\}\})=0$ and $\emptyset+\{\{s\}\}\cdot\dagger=\dagger$, but ${\{\{s\}\}}^{*}\cdot\emptyset\neq\dagger$ — contradicting the unique fixpoint axiom.

The set of $\mathsf{SF}_{1}$-expressions over $\Sigma$, denoted $\mathcal{T}_{\mathsf{SF}_{1}}$, is described by:

[TABLE]

We interpret $\mathcal{T}_{\mathsf{SF}_{1}}$ in terms of languages via $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}:\mathcal{T}_{\mathsf{SF}_{1}}\rightarrow\mathcal{L}_{\Sigma}$, defined analogously to $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$, where furthermore for $e\in\mathcal{T}_{\mathsf{SF}_{1}}$ we have

[TABLE]

Note that when $e\in\mathcal{T}_{\mathsf{SKA}}$, then $e\in\mathcal{T}_{\mathsf{SF}_{1}}$ and $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$.

Define $\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}$ as the smallest congruence on $\mathcal{T}_{\mathsf{SF}_{1}}$ induced by the axioms of $\mathsf{SF}_{1}$, where $\mathcal{T}_{\mathsf{SL}}$ fulfills the role of the semilattice — e.g., if $a\in\mathcal{T}_{\mathsf{SL}}$, then $a\times a\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}a$. This axiomatisation is sound with respect to the language model.222 Note that for the synchronous language model we know the least fixpoint axioms are sound as well (3). However, there might be other $\mathsf{SF}_{1}\text{-models}$ where the least fixpoint axioms are not valid.

Lemma 6 ()

Let $e,f\in\mathcal{T}_{\mathsf{SF}_{1}}$. If $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}f$ then $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$.

Remark 6

The caveat from 4 can be transposed to this setting. However, the condition that for $\alpha\in S$ we have that $H(\alpha)=0$ allows one to strengthen the above along the same lines as 3, that is, if $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}f$, then interpreting $e$ and $f$ in some SKA according to some valuation of $\Sigma$ in terms of semilattice elements will produce the same outcome.

Remark 7

To demonstrate the use of the new axioms, we give an algebraic proof of $\alpha^{*}\times\alpha^{*}\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}\alpha^{*}$ for $\alpha\in\mathcal{T}_{\mathsf{SL}}$:

[TABLE]

Since $H(\alpha)=0$, we can apply the unique fixpoint axiom to find $\alpha^{*}\cdot\alpha^{*}\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}\alpha^{*}\times\alpha^{*}$. In $\mathsf{SF}_{1}$, it is not hard to show that $\alpha^{*}\cdot\alpha^{*}\equiv_{\scriptscriptstyle\mathsf{F}_{1}}\alpha^{*}$; hence, we find $\alpha^{*}\times\alpha^{*}\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}\alpha^{*}$.

Remark 8

Adding $\alpha^{*}\times\alpha^{*}=\alpha^{*}$ for $\alpha\in\mathcal{T}_{\mathsf{SL}}$ as an axiom to the old axiomatisation of SKA would not have been sufficient; one can easily find another semantical truth that does not hold in our countermodel, such as $\llbracket{(\alpha\cdot\beta)}^{*}\times{(\alpha\cdot\beta)}^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket{(\alpha\cdot\beta)}^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$. Adding $e^{*}\times e^{*}=e^{*}$ as an axiom is also not an option, as this is not sound; for instance, take $e=a+b$ for $a,b\in\Sigma$. In order to keep the axiomatisation finitary, a unique fixpoint axiom provided an outcome.

5.1 Partial Derivatives

In this section we develop the theory of SKA and set up the necessary machinery for Section 6 and the completeness proof in Section 7. We start by presenting partial derivatives, which provide a termination and continuation map on $\mathcal{T}_{\mathsf{SF}_{1}}$. These derivatives allow us to turn the set of synchronous regular terms into a non-deterministic automaton structure, such that the language accepted by $e\in\mathcal{T}_{\mathsf{SF}_{1}}$ as a state in this automaton is the same as the semantics of $e$. Furthermore, partial derivatives turn out to provide a way to algebraically characterise a term by means of acceptance and reachable terms, which is useful in the completeness proof of $\mathsf{SF}_{1}$.

The termination and continuation map for $\mathsf{SF}_{1}$-expressions presented below are a trivial extension of the ones from [7]. Intuitively, the termination map is $1$ if an expression can immediately terminate, and [math] otherwise; the continuation map of a term w.r.t. $A$ gives us the set of terms reachable with an $A$-step.

Definition 7 (Termination map)

For $a\in\Sigma$, we define $o:\mathcal{T}_{\mathsf{SF}_{1}}\to 2$ inductively, as follows:

[TABLE]

Definition 8 (Continuation map)

For $a\in\Sigma$, we inductively define   $\delta:\mathcal{T}_{\mathsf{SF}_{1}}\times\mathcal{P}_{n}(\Sigma)\to\mathcal{P}(\mathcal{T}_{\mathsf{SF}_{1}})$ as follows:

[TABLE]

where $\Delta(e,f,A)$ is defined to be $\delta(e,A)$ when $o(f)=1$, and $\emptyset$ otherwise.

Definition 9 (Syntactic Automaton)

We call the NDA $(\mathcal{T}_{\mathsf{SF}_{1}},o,\delta)$ the syntactic automaton of $\mathsf{SF}_{1}$-expressions.

In Section 6 we give a proof of correctness of partial derivatives: for $e\in\mathcal{T}_{\mathsf{SF}_{1}}$ the semantics of $e$ is equivalent to the language accepted by $e$ as a state in the syntactic automaton. An analogous property holds for (partial) derivatives in Kleene algebras [8, 1], which makes derivatives a powerful tool for reasoning about language models and deciding equivalences of terms [6].

In the next two sections, we want to use terms reachable from $e$, that is to say, terms that are a result of repeatedly applying the continuation map on $e$. To this end, we define the following function:

Definition 10

For $e,f\in\mathcal{T}_{\mathsf{SF}_{1}}$ and $a\in\Sigma$, we inductively define the reach function $\rho:\mathcal{T}_{\mathsf{SF}_{1}}\to\mathcal{P}(\mathcal{T}_{\mathsf{SF}_{1}})$ as follows:

[TABLE]

Using a straightforward inductive argument, one can prove that for all $e\in\mathcal{T}_{\mathsf{SF}_{1}}$, $\rho(e)$ is finite. Note that $e$ is not always a member of $\rho(e)$. To see that $\rho(e)$ indeed contains all terms reachable from $e$, we record the following.

Lemma 7 ()

For all $e\in\mathcal{T}_{\mathsf{SF}_{1}}$ and $A\in\mathcal{P}_{n}(\Sigma)$, we have $\delta(e,A)\subseteq\rho(e)$. Also, if $e^{\prime}\in\rho(e)$, then $\delta(e^{\prime},A)\subseteq\rho(e)$.

5.2 Normal form

In this section we develop a normal form for expressions in $\mathcal{T}_{\mathsf{SL}}$, which we will use in the completeness proof for $\mathsf{SF}_{1}$. As $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SL}}$ is a surjective function it has at least one right inverse. Let us pick one and denote it by $(-)^{\Pi}$. We thus have $(-)^{\Pi}:\mathcal{P}_{n}(\Sigma)\rightarrow\mathcal{T}_{\mathsf{SL}}$ such that $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SL}}\circ(-)^{\Pi}$ is the identity on $\mathcal{P}_{n}(\Sigma)$.

The normal form for expressions in $\mathcal{T}_{\mathsf{SL}}$ is defined as follows:

Definition 11 (Normal form)

For all $e\in\mathcal{T}_{\mathsf{SL}}$ the normal form of $e$, denoted as $\overline{e}$, is defined as $(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SL}})^{\Pi}$. Let $\overline{\mathcal{T}_{\mathsf{SL}}}=\{\overline{e}:e\in\mathcal{T}_{\mathsf{SL}}\}$.

Intuitively, an expression in normal form is standardised with respect to idempotence, associativity and commutativity. For instance, for a term $(a\times a)\times(c\times b)$ with $a,b,c\in\Sigma$, the chosen normal form, dictated by the chosen right inverse, could be $(a\times b)\times c$, and all terms provably equivalent to $(a\times a)\times(c\times b)$ will have this same normal form. Using 1, we can formalise this in the following two results:

Lemma 8

For all $e\in\mathcal{T}_{\mathsf{SL}}$, we have that $e$ is provably equivalent to its normal form: $e\equiv_{\scriptscriptstyle\mathsf{SL}}\overline{e}$. Moreover, if two expressions $e,f\in\mathcal{T}_{\mathsf{SL}}$ are provably equivalent, they have the same normal form: if $e\equiv_{\scriptscriptstyle\mathsf{SL}}f$, then $\overline{e}=\overline{f}$.

Proof

As $(-)^{\Pi}$ is a right inverse of $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SL}}$, we can derive the following:

[TABLE]

From completeness we get $e\equiv_{\scriptscriptstyle\mathsf{SL}}\overline{e}$. For the second part of the statement we obtain via soundness that $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SL}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SL}}$ and subsequently that $\overline{e}=\overline{f}$.∎

Normalising normalised terms does not change anything.

Lemma 9 ()

For all $e\in\overline{\mathcal{T}_{\mathsf{SL}}}$ we have that $\overline{e}=e$.

We extend ${(-)}^{\Pi}$ from synchronous strings of length one to words and synchronous languages in the obvious way. For a synchronous string $aw$ with $a\in\mathcal{P}_{n}(\Sigma)$ and $w\in{(\mathcal{P}_{n}(\Sigma))}^{*}$, and synchronous language $L\in\mathcal{L}_{\Sigma}$ we define: {mathpar} ε^Π=ε(aw)^Π=a^Π⋅(w^Π) L^Π={w^Π : w∈L}

We abuse notation and assume the type of ${(-)}^{\Pi}$ is clear from the argument.

Since ${(-)}^{\Pi}$ is a homomorphism of languages, we have the following.

Lemma 10 ()

*For synchronous languages $L$ and $K$, all of the following hold:

(i) ${(L\cup K)}^{\Pi}=L^{\Pi}\cup K^{\Pi}$,

(ii) ${(L\cdot K)}^{\Pi}=L^{\Pi}\cdot K^{\Pi}$, and

(iii) ${(L^{*})}^{\Pi}={(L^{\Pi})}^{*}$.

6 A Fundamental Theorem for $\mathsf{SF}_{1}$

In this section we shall algebraically capture an expression in terms of its partial derivatives. This characterisation of an $\mathsf{SF}_{1}$-term will be useful later on in proving completeness but also provides us with a straightforward method to prove correctness of the partial derivatives. Following [23, 25], we call this characterisation a fundamental theorem for $\mathsf{SF}_{1}$. Before we state and prove the fundamental theorem, we prove an intermediary lemma:

Lemma 11

For all $e,f\in\mathcal{T}_{\mathsf{SF}_{1}}$, we have

[TABLE]

Proof

First note the following derivation for $A,B\in\mathcal{P}_{n}(\Sigma)$, using 8, the fact that all axioms of $\equiv_{\scriptscriptstyle\mathsf{SL}}$ are included in $\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}$, and that $(-)^{\Pi}$ is a right inverse of $\llbracket-\rrbracket_{\scriptscriptstyle\mathsf{SL}}$:

[TABLE]

Using distributivity, the synchrony axiom and the equation above, we can derive:

[TABLE]

The synchrony axiom can be applied because $A^{\Pi},B^{\Pi}\in\mathcal{T}_{\mathsf{SL}}$.∎

Theorem 6.1 (Fundamental Theorem)

For all $e\in\mathcal{T}_{\mathsf{SF}_{1}}$, we have

[TABLE]

Proof

This proof is mostly analogous to the proof of the fundamental theorem for regular expressions, such as the one that can be found in [25].

We proceed by induction on $e$. In the base, we have three cases to consider: $e\in\{0,1\}$ or $e=a$ for $a\in\Sigma$. For $e\in\{0,1\}$, the result follows immediately. For $e=a$, the only non-empty derivative is $\delta(a,\{a\})$ and the result follows:

[TABLE]

In the inductive step, we treat only the case for synchronous composition; the others can be found in the appendix. If $e=e_{0}\times e_{1}$, derive as follows:

[TABLE]

Correctness of partial derivatives for $\mathsf{SF}_{1}$

We now relate the partial derivatives for $\mathsf{SF}_{1}$ to their semantics. Let $\ell:\mathcal{T}_{\mathsf{SF}_{1}}\rightarrow\mathcal{L}_{\Sigma}$ be the semantics of the syntactic automaton $(\mathcal{T}_{\mathsf{SF}_{1}},o,\delta)$ (9), uniquely defined by Equation 1:

[TABLE]

To prove correctness of derivatives for $\mathsf{SF}_{1}$, we prove that the language semantics of the syntactic automaton and the $\mathsf{SF}_{1}$-expression coincide:

Theorem 6.2 (Soundness of derivatives)

For all $e\in\mathcal{T}_{\mathsf{SF}_{1}}$ we have:

[TABLE]

Proof

The claim follows almost immediately from the fundamental theorem. From 3 and Theorem 6.1, we obtain

[TABLE]

Note that $\llbracket A^{\Pi}\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}=\{\llbracket A^{\Pi}\rrbracket_{\scriptscriptstyle\mathsf{SL}}\}=\{A\}$ by definition of the $\mathsf{SF}_{1}$ semantics of a term in $\mathcal{T}_{\mathsf{SL}}$ and the fact that $(-)^{\Pi}$ is a right inverse. Because $\ell$ is the only function satisfying Equation 2, we obtain the desired equality between $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$ and the language $\ell(e)$ accepted by $e$ as a state of the automaton $(\mathcal{T}_{\mathsf{SF}_{1}},o,\delta)$. ∎

7 Completeness of $\mathsf{SF}_{1}$

In this section we prove completeness of the $\mathsf{SF}_{1}$-axioms with respect to the synchronous language model: we prove that for $e,f\in\mathcal{T}_{\mathsf{SF}_{1}}$, if $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$, then $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}f$. We first prove completeness of $\mathsf{SF}_{1}$ for a subset of $\mathsf{SF}_{1}$-expressions, relying on the completeness result of $\mathsf{F}_{1}$ (13). Then we demonstrate that for every $\mathsf{SF}_{1}$-expression we can find an equivalent $\mathsf{SF}_{1}$-expression in this specific subset (Theorem 7.1). This subset is formed as follows.

Definition 12

The set of $\mathsf{SF}_{1}$-expressions in normal form, $\mathcal{T}_{\mathsf{NSF}}$, is described by the grammar

[TABLE]

where $\overline{\mathcal{T}_{\mathsf{SL}}}$ is as defined in 11.

From this description it is immediate that an $\mathsf{SF}_{1}$-term $e\in\mathcal{T}_{\mathsf{NSF}}$ is formed from terms of $\overline{\mathcal{T}_{\mathsf{SL}}}$ connected via the regular $\mathsf{F}_{1}$-algebra operators. Hence, $\mathsf{F}_{1}$-expressions formed over the alphabet $\overline{\mathcal{T}_{\mathsf{SL}}}$ are the same set of terms as $\mathcal{T}_{\mathsf{NSF}}$. We shall use this observation to prove completeness for $\mathcal{T}_{\mathsf{NSF}}$ with respect to the language model by leveraging completeness of $\mathsf{F}_{1}$ .

We use the function $(-)^{\Pi}$ to give a translation between the $\mathsf{SF}_{1}$ semantics of a term in $\mathcal{T}_{\mathsf{NSF}}$ and the $\mathsf{F}_{1}$ semantics of that same term:

Lemma 12 ()

For all $e\in\mathcal{T}_{\mathsf{NSF}}$, we have ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$.

Proof

We proceed by induction on the construction of $e$. In the base, there are three cases to consider. If $e=0$, then $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}=\emptyset=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$, and we are done. If $e=1$, then ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}={(\{\varepsilon\})}^{\Pi}=\{\varepsilon\}=\llbracket 1\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$, and the claim follows. If $e=a$ for $a\in\overline{\mathcal{T}_{\mathsf{SL}}}$, we use 9 to obtain $\overline{a}=a$. As $a\in\overline{\mathcal{T}_{\mathsf{SL}}}\subseteq\mathcal{T}_{\mathsf{SL}}$, we know that ${(\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}={(\{\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}\})}^{\Pi}=\{(\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}})^{\Pi}\}=\{\overline{a}\}=\{a\}=\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$, and the claim follows.

For the inductive step, first consider $e=H(e_{0})$. ${(\llbracket H(e_{0})\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}=\{\varepsilon\}$ if $\varepsilon\in\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$ and $\emptyset$ otherwise. We also have $\llbracket H(e_{0})\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}=\{\varepsilon\}$ if $\varepsilon\in\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$ and $\emptyset$ otherwise. The induction hypothesis states that ${(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$, from which we obtain that $\varepsilon\in\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}\Leftrightarrow\varepsilon\in\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$. Hence we can conclude that ${(\llbracket H(e_{0})\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}=\llbracket H(e_{0})\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$. All other inductive cases follow immediately from 10. The details can be found in the appendix.∎

We are now ready to prove completeness of $\mathsf{SF}_{1}$ for terms in normal form.

Lemma 13

Let $e,f\in\mathcal{T}_{\mathsf{NSF}}$. If $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$, then $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}f$.

Proof

By the premise, we have that ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}={(\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}$. From 12 we get ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}=\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$ and ${(\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}})}^{\Pi}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$, which results in $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{F}_{1}}$. From Theorem 5.1 we know that this entails that $e\equiv_{\scriptscriptstyle\mathsf{F}_{1}}f$. As $\mathsf{SF}_{1}$ contains all the axioms of $\mathsf{F}_{1}$, we may then conclude that $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}f$ and the claim follows.∎

In order to prove completeness with respect to the language model for all $e\in\mathcal{T}_{\mathsf{SF}_{1}}$, we prove that for every $e\in\mathcal{T}_{\mathsf{SF}_{1}}$ there exists a term $\hat{e}\in\mathcal{T}_{\mathsf{NSF}}$ in normal form such that $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}\hat{e}$. To see this is indeed enough to establish completeness of $\mathsf{SF}_{1}$, imagine we have such a procedure to transform $e$ into $\hat{e}$ in normal form. We can then conclude that $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$ implies $\llbracket\hat{e}\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}=\llbracket\hat{f}\rrbracket_{\scriptscriptstyle\mathsf{SF}_{1}}$, which by 13 implies $\hat{e}\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}\hat{f}$, and consequently that $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}f$.

To obtain $\hat{e}$, we will make use of the “unfolding” of an $\mathsf{SF}_{1}$-expression $e$ in terms of partial derivatives, given by the fundamental theorem, which will give rise to a linear system. We will then show that this linear system has a unique solution that has the properties we require from $\hat{e}$. Since $e$ is also a solution to this linear system, we can conclude that they are provably equivalent.

Let us start with the following property of linear systems over $\mathsf{SF}_{1}$. A $Q$-vector is a function $x:Q\rightarrow\mathcal{T}_{\mathsf{SF}_{1}}$ and a $Q$-matrix is a function $M:Q\times Q\rightarrow\mathcal{T}_{\mathsf{SF}_{1}}$. We call a matrix $M$ guarded if $H(M(i,j))=0$ for all $i,j\in Q$. We say a vector $p$ and matrix $M$ are in normal form if $p(i)\in\mathcal{T}_{\mathsf{NSF}}$ for all $i\in Q$ and $M(i,j)\in\mathcal{T}_{\mathsf{NSF}}$ for all $i,j\in Q$. The following lemma is a variation of [24, Lemma 2] and the proof is a direct adaptation of the proof found in [15, Lemma 3.12].

Lemma 14 ()

Let $(M,p)$ be a $Q$-linear system such that $M$ and $p$ are guarded. We can construct $Q$-vector $x$ that is the unique (up to $\mathsf{SF}_{1}$-equivalence) solution to $(M,p)$ in $\mathsf{SF}_{1}$. Moreover, if $M$ and $p$ are in normal form, then so is $x$.

We now define the linear system associated to an $\mathsf{SF}_{1}$-expression $e$. This linear system makes use of the partial derivatives for $\mathsf{SF}_{1}$, and essentially represents an NFA that acceps the language described by $e$.

Definition 13

Let $e\in\mathcal{T}_{\mathsf{SF}_{1}}$, and choose $Q_{e}=\rho(e)\cup\{e\}$, where $\rho$ is the reach function from 10. Define the $Q_{e}$-vector $x_{e}$ and the $Q_{e}$-matrix $M_{e}$ by {mathpar} x_e(e’)=o(e’) M_e(e’,e”)= ∑_e”∈δ(e’,A)A^Π

We can now use 14 to obtain the desired normal form $\hat{e}$:

Theorem 7.1

For all $e\in\mathcal{T}_{\mathsf{SF}_{1}}$, there exists an $\hat{e}\in\mathcal{T}_{\mathsf{NSF}}$ such that $\hat{e}\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}e$.

Proof

It is clear from their definition that $x_{e}$ and $M_{e}$ are both in normal form and that $M_{e}$ is guarded. From 14 we then get that there exists a unique solution $s_{e}$ to $(M_{e},x_{e})$, and $s_{e}$ is a $Q_{e}$-vector in normal form. Now consider the $Q_{e}$-vector $y$ such that $y(q)=q$ for all $q\in Q_{e}$. Using 7 and Theorem 6.1, we can derive the following:

[TABLE]

This demonstrates that $y$ is also a solution to $(M_{e},x_{e})$. As we know from 14 that $s_{e}$ is unique, we get that $y\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}s_{e}$. This means that $e=y(e)\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}s_{e}(e)$. As $s_{e}$ is in normal form we get that $s_{e}(e)\in\mathcal{T}_{\mathsf{NSF}}$. Thus, if we take $s_{e}(e)=\hat{e}$, then we have obtained the desired result.∎

Combining Theorem 7.1 and 13 gives the main result of this section:

Theorem 7.2 (Soundness and Completeness)

For all $e,f\in\mathcal{T}_{\mathsf{SF}_{1}}$, we have

[TABLE]

As a corollary of Theorem 6.2 and Theorem 7.2 we know that $\mathsf{SF}_{1}$ is decidable by deciding language equivalence in the syntactic automaton.

8 Related Work

Synchonous cooperation among processes has been extensively studied in the context of process calculi such as ASP [4] and SCCS [21]. SKA bears a strong resemblance to SCCS, with the most notable differences being the equivalence axiomatised (bisimulation vs. language equivalence), and the use of Kleene star (unbounded finite recursion) instead of fixpoint (possibly infinite recursion). Contrary to ASP, but similar to SCCS, SKA cannot express incompatibility of action synchronisation.

In the context of Kleene algebra based frameworks for concurrent reasoning, a synchronous product is just one possible interpretation of concurrency. An interleaving-based approach with a concurrent operator (a parallel operator denoted with $\parallel$) is explored in Concurrent Kleene Algebra [15, 20, 12, 13, 15].

We have proved that $\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}$ is sound and complete with respect to the synchronous language model by making use of the completeness of $\mathsf{F}_{1}$ [24]. The strategy of transforming an expression $e$ to an equivalent expression $\hat{e}$ with a particular property is often used in literature [15, 18, 20, 14]. In particular, we adopted the use of linear systems as a representation of automata, which was first done by Conway [9] and Backhouse [2]. The machinery that we used to solve linear systems in $\mathsf{F}_{1}$ is based on Salomaa [24] and can also be found in [15] and [17]. The idea of the syntactic automaton originally comes from Brzozowski, who did this for regular expressions [8]. He worked with derivatives which turn a Kleene algebra expression into a deterministic automaton. We worked with partial derivatives instead, resulting in a non-deterministic finite automaton for each $\mathsf{SF}_{1}$-expression. Partial derivatives were first proposed by Antimirov [1].

Other related work is that of Hayes et al. [hayes1]. They explore an algebra of synchronous atomic steps that interprets the synchrony model SKA is based on (Milner’s SCCS calculus). However, their algebra is not based on a Kleene algebra — they use concurrent refinement algebra [10] instead. Later, Hayes et al. presented an abstract algebra for reasoning about concurrent programs with an abstract synchronisation operator [hayes2], of which their earlier algebra of atomic steps is an instance. A key difference seems to be that Hayes et al. use different units for synchronous and sequential composition. It would be interesting to compare expressive powers of the two algebras more extensively.

A decision procedure for equivalence between SKA terms is given by Broda et al. [7]. They defined partial derivatives for SKA that we also used in the proof of completeness, and used those to construct an NFA that accepts the semantics of a given SKA expression. Deciding language equivalence of two automata then leads to a decision procedure for semantic equivalence of SKA expressions.

9 Conclusions and Further Work

We have presented a complete axiomatisation with respect to the model of synchronous regular languages. We have first proved incompleteness of SKA via a countermodel, exploiting the fact that SKA did not have any axioms relating the synchronous product to the Kleene star. We then provided a set of axioms based on the $\mathsf{F}_{1}$-axioms from Salomaa [24] and the axioms governing the synchronous product familiar from SKA. This was shown to be a sound and complete axiomatisation with respect to the synchronous language model.

In the original SKA paper there is a presentation of synchronous Kleene algebra with tests including a wrongful claim of completeness. An obvious next step would be to see if we can prove completeness of $\mathsf{SF}_{1}$ with tests. We conjecture $\mathsf{SF}_{1}$ with tests is indeed complete and that this is straightforward to prove via a reduction to $\mathsf{SF}_{1}$ in a style similar to the completeness proof of KAT [18]. Another generalisation is to add a unit to the semilattice, making it a bounded semilattice. This will probably lead to a type of delay operation [21].

Our original motivation to study SKA was to use it as an axiomatisation of Reo, a modular language of connectors combining synchronous data flow with an asynchronous one [3]. The semantics of Reo is based on an automata model very similar to that of SKAT, in which transitions are labelled by sets of ports (representing a synchronous data flow) and constraints (the tests of SKAT). Interestingly, automata are combined using an operation analogous to the synchronous product of SKAT expressions. We aim to study the application of SKA or SKAT to Reo in future work.

Acknowledgements

The first author is grateful for discussions with Hans-Dieter Hiep and Benjamin Lion.

Appendix 0.A Appendix

See 2

Proof

The carrier $\mathcal{L}_{\Sigma}$ is obviously closed under the operations of synchronous Kleene algebra. We need only argue that each of the SKA axioms is valid on synchronous languages.

The proof for the Kleene algebra axioms follows from the observation that synchronous languages over the alphabet $\Sigma$ are simply languages over the alphabet $\mathcal{P}_{n}(\Sigma)$. Thus we know that the Kleene algebra axioms are satisfied, as languages over alphabet $\mathcal{P}_{n}(\Sigma)$ with $1=\{\varepsilon\}$ and $0=\emptyset$ form a Kleene algebra.

For the semilattice axioms, note that $S$ is isomorphic to $\mathcal{P}_{n}(\Sigma)$ (by sending a singleton set in $S$ to its sole element), and that the latter forms a semilattice when equipped with $\cup$. Since the isomorphism between $S$ and $\mathcal{P}_{n}(\Sigma)$ respects these operators, it follows that $(S,\times)$ is also a semilattice.

The first SKA axiom that we check is commutativity. We prove that $\times$ on synchronous strings is commutative by induction on the paired length of the strings. Consider synchronous strings $u$ and $v$. For the base, where $u$ and $v$ equal $\varepsilon$, the result is immediate. In the induction step, we take $u=xu^{\prime}$ with $x\in\mathcal{P}_{n}(\Sigma)$. If $v=\varepsilon$ we are done immediately. Now for the case $v=yv^{\prime}$ with $y\in\mathcal{P}_{n}(\Sigma)$. We have $u\times v=(xu^{\prime})\times(yv^{\prime})=(x\cup y)\cdot(u^{\prime}\times v^{\prime})$. From the induction hypothesis we know that $u^{\prime}\times v^{\prime}=v^{\prime}\times u^{\prime}$. Combining this with commutativity of union we have $u\times v=(x\cup y)\cdot(v^{\prime}\times u^{\prime})=v\times u$. Take synchronous languages $K$ and $L$. Now consider $w\in K\times L$. This means that $w=u\times v$ for $u\in K$ and $v\in L$. From commutativity of synchronous strings we know that $w=u\times v=v\times u$. And thus we have $w\in L\times K$. The other inclusion is analogous.

It is obvious that the axioms $K\times\emptyset=\emptyset$ and $K\times\{\varepsilon\}=K$ are satisfied.

For associativity we again first argue that $\times$ on synchronous strings is associative. Take synchronous strings $u,v$ and $w$. We will show by induction on the paired length of $u,v$ and $w$ that $u\times(v\times w)=(u\times v)\times w$. If $u,v,w=\varepsilon$ the result is immediate. Now consider $u=xu^{\prime}$ for $x\in\mathcal{P}_{n}(\Sigma)$. If $v$ or $w$ equals $\varepsilon$ the result is again immediate. Hence we consider the case where $v=yv^{\prime}$ and $w=zw^{\prime}$ for $y,z\in\mathcal{P}_{n}(\Sigma)$. From the induction hypothesis we know that $u^{\prime}\times(v^{\prime}\times w^{\prime})=(u^{\prime}\times v^{\prime})\times w^{\prime}$. We can therefore derive

[TABLE]

From associativity of union, we then know that $(x\cup(y\cup z))\cdot((u^{\prime}\times v^{\prime})\times w^{\prime})=(u\times v)\times w$. Now consider $t\in K\times(L\times J)$ for $K,L$ and $J$ synchronous languages. Thus $t=u\times(v\times w)$ for $u\in K$, $v\in L$ and $w\in J$. From associativity of synchronous strings we know that $t=u\times(v\times w)=(u\times v)\times w$, and thus we have $t\in(K\times L)\times J$. The other inclusion is analogous.

For distributivity consider $w\in K\times(L+J)$ for $K,L,J$ synchronous languages. This means that $w=u\times v$ for $u\in K$ and $v\in L+J$. Thus we know $v\in L$ or $v\in J$. We immediately get that $u\times v\in K\times L$ or $u\times v\in K\times J$ and therefore that $w\in K\times L+K\times J$. The other direction is analogous.

For the synchrony axiom we take synchronous languages $K,L$ and $A,B\in S$. Suppose $A=\{x\}$ and $B=\{y\}$ for $x,y\in\mathcal{P}_{n}(\Sigma)$. Take $w\in(A\cdot K)\times(B\cdot L)$. This means that $w=u\times v$ for $u\in A\cdot K$ and $v\in B\cdot L$. Thus we know that $u=xu^{\prime}$ with $u^{\prime}\in K$ and $v=yv^{\prime}$ with $v^{\prime}\in L$. From this we conclude $w=u\times v=(xu^{\prime})\times(yv^{\prime})=(x\cup y)\cdot(u^{\prime}\times v^{\prime})$. As $u^{\prime}\in K$ and $v^{\prime}\in L$ and $x\cup y=x\times y$ with $x\in A$ and $y\in B$, we have that $w\in(A\times B)\cdot(K\times L)$. For the other direction, consider $w\in(A\times B)\cdot(K\times L)$. This entails $w=t\cdot v$ for $t\in A\times B$ and $v\in K\times L$. As $A\times B=\{x\cup y\}$ we have $t=x\cup y$. And $v=u\times s$ for $u\in K$ and $s\in L$. Thus $t\cdot v=(x\cup y)\cdot(u\times s)=(xu)\times(ys)$ for $u\in K$, $s\in L$, $x\in A$ and $y\in B$. Hence $w\in(A\cdot K)\times(B\cdot L)$.∎

See 3

Proof

This is proved by induction on the construction of $\equiv_{\scriptscriptstyle\mathsf{SKA}}$. In the base case we need to check all the axioms generating $\equiv_{\scriptscriptstyle\mathsf{SKA}}$, which we have already done for 2. For the inductive step, we need to check the closure rules for congruence preserve soundness. This is all immediate from the definition of the semantics of SKA and the induction hypothesis. For instance, if $e=e_{0}+e_{1}$, $f=f_{0}+f_{1}$, $e_{0}\equiv_{\scriptscriptstyle\mathsf{SKA}}f_{0}$ and $e_{1}\equiv_{\scriptscriptstyle\mathsf{SKA}}f_{1}$, then $\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}+\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket f_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}+\llbracket f_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket f\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$, where use that $\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket f_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$ and $\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket f_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$ as a consequence of the induction hypothesis.

See 4

Proof

For the first inclusion, take $w\in\llbracket a^{*}\times a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\times\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$. Thus we have $w=u\times v$ for $u,v\in\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$. Hence $u=x_{1}\cdots x_{n}$ for $x_{i}\in\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$ and $v=y_{1}\cdots y_{m}$ for $y_{i}\in\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$. As $\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SKA}}=\{\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}\}$ with $\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}\in\mathcal{P}_{n}(\Sigma)$, we know that $x_{i}=\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}$ and $y_{i}=\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}$. Assume that $n\leq m$ without loss of generality. We then know that $v=u\cdot\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}^{m-n}$, where synchronous string $e^{n}$ indicates $n$ copies of string $e$ concatenated. Unrolling the definition of $\times$ on words, we find $u\times v=u\times(u\cdot\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}^{k})=(u\times u)\cdot\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}^{k}=u\cdot\llbracket a\rrbracket_{\scriptscriptstyle\mathsf{SL}}^{k}=v$, and hence $w=u\times v=v\in\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$. For the other inclusion, take $w\in\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$. As $\varepsilon\in\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$ and $w\times\varepsilon=w$, we immediately have $w\in\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\times\llbracket a^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}$.∎

Lemma 15

For $K,L\in\mathcal{L}_{s}$, $K$ a non-empty finite language and $L$ an infinite language, $K\times L$ is an infinite language.

Proof

Suppose that $K\times L$ is a finite language. Hence we have an upper bound on the length of words in $K\times L$. Since the length of the synchronous product of two words is obviously the maximum of the length of the operands, this means we also have an upper bound on the length of words in $L$, and as we have finite words over a finite alphabet in $L$ this means that $L$ is finite. Hence we get a contradiction, thus $K\times L$ is infinite.

See 5

Proof

In the main text we treated one of the least fixpoint axioms and the synchrony axiom, and here we will treat all the remaining cases. For the sake of brevity, for each axiom we omit the cases where we can appeal to the proof for (synchronous) regular languages.

The proof that $(S,\times)$ is a semilattice is the same as in 2. Next, we take a look at the Kleene algebra axioms. If $K\in\mathcal{L}_{s}$, then $K+\emptyset=\emptyset$ holds by definition of union of sets. If $K=\dagger$, we get $\dagger+\emptyset=\dagger$, and the axiom also holds.

For $K\in\mathcal{L}_{s}\cup\{\dagger\}$, the axiom $K+K=K$ also easily holds by definition of the plus operator. Same for $K\cdot\{\varepsilon\}=K=K\cdot\{\varepsilon\}$ and $K\cdot\emptyset=\emptyset=\emptyset\cdot K$ by definition of the operator for sequential composition.

It is easy to see the axioms $1+e\cdot e^{*}\equiv_{\scriptscriptstyle\mathsf{SKA}}e^{*}$ and $1+e^{*}\cdot e\equiv_{\scriptscriptstyle\mathsf{SKA}}e^{*}$ hold for $K\in\mathcal{L}_{s}$. In case $K=\dagger$, for $1+e\cdot e^{*}\equiv_{\scriptscriptstyle\mathsf{SKA}}e^{*}$ we have

[TABLE]

and a similar derivation for $1+e^{*}\cdot e\equiv_{\scriptscriptstyle\mathsf{SKA}}e^{*}$.

For the commutativity of $+$ we take $K,L\in\mathcal{L}_{s}\cup\{\dagger\}$. If $K=\dagger$ or $L=\dagger$, we have $K+L=\dagger=L+K$.

For associativity of the plus operator we take $K,L,J\in\mathcal{L}_{s}\cup\{\dagger\}$. If any of $K$, $L$ or $J$ is $\dagger$, it is easy to see the axiom holds.

For associativity of the sequential composition operator, consider $K,L,J\in\mathcal{L}_{s}\cup\{\dagger\}$. We first can observe that if one of $K$, $L$ or $J$ is empty, then the equality holds trivially. Otherwise, if one of $K$, $L$ and $J$ is $\dagger$, then $(K\cdot L)\cdot J=\dagger=K\cdot(L\cdot J)$.

Next, we verify distributivity of concatenation over $+$. We will show a detailed proof for left-distributivity only; right-distributivity can be proved similarly. Let $K,L,J\in\mathcal{L}_{s}\cup\{\dagger\}$. If one of $K$, $L$, or $J$ is empty, then the claim holds immediately (the derivation is slightly different for $K$ versus $L$ or $J$). Otherwise, if one of $K$, $L$ or $J$ is $\dagger$, then $K\cdot(L+J)=\dagger=K\cdot L+K\cdot J$.

For the remaining least fixpoint axiom, let $K,L,J\in\mathcal{L}_{s}\cup\{\dagger\}$. Assume that $K+L\cdot J\leq L$. We need to prove that $K\cdot J^{*}\leq L$. If $L=\dagger$, then the claim holds immediately. If $L\in\mathcal{L}_{s}$ and $J=\dagger$, then $L$ must be empty, hence $K$ is empty, and the claim holds. If $L,J\in\mathcal{L}_{s}$, then also $K\in\mathcal{L}_{s}$ and the proof goes through as it does for KA.

We now get to the axioms for the $\times$-operator. The commutativity axiom is obvious from the commutative definition of $\times$ (as we already know that $\times$ is commutative on synchronous strings). The axiom $K\times\emptyset=\emptyset$ is also satisfied by definition. The same holds for the axiom $K\times\{\varepsilon\}=K$ as $\{\varepsilon\}$ is finite.

For associativity of the synchronous product, consider $K,L,J\in\mathcal{L}_{s}\cup\{\dagger\}$. If one of $K$, $L$ or $J$ is empty, then both sides of the equation evaluate to $\emptyset$. Otherwise, if one of $K$, $J$, or $L$ is $\dagger$, then both sides of the equation evaluate to $\dagger$. If $K$, $J$ and $L$ are all languages, and at most one of them is finite, then either $K\times L=\dagger$, in which case the left-hand side evaluates to $\dagger$, or $K\times L$ is infinite (by 15) and $J=\dagger$, in which case the right-hand side evaluates to $\dagger$ again. The right-hand side can be shown to evaluate to $\dagger$ by a similar argument. In the remaining cases (at least two out of $K$, $J$ and $L$ are finite languages and none of them is $\dagger$ or $\emptyset$), the proof of associativity for the language model applies.

For distributivity of synchronous product over $+$, let $K,L,J\in\mathcal{L}_{s}\cup\{\dagger\}$. If one of $K$, $L$ or $J$ is $\emptyset$, then the proof is straightforward. Otherwise, if one of $K$, $L$ or $J$ is $\dagger$, then both sides evaluate to $\dagger$. If $K$ and $L+J$ are infinite, then the outcome is again $\dagger$ on both sides (note that $L+J$ being infinite implies that either $L$ or $J$ is infinite). In the remaining cases, $K$, $L$ and $J$ are languages and either $K$ or $L+J$ (hence $L$ and $J$) is finite. In either case the proof for synchronous regular languages goes through. ∎

See 6

Proof

We need to verify each of the axioms of $\mathsf{SF}_{1}$. The proof for the axioms of $\mathsf{F}_{1}$ is immediate via the observation that synchronous languages over the alphabet $\Sigma$ are simply languages over the alphabet $\mathcal{P}_{n}(\Sigma)$. Thus we know that the $\mathsf{F}_{1}$-axioms are satisfied, as languages over alphabet $\mathcal{P}_{n}(\Sigma)$ with $1=\{\varepsilon\}$ and $0=\emptyset$ form an $\mathsf{F}_{1}$-algebra. The additional axioms are the same as the ones that were added to KA for SKA, and we know they are sound from 3. ∎

See 7

Proof

We prove the first statement by induction on the structure of $e$. In the base, if we have $e\in\{0,1\}$, the claim holds vacuously. If we have $a\in\Sigma$, then $\rho(a)=\{1,a\}$ and $\delta(a,A)=\{1:A=\{a\}\}$, so the claim follows. For the inductive step, there are five cases to consider.

• •

If $e=H(e_{0})$, then immediately $\delta(H(e_{0}),A)=\emptyset$ so the claim holds vacuously.

• •

If $e=e_{0}+e_{1}$, then by induction we have $\delta(e_{0},A)\subseteq\rho(e_{0})$ and $\delta(e_{1},A)\subseteq\rho(e_{1})$. Hence, we find that $\delta(e,A)=\delta(e_{0},A)\cup\delta(e_{1},A)\subseteq\rho(e_{0})\cup\rho(e_{1})=\rho(e)$.

• •

If $e=e_{0}\cdot e_{1}$, then by induction we have $\delta(e_{0},A)\subseteq\rho(e_{0})$ and $\delta(e_{1},A)\subseteq\rho(e_{1})$. Hence, we can calculate that

[TABLE]

• •

If $e=e_{0}\times e_{1}$, then by induction we have $\delta(e_{0},A)\subseteq\rho(e_{0})$ and $\delta(e_{1},A)\subseteq\rho(e_{1})$ for all $A\in\mathcal{P}_{n}(\Sigma)$. Hence, we can calculate that

[TABLE]

• •

If $e=e_{0}^{*}$, then by induction we have $\delta(e_{0},A)\subseteq\rho(e_{0})$. Hence, we find that

[TABLE]

For the second statement, we prove that if $e^{\prime}\in\rho(e)$, then $\rho(e^{\prime})\subseteq\rho(e)$. The result of the first part tells us that $\delta(e^{\prime},A)\subseteq\rho(e^{\prime})$, which together with $\rho(e^{\prime})\subseteq\rho(e)$ proves the claim. We proceed by induction on $e$. In the base, there are two cases to consider. First, if $e=0$, then the claim holds vacuously. If $e=1$, then the only $e^{\prime}\in\rho(e)$ is $e^{\prime}=1$, so the claim holds. If $e=a$ for $a\in\Sigma$, we have $\rho(e)=\{1,a\}$. It trivially holds that $\rho(e^{\prime})\subseteq\rho(e)$ for $e^{\prime}\in\rho(e)$.

For the inductive step, there are four cases to consider.

• •

If $e=H(e_{0})$, then $\rho(e)=\{1\}$, and the proof is as in the case where $e=1$.

• •

If $e=e_{0}+e_{1}$, assume w.l.o.g. that $e^{\prime}\in\rho(e_{0})$. By induction, we derive that

[TABLE]

• •

If $e=e_{0}\cdot e_{1}$ then there are two cases to consider.

• –

If $e^{\prime}=e_{0}^{\prime}\cdot e_{1}$ where $e_{0}^{\prime}\in\rho(e_{0})$, then we calculate

[TABLE]

• –

If $e^{\prime}\in\rho(e_{1})$, then by induction we have $\rho(e^{\prime})\subseteq\rho(e_{1})\subseteq\rho(e)$.

• •

If $e=e_{0}\times e_{1}$ then there are three cases to consider.

• –

The first case is $e^{\prime}=e_{0}^{\prime}\times e_{1}^{\prime}$ where $e_{0}^{\prime}\in\rho(e_{0})$ and $e_{1}^{\prime}\in\rho(e_{1})$, we get $\rho(e_{0}^{\prime})\subseteq\rho(e_{0})$ and $\rho(e_{1}^{\prime})\subseteq\rho(e_{1})$ by induction. We calculate

[TABLE]

• –

For $e^{\prime}\in\rho(e_{0})$, then by induction we have $\rho(e^{\prime})\subseteq\rho(e_{0})\subseteq\rho(e)$.

• –

For $e^{\prime}\in\rho(e_{1})$, the argument is similar to the previous case.

• •

If $e=e_{0}^{*}$, then either $e^{\prime}=1$ or $e^{\prime}=e_{0}^{\prime}\cdot e_{0}^{*}$ for some $e_{0}^{\prime}\in\rho(e_{0})$. In the former case, $\rho(e^{\prime})=\{1\}\subseteq\rho(e)$. In the latter case, we find by induction that

[TABLE]

See 9

Proof

As $e\in\overline{\mathcal{T}_{\mathsf{SL}}}$ we have that $e=\overline{e_{0}}$ for some $e_{0}\in\mathcal{T}_{\mathsf{SL}}$. From 8 we know that $\overline{e_{0}}\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}e_{0}$. So we get $e\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}e_{0}$. Again from 8 we then know that $\overline{e}=\overline{e_{0}}=e$.∎

Lemma 16

For $x,y\in{(\mathcal{P}_{n}(\Sigma))}^{*}$, we have ${(x\cdot y)}^{\Pi}=x^{\Pi}\cdot y^{\Pi}$.

Proof

We proceed by induction on the lenth of $xy$. In the base, we have $xy=\varepsilon$. Thus $x=\varepsilon$ and $y=\varepsilon$. We have $\varepsilon^{\Pi}=\varepsilon$ so the result follows immediately. In the inductive step we consider $xy=aw$ for $a\in\mathcal{P}_{n}(\Sigma)$. We have to consider two cases. In the first case we have $x=ax^{\prime}$. The induction hypothesis gives us that ${(x^{\prime}\cdot y)}^{\Pi}=x^{\prime\Pi}\cdot y^{\Pi}$. We then have ${(x\cdot y)}^{\Pi}={(ax^{\prime}\cdot y)}^{\Pi}=a^{\Pi}\cdot{(x^{\prime}\cdot y)}^{\Pi}=a^{\Pi}\cdot x^{\prime\Pi}\cdot y^{\Pi}=x^{\Pi}\cdot y^{\Pi}$. In the second case we have $x=\varepsilon$ and $y=aw$. We then conclude that ${(x\cdot y)}^{\Pi}=y^{\Pi}=x^{\Pi}\cdot y^{\Pi}$.∎

See 10

Proof

1. (i)

First, suppose $w\in{(L\cup K)}^{\Pi}$. Thus we have $w=v^{\Pi}$ for $v\in L\cup K$. This gives us $v\in L$ or $v\in K$. We assume the former without loss of generality. Thus we know $w=v^{\Pi}\in L^{\Pi}$. Hence we know $w\in L^{\Pi}\cup K^{\Pi}$. The other direction can be proved analogously. 2. (ii)

First, suppose $w\in{(L\cdot K)}^{\Pi}$. Thus we have $w=v^{\Pi}$ for some $v\in L\cdot K$. This gives us $v=v_{1}\cdot v_{2}$ for some $v_{1}\in L$ and some $v_{2}\in K$. By definition of ${(-)}^{\Pi}$ we know that $v_{1}^{\Pi}\in L^{\Pi}$ and $v_{2}^{\Pi}\in K^{\Pi}$. Thus we have $v_{1}^{\Pi}\cdot v_{2}^{\Pi}\in L^{\Pi}\cdot K^{\Pi}$. From 16 we know that $w=v^{\Pi}={(v_{1}\cdot v_{2})}^{\Pi}=v_{1}^{\Pi}\cdot v_{2}^{\Pi}$, which gives us the desired result of $w\in L^{\Pi}\cdot K^{\Pi}$. The other direction can be proved analogously. 3. (iii)

Take $w\in{(L^{*})}^{\Pi}$. Thus we have $w=v^{\Pi}$ for some $v\in L^{*}$. By definition of the star of a synchronous language we know that $v=u_{1}\cdots u_{n}$ for $u_{i}\in L$. As $u_{i}\in L$, we have $u_{i}^{\Pi}\in L^{\Pi}$ and $u_{1}^{\Pi}\cdots u_{n}^{\Pi}\in{(L^{\Pi})}^{*}$. By 16, we know that $w=v^{\Pi}={(u_{1}\cdots u_{n})}^{\Pi}=u_{1}^{\Pi}\cdots u_{n}^{\Pi}$. Thus we have $w\in{(L^{\Pi})}^{*}$, which is the desired result. The other direction can be proved analogously. ∎

See 6.1

Proof

Here we treat the inductive cases not displayed in the main proof, where we treated only the synchronous case.

• •

If $e=H(e_{0})$, derive:

[TABLE]

• •

If $e=e_{0}+e_{1}$, derive:

[TABLE]

• •

If $e=e_{0}\cdot e_{1}$, derive:

[TABLE]

• •

If $e=e_{0}^{*}$, we derive:

[TABLE]

See 12

Proof

In the main text we have treated the base cases. The inductive cases work as follows. There are three cases to consider. If $e=e_{0}+e_{1}$, then ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}={(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\cup\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}={(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}\cup{(\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}$ (10). From the induction hypothesis we obtain ${(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$ and ${(\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$. Combining these results we get ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{KA}}\cup\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{KA}}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{KA}}+\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{KA}}=\llbracket e_{0}+e_{1}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$, so the claim follows. Secondly, if $e=e_{0}\cdot e_{1}$, then ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}={(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}}\cdot\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}={(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}\cdot{(\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}$ (10). From the induction hypothesis we obtain ${(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$ and ${(\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$. We can then conclude that ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{KA}}\cdot\llbracket e_{1}\rrbracket_{\scriptscriptstyle\mathsf{KA}}=\llbracket e_{0}\cdot e_{1}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$. Lastly, if $e=e_{0}^{*}$, we get ${(\llbracket e_{0}^{*}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}={({(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{*})}^{\Pi}={({(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi})}^{*}$ (10). From the induction hypothesis we obtain ${(\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$. Thus we have ${(\llbracket e\rrbracket_{\scriptscriptstyle\mathsf{SKA}})}^{\Pi}=\llbracket e_{0}\rrbracket_{\scriptscriptstyle\mathsf{KA}}^{*}=\llbracket e_{0}^{*}\rrbracket_{\scriptscriptstyle\mathsf{KA}}$ and the claim follows.∎

See 14

Proof

We will construct $x$ by induction on the size of $Q$. In the base, let $Q=\emptyset$. In this case the unique $Q$-vector is a solution. In the inductive step, take $k\in Q$ and let $Q^{\prime}=Q\setminus\{k\}$. Then construct the $Q^{\prime}$-linear system $(M^{\prime},p^{\prime})$ as follows:

[TABLE]

As $Q^{\prime}$ is a strictly smaller set than $Q$ and $M^{\prime}$ is guarded, we can apply our induction hypothesis to $(M^{\prime},p^{\prime})$. So we know by induction that $(M^{\prime},p^{\prime})$ has a unique solution $x^{\prime}$. Moreover, if $M^{\prime}$ and $p^{\prime}$ are in normal form, so is $x^{\prime}$; note that if $M$ and $p$ are in normal form, then so are $M^{\prime}$ and $p^{\prime}$.

We use $x^{\prime}$ to construct the $Q$-vector $x$:

[TABLE]

The first thing to show now is that $x$ is indeed a solution of $(M,p)$. To this end, we need to show that $M\cdot x+p\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}x$. We have two cases. For $i\in Q^{\prime}$ we derive:

[TABLE]

For $i=k$, we derive:

[TABLE]

We now know that $x$ is a solution to $(M,p)$ because $M\cdot x+p\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}x$. Furthermore, if $M$ and $p$ are in normal form, then so is $x^{\prime}$, and thus $x$ is in normal form by construction.

Next we claim that $x$ is unique. Let $y$ be any solution of $(M,p)$. We choose the $Q^{\prime}$-vector $y^{\prime}$ by taking $y^{\prime}(i)=y(i)$. To see that $y^{\prime}$ is a solution to $(M^{\prime},p^{\prime})$, we first claim that the following holds:

[TABLE]

To see that this is true, derive

[TABLE]

Note that we can apply the unique fixpoint axiom because we know that $M$ is guarded and thus that $H(M(k,k))=0$.

Now we can derive the following:

[TABLE]

Thus $y^{\prime}$ is a solution to $(M^{\prime},p^{\prime})$. As $x^{\prime}$ is the unique solution to $(M^{\prime},p^{\prime})$, we know that $y^{\prime}\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}x^{\prime}$.

For $i\neq k$ we know that $x(i)=x^{\prime}(i)\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}y^{\prime}(i)=y(i)$. For $i=k$ we can derive:

[TABLE]

Thus, $y\equiv_{\scriptscriptstyle\mathsf{SF}_{1}}x$, thereby proving that $x$ is the unique solution to $(M,p)$. ∎