Right-Linear Lattices

$\omega$-automata, i.e. finite state machines running on infinite inputs, are useful for modelling behaviour of systems that are not expected to terminate, such as hardware, operating systems and control systems. The prototypical $\omega$-automaton model, Büchi automaton, is widely used in model checking [30, 15, 14, 17].

The theory of $\omega$-regular languages, i.e. languages accepted by $\omega$-automata, have been studied for more than half a century. Büchi’s famous complementation theorem [7] for his automata is the engine underlying his proof of the decidability of monadic second-order logic (MSOL) over infinite words. Its extension to infinite trees, Rabin’s Tree Theorem [24], is often referred to as the “mother of all decidability results”.

McNaughton [23] showed that, while Büchi automata could not be determinised per se, a naturally larger class of acceptance conditions (Muller or parity) allowed such determinisation, a highly technical result later improved by Safra [26]. A later relaxation was the symmetrisation of the transition relation itself: instead of only allowing non-deterministic states, allow co-nondeterministic ones too. This has led to beautiful accounts of $\omega$-regular language theory via the theory of positional and finite memory games. The resulting computational model, alternating parity automaton (APA), is now the go-to model in textbook presentations, e.g. [16]. Indeed, their features more closely mimic those of logical settings where such symmetries abound, e.g. linear-time $\mu$-calculus [29] and MSOL over infinite words.

In the world of finite words, the theory of regular languages have been axiomatised as Kleene Algebras ($\mathrm{𝖪𝖠}$s). In fact, $\mathrm{𝖪𝖠}$s are part of a bigger cohort of regular algebras and they have been studied for several decades and completeness proofs for different variants have been obtained [27, 21, 20, 3, 4]. $\mathrm{𝖪𝖠}$s and various extensions have found applications in specification and verification of programs and networks [1].

Note that $\mathrm{𝖪𝖠}$s and other regular algebras axiomatise the equational theory of regular expressions. An alternative (and arguably more faithful) notation for NFAs may be given by identifying them with right-linear grammars. Recall that a right-linear grammar is a CFG where each production has RHS either $aX$ or $\epsilon$. They may also be written as right-linear expressions, by choosing an order for resolving non-terminals. Formally, right-linear expressions (aka RLA expressions), written $e,f,\mathrm{\dots }$, are generated by:

for $a\in 𝒜$, a finite alphabet and $X\in 𝒱$, a countable set of variables. Indeed [10] takes this viewpoint seriously and proposed an alternative algebraic foundation of regular language theory, via right-linear algebras ($\mathrm{𝖱𝖫𝖠}$s). Notably, $\mathrm{𝖱𝖫𝖠}$s are strictly more general than $\mathrm{𝖪𝖠}$s, as they lack any multiplicative structure. In particular, this means that $\omega$-languages naturally form a model of them (unlike $\mathrm{𝖪𝖠}$s). This is the starting point of the current work.

In this work, we investigate the algebraic structures induced by the theory of APAs. To do so, we dualise the (1-free)¹¹1This restriction imposed to so that the intended interpretation is over $\omega$-words only, not $\le \omega$-words. syntax of RLA expressions to obtain right-linear lattice (RLL) expressions, formally generated by:

Compared to RLA expressions, RLL expressions enjoy more symmetric relationships to games and consequently, are a notation for APAs. Our main contribution is a sound and complete axiomatisation ${\mathrm{𝖱𝖫𝖫}}_{ℒ}$ of the theory of RLL expressions for the language model.

Two kinds of variations of $\mathrm{𝖪𝖠}$s are relevant to this work. Firstly, the generalisation of regular algebras to $\omega$-regular algebras [31, 8, 22, 9], by axiomatising the theory of $\omega$-regular expressions, a generalisation of regular expressions admitting terms of the form $e^{\omega }$. Secondly, following the idea of dualisation from $\mathrm{𝖪𝖠}$s leads to action lattices, an extension with meet (dual to the sum), and residuals (adjoint to the product). Since $\mathrm{𝖱𝖫𝖠}$ does not have products we do not consider residuals, – so perhaps Kleene lattices [6, 12], the extension of $\mathrm{𝖪𝖠}$s with meet is the closest cousin of our proposed right-linear lattices.

In Section 2, we recall right-linear algebras and define RLL expressions, a notation for APAs. We identify several principles governing their behaviour in the standard model $ℒ$ of $\omega$-languages; namely, their interpretations satisfy a theory of bounded distributive lattices, certain lattice homomorphisms and least and greatest fixed points (of definable operators). In Section 3 recover a syntactic form of complements, and we present our ultimate axiomatisation in Section 4. In Section 5, we prove the completeness of the axiomatisation by reducing it to the completeness of linear time $\mu$-calculus. We conclude with some remarks on the axiomatisation and comparison with existing literature in Section 6. Further examples and detailed proofs can be found in an accompanying preprint [11].

RLL expressions, written $e,f,\mathrm{\dots }$, are generated by:

