# Kleene Algebra with Dynamic Tests: Completeness and Complexity

Igor Sedlár  The Czech Academy of Sciences, Institute of Computer Science
Pod Vodárenskou věží 271/2, Prague, The Czech Republic

###### Abstract

We study versions of Kleene algebra with dynamic tests, that is, extensions of
Kleene algebra with domain and antidomain operators. We show that Kleene
algebras with tests and Propositional dynamic logic correspond to special
cases of the dynamic test framework. In particular, we establish completeness
results with respect to relational models and guarded-language models, and we
show that two prominent classes of Kleene algebras with dynamic tests have an
$\mathrm{EXPTIME}$-complete equational theory.

##  1 Introduction

Kleene algebra with tests ($\mathsf{KAT}$) is a well-known algebraic framework
for equational reasoning about program equivalence and correctness [15, 17].
$\mathsf{KAT}$ adds to Kleene algebra ($\mathsf{KA}$) [14] a Boolean algebra
of tests together with a negation operator that applies only to tests. Various
extensions of $\mathsf{KA}$ and $\mathsf{KAT}$ with more general (double)
negation operators were considered in [2, 3, 4, 5], for example. These
operators include the antidomain operator, related to dynamic negation of
Dynamic Predicate Logic [9], and the domain operator, equivalent to double
antidomain. Intuitively, both operators form tests out of programs — or
dynamic tests — where the antidomain (domain) of a program is the test if the
program diverges (halts).

In contrast to $\mathsf{KA}$ and $\mathsf{KAT}$, completeness and complexity
results for their extensions with dynamic tests are largely
missing.111However, already [6] note that the equational theory of “separable”
$\mathsf{KAT}$ with domain is $\mathrm{EXPTIME}$-complete. Our result is
stronger since it does not hinge on separability. We fill this gap by proving
relational completeness and (parametrized) guarded-language completeness
results for $\mathsf{dKA}$ ($\mathsf{KA}$ with domain), $\mathsf{aKA}$
($\mathsf{KA}$ with both domain and antidomain), $\mathsf{dKAT}$
($\mathsf{KAT}$ with domain) and $\mathsf{aKAT}$ ($\mathsf{KAT}$ with both
domain and antidomain), and $\mathrm{EXPTIME}$-completeness results for
$\mathsf{aKAT}$ and $\mathsf{aKA}$.

A central role in our results is played by $\mathsf{aKAT}$, which can be seen
as an algebraic counterpart of Propositional Dynamic Logic ($\mathsf{PDL}$)
[7, 10], providing a one-sorted alternative to two-sorted Dynamic algebras
[13, 22, 23] or Test algebras [26]. $\mathsf{KA}$, $\mathsf{KAT}$ and their
extensions with dynamic tests can all be seen as syntactic fragments of
$\mathsf{aKAT}$. Hence, our completeness results for $\mathsf{aKAT}$ yield
similar results for other extensions for free. The close relation of
$\mathsf{aKAT}$ and $\mathsf{PDL}$ is used to establish the
$\mathrm{EXPTIME}$-completeness result for the former. We show, in addition,
that $\mathsf{aKA}$ has a distinguished position in the family in the sense
that all the other members, including $\mathsf{aKAT}$, embed into
$\mathsf{aKA}$. This shows that $\mathsf{aKA}$ is $\mathrm{EXPTIME}$-complete
as well.

This paper is an extended version of the conference paper [24]. The main
result of the conference paper is the $\mathrm{EXPTIME}$-completeness result
for $\mathsf{aKA}$, established by constructing a mutual embedding between
$\mathsf{aKA}$ and the equational theory of Relational test algebras
($\mathsf{RTA}$) studied by Marco Hollenberg [12]. Hollenberg’s completeness
result for $\mathsf{RTA}$ is a crucial lemma in [24]. Another result reported
in [24] is that the equational theory of $\mathsf{aKA}$ coincides with the
equational theory of ∗-continuous $\mathsf{aKA}$. The proofs in [24] also show
that the equational theory of $\mathsf{aKA}$ coincides with the equational
theory of relational $\mathsf{aKA}$, although this is not noted in the paper.
The present paper bypasses $\mathsf{RTA}$ and applies Hollenberg’s relational
completeness proof strategy directly to $\mathsf{aKAT}$, obtaining a
(parametrized) guarded-language completeness result for $\mathsf{aKAT}$ along
the way. Hollenberg’s strategy is also somewhat simplified here. The scope of
the present paper is also more general than those of [12] and [24]. We also
strengthen the following relational completeness results: (i) Bochman and
Gabbay [1] formulate a sequent system (generalizing Kozen and Tiuryn’s [18]
substructural logic of partial correctness $\mathsf{S}$) that is sound and
complete with respect to a fragment of the equational theory of relational
$\mathsf{aKAT}$, (ii) Hollenberg [11] gives an axiomatization of the
equational theory of ∗-free relational $\mathsf{aKAT}$, and (iii) McLean [20]
(based on the work of Mbacke [19]) establishes a relational completeness
result for ∗-free relational $\mathsf{dKA}$.

The rest of the paper is organized as follows. Section 2 introduces Kleene
algebras with dynamic tests, with focus on languages and equational theories.
Section 3 introduces relational models for the language of Kleene algebras
with dynamic tests and Section 4 notes that $\mathsf{aKAT}$, the strongest
version of Kleene algebra with dynamic tests we consider, is “$\mathsf{PDL}$
in disguise”. Section 5 discusses models based on guarded strings and Section
6 proves the language completeness result. Relational completeness is
established in Section 7, along with the corollary that the equational theory
of $\mathsf{aKAT}$ is $\mathrm{EXPTIME}$-complete. Section 8 discusses
completeness for syntactic fragments of the equational theory of
$\mathsf{aKAT}$ and proves an $\mathrm{EXPTIME}$-completeness result for
$\mathsf{aKA}$. The final section concludes the paper and points out some
interesting problems for future research.

##  2 Dynamic tests

In this section we introduce Kleene algebras with dynamic tests. In
particular, we discuss their language and some of its fragments (Sect. 2.1)
and we define a congruence on the language that represents their equational
theory (Sect. 2.2).

###  2.1 Languages

Let $\Sigma$ be an “action alphabet” and $\Pi$ a “propositional alphabet”,
disjoint from $\Sigma$. For the sake of simplicity, both alphabets are assumed
to be countably infinite. Both alphabets will be fixed throughout the paper.

######  Definition 1.

The set $\mathbb{E}$ of  regular expressions with dynamic tests (over $\Sigma$
and $\Pi$) is defined by the following grammar:

$e,f:=\mathtt{a}\in\Sigma\mid\mathtt{p}\in\Pi\mid\mathtt{0}\mid\mathtt{1}\mid
e+f\mid e\cdot f\mid e^{\bot}\mid e^{\top}\mid e^{*}$

We will often refer to regular expressions with dynamic tests just as
expressions. Our definition of an expression uses the regular operators $+$
(sum), $\cdot$ (multiplication, concatenation) and $\,{}^{*}$ (Kleene star),
together with constants $\mathtt{0}$ (zero, annihilator) and $\mathtt{1}$
(one, multiplicative identity). The dynamic test operators are $\,{}^{\bot}$
(antidomain) and $\,{}^{\top}$ (domain). For technical reasons explained
shortly, we take both as primitive.222We diverge from the notation used in the
literature. In some papers on Kleene algebra with domain, e.g. [5], antidomain
is denoted as a in prefix notation and domain as d. Desharnais et al. [2] use
$\ulcorner$ in prefix notation for domain and in [3] they use $\delta$. We
consider $\,{}^{\bot}$ and $\,{}^{\top}$ to be a better fit with the Kleene
algebra tradition, and a good choice when it comes to comparisons with
$\mathsf{PDL}$. The notation $\,{}^{\bot}$ for antidomain is also related to
the interpretation of antidomain in terms of divergence – recall that $\bot$
is sometimes used as a symbol denoting the “absurd state” to which all the
diverging computations lead. We will see in the next section that $\Sigma$ and
$\Pi$ will have different semantics: while $\Sigma$ will be seen a set of
atomic actions, $\Pi$ will be seen as a set of atomic propositions.

######  Definition 2.

The set $\mathbb{F}$ of  formulas (over $\Sigma$ and $\Pi$) is defined by the
following grammar:

$\phi,\psi:=\mathtt{p}\in\Pi\mid\mathtt{0}\mid\mathtt{1}\mid\phi+\psi\mid\phi\cdot\psi\mid
e^{\bot}\mid e^{\top}\,,$

where $e\in\mathbb{E}$.

The notion of a  subexpression is defined as expected. A  subformula of an
expression $e$ is a subexpression of $e$ which is also a formula. Let
$\mathrm{Sf}(e)$ be the set of subformulas of $e\in\mathbb{E}$ and let
$\mathrm{Sf}(E)=\bigcup_{e\in E}\mathrm{Sf}(e)$. For
$\Gamma\subseteq\mathbb{E}$, we define $\Gamma^{\bot}=\\{e^{\bot}\mid
e\in\Gamma\\}$ and $\Gamma^{\pm}=\Gamma\cup\Gamma^{\bot}$.

######  Definition 3.

An expression $e\in\mathbb{E}$ is  testable iff it does not contain
occurrences of $\,{}^{\top}$. A  test is an expression $e^{\top}$ where $e$ is
testable. A  parameter is either a test or an element of $\Pi$.

Note that every test (parameter) is a formula and if $\phi$ is a test
(parameter) then $\phi^{\bot}$ is not a test (parameter).

######  Definition 4.

Various  fragments of $\mathbb{E}$ are defined in Figure 1:
$\mathbb{E}_{\mathsf{K}}$ is the smallest set of expressions that contains the
base as a subset, is closed under the regular operators, and

  * •

contains $e^{\top}$ if $e$ is in the set indicated under $\top$

  * •

contains $e^{\bot}$ if $e$ is in the set indicated under $\bot$

We assume that $\Phi$ is a set of parameters extending $\Pi$. A
$\mathsf{K}$-expression is any $e\in\mathbb{E}_{\mathsf{K}}$.

$\mathsf{K}$ |  Base |  $\top$ |  $\bot$
---|---|---|---
$\mathsf{KA}$ |  $\Sigma$ |  $\emptyset$ |  $\emptyset$
$\mathsf{KA}(\Phi)$ |  $\Sigma\cup\Phi$ |  $\emptyset$ |  $\emptyset$
$\mathsf{dKA}$ |  $\Sigma$ |  $\mathbb{E}_{\mathsf{dKA}}$ |  $\emptyset$
$\mathsf{aKA}$ |  $\Sigma$ |  $\mathbb{E}_{\mathsf{aKA}}$ |  $\mathbb{E}_{\mathsf{aKA}}$
$\mathsf{KAT}$ |  $\Sigma\cup\Pi$ |  $\emptyset$ |  $\Pi$
$\mathsf{KAT}(\Phi)$ |  $\Sigma\cup\Phi$ |  $\emptyset$ |  $\Phi$
$\mathsf{dKAT}$ |  $\Sigma\cup\Pi$ |  $\mathbb{E}_{\mathsf{dKAT}}$ |  $\Pi$
$\mathsf{aKAT}$ |  $\Sigma\cup\Pi$ |  $\mathbb{E}_{\mathsf{aKAT}}$ |  $\mathbb{E}_{\mathsf{aKAT}}$

$\mathsf{KA}$$\mathsf{KA}(\Phi)$$\mathsf{KAT}$$\mathsf{KAT}(\Phi)$$\mathsf{dKA}$$\mathsf{aKA}$$\mathsf{dKAT}$$\mathsf{aKAT}$

Figure 1: Fragments of the language of regular expressions with dynamic tests.

These fragments can be seen as being defined by a restricted version of the
grammar defining $\mathbb{E}$. For instance, $\mathbb{E}_{\mathsf{dKA}}$ is
defined by the grammar

$e,f:=\mathtt{a}\in\Sigma\mid\mathtt{0}\mid\mathtt{1}\mid e+f\mid e\cdot f\mid
e^{\top}\mid e^{*}$

whereas $\mathsf{KAT}(\Phi)$ is defined by (recall that
$\Phi^{\pm}=\Phi\cup\\{e^{\bot}\mid e\in\Phi\\}$)

$e,f:=\mathtt{a}\in\Sigma\mid f\in\Phi^{\pm}\mid\mathtt{0}\mid\mathtt{1}\mid
e+f\mid e\cdot f\mid e^{*}$

The set $\mathbb{E}_{\mathsf{KA}(\Phi)}$ can be seen as the set of regular
expressions over $\Sigma\cup\Phi$. Similarly,
$\mathbb{E}_{\mathsf{KAT}(\Phi)}$ can be seen as the set of regular
expressions over $\Sigma\cup\Phi^{\pm}$. We will sometimes denote the former
as $\mathbb{RE}(\Phi)$ and the latter as $\mathbb{RE}(\Phi^{\pm})$. It can be
shown that all fragments $\mathbb{E}_{\mathsf{K}}$ as well as
$\mathbb{RE}(\Phi^{\pm})$ admit a well-defined complexity measure allowing
proofs by structural induction.333In the case of $\mathbb{RE}(\Psi)$ for
$\Psi\in\\{\Phi,\Phi^{\pm}\\}$, we may define
$Co:\mathbb{RE}(\Psi)\to\mathbb{N}$ such that $Co(\mathtt{a})=Co(\phi)=0$ for
$\mathtt{a}\in\Sigma$ and $\phi\in\Psi$, and
$Co(\sharp(e_{1},\ldots,e_{n}))=1+\sum_{i\leq n}Co(e_{i})$ for
$\sharp\in\\{\mathtt{0},\mathtt{1},+,\cdot,\,^{*}\\}$. This works since
$\sharp\notin\\{\top,\bot\\}$.

$\mathsf{KA}$-expressions are regular expressions over $\Sigma$, and
$\mathsf{KAT}$-expressions are a variant of the expressions used in Kleene
algebra with tests [15]. In our formulation, negation (antidomain) applies
only to atomic propositions $\mathtt{p}\in\Pi$. Since propositions (tests)
form a Boolean algebra in $\mathsf{KAT}$, we can do without negations of
complex Boolean formulas. $\mathsf{KA}(\Phi)$-expressions and
$\mathsf{KAT}(\Phi)$-expressions will serve a technical role in our proofs
later. $\mathsf{dKAT}$-expressions provide a fitting language for “Kleene
algebras with domain” of [6, 21, 3], also called “modal Kleene algebras” in
[2]. $\mathsf{dKA}$-expressions are a language for “Kleene algebras with
domain” as defined in [4, 5] (which may also be called “domain Kleene
algebras” based on the terminology used in these two papers), and
$\mathsf{aKA}$-expressions are a language for “Boolean domain Kleene algebras”
as defined in [4, 5] (called “Kleene algebras with domain” in [25] and
“antidomain Kleene algebras” in [8]).

Expressions of the full $\mathsf{aKAT}$-language inherit from
$\mathsf{KAT}$-expressions the ability to represent basic imperative
programming constructs. The constant $\mathtt{1}$ represents the program skip
(“do nothing”), $\mathtt{0}$ represents abort (“abort computation”) and
multiplication corresponds to sequential composition of programs (one may read
$e\cdot f$ as “do $e$ and, after it terminates, do $f$”). Conditionals and
while loops can be represented as follows:

${\textbf{if }}\phi{\textbf{ then }}e{\textbf{ else }}f\text{ as }(\phi\cdot
e)+(\phi^{\bot}\cdot f)\qquad{\textbf{while }}\phi{\textbf{ do }}e\text{ as
}(\phi\cdot e)^{*}\cdot\phi^{\bot}$

As we shall see in the next section, it is natural to read $e^{\bot}$ as the
statement “program $e$ diverges” and $e^{\top}$ as “program $e$ halts”. Hence,
$\mathsf{aKAT}$ is able to represent imperative programs where conditions in
conditionals and while loops refer to halting or divergence of other programs.

######  Definition 5.

A set of parameters $\Gamma$ is  Fischer–Ladner closed (FL-closed) iff

  * •

$\mathtt{p}^{\top}\in\Gamma$ only if $\mathtt{p}\in\Gamma$

  * •

$\mathtt{1}^{\top},\mathtt{0}^{\top}\in\Gamma$

  * •

$(\phi+\psi)^{\top}\in\Gamma$ only if $\phi^{\top}\in\Gamma$ and
$\psi^{\top}\in\Gamma$

  * •

$(\phi\cdot\psi)^{\top}\in\Gamma$ only if $\phi^{\top}\in\Gamma$ and
$\psi^{\top}\in\Gamma$

  * •

$(e^{*})^{\top}\in\Gamma$ only if $e^{\top}\in\Gamma$

  * •

if $e\neq(f\cdot\mathtt{1})$, then $e^{\top}\in\Gamma$ only if
$(e\cdot\mathtt{1})^{\top}\in\Gamma$

  * •

$e^{\bot\top}\in\Gamma$ only if $(e\cdot\mathtt{1})^{\top}\in\Gamma$

  * •

$((e+f)\cdot\phi)^{\top}$ only if $(e\cdot f)^{\top}\in\Gamma$ and
$(f\cdot\phi)^{\top}\in\Gamma$

  * •

$((e\cdot f)\cdot\phi)^{\top}\in\Gamma$ only if $(f\cdot\phi)^{\top}\in\Gamma$
and $(e\cdot(f\cdot\phi)^{\bot\bot})^{\top}\in\Gamma$

  * •

$(e^{*}\cdot\phi)^{\top}\in\Gamma$ only if
$(e\cdot(e^{*}\cdot\phi)^{\bot\bot})^{\top}\in\Gamma$

The  Fischer–Ladner closure (FL-closure) of a set of tests $\Gamma$ is the
smallest Fischer–Ladner closed $\Gamma^{\prime}\supseteq\Gamma$.

We note that the FL-closure of a finite set of tests is a finite set of tests.

###  2.2 Equational theory

This section defines the equational theory of Kleene algebras with dynamic
tests. Syntactic fragments of the equational theory corresponding to the
language fragments from the previous subsection are also discussed.

######  Definition 6.

Let $\equiv$ be the smallest congruence $\equiv$ on $\mathbb{E}$ such that

$\displaystyle(e\cdot f)\cdot g$ $\displaystyle\equiv e\cdot(f\cdot g)$ (1)
$\displaystyle e\cdot\mathtt{1}$ $\displaystyle\equiv e\equiv\mathtt{1}\cdot
e$ (2) $\displaystyle(e+f)+g$ $\displaystyle\equiv e+(f+g)$ (3)
$\displaystyle\mathtt{0}+e$ $\displaystyle\equiv\mathtt{0}\equiv e+\mathtt{0}$
(4) $\displaystyle e$ $\displaystyle\equiv e+e$ (5) $\displaystyle
e\cdot(f+g)$ $\displaystyle\equiv(e\cdot f)+(e\cdot g)$ (6)
$\displaystyle(e+f)\cdot g$ $\displaystyle\equiv(e\cdot g)+(f\cdot g)$ (7)
$\displaystyle\mathtt{1}+(e\cdot e^{*})$ $\displaystyle\leqq e^{*}$ (8)
$\displaystyle\mathtt{1}+(e^{*}\cdot e)$ $\displaystyle\leqq e^{*}$ (9)
$\displaystyle f+(e\cdot g)\leqq g$ $\displaystyle\implies e^{*}\cdot f\leqq
g$ (10) $\displaystyle f+(g\cdot e)\leqq g$ $\displaystyle\implies f\cdot
e^{*}\leqq g$ (11) $\displaystyle e^{\bot}\cdot e$
$\displaystyle\equiv\mathtt{0}$ (12) $\displaystyle(e\cdot f)^{\bot}$
$\displaystyle\equiv(e\cdot f^{\top})^{\bot}$ (13) $\displaystyle
e^{\bot}+e^{\top}$ $\displaystyle\equiv\mathtt{1}$ (14)
$\displaystyle\mathtt{p}^{\top}$ $\displaystyle\equiv\mathtt{p}$ (15)
$\displaystyle e^{\top}$ $\displaystyle\equiv e^{\bot\bot}$ (16)

for all $e,f\in\mathbb{E}$ and $\mathtt{p}\in\Pi$, where $e\leqq f$ means
$e+f\equiv f$. If $e\equiv f$, the we will often say that $e$ and $f$ are
equivalent .

######  Proposition 1.

The following hold:

$\displaystyle e^{\bot\top}$ $\displaystyle\equiv e^{\bot}$ (17)
$\displaystyle\mathtt{1}^{\bot}$ $\displaystyle\equiv\mathtt{0}$ (18)
$\displaystyle\mathtt{0}^{\bot}$ $\displaystyle\equiv\mathtt{1}$ (19)
$\displaystyle(e+f)^{\top}$ $\displaystyle\equiv e^{\top}+f^{\top}$ (20)
$\displaystyle(e^{\top}\cdot f)^{\top}$ $\displaystyle\equiv e^{\top}\cdot
f^{\top}$ (21) $\displaystyle e^{\top}\cdot e$ $\displaystyle\equiv e$ (22)
$\displaystyle(e^{*})^{\top}$ $\displaystyle\equiv\mathtt{1}$ (23)
$\displaystyle e\cdot f^{\top}\equiv\mathtt{0}$ $\displaystyle\iff e\cdot
f\equiv\mathtt{0}$ (24) $\displaystyle\phi\cdot\bar{\phi}$
$\displaystyle\equiv\mathtt{0}$ (25) $\displaystyle\phi+\bar{\phi}$
$\displaystyle\equiv\mathtt{1}$ (26) $\displaystyle\bar{\bar{\phi}}$
$\displaystyle\equiv\phi$ (27) $\displaystyle\phi\cdot e\equiv\mathtt{0}$
$\displaystyle\iff\phi\leqq e^{\bot}$ (28) $\displaystyle\phi\cdot\phi$
$\displaystyle\equiv\phi$ (29) $\displaystyle\phi\cdot\psi$
$\displaystyle\equiv\psi\cdot\phi$ (30) $\displaystyle\phi^{\top}$
$\displaystyle\equiv\phi$ (31) $\displaystyle(e\cdot\phi)^{\top}\leqq\phi$
$\displaystyle\implies(e^{*}\cdot\phi)^{\top}\leqq\phi$ (32)
$\displaystyle\phi\leqq(e\cdot\phi^{\bot})^{\bot}$
$\displaystyle\implies\phi\leqq(e^{*}\cdot\phi^{\bot})^{\bot}$ (33)

###### Proof.

(32) is established as follows. We show first that

$e\cdot\phi\leqq\phi\cdot(e\cdot\phi)\implies
e^{*}\cdot\phi\leqq\phi\cdot(e^{*}\cdot\phi)$ (34)

First, note that $\phi\leqq\phi\cdot\mathtt{1}\cdot\phi\leqq\phi\cdot
e^{*}\cdot\phi$. Second, $e\cdot\phi\leqq\phi\cdot(e\cdot\phi)$ entails
$e\cdot\phi\leqq\phi\cdot e$, and so we have
$e\cdot\phi\cdot(e^{*}\cdot\phi)\leqq\phi\cdot((e\cdot e^{*})\cdot\phi)$,
which entails $e\cdot\phi\cdot(e^{*}\cdot\phi)\leqq\phi\cdot(e^{*}\cdot\phi)$
by (9). By combining these two observations, we obtain

$e\cdot\phi\leqq\phi\cdot(e\cdot\phi)\implies\phi+e\cdot(\phi\cdot(e^{*}\cdot\phi))\leqq\phi\cdot(e^{*}\cdot\phi)$

Then, using (10) we obtain (34). We then proceed as follows. If
$(e\cdot\phi)^{\top}\leq\phi$, then
$(e\cdot\phi)^{\top}\cdot(e\cdot\phi)\leqq\phi\cdot(e\cdot\phi)$ and so
$e\cdot\phi\leqq\phi\cdot(e\cdot\phi)$ by (22). Using (34) we obtain
$e^{*}\cdot\phi\leqq\phi\cdot(e^{*}\cdot\phi)$, which yields
$e^{*}\cdot\phi\leqq\phi\cdot e^{*}$. Using monotonicity of $\top$ and (13),
we infer $(e^{*}\cdot\phi)^{\top}\leqq(\phi\cdot(e^{*})^{\top})^{\top}$ which
entails our goal $(e^{*}\cdot\phi)^{\top}\leqq\phi$ by (23) and (31). (33)
follows from (32).444I am grateful to Damien Pous for a suggestion on which
this proof is based. ∎

It is clear from (16) that every expression is equivalent to a testable
expression. Let $e?:=f^{\top}$ where $f$ is obtained from $e$ by replacing
every occurrence of $\top$ by $\bot\bot$. Let $\mathrm{St}(e)=\\{f?\mid
f\in\mathrm{Sf}(e)\\}$ and $\mathrm{St}(E)=\bigcup_{e\in E}\mathrm{St}(e)$.

In what follows, we will use the notation
$e\overset{\scriptscriptstyle\mathsf{K}}{\equiv}f$ to indicate that
$e,f\in\mathbb{E}_{\mathsf{K}}$ and $e\equiv f$. The following is immediate:

######  Observation 1.

$e\overset{\scriptscriptstyle\mathsf{K}}{\equiv}f\implies e\equiv f$ for all
fragments $\mathsf{K}$.

We note that $\overset{\scriptscriptstyle\mathsf{aKA}}{\equiv}$ clearly
coincides with the equational theory of “Boolean domain Kleene algebras” as
defined in [4, 5] (called “Kleene algebras with domain” in [25] and
“antidomain Kleene algebras” in [8]).

##  3 Relational models

This section discusses the relational semantics for regular expressions with
dynamic tests.

######  Definition 7.

A  relational model (for $\Sigma$ and $\Pi$) is a structure $M=\langle
X,\mathsf{rel}_{M},\mathsf{sat}_{M}\rangle$ where $X$ is a set,
$\mathsf{rel}_{M}:\Sigma\to 2^{X\times X}$ and $\mathsf{sat}_{M}:\Pi\to
2^{X}$.

The intuition behind the relational models is that elements of the action
alphabet $\Sigma$ express actions that are associated with state transitions
on a set of states $X$, and that elements of $\Pi$ express propositions
associated with sets of states. In particular, the fact that $\langle
x,y\rangle\in\mathsf{rel}_{M}(\mathtt{a})$ (or $x\xrightarrow{\mathtt{a}}y$ in
$M$, as we shall sometimes write) means that performing action $\mathtt{a}$ in
state $x$ may result in state $y$,555We do not assume that actions are
deterministic, that is, $\textsf{rel}_{M}(\mathtt{a})$ is not necessarily a
total function. and the fact that $x\in\textsf{sat}_{M}(\mathtt{p})$ means
that proposition $\mathtt{p}$ is satisfied (or true) in state $x$.

######  Definition 8.

For each relational model $M=\langle
X,\mathsf{rel}_{M},\mathsf{sat}_{M}\rangle$ (for $\Sigma$ and $\Pi$) we define
the  $M$-interpretation of $\mathbb{E}$ as the function
$\llbracket-\rrbracket_{M}:\mathbb{E}\to 2^{X\times X}$ such that:

$\displaystyle\llbracket\mathtt{a}\rrbracket_{M}=\mathsf{rel}_{M}(\mathtt{a})\qquad\llbracket\mathtt{p}\rrbracket_{M}=1_{\mathsf{sat}_{M}(\mathtt{p})}\qquad\llbracket\mathtt{0}\rrbracket_{M}=\emptyset\qquad\llbracket\mathtt{1}\rrbracket_{M}=1_{X}$
$\displaystyle\llbracket e+f\rrbracket_{M}=\llbracket
e\rrbracket_{M}\cup\llbracket f\rrbracket_{M}\qquad\llbracket e\cdot
f\rrbracket_{M}=\llbracket e\rrbracket_{M}\circ\llbracket f\rrbracket_{M}$
$\displaystyle\llbracket e^{*}\rrbracket_{M}=\left(\llbracket
e\rrbracket_{M}\right)^{*}=\bigcup_{n\geq 0}\llbracket e\rrbracket^{n}_{M}$
$\displaystyle\llbracket e^{\bot}\rrbracket_{M}=\mathsf{a}\left(\llbracket
e\rrbracket_{M}\right)=\bigcup_{R\subseteq 1_{X}}\left(R\circ\llbracket
e\rrbracket_{M}=\emptyset\right)$ $\displaystyle\llbracket
e^{\top}\rrbracket_{M}=\mathsf{d}\left(\llbracket
e\rrbracket_{M}\right)=1_{X}\setminus\mathsf{a}(\llbracket e\rrbracket_{M})$

where, for $R\subseteq 2^{X\times X}$, $R^{0}=1_{X}$ and $R^{n+1}=R^{n}\circ
R$. Expressions $e$ and $f$ are  relationally equivalent ) iff $\llbracket
e\rrbracket_{M}=\llbracket f\rrbracket_{M}$ for all $M$.

In other words,

$\llbracket e^{\bot}\rrbracket_{M}=\\{\langle x,x\rangle\mid\neg\exists
y\left(\langle x,y\rangle\in\llbracket
e\rrbracket_{M}\right)\\}\qquad\llbracket e^{\top}\rrbracket_{M}=\\{\langle
x,x\rangle\mid\exists y\left(\langle x,y\rangle\in\llbracket
e\rrbracket_{M}\right)\\}$

Hence, in the relational setting, the antidomain operator coincides with
dynamic negation studied in Dynamic Predicate Logic [9, 11]. If a program is
seen as a binary relation on $X$ and a proposition is seen as a subset of $X$
(or, equivalently, a subset of the identity relation on $X$), then the dynamic
test operators ⊤ and ⊥ turn programs into propositions. More specifically,
$R^{\top}$ is the proposition expressing the fact that $R$ halts: $x\in
R^{\top}$ iff there is $y$ such that $\langle x,y\rangle\in R$ (there is a
terminating computation of $R$ starting in $x$). Similarly, $R^{\bot}$ is the
proposition expressing the fact that $R$ diverges: $x\in R^{\bot}$ iff there
is no $y$ such that $\langle x,y\rangle\in R$ (there is no halting computation
of $R$ starting in $x$).

The following relational soundness result is easily verified. One of the tasks
of this paper is to prove the converse; see Sect.7.

######  Lemma 1 (Relational soundness).

For all $e,f\in\mathbb{E}$, if $e\equiv f$, then $\llbracket
e\rrbracket_{M}=\llbracket f\rrbracket_{M}$ for all relational $M$.

##  4 Complexity of deciding relational equivalence

In this section we point out the close relation between relational equivalence
and validity in Propositional Dynamic Logic ($\mathsf{PDL}$) [7, 10]. In fact,
$\mathsf{aKAT}$ can be seen as “$\mathsf{PDL}$ in disguise”. It follows from
our observations that the problem of deciding relational equivalence between
arbitrary expressions is $\mathrm{EXPTIME}$-complete.

It is easy to prove by induction on the structure of $\phi$ that
$\llbracket\phi\rrbracket_{M}\subseteq 1_{X}$ for all formulas $\phi$ and all
$M$. We will write

$(M,x)\vDash\phi\iff\langle x,x\rangle\in\llbracket\phi\rrbracket_{M}$

######  Observation 2.

For all $\phi$ and all $M$:

  1. 1.

$(M,x)\vDash\phi$ iff $\langle
x,x\rangle\in\llbracket\phi^{\top}\rrbracket_{M}$

  2. 2.

$(M,x)\not\vDash\mathtt{0}$ and $(M,x)\vDash\mathtt{1}$ for all $x$

  3. 3.

$(M,x)\vDash\phi^{\bot}$ iff $(M,x)\not\vDash\phi$

  4. 4.

$(M,x)\vDash\phi+\psi$ iff $(M,x)\vDash\phi$ or $(M,x)\vDash\psi$

  5. 5.

$(M,x)\vDash\phi\cdot\psi$ iff $(M,x)\vDash\phi$ and $(M,x)\vDash\psi$

  6. 6.

$(M,x)\vDash(e\cdot\phi)^{\bot\bot}$ iff there is $y$ such that $\langle
x,y\rangle\in\llbracket e\rrbracket_{M}$ and $(M,y)\vDash\phi$

  7. 7.

$(M,x)\vDash(e\cdot\phi^{\bot})^{\bot}$ iff for all $y$, $\langle
x,y\rangle\in\llbracket e\rrbracket_{M}$ implies that $(M,y)\vDash\phi$

Hence, we can write

$\displaystyle\phi?\quad$ $\displaystyle\text{instead of}\quad\phi^{\top}$
$\displaystyle\neg\phi\quad$ $\displaystyle\text{instead of}\quad\phi^{\bot}$
$\displaystyle\phi\land\psi\quad$ $\displaystyle\text{instead
of}\quad\phi\cdot\psi$ $\displaystyle\phi\lor\psi\quad$
$\displaystyle\text{instead of}\quad\phi+\psi$
$\displaystyle\scalebox{0.9}{{\textlangle}}e\scalebox{0.9}{{\textrangle}}\phi\quad$
$\displaystyle\text{instead of}\quad(e\cdot\phi)^{\bot\bot}$
$\displaystyle\scalebox{0.9}{{[}}e\scalebox{0.9}{{]}}\phi\quad$
$\displaystyle\text{instead of}\quad(e\cdot\phi^{\bot})^{\bot}$

and the expressions on the left hand side will have their usual semantics if
seen as expressions in the standard language of $\mathsf{PDL}$.

######  Theorem 1.

The problem of deciding relational equivalence between arbitrary expressions
is $\mathrm{EXPTIME}$-complete.

###### Proof.

Lower bound: It is shown in [10, Ch. 8.2] that the ($\mathrm{EXPTIME}$-hard)
membership problem for polynomial-space alternating Turing machines reduces to
the problem of satisfiability of PDL-formulas in relational models: For each
machine $A$ and input $t$, there is a PDL-formula $\mathsf{F}_{A,t}$ such that
$A$ accepts $t$ iff $\mathsf{F}_{A,t}$ is satisfiable, that is, iff there is
$M$ such that
$\llbracket\mathsf{F}_{A,t}\rrbracket_{M}\neq\llbracket\mathtt{0}\rrbracket_{M}$
iff $\mathsf{F}_{A,t}\not\equiv\mathtt{0}$ (by Theorem 4).

Upper bound: It is sufficient to show that for every $e\in\mathbb{E}$ there is
an equivalent $e^{\prime}$ in the fragment corresponding to programs of
$\mathsf{PDL}$ and that $e^{\prime}$ is polynomially computable from $e$. We
omit the tedious but straightforward details. It is known that the problem of
deciding (relational) equivalence between PDL-programs is in
$\mathrm{EXPTIME}$. ∎

We note that the the $\mathrm{EXPTIME}$-hardness proof does not automatically
carry over to fragments of the full language. We would need to check the
construction of $\mathsf{F}_{A,t}$ for arbitrary $A,t$ and determine if the
formula is guaranteed to belong to the given fragment. We leave this to future
work.

##  5 Language models

This section introduces some notions we will use in the language completeness
proof of Section 6. In particular, we formulate a generalization of the
guarded string model for Kleene algebra with tests where atoms are formed over
an arbitrary set of formulas, not necessarily a set of propositional letters
(Sect. 5.1). Then we introduce a variant of these models where atoms are
required to be consistent (Sect. 5.2).

###  5.1 Guarded languages and Kleene algebra with tests

Let $\Phi$ be a finite set of parameters which is ordered in some fixed but
arbitrary way as $\phi_{1},\ldots,\phi_{n}$ (all $\phi_{i}$ are assumed to be
mutually distinct). An  atom over $\Phi$ is a sequence
$\psi_{1}\ldots\psi_{n}$ where $\psi_{i}\in\\{\phi_{i},\phi_{i}^{\bot}\\}$.
The set of all atoms over $\Phi$ is denoted as $\mathbb{A}(\Phi)$ and atoms
are denoted by capital letters $G,H$ etc. If $\phi\in\Phi$ and
$G\in\mathbb{A}(\Phi)$ then we will write

$G\triangleleft\phi\quad\text{ iff}\quad\phi\text{ occurs in }G$

It is easily seen that $G\triangleleft\phi^{\bot}$ iff not
$G\triangleleft\phi$, for all $\phi\in\Phi$ and $G\in\mathbb{A}(\Phi)$, since
if $\phi$ is a parameter, then $\phi^{\bot}$ is not a parameter.

A  guarded string over $\Phi$ is any sequence of the form

$G_{1}\mathtt{a}_{1}G_{2}\ldots\mathtt{a}_{n-1}G_{n}$

where each $G_{i}\in\mathbb{A}(\Phi)$ and $\mathtt{a}_{j}\in\Sigma$. The set
of all guarded strings over $\Phi$ is denoted as $\mathbb{GS}(\Phi)$.  Fusion
product is a partial binary operation on $\mathbb{GS}(\Phi)$ defined as
follows:

$xG\diamond Hy=\begin{cases}xGy&G=H\\\ \text{undefined}&G\neq H\end{cases}$

Fusion product is lifted to  $\Phi$-guarded languages
$K,L\subseteq\mathbb{GS}(\Phi)$ as expected: $L\diamond K=\\{w\diamond u\mid
w\in L\And u\in K\\}$. Lifted fusion product is a total operation on guarded
languages.

######  Definition 9.

The  algebra of $\Phi$-guarded languages is

$\mathbf{GL}(\Phi)=\langle
2^{\mathbb{GS}(\Phi)},2^{\mathbb{A}(\Phi)},\cup,\,\diamond,\,^{*},\,^{\bot},\,^{\top},\emptyset,\mathbb{A}(\Phi)\rangle$

where $K^{*}=\bigcup_{n\geq 0}K^{n}$ (assuming that $K^{0}=\mathbb{A}(\Phi)$
and $K^{n+1}=K^{n}\diamond K$) and

$L^{\bot}=\\{G\in\mathbb{A}(\Phi)\mid\\{G\\}\diamond L=\emptyset\\}\qquad
L^{\top}=\\{G\in\mathbb{A}(\Phi)\mid\\{G\\}\diamond L\neq\emptyset\\}\,.$

As a special case, an atom over $\emptyset$ is the empty sequence $\epsilon$,
and so $\mathbb{GS}(\emptyset)=\Sigma^{*}$. Fusion product on
$\mathbb{GS}(\emptyset)$ reduces to concatenation of strings over
$\Sigma^{*}$. $\mathbf{GL}(\emptyset)$ is an expansion of the algebra of
formal languages over $\Sigma$ with $\,{}^{\bot}$ that sends every non-empty
language to $\emptyset$ and $\emptyset$ to $\\{\epsilon\\}$ and $\,{}^{\top}$
that sends every non-empty language to $\\{\epsilon\\}$ and $\emptyset$ to
$\emptyset$. Algebras of guarded languages as used in Kleene algebra with
tests [15, 17] are a special case where $\Phi$ is a finite subset of $\Pi$.

######  Definition 10.

If $\Phi$ is a finite set of parameters, then the  standard
$\Phi$-interpretation of $\mathbb{RE}(\Phi^{\pm})$ is the unique homomorphism
$[-]_{\Phi}:\mathbb{RE}(\Phi^{\pm})\to\mathbf{GL}(\Phi)$ such that

$[\mathtt{a}]_{\Phi}=\\{G\mathtt{a}H\mid
G,H\in\mathbb{A}(\Phi)\\}\qquad\quad[\phi]_{\Phi}=\\{G\mid
G\in\mathbb{A}(\Phi)\And G\triangleleft\phi\\}$

for $\mathtt{a}\in\Sigma$ and $\phi\in\Phi^{\pm}$.

In the next section we will use a variant of Kozen and Smith’s language
completeness result for Kleene algebras with tests [17]:

######  Theorem 2 (Essentially Kozen and Smith [17]).

Let $\Phi$ be a finite set of parameters. For all
$e,f\in\mathbb{E}_{\mathsf{KAT}(\Phi)}$,

$e\overset{\scriptscriptstyle\mathsf{KAT}(\Phi)}{\equiv}f\iff[e]_{\Phi}=[f]_{\Phi}$

Note that Theorem 2 and Observation 1 imply a form of language completeness,
namely,

$[e]_{\Gamma}=[f]_{\Gamma}\implies e\equiv f$

for all $e,f\in\mathbb{RE}(\Gamma^{\pm})\subseteq\mathbb{E}$. The problem with
this result is that it is not accompanied by a suitable soundness result.
Since both $\mathtt{a}$ and $\mathtt{a}^{\bot}$ are testable, both
$\mathtt{a}^{\top}$ and $\mathtt{a}^{\bot\top}$ are tests and
$\mathtt{a^{\top}}\mathtt{a}^{\bot\top}\in\mathbb{A}\left(\Gamma\right)$ for
$\Gamma=\\{\mathtt{a^{\top}},\mathtt{a}^{\bot\top}\\}$. Hence,
$[\mathtt{a^{\top}}\cdot\mathtt{a}^{\bot\top}]_{\Gamma}\neq\emptyset$ even if
$\mathtt{a^{\top}}\cdot\mathtt{a}^{\bot\top}\equiv\mathtt{0}$. We have to pay
attention to consistency of atoms. Moreover the standard interpretation of the
action alphabet is an issue too:
$\mathtt{a}^{\bot}\cdot\mathtt{a}\equiv\mathtt{0}$, but
$[\mathtt{a}^{\bot}\cdot\mathtt{a}]_{\Gamma}=\\{G\mathtt{a}H\mid
G\triangleleft\mathtt{a}^{\bot}\\}\neq\emptyset$.

###  5.2 Algebras of consistently guarded languages

We will not distinguish between a non-empty sequence of expressions
$e_{1}\ldots e_{n}$ and the expression $e_{1}\cdot\ldots\cdot e_{n}$ (assuming
some fixed bracketing). An atom $G$ is  consistent iff
$G\not\equiv\mathtt{0}$. The set of all consistent atoms over $\Phi$ will be
denoted as $\mathbb{C}(\Phi)$. A  consistently guarded string over $\Phi$ is
any guarded string $G_{1}\mathtt{a_{1}}\ldots\mathtt{a}_{n-1}G_{n}$ where all
$G_{i}\in\mathbb{C}(\Phi)$. The set of all consistently guarded strings over
$\Phi$ is denoted as $\mathbb{CS}(\Phi)$.666Hollenberg [12] uses the same
notation for consistent guarded strings. Note that a guarded string can be
consistently guarded without being consistent. A crucial role in the proof of
language completeness in the next section will be played by the following
variant of $\mathbf{GL}(\Phi)$, based on $\mathbb{CS}(\Phi)$:

######  Definition 11.

The  algebra of consistently $\Phi$-guarded languages is

$\mathbf{CL}(\Phi)=\langle
2^{\mathbb{CS}(\Phi)},2^{\mathbb{C}(\Phi)},\cup,\,\diamond,\,^{*},\,^{\bot},\,^{\top},\emptyset,\mathbb{C}(\Phi)\rangle$

where $K^{*}=\bigcup_{n\geq 0}K^{n}$ (assuming that $K^{0}=\mathbb{C}(\Phi)$
and $K^{n+1}=K^{n}\diamond K$) and

$L^{\bot}=\\{G\in\mathbb{C}(\Phi)\mid\\{G\\}\diamond L=\emptyset\\}\qquad
L^{\top}=\\{G\in\mathbb{C}(\Phi)\mid\\{G\\}\diamond L\neq\emptyset\\}\,.$

Note that $\mathbf{CL}(\Phi)$ is in general not a subalgebra of
$\mathbf{GL}(\Phi)$ since $\mathbb{A}(\Phi)$, the multiplicative identity of
$\mathbf{GL}(\Phi)$, is not necessarily an element of $\mathbf{CL}(\Phi)$.
However, clearly $\mathbb{CS}(\Phi)\subseteq\mathbb{GS}(\Phi)$.

######  Definition 12.

Let $\Gamma$ be a set of tests. The  canonical $\Gamma$-interpretation of
$\mathbb{E}$ is the unique homomorphism
$\llbracket-\rrbracket:\mathbb{E}\to\mathbf{CL}(\Gamma)$ such that

$\llbracket\mathtt{a}\rrbracket_{\Gamma}=\\{G\mathtt{a}H\in\mathbb{CS}(\Gamma)\mid
G\mathtt{a}H\not\equiv\mathtt{0}\\}\qquad\quad\llbracket\mathtt{p}\rrbracket_{\Gamma}=\\{G\mid
G\in\mathbb{C}(\Gamma)\And G\leqq\mathtt{p}\\}$

for all $\mathtt{a}\in\Sigma$ and $\mathtt{p}\in\Pi$.

In the cases where $\Phi\in\\{\emptyset,\Pi\\}$, the above definition reduces
to the usual notions of the canonical language interpretation from Kleene
algebra and Kleene algebra with tests, respectively.

##  6 Language completeness

In this section we establish a “parametrized” language completeness result for
Kleene algebra with dynamic tests. Our proof draws heavily on Hollenberg’s
[12] completeness proof for an axiomatization of program equations in tests
algebras, which is in turn inspired by Kozen and Smith’s [17] proof of
language completeness of Kleene algebra with tests. Our proof introduces some
simplifications into Hollenberg’s general strategy – for instance, we do not
use consistent guarded strings, only consistently guarded strings. This has
the advantage of not requiring a proof that the salient set of guarded strings
is closed under fusion product.

######  Lemma 2 (Language soundness).

Let $\Gamma$ be any finite set of parameters. For all $e,f\in\mathbb{E}$:

$e\equiv f\implies\llbracket e\rrbracket_{\Gamma}=\llbracket
f\rrbracket_{\Gamma}\,.$

###### Proof.

It is sufficient to show that axioms (12–15) are valid under every
$\Phi$-canonical interpretation. This is left to the reader as an easy
exercise. ∎

For the rest of this section, fix an arbitrary finite set of parameters. We
define $\mathbb{C}(\phi):=\sum\\{G\in\mathbb{C}(\Gamma)\mid G\leqq\phi\\}$,
for any $\phi$.

######  Lemma 3.

If $\phi\in\Gamma$, then $\phi\equiv\mathbb{C}(\phi)$.

###### Proof.

It is clear that $\mathbb{C}(\phi)\leqq\phi$. If
$\phi\not\leqq\mathbb{C}(\phi)$, then
$\phi\cdot\mathbb{C}(\phi)^{\bot}\not\equiv\mathtt{0}$. But then there is a
maximal consistent set of formulas $F$ such that $\phi\in F$ and
$\mathbb{C}(\phi)\notin F$.777$F$ is a  consistent set of formulas iff there
is no finite $\\{\chi_{1},\ldots,\chi_{n}\\}\subseteq F$ such that
$\chi_{1}\ldots\chi_{n}\equiv\mathtt{0}$. $F$ is a  maximal consistent set of
formulas if $F$ is consistent but $\psi\notin F$ implies that
$F\cup\\{\psi\\}$ is not consistent. Since formulas satisfy the axioms of
Boolean algebra by Proposition 1, every consistent set of formulas is extended
by a maximal consistent set by Lindenbaum’s Lemma. But then $G\notin F$ for
all $G\in\mathbb{C}(\Gamma)$ such that $G\leqq\phi$. Now take the sequence of
tests $H=\psi_{1}\ldots\psi_{n}$ where $\psi_{i}=\gamma_{i}$ if $\gamma_{i}\in
F$ and $\psi_{i}=\gamma_{i}^{\bot}$ if $\gamma_{i}\notin F$, for all
$\gamma_{i}\in\Gamma$. It is clear that $H$ is a consistent atom over $\Gamma$
and $H\leqq\phi$ since $\phi\in\Gamma$. This contradicts the properties of
$F$, and so we conclude that $\phi\leqq\mathbb{C}(\phi)$. ∎

######  Lemma 4.

For all $\phi\in\Gamma$,
$\llbracket\phi\rrbracket_{\Gamma}=\\{G\in\mathbb{C}(\Gamma)\mid
G\leqq\phi\\}$.

###### Proof.

The proof of this lemma is based on Kozen and Parikh’s completeness proof for
PDL [16]. See the appendix, Section A.1. ∎

######  Definition 13.

We define $\>\widehat{}\>$ as the smallest function
$\mathbb{RE}(\Gamma)\to\mathbb{RE}(\Gamma^{\pm})$ such that (for
$\phi\in\Gamma$ and $\mathtt{a}\in\Sigma$)

$\widehat{\phi}=\mathbb{C}(\phi)\qquad\quad\widehat{\mathtt{a}}=\sum\llbracket\mathtt{a}\rrbracket_{\Gamma}\qquad\quad\widehat{\mathtt{1}}=\sum\mathbb{C}(\Gamma)$

and that commutes with $\mathtt{0}$, $\cdot,+$ and $\,{}^{*}$.

######  Lemma 5.

For all $e\in\mathbb{RE}(\Gamma)$, $e\equiv\widehat{e}$.

###### Proof.

Induction on the complexity of $e$. The base case $e=\phi\in\Gamma$ holds by
Lemma 3. The base case $e=\mathtt{a}\in\Sigma$ is established as follows:

$\displaystyle\mathtt{a}$
$\displaystyle\equiv\mathtt{1}\cdot\mathtt{a}\cdot\mathtt{1}\equiv\mathbb{C}(\mathtt{1})\cdot\mathtt{a}\cdot\mathbb{C}(\mathtt{1})$
$\displaystyle\equiv\sum\mathbb{C}(\Gamma)\cdot\mathtt{a}\cdot\sum\mathbb{C}(\Gamma)$
$\displaystyle\equiv\sum\\{G\mathtt{a}H\mid G,H\in\mathbb{C}(\Gamma)\\}$
$\displaystyle\equiv\sum\\{G\mathtt{a}H\mid G,H\in\mathbb{C}(\Gamma)\And
G\mathtt{a}H\not\equiv\mathtt{0}\\}$
$\displaystyle\equiv\sum\llbracket\mathtt{a}\rrbracket_{\Gamma}\equiv\widehat{\mathtt{a}}$

(The second equivalence relies on Lemma 3.) The induction step for
$\mathtt{1}$ follows from Lemma 3. The rest of the proof is easy since
$\>\widehat{\,}\>$ commutes with $\mathtt{0}$, $\cdot$, $+$ and $\,{}^{*}$. ∎

######  Lemma 6.

$[w]_{\Gamma}=\\{w\\}$ for all $w\in\mathbb{GS}(\Gamma)$.

######  Lemma 7.

$\llbracket e\rrbracket_{\Gamma}=[\widehat{e}\,]_{\Gamma}$ for all
$e\in\mathbb{RE}(\Gamma)$.

###### Proof.

Induction on the structure of $e$, relying heavily on Lemma 6. The base case
$e=\phi\in\Gamma$ is established as follows (we omit the subscript $\Gamma)$:

$\displaystyle[\widehat{\phi}\,]$ $\displaystyle=\left[\sum\\{G\mid
G\in\mathbb{C}(\Gamma)\And G\leqq\phi\\}\right]$
$\displaystyle=\bigcup\\{[G]\mid G\in\mathbb{C}(\Gamma)\And G\leqq\phi\\}$
$\displaystyle=\\{G\mid G\in\mathbb{C}(\Gamma)\And
G\leqq\phi\\}=\llbracket\phi\rrbracket$

The third equation holds thanks to Lemma 6 and the last equation holds thanks
to Lemma 4. The base case for $e=\mathtt{a}\in\Sigma$ is established as
follows:

$\displaystyle[\widehat{\mathtt{a}}\,]$
$\displaystyle=\left[\sum\\{G\mathtt{a}H\mid
G\mathtt{a}H\not\equiv\mathtt{0}\\}\right]$
$\displaystyle=\bigcup\\{[G\mathtt{a}H]\mid
G\mathtt{a}H\not\equiv\mathtt{0}\\}$ $\displaystyle=\\{G\mathtt{a}H\mid
G\mathtt{a}H\not\equiv\mathtt{0}\\}=\llbracket\mathtt{a}\rrbracket$

The third equation holds thanks to Lemma 6. The induction step for
$\mathtt{1}$ is established as follows:

$\displaystyle[\widehat{\mathtt{1}}\,]$
$\displaystyle=\left[\sum\mathbb{C}(\Gamma)\right]=\bigcup\\{[G]\mid
G\in\mathbb{C}(\Gamma\\}$
$\displaystyle=\mathbb{C}(\Gamma)=\llbracket\mathtt{1}\rrbracket$

The third equation holds thanks to Lemma 6 and the last equation holds thanks
to Lemma 4. The rest is established easily using the induction hypothesis
since $\>\widehat{\>}\,$ is assumed to commute with $\mathtt{0}$, $\cdot$, $+$
and $\,{}^{*}$. ∎

######  Theorem 3 (Language completeness).

Let $E\subseteq\mathbb{E}$ be finite and let $\Gamma$ be the FL-closure of
$\mathrm{St}(E)$. Then, for all $e,f\in E$:

$e\equiv f\iff\llbracket e\rrbracket_{\Gamma}=\llbracket f\rrbracket_{\Gamma}$

###### Proof.

The implication from left to right follows from Lemma 2. The converse
implication is established as follows:

$\llbracket e\rrbracket_{\Gamma}=\llbracket f\rrbracket_{\Gamma}\>\ext@arrow
0359\Rightarrowfill@{}{\text{Lemma
\ref{lem:hat-2}}\,}\>[\widehat{e}\,]_{\Gamma}=[\widehat{f}\,]_{\Gamma}\>\ext@arrow
0359\Rightarrowfill@{}{\text{Theorem \ref{thm:KAT-
completeness}}\,}\>\widehat{e}\overset{\scriptscriptstyle\mathsf{KAT}(\Gamma)}{\equiv}\widehat{f}$

$\widehat{e}\overset{\scriptscriptstyle\mathsf{KAT}(\Gamma)}{\equiv}\widehat{f}\>\ext@arrow
0359\Rightarrowfill@{}{\text{Observation
\ref{obs:EQ}}\,}\>\widehat{e}\equiv\widehat{f}\>\ext@arrow
0359\Rightarrowfill@{}{\text{Lemma \ref{lem:hat-1}}\,}\>e\equiv f$

∎

Similarly to well known language completeness results of Kleene algebra and
Kleene algebra with tests, the completeness result presented in this section
shows that two expressions are equivalent iff they denote the same language in
a given language model. However, the result is “parametrized” in the sense
that it relies on expressions not denoting languages simpliciter but via a
parameter $\Gamma$. The completeness result then holds only if a right kind of
parameter is chosen.

The relation between expressions and languages used here can be seen as a
generalization of the unmediated relation between regular expressions and
regular languages. In our setting, expressions can be seen as denoting
generalized languages, that is, functions
$\lambda:\mathbb{E}\to(2^{\mathbb{E}}\to 2^{\mathbb{GS}})$. Standard languages
are a special case where $\lambda(e)$ is a constant function.

##  7 Relational completeness

In this section we prove a relational completeness result for Kleene algebra
with dynamic tests. We rely on Theorem 3. In the rest of the section, let
$\Gamma$ be a fixed finite set of parameters.

######  Definition 14.

We define the function $\mathsf{cay}:2^{\mathbb{CS}(\Gamma)}\to
2^{\mathbb{CS}(\Gamma)\times\mathbb{CS}(\Gamma)}$ as follows:

$\mathsf{cay}(L)=\\{\langle w,w\diamond u\rangle\mid
w\in\mathbb{CS}(\Gamma)\And u\in L\\}$

We define a relational model
$CS(\Gamma)=\langle\mathbb{CS}(\Gamma),\mathsf{rel}_{CS(\Gamma)},\mathsf{sat}_{CS(\Gamma)}\rangle$
where

$\mathsf{rel}_{CS(\Gamma)}(\mathtt{a})=\mathsf{cay}(\llbracket\mathtt{a}\rrbracket_{\Gamma})\qquad\mathsf{sat}_{CS(\Gamma)}(\mathtt{p})=\\{w\mid\mathsf{last}(w)\leqq\mathtt{p}\\}$

for $\mathtt{a}\in\Sigma$ and $\mathtt{p}\in\Pi$. (Of course,
$\mathsf{last}(w)$ is the last atom occurring in $w$, and we denote as
$\mathsf{first}(w)$ the first one.)

######  Lemma 8.

For all $\phi\in\Gamma$, $\llbracket\phi\rrbracket_{CS(\Gamma)}=\\{\langle
w,w\rangle\mid\mathsf{last}(w)\leqq\phi\\}$.

###### Proof.

See the appendix, Sect. A.2. ∎

######  Lemma 9.

For all $e\in\mathbb{RE}(\Gamma)$,

$\mathsf{cay}\left(\llbracket e\rrbracket_{\Gamma}\right)=\llbracket
e\rrbracket_{CS(\Gamma)}\,.$

###### Proof.

Induction on the complexity of $e$. We omit the subscript $CS(\Gamma)$ in the
rest of the proof. The base case for $e=\phi\in\Gamma$ is established using
Lemma 4 and Lemma 8:
$\mathsf{cay}\left(\llbracket\phi\rrbracket_{\Gamma}\right)=\\{\langle
w,w\rangle\mid\mathsf{last}(w)\leqq\phi\\}=\llbracket\phi\rrbracket$. The base
case for $e=\mathtt{a}\in\Sigma$ holds by definition.

The induction step for $\mathtt{1}$ follows from Lemma 4:
$\llbracket\mathtt{1}\rrbracket_{\Gamma}=\mathbb{C}(\Gamma)$ and so
$\mathsf{cay}\left(\llbracket\mathtt{1}\rrbracket_{\Gamma}\right)=1_{\mathbb{CS}(\Gamma)}=\llbracket\mathtt{1}\rrbracket$.
The induction step for $\mathtt{0}$ is trivial.

The induction step for $e+f$ is established as follows: $\llbracket
e+f\rrbracket=\llbracket e\rrbracket\cup\llbracket
f\rrbracket=\mathsf{cay}(\llbracket
e\rrbracket_{\Gamma})\cup\mathsf{cay}(\llbracket
f\rrbracket_{\Gamma})=\mathsf{cay}(\llbracket
e\rrbracket_{\Gamma}\cup\llbracket
f\rrbracket_{\Gamma})=\mathsf{cay}\left(\llbracket
e+f\rrbracket_{\Gamma}\right)$. The induction step for $e\cdot f$ is
established as follows:

$\displaystyle\llbracket e\cdot f\rrbracket$ $\displaystyle=\llbracket
e\rrbracket\circ\llbracket f\rrbracket$ $\displaystyle=\\{\langle w,w\diamond
u\rangle\mid w\in\mathbb{CS}(\Gamma)\And u\in\llbracket
e\rrbracket_{\Gamma}\\}$ $\displaystyle\qquad\circ\\{\langle
w^{\prime},w^{\prime}\diamond u^{\prime}\rangle\mid
w^{\prime}\in\mathbb{CS}(\Gamma)\And u^{\prime}\in\llbracket
f\rrbracket_{\Gamma}\\}$ $\displaystyle=\\{\langle w,w\diamond u\rangle\mid
w\in\mathbb{CS}(\Gamma)\And u\in\llbracket e\rrbracket_{\Gamma}\\}$
$\displaystyle\qquad\circ\\{\langle w\diamond u,w\diamond u\diamond
u^{\prime}\rangle\mid w\in\mathbb{CS}(\Gamma)\And u\in\llbracket
e\rrbracket_{\Gamma}\And u^{\prime}\in\llbracket f\rrbracket_{\Gamma}\\}$
$\displaystyle=\\{\langle w,w\diamond u\diamond u^{\prime}\rangle\mid
w\in\mathbb{CS}(\Gamma)\And u\in\llbracket e\rrbracket_{\Gamma}\And
u^{\prime}\in\llbracket f\rrbracket_{\Gamma}\\}$ $\displaystyle=\\{\langle
w,w\diamond v\rangle\mid w\in\mathbb{CS}(\Gamma)\And v\in\llbracket e\cdot
f\rrbracket_{\Gamma}\\}$ $\displaystyle=\mathsf{cay}(\llbracket e\cdot
f\rrbracket_{\Gamma})$

The induction step for $e^{*}$ is established as follows:

$\displaystyle\llbracket e^{*}\rrbracket$ $\displaystyle=\bigcup_{n\geq
0}\left\llbracket e\right\rrbracket^{n}=\bigcup_{n\geq
0}\mathsf{cay}\left(\llbracket e\rrbracket_{\Gamma}\right)^{n}$
$\displaystyle=\mathsf{cay}\left(\bigcup_{n\geq 0}\llbracket
e\rrbracket^{n}_{\Gamma}\right)=\mathsf{cay}\left(\llbracket
e^{*}\rrbracket_{\Gamma}\right)$

∎

######  Theorem 4 (Relational completeness).

For all $e,f\in\mathbb{E}$:

$e\equiv f\iff(\forall M)(\llbracket e\rrbracket_{M}=\llbracket
f\rrbracket_{M})$

###### Proof.

The implication from left to right is Lemma 1. The converse implication is
established as follows. Fix $e,f$ such that $e\not\equiv f$ and let $\Gamma$
be the FL-closure of $\mathrm{Sf}(e,f)?$. We obtain $\llbracket
e\rrbracket_{\Gamma}\neq\llbracket f\rrbracket_{\Gamma}$ using Theorem 3 and
so $\mathsf{cay}\left(\llbracket
e\rrbracket_{\Gamma}\right)\neq\mathsf{cay}\left(\llbracket
f\rrbracket_{\Gamma}\right)$ since $\mathsf{cay}$ is injective.888Suppose
without loss of generality that $w\in L\setminus K$. Then
$\langle\mathsf{first}(w),w\rangle\in\mathsf{cay}(L)\setminus\mathsf{cay}(K)$.
Then $\llbracket e\rrbracket_{CS(\Gamma)}\neq\llbracket
f\rrbracket_{CS(\Gamma)}$ and we are done. ∎

######  Theorem 5.

The problem of deciding equivalence of arbitrary expressions is
$\mathrm{EXPTIME}$-complete.

###### Proof.

By Theorem 4, equivalence coincides with relational equivalence. The rest
follows from Theorem 1. ∎

##  8 Fragments

This section discusses the bearing of the results discussed in previous
sections on various fragments of $\mathsf{aKAT}$.

First, it is straightforward that we obtain both kinds of completeness for
fragments of $\equiv$ as a corollary of Theorems 3 and 4:

######  Theorem 6.

Take a finite $E\subseteq\mathbb{E}$ and $e,f\in E$. The following are
equivalent:

  1. 1.

$e\overset{\scriptscriptstyle\mathsf{K}}{\equiv}f$

  2. 2.

$\llbracket e\rrbracket_{\Gamma}=\llbracket f\rrbracket_{\Gamma}$ where
$\Gamma$ is the FL-closure of $\mathrm{St}(E)$

  3. 3.

$\llbracket e\rrbracket_{M}=\llbracket f\rrbracket_{M}$ for all relational
models $M$

Our complexity result for $\mathsf{aKAT}$ can be used to establish
$\mathrm{EXPTIME}$-completeness of $\mathsf{aKA}$ as follows.

The upper bound of the complexity of deciding equivalence between
$\mathsf{aKA}$-expressions follows directly from the upper bound for arbitrary
expressions. The lower bound result will use the following lemma.

######  Lemma 10.

Let $e^{\prime}$ be the result of replacing every occurrence of
$\mathtt{a}_{n}$ in $e$ by an occurrence of $\mathtt{a}_{2n}$ and replacing
every occurrence of $\mathtt{p}_{n}$ by an occurrence of
$(\mathtt{a}_{2n+1})^{\top}$. Then

$e\equiv f\iff e^{\prime}\equiv f^{\prime}\,.$

###### Proof.

Left to right: Equivalence is preserved under substitution. Moreover, clearly
$\mathtt{p}^{\prime}\equiv(\mathtt{p}^{\prime})^{\top}$. Right to left: If
$e\not\equiv f$, then there is a relational model $M$ where $\llbracket
e\rrbracket_{M}\neq\llbracket f\rrbracket_{M}$ (Theorem 4). We define
$M^{\prime}$ by taking the universe $X$ of $M$ and stipulating that

$\mathsf{rel}_{M^{\prime}}(\mathtt{a}_{m})=\begin{cases}\mathsf{rel}_{M}(\mathtt{a}_{n})&m=2n\\\
1_{\mathsf{sat}_{M}(\mathtt{p}_{n})}&m=2n+1\end{cases}\qquad\mathsf{sat}_{M^{\prime}}(\mathtt{p})=\emptyset$

It can be shown by induction on $g$ that $\llbracket
g\rrbracket_{M}=\llbracket g^{\prime}\rrbracket_{M^{\prime}}$. Only the base
case is interesting. The base case for $\mathtt{a}_{n}$:
$\llbracket(\mathtt{a}_{n})^{\prime}\rrbracket_{M^{\prime}}=\llbracket\mathtt{a}_{2n}\rrbracket_{M^{\prime}}=\llbracket\mathtt{a}_{n}\rrbracket_{M}$.
The base case for $\mathtt{p}_{n}$:
$\llbracket(\mathtt{p}_{n})^{\prime}\rrbracket_{M^{\prime}}=\llbracket(\mathtt{a}_{2m+1})^{\top}\rrbracket_{M^{\prime}}=\\{\langle
x,x\rangle\mid\exists y.\langle
x,y\rangle\in\llbracket\mathtt{a}_{2n+1}\rrbracket_{M^{\prime}}\\}=\llbracket\mathtt{p}_{n}\rrbracket_{M}$.
Now clearly $\llbracket e^{\prime}\rrbracket_{M^{\prime}}\neq\llbracket
f^{\prime}\rrbracket_{M^{\prime}}$ and so $e^{\prime}\not\equiv f^{\prime}$ by
Lemma 1. ∎

Before using this lemma in the proof of the complexity result for
$\mathsf{aKA}$, we should pause to appreciate what it says about
$\mathsf{aKA}$. Since every $\overset{\scriptscriptstyle\mathsf{K}}{\equiv}$
trivially embeds into $\equiv$ and $\equiv$ embeds into
$\overset{\scriptscriptstyle\mathsf{aKA}}{\equiv}$ by Lemma 10, we obtain the
result that every $\overset{\scriptscriptstyle\mathsf{K}}{\equiv}$ embeds into
$\overset{\scriptscriptstyle\mathsf{aKA}}{\equiv}$. Thus, $\mathsf{aKA}$
occupies a central position in the family of Kleene algebras with dynamic
tests.

######  Theorem 7.

The problem of deciding equivalence between $\mathsf{aKA}$-expressions is
$\mathrm{EXPTIME}$-complete.

###### Proof.

The problem is in $\mathrm{EXPTIME}$ since so is deciding equivalence between
arbitrary expressions. The problem is $\mathrm{EXPTIME}$-complete thanks to
Lemma 10: deciding equivalence between arbitrary expressions can be
polynomially reduced to deciding equivalence between
$\mathsf{aKA}$-expressions. The former is $\mathrm{EXPTIME}$-complete by
Theorem 1. ∎

##  9 Conclusion

In this paper we discussed several versions of Kleene algebra with dynamic
tests, extending Kleene algebra with dynamic tests operators ⊥ (antidomain)
and $\top$ (domain). Kleene algebra with tests is a special case where
antidomain applies only to Boolean variables. On the other side of the
spectrum, the strongest version of Kleene algebra with dynamic tests
considered here, $\mathsf{aKAT}$, was shown to correspond to $\mathsf{PDL}$.
Our main results are (i) completeness results for $\mathsf{aKAT}$ and its
syntactic fragments with respect to relational models and specific models
based on guarded strings, and (ii) an $\mathrm{EXPTIME}$-completeness result
for $\mathsf{aKAT}$ following from relational completeness and the relation
between $\mathsf{aKAT}$ and $\mathsf{PDL}$) and for $\mathsf{aKA}$ (following
from the fact that $\mathsf{aKAT}$ embeds into $\mathsf{aKA}$, showing that
$\mathsf{aKA}$ occupies a central position in the family).

A number of interesting problems remain to be solved. First, are
$\mathsf{dKA}$ and $\mathsf{dKAT}$ $\mathrm{EXPTIME}$-hard? Second, do
fragments of quasi-equational theories of $\mathsf{aKAT}$ and its fragments
where all assumptions are of the form $e\equiv\mathtt{0}$ reduce to their
equational theories, similarly as in $\mathsf{KA}$ and $\mathsf{KAT}$? Third,
are there natural fragments of $\mathsf{aKAT}$ that are stronger than
$\mathsf{KAT}$ but still have a $\mathrm{PSPACE}$-complete equational theory?
Fourth, echoing the links between $\mathsf{KA}$ ($\mathsf{KAT}$) and finite
automata (on guarded strings), what is the natural automata-theoretic
formulation of the various versions of Kleene algebra with dynamic tests
considered here?

## References

  * [1] A. Bochman and D. M. Gabbay.  Sequential dynamic logic.  Journal of Logic, Language and Information, 21(3):279–298, 2012\.  doi:10.1007/s10849-011-9152-y.
  * [2] J. Desharnais, B. Möller, and G. Struth.  Modal Kleene Algebra and Applications – A Survey.  Journal on Relational Methods in Computer Science, 1:93–131, 2004\.  URL: http://www.cosc.brocku.ca/Faculty/Winter/JoRMiCS/Vol1/PDF/v1n5.pdf.
  * [3] J. Desharnais, B. Möller, and G. Struth.  Kleene algebra with domain.  ACM Trans. Comput. Logic, 7(4):798–833, oct 2006.  doi:10.1145/1183278.1183285.
  * [4] J. Desharnais and G. Struth.  Modal semirings revisited.  In International Conference on Mathematics of Program Construction, pages 360–387. Springer, 2008.
  * [5] J. Desharnais and G. Struth.  Internal axioms for domain semirings.  Science of Computer Programming, 76(3):181–203, 2011.  Special issue on the Mathematics of Program Construction (MPC 2008).  doi:10.1016/j.scico.2010.05.007.
  * [6] T. Ehm, B. Möller, and G. Struth.  Kleene modules.  In a. M. B. Berghammer, R. and G. Struth, editors, International Conference on Relational Methods in Computer Science, pages 112–123. Springer, 2003.  doi:10.1007/978-3-540-24771-5_10.
  * [7] M. J. Fischer and R. E. Ladner.  Propositional dynamic logic of regular programs.  Journal of Computer and System Sciences, 18:194–211, 1979.  doi:10.1016/0022-0000(79)90046-1.
  * [8] V. Gomes and G. Struth.  Modal Kleene algebra applied to program correctness.  In International Symposium on Formal Methods, pages 310–325. Springer, 2016.  doi:10.1007/978-3-319-48989-6_19.
  * [9] J. Groenendijk and M. Stokhof.  Dynamic predicate logic.  Linguistics and Philosophy, 14(1):39–100, 1991.  doi:10.1007/BF00628304.
  * [10] D. Harel, D. Kozen, and J. Tiuryn.  Dynamic Logic.  MIT Press, 2000.
  * [11] M. Hollenberg.  An equational axiomatization of dynamic negation and relational composition.  Journal of Logic, Language and Information, 6(4):381–401, 1997\.  doi:10.1023/A:1008271805106.
  * [12] M. Hollenberg.  Equational axioms of test algebra.  In M. Nielsen and W. Thomas, editors, International Workshop on Computer Science Logic. CSL 1997, pages 295–310, Berlin, Heidelberg, 1998. Springer.  doi:10.1007/BFb0028021.
  * [13] D. Kozen.  On the duality of dynamic algebras and Kripke models.  In E. Engeler, editor, Proc. 1st Workshop on Logic of Programs, volume 125 of Lecture Notes in Computer Science, pages 1–11. Springer-Verlag, 1979.
  * [14] D. Kozen.  A completeness theorem for Kleene algebras and the algebra of regular events.  Information and Computation, 110(2):366 – 390, 1994.  doi:10.1006/inco.1994.1037.
  * [15] D. Kozen.  Kleene algebra with tests.  ACM Trans. Program. Lang. Syst., 19(3):427–443, May 1997.  doi:10.1145/256167.256195.
  * [16] D. Kozen and R. Parikh.  An elementary proof of the completeness of PDL.  Theoretical Computer Science, 14:113–118, 1981.  doi:10.1016/0304-3975(81)90019-0.
  * [17] D. Kozen and F. Smith.  Kleene algebra with tests: Completeness and decidability.  In D. van Dalen and M. Bezem, editors, Computer Science Logic, pages 244–259, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.  doi:10.1145/256167.256195.
  * [18] D. Kozen and J. Tiuryn.  Substructural logic and partial correctness.  ACM Trans. Computational Logic, 4(3):355–378, July 2003.  doi:10.1145/772062.772066.
  * [19] S. D. Mbacke.  Completeness for Domain Semirings and Star-continuous Kleene Algebras with Domain.  M.Sc. thesis, Université Laval, 2018.
  * [20] B. McLean.  Free Kleene algebras with domain.  Journal of Logical and Algebraic Methods in Programming, 117:100606, 2020.  doi:10.1016/j.jlamp.2020.100606.
  * [21] B. Möller and G. Struth.  Algebras of modal operators and partial correctness.  Theoretical Computer Science, 351(2):221 – 239, 2006.  Algebraic Methodology and Software Technology.  doi:https://doi.org/10.1016/j.tcs.2005.09.069.
  * [22] V. Pratt.  Dynamic algebras: Examples, constructions, applications.  Studia Logica, 50(3):571–605, 1991.  doi:10.1007/BF00370685.
  * [23] V. R. Pratt.  Models of program logics.  In Proceedings of the 20th Annual Symposium on Foundations of Computer Science, FOCS ’79, page 115–122, USA, 1979. IEEE Computer Society.  doi:10.1109/SFCS.1979.24.
  * [24] I. Sedlár.  On the complexity of Kleene algebra with domain.  In R. Glück, L. Santocanale, and M. Winter, editors, Relational and Algebraic Methods in Computer Science (RAMiCS 2023), number 13896 in Lecture Notes in Computer Science, pages 208–223, Cham, 2023. Springer.  doi:10.1007/978-3-031-28083-2_13.
  * [25] G. Struth.  On the expressive power of Kleene algebra with domain.  Information Processing Letters, 116(4):284–288, 2016.  doi:10.1016/j.ipl.2015.11.007.
  * [26] V. Trnková and J. Reiterman.  Dynamic algebras with test.  Journal of Computer and System Sciences, 35(2):229 – 242, 1987\.  doi:10.1016/0022-0000(87)90014-6.

##  Appendix A Technical appendix

###  A.1 Proof of Lemma 4

The proof follows the general strategy of [16]. It will be convenient to prove
our result using a canonical relational model.

######  Definition A.1.

Let $\Gamma$ be a finite set of parameters. The  canonical relational
$\Gamma$-model is
$C(\Gamma)=\langle\mathbb{C}(\Gamma),\mathsf{rel}_{C(\Gamma)},\mathsf{sat}_{C(\Gamma)}\rangle$
where

$\mathsf{rel}_{C(\Gamma)}(\mathtt{a})=\\{\langle G,H\rangle\mid
G\mathtt{a}H\not\equiv\mathtt{0}\\}\qquad\mathsf{sat}_{C(\Gamma)}(\mathtt{p})=\\{G\mid
G\leqq\mathtt{p}\\}$

for all $\mathtt{a}\in\Sigma$ and $\mathtt{p}\in\Pi$. The
$C(\Gamma)$-interpretation of expressions is defined as usual in relational
models.

We write $G\xrightarrow{e}H$ iff $\langle G,H\rangle\in\llbracket
e\rrbracket_{C(\Gamma)}$. Note that

  * •

$G\xrightarrow{\mathtt{a}}H$ iff $G\mathtt{a}H\not\equiv\mathtt{0}$

  * •

$G\xrightarrow{\mathtt{p}}H$ iff $G=H$ and $G\leqq\mathtt{p}$

  * •

$G\xrightarrow{\mathtt{1}}H$ iff $G=H$

  * •

$G\xrightarrow{\mathtt{0}}H$ iff $H\neq H$ (i.e. never)

  * •

$G\xrightarrow{e+f}H$ iff $G\xrightarrow{e}H$ or $G\xrightarrow{f}H$

  * •

$G\xrightarrow{e\cdot f}H$ iff there is $I$:
$G\xrightarrow{e}I\xrightarrow{f}H$

  * •

$G\xrightarrow{e^{*}}H$ iff there are $I_{1},\ldots,I_{n}$ such that

$G=I_{1}\xrightarrow{e}\ldots\xrightarrow{e}I_{n}=H$

  * •

$G\xrightarrow{e^{\bot}}H$ iff $G=H$ and there is no $I$: $G\xrightarrow{e}I$

  * •

$G\xrightarrow{e^{\top}}H$ iff $G=H$ and there is $I$: $G\xrightarrow{e}I$

The relation between relational and guarded-string interpretations of
expressions can be compactly described using the function
$\mathsf{pair}:2^{\mathbb{CS}(\Gamma)}\to
2^{\mathbb{C}(\Gamma)\times\mathbb{C}(\Gamma)}$ defined in the obvious way:

$\mathsf{pair}(L)=\\{\langle G,H\rangle\mid\exists
G\mathtt{a}_{1}\ldots\mathtt{a}_{n-1}H\in L\\}$

######  Lemma A.1.

For all $e\in\mathbb{E}$, $\llbracket
e\rrbracket_{C(\Gamma)}=\mathsf{pair}\left(\llbracket
e\rrbracket_{\Gamma}\right)$.

######  Lemma A.2.

Let $\Gamma$ be a FL-closed set of parameters. Then the following holds in
$C(\Gamma)$ for all $e\in\mathbb{E}$:

  * (i)

If $e^{\top}\in\Gamma$, then $GeH\not\equiv\mathtt{0}$ implies
$G\xrightarrow{e}H$.

  * (ii)

If $(e\cdot\phi)^{\top}\in\Gamma$, then $G\xrightarrow{e}H\leqq\phi$ implies
$G\leqq(e\cdot\phi)^{\top}$.

###### Proof.

Both claims are established simultaneously by induction on the structure of
$e$. The base case (i) for $\mathtt{a}\in\Sigma$ holds by definition. The base
case (i) for $\mathtt{p}\in\Pi$ holds since $G\mathtt{p}\not\equiv\mathtt{0}$
implies (a) $G\triangleleft\mathtt{p}$ ($\mathtt{p}^{\top}\in\Gamma$ only if
$\mathtt{p}\in\Gamma$) and so (b) $G\cdot H\not\equiv\mathtt{0}$ which is
possible only if $G=H$. Base case (ii) for $\mathtt{a}\in\Sigma$: If
$G\xrightarrow{\mathtt{a}}H\leqq\phi$, then $G\mathtt{a}H\not\equiv\mathtt{0}$
and $H\leqq\phi$. Then $G(\mathtt{a}\cdot\phi)\not\leqq\mathtt{0}$, which
means that
$G\not\leqq(\mathtt{a}\cdot\phi)^{\bot}\equiv(\mathtt{a}\cdot\phi)^{\top\bot}$.
Hence, $G\leqq(\mathtt{a}\cdot\phi)^{\top}$. Base case (ii) for
$\mathtt{p}\in\Pi$: $G\xrightarrow{\mathtt{p}}H$ means that $G=H$ and
$H\leqq\mathtt{p}$. If also $H\leqq\phi$, then
$G\leqq(\mathtt{p}\cdot\phi)\equiv(\mathtt{p}\cdot\phi)^{\top}$.

Claim (i) for $\mathtt{1}$: If $G\mathtt{1}H\not\equiv\mathtt{0}$, then
$GH\not\equiv\mathtt{0}$, but this is possible only if $G=H$. Claim (ii) for
$\mathtt{1}$: If $G\xrightarrow{\mathtt{1}}H$, then $G=H$. If also
$H\leqq\phi$, then
$G\leqq(\mathtt{1}\cdot\phi)\equiv(\mathtt{1}\cdot\phi)^{\top}$. Claims (i)
and (ii) for $\mathtt{0}$ hold vacuously.

The induction hypothesis is that both (i) and (ii) hold for $e,f$. We will
prove (i) and (ii) for $e+f$, $e\cdot f$, $e^{*}$, $e^{\top}$ and $e^{\bot}$.

Induction step (i) for $e+f$: If $(e+f)^{\top}\in\Gamma$, then
$e^{\top}\in\Gamma$ and $f^{\top}\in\Gamma$. If $G(e+f)H\not\equiv\mathtt{0}$,
then $GeH\not\equiv\mathtt{0}$ or $GfH\not\equiv\mathtt{0}$ by distributivity.
Hence, $G\xrightarrow{e}H$ or $G\xrightarrow{f}H$ by the induction hypothesis.
It follows that $G\xrightarrow{e+f}H$.

Induction step (i) for $e\cdot f$: If $(e\cdot f)^{\top}\in\Gamma$, then
$e^{\top}\in\Gamma$ and $f^{\top}\in\Gamma$. If $G(e\cdot
f)H\not\equiv\mathtt{0}$, then there is $I$ such that
$GeI\not\equiv\mathtt{0}$ and $IfH\not\equiv\mathtt{0}$.999If for all $I$
either $GeI\equiv\mathtt{0}$ or $IfH\equiv\mathtt{0}$, then
$GeIfH\equiv\mathtt{0}$ for all $I\in\mathbb{C}(\Gamma)$. Then
$Ge\mathbb{C}(\mathtt{1}^{\top})fH\equiv\mathtt{0}$ and so
$Ge\mathtt{1}fH\equiv\mathtt{0}$ by Lemma 3 and
$\mathtt{1}^{\top}\equiv\mathtt{1}$. This means that $G(e\cdot
f)H\equiv\mathtt{0}$ and we are done. Using the induction hypothesis we infer
that $G\xrightarrow{e}I\xrightarrow{f}H$, and so $G\xrightarrow{e\cdot f}H$.

Induction step (i) for $e^{*}$: If $(e^{*})^{\top}\in\Gamma$, then
$e^{\top}\in\Gamma$. Assume that $Ge^{*}H\not\equiv\mathtt{0}$. Let $X$ be the
smallest subset of $\mathbb{C}(\Gamma)$ such that

  * •

$G\in X$

  * •

$I\in X$ and $IeJ\not\equiv\mathtt{0}$ only if $J\in X$

Since $e^{\top}\in\Gamma$, we may use the induction hypothesis to show that
$I\xrightarrow{e}J$ for all $I,J$ satisfying the above conditions. From this
we infer that $G\xrightarrow{e^{*}}J$ for all $J\in X$. Hence, we have to show
that $H\in X$. We will write $X$ instead of $\sum X$. It is sufficient to show
that $H\cdot X\not\equiv\mathtt{0}$.101010If $H\cdot\sum_{J\in
X}J\not\equiv\mathtt{0}$, then there is $J\in X$ such that $H\cdot
J\not\equiv\mathtt{0}$. If $H\cdot J\not\equiv\mathtt{0}$, then $H=J$ by (25).
If $XeX^{\bot}\not\equiv\mathtt{0}$, then there are $I\in X$ and $J\notin X$
such that $IeJ\not\equiv\mathtt{0}$.111111If $XeX^{\bot}\not\equiv\mathtt{0}$,
then there is $I\in X$ such that $IeX^{\bot}\not\equiv\mathtt{0}$. If
$IeJ\equiv\mathtt{0}$ for all $J\notin X$, then $Ie\left(\sum_{J\notin
X}J\right)\equiv\mathtt{0}$ and so $IeX^{\bot}\equiv\mathtt{0}$, contrary to
what we have observed, since $X^{\bot}\leqq\sum_{J\notin X}J$. This last claim
is established by noting that if $X^{\bot}\not\leqq\sum_{J\notin X}J$, then
$G^{\bot}_{1}\ldots G_{n}^{\bot}\not\equiv\mathtt{0}$ for
$\mathbb{C}(\Gamma)=\\{G_{1},\ldots,G_{n}\\}$. However, then
$\mathbb{C}(\mathtt{1})^{\bot}\not\equiv\mathtt{0}$, contradicting Lemma 3.
This contradicts our assumptions about $X$, and so
$XeX^{\bot}\equiv\mathtt{0}$. Hence, $X\leqq(e\cdot X^{\bot})^{\bot}$ and so
$X\leqq(e^{*}\cdot X^{\bot})^{\bot}$ by (33). Since $G\leqq X$, we obtain
$Ge^{*}X^{\bot}\equiv\mathtt{0}$. Using the assumption
$Ge^{*}H\not\equiv\mathtt{0}$, we conclude that $H\not\leqq X^{\bot}$ and so
$H\cdot X\not\equiv\mathtt{0}$.

The induction step (i) for $e^{\top}$ holds vacuously ($e^{\top\top}$ is not a
parameter). Induction step (i) for $e^{\bot}$: If $e^{\bot\top}\in\Gamma$,
then $(e\cdot\mathtt{1})^{\top}\in\Gamma$. Assume
$Ge^{\bot}H\not\equiv\mathtt{0}$. Then $E\cdot H\not\equiv\mathtt{0}$, which
is possible only in case $G=H$. Now suppose that there is $I$ such that
$G\xrightarrow{e}I$. Since $I\leqq\mathtt{1}$ and
$(e\cdot\mathtt{1})^{\top}\in\Gamma$, the induction hypothesis (ii) entails
$G\leqq(e\cdot\mathtt{1})^{\top}\equiv e^{\top}$. But then $Ge^{\bot}\leqq
e^{\top}e^{\bot}\leqq\mathtt{0}$, which contradicts the assumption that
$Ge^{\bot}H\not\equiv\mathtt{0}$. Hence, there is no $I$ such that
$G\xrightarrow{e}I$, which means that $G\xrightarrow{e^{\bot}}G=H$.

Now we consider the induction step (ii). Induction step (ii) for $e+f$: If
$G\xrightarrow{e+f}H$, then $G\xrightarrow{e}H$ or $G\xrightarrow{f}H$. Since
$\Gamma$ is FL-closed, $((e+f)\cdot\phi)^{\top}$ entails
$(e\cdot\phi)^{\top}\in\Gamma$ and $(f\cdot\phi)^{\top}\in\Gamma$. If
$H\leqq\phi$, then it suffices to use the induction hypothesis in both cases
$G\xrightarrow{e}H$ or $G\xrightarrow{f}H$ to obtain
$G\leqq(e\cdot\phi)^{\top}+(f\cdot\phi)^{\top}\equiv((e+f)\cdot\phi)^{\top}$.

Induction step (ii) for $e\cdot f$: If $G\xrightarrow{e\cdot f}H$, then there
is $I$ such that $G\xrightarrow{e}I$ and $I\xrightarrow{f}H$. If $H\leqq\phi$,
then we reason as follows. Since $\Gamma$ is FL-closed, $((e\cdot
f)\cdot\phi)^{\top}\in\Gamma$ entails $(f\cdot\phi)^{\top}\in\Gamma$ and
$(e\cdot(f\cdot\phi)^{\bot\bot})^{\top}\in\Gamma$. Using the induction
hypothesis, we obtain $I\leqq(f\cdot\phi)^{\top}\equiv(f\cdot\phi)^{\bot\bot}$
and also $G\leqq(e\cdot(f\cdot\phi)^{\bot\bot})^{\top}\equiv((e\cdot
f)\cdot\phi)^{\top}$.

Induction step (ii) for $e^{*}$: If $G\xrightarrow{e^{*}}H$, then there are
$I_{1},\ldots,I_{n}$ such that
$G=I_{1}\xrightarrow{e}\ldots\xrightarrow{e}I_{n}=H$. We show that if
$H\leqq\phi$, then $I_{m}\leqq(e^{*}\cdot\phi)^{\top}$ for all $m\leq n$.
First, $I_{n}\leqq\phi\equiv
G\leqq\mathtt{1}\cdot\phi\equiv(\mathtt{1}\cdot\phi)^{\top}\leqq(e^{*}\cdot\phi)^{\top}$.
Second, assume that
$I_{k+1}\leqq(e^{*}\cdot\phi)^{\top}\equiv(e^{*}\cdot\phi)^{\bot\bot}$. Since
$\Gamma$ is FL-closed, we have
$(e\cdot(e^{*}\cdot\phi)^{\bot\bot})^{\top}\in\Gamma$. Hence, using the
induction hypothesis we obtain
$I_{k}\leqq(e\cdot(e^{*}\cdot\phi)^{\bot\bot})^{\top}\equiv(e\cdot
e^{*}\cdot\phi)^{\top}\leqq(e^{*}\cdot\phi)^{\top}$.

The induction step (ii) for $e^{\top}$ holds vacuously since
$(e^{\top}\cdot\phi)^{\top}$ is not a parameter. Induction step (ii) for
$e^{\bot}$: If $G\xrightarrow{e^{\bot}}H$, then $G=H$ and there is no $I$ such
that $G\xrightarrow{e}I$. Using Lemma 3 and the induction hypothesis (i) we
obtain $Ge\equiv\mathtt{0}$, and so $G\leqq e^{\bot}$. If $H\leqq\phi$, then
$G\leqq(e^{\bot}\cdot\phi)\equiv(e^{\bot}\cdot\phi)^{\top}$. ∎

Lemma 4. If $\Gamma$ is a FL-closed set of parameters, then $\phi\in\Gamma$
only if

$\llbracket\phi\rrbracket_{\Gamma}=\\{G\in\mathbb{C}(\Gamma)\mid
G\leqq\phi\\}$

###### Proof.

The claim for $\phi\in\Pi$ holds by definition. Hence, it remains to show that
that if $e^{\top}\in\Gamma$, then $\llbracket
e^{\top}\rrbracket_{\Gamma}=\\{G\in\mathbb{C}(\Gamma)\mid G\leqq e^{\top}\\}$.
In particular, using the definition of a canonical $\Gamma$-interpretation, we
have to show that, for all $G\in\mathbb{C}(\Gamma)$

$G\leqq e^{\top}\iff\exists H.G\xrightarrow{e}H$

Left to right: If $G\leqq e^{\top}$, then $GeH\not\equiv\mathtt{0}$ for some
$H$ since otherwise we would have
$Ge\left(\sum\mathbb{C}(\Gamma)\right)\equiv\mathtt{0}$ which entails $G\leqq
e^{\bot}$ by Lemma 3. This would mean that $G$ is inconsistent. Hence,
$GeH\not\equiv\mathtt{0}$ for some $H$ and so we may infer $G\xrightarrow{e}H$
using Lemma A.2(i). Right to left: Assume that $G\xrightarrow{e}H$. If
$e\neq(f\cdot\mathtt{1})$ for all $f$, then $e^{\top}\in\Gamma$ implies
$(e\cdot\mathtt{1})^{\top}\in\Gamma$. Hence,
$G\leqq(e\cdot\mathtt{1})^{\top}\equiv e^{\top}$ by Lemma A.2(ii) since
obviously $H\leqq\mathtt{1}$. If $e=(f\cdot\mathtt{1})$ for some $f$, then
$G\xrightarrow{e}H$ entails $G\xrightarrow{f}H$. Since
$(f\cdot\mathtt{1})^{\top}$ in that case, we may use Lemma A.2(ii) to infer
$G\leqq(f\cdot\mathtt{1})^{\top}=e^{\top}$. ∎

###  A.2 Proof of Lemma 8

The relational model $CS(\Gamma)$ is what modal logicians call an
“unravelling” of the model $C(\Gamma)$ discussed in Section A.1. As such,
$CS(\Gamma)$ and $C(\Gamma)$ are related in a useful way.

######  Definition A.2.

Let $M_{1}=\langle X_{1},\mathsf{rel}_{1},\mathsf{sat}_{1}\rangle$ and
$M_{2}=\langle X_{2},\mathsf{rel}_{2},\mathsf{sat}_{2}\rangle$ be two
relational models. A binary relation $\sim$ between $X_{1}$ and $X_{2}$ is a
bisimulation between $M_{1}$ and $M_{2}$ iff $x_{1}\sim x_{2}$ implies

  1. 1.

$x_{1}\in\mathsf{sat}_{1}(\mathtt{p})\iff
x_{2}\in\mathsf{sat}_{2}(\mathtt{p})$ for all $\mathtt{p}$

  2. 2.

$\langle x_{1},y_{1}\rangle\in\mathsf{rel}_{1}(\mathtt{a})$ only if there is
$y_{2}\in X_{2}$ such that $\langle
x_{2},y_{2}\rangle\in\mathsf{rel}_{2}(\mathtt{a})$ and $y_{1}\sim y_{2}$, for
all $\mathtt{a}$

  3. 3.

$\langle x_{2},y_{2}\rangle\in\mathsf{rel}_{2}(\mathtt{a})$ only if there is
$y_{1}\in X_{1}$ such that $\langle
x_{1},y_{1}\rangle\in\mathsf{rel}_{1}(\mathtt{a})$ and $y_{1}\sim y_{2}$, for
all $\mathtt{a}$

If there is a bisimulation between $M_{1}$ and $M_{2}$, then we say that the
models are  bisimilar . If there is a bisimulation $\sim$ between $M_{1}$ and
$M_{2}$ such that $x_{1}\sim x_{2}$, then we write
$(M_{1},x_{1})\mathrel{\underline{\leftrightarrow}}(M_{2},x_{2})$.

The following is a standard result in modal logic, transposed to our setting.
Recall that $(M,x)\vDash\phi$ is our notation for $\langle
x,x\rangle\in\llbracket\phi\rrbracket_{M}$.

######  Lemma A.3.

If $(M,x)\mathrel{\underline{\leftrightarrow}}(N,y)$, then
$(M,x)\vDash\phi\iff(N,y)\vDash\phi$ for all $\phi\in\mathbb{F}$.

######  Lemma A.4.

For each set of tests $\Gamma$, the relation $\sim$ between
$\mathbb{C}(\Gamma)$ and $\mathbb{CS}(\Gamma)$ defined by

$G\sim H_{1}\mathtt{a}_{1}\ldots\mathtt{a}_{n-1}H_{n}\iff G=H_{n}$

is a bisimulation between $C(\Gamma)$ and $CS(\Gamma)$.

Lemma 8. For all $\phi\in\Gamma$, $\llbracket\phi\rrbracket_{M}=\\{\langle
w,w\rangle\mid\mathsf{last}(w)\leqq\phi\\}$.

###### Proof.

$\displaystyle(CS(\Gamma),w)\vDash\phi$
$\displaystyle\iff(C(\Gamma),\mathsf{last}(w))\vDash\phi$ by Lemmas A.3 and
A.4 $\displaystyle\iff\mathsf{last}(w)\leqq\phi$ by Lemmas 4 and A.1

∎