for $a\in 𝒜$ and $X\in 𝒱$. We usually just write $ae$ instead of $a\cdot e$. A variable $X$ is said to occur freely in an expression $e$ if it not under the scope of any binder $\mu X$ or $\nu X$. An expression is said to be closed if it has no occurrences of free variables.

The intended interpretation of an RLL expression is a language of $\omega$-words over $𝒜$.

Note that Remark 1 is justified by this interpretation: indeed $ℒ(\mu XX)$ is just the empty language. Furthermore:

To justify that $\mu$ and $\nu$ are indeed interpreted as fixed point operators, we will first recall some terminology. For $(S,{⩽}_S)$ a complete lattice, $x\in S$ is a prefixed (postfixed respectively) point of a map $f:S\to S$ if $f(x){⩽}_{S}x$ ($x{⩽}_{S}f(x)$ respectively). If $x$ is both a pre and postfixed point, it is called a fixed point of $f$.

Let us now point out that $𝒫({𝒜}^{\omega })$ indeed forms a complete lattice under $\subseteq$, and closed under concatenation with letters on the left. Since all the operations are monotone, $ℒ(\mu Xe(X))$ and $ℒ(\nu Xe(X))$ are indeed the least and greatest fixed points, respectively, of the operation $A\mapsto ℒ(e(A))$, by the Knaster-Tarski theorem.

As the reader might have expected, the range of $ℒ(\cdot )$ is just the $\omega$-regular languages.

One direction, exhaustion of all $\omega$-regular languages, follows swiftly from the inductive definition of the set of all $\omega$-regular languages and was established in previous work [10], without making use of $\cap$. One way to prove the converse is to introduce a game-theoretic mechanism for deciding word membership in $ℒ(e)$. This was introduced in [10] without $\cap$ and can be straightforwardly lifted to our setting. We will illustrate with an example.

Let us take a moment to remark upon some principles valid in the intended interpretation $ℒ$ of RLL expressions, in order to motivate the axiomatisation we introduce later. As usual we write $e\le f$ for $e+f=f$, equivalently $e=e\cap f$ (so in $ℒ$, $\le$ just means $\subseteq )$. First:

• $\mathrm{■}$

  $(0,\top ,+,\cap )$ forms a bounded distributive lattice:²²2Some of these axioms are redundant, but we include them all to facilitate the exposition.

  (1)

• $\mathrm{■}$

  Each $a\in 𝒜$ is a (lower) semibounded lattice homomorphism:

  (2)

In particular, of course $ℒ\vDash ̸a\top =\top$, so in this sense $0$ and $\top$ do not behave dually in $ℒ$. Instead we have a variant of this principle, indicating that the homomorphisms freely factor the structure:

• $\mathrm{■}$

  The ranges of $a\in 𝒜$ partition the domain:

  (3)

Finally, $ℒ$ is a complete lattice and so interprets the least and greatest fixed points as such. Being a complete lattice is a second-order property, but we have the following first order (even quasi-equational) consequences:

• $\mathrm{■}$

  $\mu Xe(X)$ is a least prefixed point of $X\mapsto e(X)$:

  (4)

• $\mathrm{■}$

  $\nu Xe(X)$ is a greatest postfixed point of $X\mapsto e(X)$:

  (5)

Note that Induction and Coinduction are axiom schemas, as one might expect (e.g. as in Peano Arithmetic).

The principles above also suffice to derive some basic properties of the operators defined by RLL expressions:

As an immediate corollary of functoriality, we have:

Recall that RLA expressions are notation for NFAs and thus can be duly interpreted as regular languages over finite words. In previous work [10] we showed soundness and completeness of a subset of the above mentioned axioms for RLA expressions with respect to the language interpretation (also written $ℒ$ hedging the risk of confusion). Writing $\mathrm{𝖱𝖫𝖠}$ for the subset of axioms from Equations 1, 2, 3, 4, and 5 not involving $\cap ,\top ,\nu$, we have:

The goal of the present work is to establish a similar sort of result for RLL expressions, in the $\omega$-regular world rather than the (finitely) regular world.

We can define complements of the RLL expressions, wrt $ℒ$, quite simply, thanks to closure of the syntax under duality:

Thus the set of RLL expressions denote a Boolean subalgebra of $ℒ$, a fact subsumed by adequacy for $\omega$-regular languages, Proposition 6. Of course duality of $+,\cap$ hold in any bounded distributive lattice. The homomorphism axioms also guarantee that our definition of ${(ae)}^c$ is well-behaved:

However, the issue with the principles thusfar, Equations 1, 2, 3, 4, and 5, is that they do not guarantee such duality of $\mu$ and $\nu$. Let us address this issue now.

Not all models of Equations 1, 2, 3, 4, and 5 interpret $e$ and $e^c$ as complements. Indeed it is well known that there are even completely distributive lattices, let alone models of Equations 1, 2, 3, 4, and 5, that are not even Heyting algebras, let alone Boolean algebras. Still, this does not quite yet give unprovability of the complementary laws for closed expressions (which carve out a substructure of a model). Indeed in even complete distributive lattices $\mu$ and $\nu$ are at least dual, in the sense that they preserve complements. Let us develop an appropriate counterexample, exploiting the incompleteness of the lattice structure:

The issue for Equations 1, 2, 3, 4, and 5, towards completeness for $ℒ$, is that, in the absence of completeness of the lattice, it is not immediately clear that $\mu$ and $\nu$ are dual. Duality is derivable for $+$ and $\cap$ from Equation 1, but the infinitary nature of the fixed points means that it does not follow as a consequence of Equations 1, 2, 3, 4, and 5.

Linear temporal logic ($\mathrm{𝖫𝖳𝖫}$) is a modal logic with modalities referring to time. In $\mathrm{𝖫𝖳𝖫}$, one can encode formulas about the future of paths. In particular, we have formulas of the form $○\phi$ and $\phi 𝐔\psi$ that are (informally) interpreted as “at the next time step $\phi$ holds” and “$\phi$ holds until $\psi$ holds.” Naturally they are interpreted over discrete linear orders.

We can construe $\phi 𝐔\psi$ as a fixed point $\nu X(\psi \vee (\phi \wedge ○X))$. Generalising this idea leads to $\mu \mathrm{𝖫𝖳𝖫}$, the extension of $\mathrm{𝖫𝖳𝖫}$ with arbitrary fixed points.

We shall write $P,Q,\mathrm{\dots }$ for propositional symbols. $\mu \mathrm{𝖫𝖳𝖫}$ formulas, written $\phi ,\psi ,\mathrm{\dots }$, are generated by:

Formulas are interpreted over infinite words. To this end, we shall assume that the propositional symbols $P,Q,\mathrm{\dots }$ are from some finite set $𝐏$, and henceforth fix an alphabet $𝒜=𝒫(𝐏)$.

$\mu \mathrm{𝖫𝖳𝖫}$ enjoys a sound and complete axiomatisation, due to Kaivola [18] (see also [13]). To recast this axiomatisation in the current logical basis, let us point out that we can extend negation to all $\mu \mathrm{𝖫𝖳𝖫}$ formulas by defining $\overline{\phi }$ exploiting De Morgan duality of $\perp ,\top$ and $\vee ,\wedge$ and $\mu ,\nu$, and finally self-duality of $○$: $\overline{○\phi }:=○\overline{\phi }$. Therefore, we may freely use other propositional connectives such as $\neg ,\to ,\leftrightarrow$ as suitable macros. The following axiomatisation is equivalent to that of [18], only adapted to our negation normal syntax.

Note that the self-duality of $○$, semantically, is reflected in the axioms too, with $○$ distributing over both $\wedge$ and $\vee$.

Our aim is to reduce the completeness of ${\mathrm{𝖱𝖫𝖫}}_{ℒ}$ to that of $\mu \mathrm{𝖫𝖳𝖫}$. For this reason we need to embed ${\mathrm{𝖱𝖫𝖫}}_{ℒ}$ into $\mu \mathrm{𝖫𝖳𝖫}$.

We need to show that the translation above is faithful wrt. the two semantics we have presented, for RLL expressions and for $\mu \mathrm{𝖫𝖳𝖫}$ formulas. Writing $ℒ(\phi ):=\{\sigma \vDash \phi \}$ for closed $\mu \mathrm{𝖫𝖳𝖫}$ formulas $\phi$, we have:

To prove this, we must first address the fact that our two semantics interpret syntax as different types of sets, and duly have different types of constant symbols. To this end, let us temporarily introduce into the language of $\mu \mathrm{𝖫𝖳𝖫}$ a constant symbol $A$ for each language $A\subseteq {𝒜}^{\omega }$. We extend the definition of ${-}^{\circ }$ by the clause $A^{\circ }:=A$ and duly extend the definition of ${-}^{\sigma }$ by the clause $A^{\sigma }:=\{n\in \omega :{\sigma }^n\in A\}$ where ${\sigma }^n$ is the $n$^th tail of $\sigma$, i.e. we set ${\sigma }^0:=\sigma$, and ${\sigma }^{n+1}$ to be the tail of ${\sigma }^n$. Now we can establish a sort of substitution lemma that relates our two semantics:

In order to leverage the completeness of $\mu \mathrm{𝖫𝖳𝖫}$ within ${\mathrm{𝖱𝖫𝖫}}_{ℒ}$, we need to simulate its reasoning, for which we must embed $\mu \mathrm{𝖫𝖳𝖫}$ back into ${\mathrm{𝖱𝖫𝖫}}_{ℒ}$. As mentioned at the beginning of this section, a key component here is our recovery of syntactic complements, Proposition 20, allowing for Boolean reasoning on RLL expressions in ${\mathrm{𝖱𝖫𝖫}}_{ℒ}$.

We can again establish the adequacy of this interpretation, though this time we need a syntactic result rather than a semantic one: