# The Krohn-Rhodes Logics

Alessandro Ronca Sapienza University of Rome<EMAIL_ADDRESS>
###### Abstract

We present a new family of modal temporal logics of the past, obtained by
extending _Past LTL_ with a rich set of temporal operators based on the theory
by Krohn and Rhodes for automata cascades. The theory says that every
automaton can be expressed as a cascade of some basic automata called _prime
automata_. They are the building blocks of all automata, analogously to prime
numbers being the building blocks of all natural numbers. We show that Past
LTL corresponds to cascades of one kind of prime automata called _flip-flops_.
In particular, the temporal operators of Past LTL are captured by flip-flops,
and they cannot capture any other prime automaton, confining the expressivity
within the star-free regular languages. We propose novel temporal operators
that can capture other prime automata, and hence extend the expressivity of
Past LTL. Such operators are infinitely-many, and they yield an infinite
number of logics capturing an infinite number of distinct fragments of the
regular languages. The result is a yet unexplored _landscape of extensions of
Past LTL_ , that we call Krohn-Rhodes Logics, each of them with the potential
of matching the expressivity required by specific applications.

##  1 Introduction

The theory started by Krohn and Rhodes (1965) shows how every automaton can be
expressed as the cascade (i.e., sequential) composition of some basic building
blocks. The theory identifies such building blocks in the so-called _prime
automata_ , which are automata that closely correspond to some elementary
kinds of (finite) semigroups. Prime automata can be seen as implementing
specific functionalities. For instance, flip-flop automata implement the
fundamental functionality of storing one bit of information; and counter
automata implement modular counting. Other prime automata can be used to
capture several kinds of symmetries, such as capturing whether a regular
polygon is in its initial position after applying a sequence of rotations and
reflections. Except for the flip-flop automaton, which is of a special sort,
all other prime automata correspond to groups. In particular to _simple
groups_ —the building blocks of all groups. Simple groups have been
systematically classified into a finite number of families, as the result of a
huge collaborative effort that spanned about 50 years, cf. (?). The
classification provides a compass in the landscape of groups, and a roadmap
for the exploration of temporal logics, as it will become clear in this paper.

We start our investigation from the observation that flip-flop automata
correspond to the since operator of Past Linear Temporal Logic (Past LTL). The
correspondence of Past LTL formulas with cascades is not immediate. Cascades
have the additional capabilities of defining intermediate objects. In a
cascade, the output of a component can be used by all subsequent components,
i.e., the graph of dependencies in a cascade is a directed acyclic graph
(DAG). This clashes with the treelike structure of formulas. So we turn to
logic programs, which are able to capture the DAG-like structure present in
cascades. Note that, in the end, it is just a matter of succinctness, as rules
(with no cyclic dependencies) can always be unfolded into a single formula.
However, unfolding can incur an exponential blow-up, and it amounts to losing
structure, which may be undesirable. Namely, in the resulting formulas would
not be explicit whether several subformulas are identical.

We propose the _Krohn-Rhodes Logics_. They are a family of logics that come in
the form of logic programs, where rules feature temporal modal operators
defined in terms of automata. We show they have a close structural
correspondence with automata cascades, both ways. Thus, on one hand, they can
be seen as logics for specifying automata cascades. On the other hand, they
inherit the support of the Krohn-Rhodes theory for automata cascades. In
particular, we can define _prime operators_ using prime automata, which yields
a series of fundamental results about the expressivity of such logics. Using
different sets of prime operators, one obtains Krohn-Rhodes Logics whose
expressivity ranges from the star-free regular languages to all regular
languages, with the capability of capturing infinite hierarchies of languages
between the former two classes. The Krohn-Rhodes Logics open to the
possibility of investigating such languages, to understand which ones have the
expressivity required by specific applications. Dually, the Krohn-Rhodes
Logics effectively import (semi)group theory into the realm of logic, with the
possibility of investigating (semi)group-theoretic questions through the lens
of logic, and of solving group-theoretic problems via logical reasoning.

The Krohn-Rhodes Logics are a valuable addition to the rich set of past
temporal and dynamic logics adopted in knowledge representation, with many
applications in AI and in computer science. Such logics are used in
Reinforcement Learning to specify reward functions (?; ?; ?) as well as for
specifying the dynamics of a domain (?). Furthrmore, they are used in process
mining to describe the traces of a process (?). Finally, an application that
we envision is as specification languages for priors in learning applications
(?; ?). Here providing learning algorithms with priors such as the existence
of symmetries reduces the amount of data required to learn. Symmetries are
captured by groups, which in turn can be natively expressed in our KR Logics.

Background is covered in Section 2–5. Our novel contribution is Section 6.
Related work is Section 7. All proofs are included, with some proofs deferred
to the appendix.

##  2 Temporal Logic

We introduce _Past Linear Temporal Logic_ (Past LTL), c.f. (?). It provides
the context of the temporal logics, and it will be directly considered in the
paper.

Syntax. A _propositional variable_ is an element from a set $\mathcal{V}$ that
we consider as given. Typically we denote propositional variables by lowercase
Latin letters. A _propositional constant_ is either _top_ $\top$ or _bottom_
$\bot$. A _propositional atom_ is either a variable or a constant. A _static
formula_ is built out of propositional atoms and the _Boolean operators_
$\\{\neg,\land,\lor\\}$. It is defined inductively as a propositional atom or
one of the following expressions: $\neg\alpha$, $\alpha\land\beta$,
$\alpha\lor\beta$. Additional Boolean operators may be defined, but it is not
necessary as the former operators are _universal_ , they suffice to express
all Boolean functions. A _(Past LTL) formula_ is built out of static formulas
by means of the _temporal operators_ $\\{\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}},\operatorname{\mathcal{S}}\\}$,
called the _before operator_ and the _since operator_ , respectively. It is
defined inductively as a static formula or one of the following two
expressions: $\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\alpha$,
$\alpha\operatorname{\mathcal{S}}\beta$. Additional temporal operators can be
defined in terms of the previous operators, e.g., _sometimes in the past_
$\operatorname{\leavevmode\hbox to8.7pt{\vbox
to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{2.58333pt}\pgfsys@lineto{5.5972pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\alpha:=\top\operatorname{\mathcal{S}}\alpha$
and _always in the past_ $\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{2.58333pt}\pgfsys@lineto{4.95137pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\alpha:=\neg\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{2.58333pt}\pgfsys@lineto{5.5972pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg\alpha$.

Semantics. An _interpretation $I$ for a static formula $\alpha$_ is a subset
of the propositional variables $V_{\alpha}$ in the formula. Intuitively, the
fact that a variable appears in the intepretation means that the variable
stands for a proposition that is true. It can also be seen as an assignment.
An _assignment_ for a formula $\alpha$ is a function
$\nu:V_{\alpha}\to\mathbb{B}$ where $\mathbb{B}=\\{0,1\\}$ is called _Boolean
domain_. An interpretation $I$ corresponds to the assignment $\nu$ such that
$\nu(a)=1$ iff $a\in I$. Then, the semantics of formulas is defined in terms
of the following satisfiability relation. Given a static formula $\alpha$ and
an interpretation $I$ for $\alpha$, the _satisfiability relation_
$I\models\alpha$ is defined following the structural definition of formulas,
for atoms as

  * •

$I\models\top$, $I\not\models\bot$,

  * •

$I\models a$ iff $a\in I$,

and inductively for non-atomic formulas as

  * •

$I\models\neg\alpha$ iff $I\neg\models\alpha$,

  * •

$I\models\alpha\lor\beta$ iff $I\models\alpha$ or $I\models\beta$,

  * •

$I\models\alpha\land\beta$ iff $I\models\alpha$ and $I\models\beta$.

An _interpretation for a temporal formula $\alpha$_ is a finite non-empty
sequence of sets of propositional variables—note that the sequence consisting
of the empty set is valid, since it consists of one element. Intuitively, the
fact that an atom appears in the $t$-th element of the intepretation means
that the variable stands for a proposition that is true at time $t$. Such
interpretation can also be seen as a sequence of assignments. The semantics of
formulas is defined in terms of the following satisfiability relation, which
extends the one above, also making it relative to time $t\in\\{1,2,\dots,\\}$.
Given a temporal formula $\alpha$, and an interpretation $I=I_{1},\dots,I_{n}$
for $\alpha$, the _satisfiability relation_ $I,t\models\alpha$ is defined
following the structural definition of formulas:

  * •

$I,t\models\top$, $I,t\not\models\bot$,

  * •

$I,t\models a$ iff $a\in I_{t}$,

  * •

$I,t\models\neg\alpha$ iff $I,t\neg\models\alpha$,

  * •

$I,t\models\alpha\lor\beta$ iff $I,t\models\alpha$ or $I,t\models\beta$,

  * •

$I,t\models\alpha\land\beta$ iff $I,t\models\alpha$ and $I,t\models\beta$.

  * •

$I,t\models\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\alpha$ iff
$I,t-1\models\alpha$,

  * •

$I,t\models\alpha\operatorname{\mathcal{S}}\beta$ iff there exists $j\in[1,t]$
such that $I,j\models\beta$ and, for every $k\in[j+1,t]$, it holds that
$I,k\models\alpha$.

We observe that the since operator admits an equivalent, inductive,
caracterisation of its semantics, cf. (?). We have that
$I,t\models\alpha\operatorname{\mathcal{S}}\beta$ holds iff any of the two
following conditions hold:

  1. 1.

$I,t\models\beta$,

  2. 2.

$I,t-1\models\alpha\operatorname{\mathcal{S}}\beta$ and
$\Pi,I,t\models\alpha$.

An assignment $\nu$ to variables $\\{a_{1},\dots,a_{m}\\}$ can be seen as the
conjunction $l_{1}\land\dots\land l_{m}$ where $l_{i}=a_{i}$ if $\nu(a_{i})=1$
and $l_{i}=\neg a_{i}$ otherwise. This allows us to write $I,t\models\nu$.

##  3 Languages and Expressivity

An _alphabet_ $\Sigma$ is a nonempty finite set of elements called _letters_.
A _string_ over $\Sigma$ is a finite concatenation $\sigma_{1}\dots\sigma_{n}$
of letters from $\Sigma$. A _language_ over $\Sigma$ is a set of strings over
$\Sigma$.

Given an ordered set $V=\\{a_{1},\dots,a_{m}\\}$ of propositional variables,
we can see every letter $\sigma$ of $\Sigma=\mathbb{B}^{m}$ as assignment to
such variables. Namely, we have $\sigma(a_{i})=b_{i}$ when $\sigma$ is the
Boolean tuple $\sigma=\langle b_{1},\dots,b_{m}\rangle$. Note that $b_{i}$ in
this case is not a variable but a Boolean value. In turn, $\sigma$ can be seen
as an interpretation for a static formula, and a string
$I=\sigma_{1}\dots\sigma_{\ell}$ over $\Sigma$ can be seen as an
interpretation for a temporal formula. Then, given a formula $\alpha$ on
variables $V$, we say that the formula _accepts_ a string $I$ if and only if
$(I,\ell)\models\alpha$. The _language recognised_ by $\alpha$ is the set of
strings that are accepted by $\alpha$.

The _expressivity_ of a (temporal) logic is the set of languages the logic
recognises. Given two logics $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, we say
$\mathcal{L}_{1}\sqsubseteq\mathcal{L}_{2}$ when the expressivity of
$\mathcal{L}_{1}$ is contained in the expressivity of $\mathcal{L}_{2}$;
furthermore, we say $\mathcal{L}_{1}\equiv\mathcal{L}_{2}$ when
$\mathcal{L}_{1}\sqsubseteq\mathcal{L}_{2}$ and
$\mathcal{L}_{2}\sqsubseteq\mathcal{L}_{1}$.

##  4 Automata

Figure 1: State diagrams of two automata.

We introduce _finite-state automata_ , c.f. (?; ?), which here we term simply
automata.

An automaton is a mathematical description of a stateful machine that
processes strings in a synchronous sequential manner, by performing an
elementary computation step on each input letter, and returning an output
letter as a result of the step. At its core lies the mechanism that updates
the internal state at each step. This mechanism is captured by the notion of
semiautomaton. A _semiautomaton_ is a tuple $D=\langle\Sigma,Q,\delta\rangle$
where: $\Sigma$ is an alphabet called the _input alphabet_ ; $Q$ is a finite
non-empty set of elements called _states_ ; $\delta:Q\times\Sigma\to Q$ is a
function called _transition function_. A semiautomaton is trivial if $|Q|=1$.
Automata are obtained from semiautomata by adding an initial state and output
functionality. An _automaton_ is a tuple
$A=\langle\Sigma,Q,\delta,q_{\mathrm{init}},\Gamma,\theta\rangle$ where:
$D_{A}=\langle\Sigma,Q,\delta\rangle$ is a semiautomaton, called the
_semiautomaton_ of $A$; $q_{\mathrm{init}}\in Q$ is called _initial state_ ;
$\Gamma$ is an alphabet called _output alphabet_ ,
$\theta:Q\times\Sigma\to\Gamma$ is called _output function_. An _acceptor_ is
a special kind of automaton where the output function is a Boolean-valued
function $\theta:Q\times\Sigma\to\\{0,1\\}$. Automata can be represented via
their _state diagram_ , such as the one in Figure 1. It is a graph where every
node stands for a state, and labelled edges stand for transitions. The initial
state can be marked by an arrow.

The _execution_ of automaton $A$ on an input string
$s=\sigma_{1}\dots\sigma_{n}$ proceeds as follows. Initially, the automaton is
in state $q_{0}=q_{\mathrm{init}}$. Upon reading letter $\sigma_{i}$, the
state is updated as $q_{i}=\delta(q_{i-1},\sigma_{i})$, and the automaton
returns the letter $\theta(q_{i-1},\sigma_{i})$.111We adopt a Mealy-style
output function, where the last state $q_{n}$ does not play a direct role in
determining the last output, as it happens instead with a Moore-style output
function. It is well-known that the latter can be mimicked as
$\theta(q_{n-1},\sigma_{n})=\theta^{\prime}(\delta(q_{n-1},\sigma_{n}),\sigma_{n})$.
The _language recognised_ by an acceptor $A$ is the set of strings on which it
returns $1$ as its last output. The _expressivity_ of a class of acceptors is
the set of languages they recognise. The expressivity of all acceptors is the
_regular languages_ (?), i.e., the languages that can be specified by regular
expressions.

State Transformations. In order to analyse automata, it is convenient to
introduce the notion of state transformation. A _state transformation_ is a
function $\tau:Q\to Q$ from states to states, and it is called: (i) a
_permutation_ if it is a bijection, i.e., $Q=\\{\tau(q)\mid q\in Q\\}$, (ii) a
_reset_ if it constant, i.e., there is $q_{0}\in Q$ such that $\tau(q)=q_{0}$
for every $q\in Q$, (iii) an _identity_ if it is an identity function, i.e.,
$\tau(q)=q$ for every $q\in Q$. Note that an identity transformation is, in
particular, a permutation transformation. Every input letter $\sigma\in\Sigma$
induces the state transformation $\delta_{\sigma}(q)=\delta(q,\sigma)$. Such
state transformation $\delta_{\sigma}$ describes all state updates triggered
by the input letter $\sigma$. In particular, the _set of state
transformations_ of a (semi)automaton is
$\\{\delta_{\sigma}\mid\sigma\in\Sigma\\}$. Any two letters that induce the
same state transformation are equivalent for the semiautomaton, in the sense
that they trigger the same state updates. Such equivalence can be made
explicit by writing a semiautomaton as consisting of two components. The first
component is an _input function_ that translates input letters into letters of
an _internal alphabet_ $\Pi$, where each letter represents an equivalence
class of inputs. The second component is a semiautomaton operating on the
internal alphabet $\Pi$. This way, the internal letters induce distinct state
transformations.

######  Definition 1.

Given a function $\phi:\Sigma\to\Pi$, and a semiautomaton
$\langle\Pi,Q,\delta\rangle$ their _composition_ is the semiautomaton
$\langle\Sigma,Q,\delta_{\phi}\rangle$ where $\delta_{\phi}$ is defined as
$\delta_{\phi}(q,\sigma)=\delta(q,\phi(\sigma))$. We call $\phi$ the _input
function_ of the resulting semiautomaton, and we call $\Pi$ its _internal
alphabet_.

We will often write semiautomata with an explicit input function—w.l.o.g.
since we can always choose the identity function.

###  4.1 Automata on Assignments

We describe automata that operate on Boolean tuples, seen as assignments to
propositional variables. These automata can process interpretations of
temporal formulas. An _automaton on assignments_ is an automaton
$A=\langle\Sigma,Q,\delta,q_{\mathrm{init}},\Gamma,\theta\rangle$ where
$\Sigma=\mathbb{B}^{m}$ and $\Gamma=\mathbb{B}^{k}$. Given two ordered sets
$U=\\{a_{1},\dots,a_{m}\\}$ and $V=\\{b_{1},\dots,b_{k}\\}$ of propositional
variables, the automaton can be seen as reading interpretations of $U$, and
returning interpretations for $V$. Note that the actual variables being
assigned do not matter for the automaton, but fixing input and output
variables makes the notation easier. In particular, when the output of the
automaton on $I=\sigma_{1}\dots\sigma_{\ell}$ upon reading $\sigma_{t}$ is
$\gamma$, for every $b_{i}\in V$, we write $(A,I,t)\vdash b_{i}$ if and only
if $\gamma(b_{i})=1$.

###  4.2 Automata Cascades

Automata can be described in a structured, modular, way as _cascades_ of
simpler (semi)automata, where components are arranged in a sequence, with each
component receiving information from the previous ones, in addition to
receiving the external input, c.f. (?). First, we can use cascades to build
semiautomata out of simpler semiautomata.

######  Definition 2.

A _semiautomata cascade_ is a semiautomaton $A=\langle\Sigma,Q,\delta\rangle$
given by the composition of $d$ semiautomata
$A_{i}=\langle\Sigma_{i},Q_{i},\delta_{i}\rangle$ as described next. The
alphabets are require to be of the form:

$\displaystyle\Sigma_{i}$
$\displaystyle=\Sigma\times\Sigma_{1}\times\dots\times\Sigma_{i-1},$

The state space of $A$ is

$\displaystyle Q$ $\displaystyle=Q_{1}\times\dots\times Q_{d},$

and its transition function is

$\displaystyle\delta(\langle
q_{1},\dots,q_{d}\rangle,\sigma)=\langle\delta_{1}(q_{1},\sigma_{1}),\dots,\delta_{d}(q_{d},\sigma_{d})\rangle,$
$\displaystyle\text{where
}\sigma_{i}=\langle\sigma,q_{1},\dots,q_{i-1}\rangle.$

We write the cascade as $A=A_{1}\ltimes\dots\ltimes A_{d}$, and we call each
semiautomaton $A_{i}$ a _component_ of the cascade.

A more general approach is to build automata directly out of simpler
automata—rather than semiautomata.

######  Definition 3.

An _automata cascade_ is an automaton
$A=\langle\Sigma,Q,\delta,q_{\mathrm{init}},\Gamma,\theta\rangle$ given by the
composition of $d$ automata
$A_{i}=\langle\Sigma_{i},Q_{i},\delta_{i},q_{i}^{\mathrm{init}},\Gamma_{i},\theta_{i}\rangle$
as described next. The alphabets are required to satisfy:

$\displaystyle\Sigma_{i}$
$\displaystyle=\Sigma\times\Gamma_{1}\times\dots\times\Gamma_{i-1},$
$\displaystyle\Gamma_{d}$ $\displaystyle=\Gamma.$

The state space of $A$ and its initial state are

$\displaystyle Q$ $\displaystyle=Q_{1}\times\dots\times Q_{d},$ $\displaystyle
q_{\mathrm{init}}$ $\displaystyle=\langle
q_{1}^{\mathrm{init}},\dots,q_{d}^{\mathrm{init}}\rangle,$

its transition function is

$\displaystyle\delta(\langle
q_{1},\dots,q_{d}\rangle,\sigma)=\langle\delta_{1}(q_{1},\sigma_{1}),\dots,\delta_{d}(q_{d},\sigma_{d})\rangle,$
$\displaystyle\text{where
}\sigma_{i}=\langle\sigma,\theta_{1}(q_{1},\sigma_{1}),\dots,\theta_{i-1}(q_{i-1},\sigma_{i-1})\rangle,$

and its output function is

$\displaystyle\theta(q,\sigma)=\theta_{d}(q_{d},\sigma_{d}).$

We write the cascade as $A=A_{1}\ltimes\dots\ltimes A_{d}$, and we call each
automaton $A_{i}$ a _component_ of the cascade. A cascade is _simple_ if
$\theta_{i}(q_{i},\sigma_{i})=q_{i}$ for every $1\leq i\leq d-1$.

The main advantage of having automata as components is the additional
flexibility given by the intermediate output functions. A component can use
its output function to return values based on its state and input, instead of
simply returning its state. This way, output functions allow for extra
factorisation, as otherwise any computation performed by the output function
of a component in the cascade should be repeated by all subsequent components
that needs it. We will avoid to distinguish between the two kinds of cascades
except when it is important from a technical point of view.

##  5 The Krohn-Rhodes Theory

The Krohn-Rhodes theory describes how automata can be expressed as cascades of
basic automata (?). At a high-level, the theory identifies classes of basic
semiautomata, called _primes_ , that suffice to express a given semiautomaton
as a cascade. One such class are the flip-flop semiautomata. They are the
automaton version of the flip-flops from digital circuits, implementing the
fundamental functionality of storing one bit of information. Below, we present
the canonical flip-flop, which has descriptive names for inputs and states.

######  Definition 4.

Let $\mathit{set}$, $\mathit{reset}$, $\mathit{read}$, and $\mathit{high}$,
$\mathit{low}$ be distinguished symbols. The _canonical flip-flop
semiautomaton_ is the semiautomaton $\langle\Pi,Q,\delta\rangle$ where the
input alphabet is $\Pi=\\{\mathit{set},\mathit{reset},\mathit{read}\\}$, the
states are $Q=\\{\mathit{high},\mathit{low}\\}$, and the transition function
is defined as:

$\displaystyle\delta(\mathit{read},q)=q,\quad\delta(\mathit{set},q)=\mathit{high},\quad\delta(\mathit{reset},q)=\mathit{low}.$

The state diagram of the canonical flip-flop semiautomaton is shown in Figure
1. Another class of prime semiautomata is the class of $n$-counters for $n$ a
prime number. Below, we present the canonical $n$-counter.

######  Definition 5.

The _canonical $n$-counter_ is the semiautomaton $\langle\Pi,Q,\delta\rangle$
where $\Pi=Q=[0,n-1]$ and the transition function is:

$\displaystyle\delta(i,j)=i+j\,(\operatorname{mod}n).$

We introduce the theory below, following (?).

###  5.1 Homomorphic Representations

A pair $\psi=\langle\psi_{1},\psi_{2}\rangle$ of surjective mappings
$\psi_{1}:\Sigma\to\Sigma^{\prime}$ and $\psi_{2}:Q\to Q^{\prime}$ is a
_homomorphism_ of $A=\langle\Sigma,Q,\delta\rangle$ onto
$A^{\prime}=\langle\Sigma^{\prime},Q^{\prime},\delta^{\prime}\rangle$ if, for
every $\sigma\in\Sigma,q\in Q$, it holds that
$\psi_{1}(\delta(q,\sigma))=\delta^{\prime}(\psi_{1}(q),\psi_{2}(\sigma))$. If
$\psi_{1}$ and $\psi_{2}$ are bijective functions, then $A$ and $A^{\prime}$
are said to be _isomorphic_. Given a semiautomaton
$A=\langle\Sigma,Q,\delta\rangle$, a semiautomaton
$A^{\prime}=\langle\Sigma^{\prime},Q^{\prime},\delta^{\prime}\rangle$ is a
_subsemiautomaton_ of $A$ if $\Sigma^{\prime}\subseteq\Sigma$,
$Q^{\prime}\subseteq Q$, and $\delta^{\prime}$ is the restriction of $\delta$
to $\Sigma^{\prime}\times Q^{\prime}$ satisfies
$\delta^{\prime}(q^{\prime},\sigma^{\prime})\in Q^{\prime}$ for every
$q^{\prime}\in Q^{\prime},\sigma^{\prime}\in\Sigma^{\prime}$. If $A$ has a
subsemiautomaton which can be mapped homomorphically by $\psi$ onto
$A^{\prime}$, then we say that $A$ _homomorphically represents_ $A^{\prime}$.

The notion of homomorphic representation is important because of the following
propositions, which show that it describes the capabilities of a
semiautomaton.

######  Proposition 1.

If a semiautomaton $D_{2}$ is homomorphically represented by a semiautomaton
$D_{1}$, then every language recognised by an acceptor with semiautomaton
$D_{2}$ is also recognised by an acceptor whose semiautomaton is the
composition of $D_{1}$ with an input function.

######  Proposition 2.

If a semiautomaton $D_{2}$ is not homomorphically represented by a
semiautomaton $D_{1}$, and $D_{2}$ admits a state from which all the other
states can be reached, then there is a language recognised by an acceptor with
semiautomaton $D_{2}$ that is not recognised by any acceptor whose
semiautomaton is the composition of $D_{1}$ with an input function.

###  5.2 Algebraic Preliminaries

A _semigroup_ is a non-empty set together with an _associative_ binary
operation that combines any two elements $a$ and $b$ of the set to form a
third element $c$ of the set, written $c=(a\cdot b)$. A _monoid_ is a
semigroup that has an _identity element_ $e$, i.e., $(a\cdot e)=(e\cdot a)=a$
for every element $a$. The identity element is unique when it exists. A _flip-
flop monoid_ is a three-element monoid $\\{s,r,e\\}$ where $(r\cdot s)=s$,
$(s\cdot s)=s$, $(r\cdot r)=r$, $(s\cdot r)=r$. A _group_ is a monoid where
every element $a$ has an _inverse_ $b$, i.e., $(a\cdot b)=(b\cdot a)=e$ where
$e$ is the identity element. A _subsemigroup_ (_subgroup_) of a semigroup $G$
is a subset of $G$ that is a semigroup (group).

Let $G$ be a group and let $H$ be a subgroup of $G$. For every $g\in G$, the
_right coset_ of $G$ is $gH=\\{gh\mid h\in H\\}$, and its _left coset_ is
$Hg=\\{hg\mid h\in H\\}$. Subgroup $H$ is _normal_ if its left and right
cosets coincide, i.e., $gH=Hg$ for every $g\in G$. A group is _trivial_ if it
is $\\{e\\}$ where $e$ is the identity element. A _simple group_ is a group
$G$ such that every normal subgroup of $G$ is either trivial or $G$ itself.

A _homomorphism_ from a semigroup $S$ to a semigroup $T$ is a mapping
$\psi:S\to T$ such that $\psi(s_{1}\cdot s_{2})=\psi(s_{1})\cdot\psi(s_{2})$
for every $s_{1},s_{2}\in S$. If $\psi$ is surjective, we say that $T$ is a
_homomorphic image_ of $S$. If $\psi$ is bijective, we say that $S$ and $T$
are _isomorphic_ , and $\psi$ is called an _isomorphism_. A semigroup $S$
_divides_ a semigroup $T$ if $T$ has a subsemigroup $T^{\prime}$ such that $S$
is a homomorphic image of $T^{\prime}$. If $G$ is _simple_ , then every
homomorphic image of $G$ is isomorphic to $\\{e\\}$ or $G$. For $G$ and $H$
semigroups, we write $GH=\\{g\cdot h\mid g\in G,h\in H\\}$. We also write
$H^{1}=H$ and $H^{k}=HH^{k-1}$. A semigroup $S$ is _generated_ by a semigroup
$H$ if $S=\bigcup_{n}H^{n}$; then $H$ is called a _generator_ of $S$.

###  5.3 Algebraic Notions for Automata

We consider semigroups consisting of transformations, where the associative
binary operation is function composition. The _characteristic semigroup_
$\operatorname{\mathbf{S}}(A)$ of a semiautomaton $A$ is the semigroup
generated by its transformations. The characteristic semigroup of an automaton
is the one of its semiautomaton.

Given a semigroup $S$, the semiautomaton defined by $S$ is $A_{S}=\langle
S\cup\\{e\\},S,\delta\rangle$ where $e$ is the identity element and
$\delta(s_{1},s_{2})=s_{1}\cdot s_{2}$.

A _flip-flop semiautomaton_ is a semiautomaton $A_{F}$ that is defined by a
flip-flop monoid $F$. A _(simple) grouplike semiautomaton_ is a semiautomaton
defined $A_{G}$ by a (simple) group $G$. For an automaton, if so is its
semiautomaton. A _prime semiautomaton_ is a semiautomaton that is isomorphic
to a flip-flop semiautomaton or to a simple grouplike semiautomaton. An
automaton is prime if so is its semiautomaton. Two notes about the canonical
semiautomata introduced above: (i) the canonical flip-flop semiautomaton is a
flip-flop semiautomaton; (ii) the canonical $n$-counter is defined by a cyclic
group $C_{n}$ of order $n$, and hence it is prime if so is $n$, since $C_{n}$
is simple iff $n$ is prime.

A _permutation (semi)automaton_ is a (semi)automaton whose transformations are
permutations. A _group-free (semi)automaton_ is a (semi)automaton only trivial
groups divide its characteristic semigroup.

###  5.4 The Prime Decomposition Theorem

The notions in the previous sections suffice to state the Krohn-Rhodes
theorem.

######  Theorem 1 (Krohn-Rhodes Prime Decomposition).

Let $A$ be a semiautomaton, and let $G_{1},\dots,G_{n}$ be the simple groups
that divide the characteristic semigroup $\operatorname{\mathbf{S}}(A)$. Then
$A$ can be represented homomorphically by a semiautomata cascade of components
with characteristic semigroup from $\\{F,G_{1},\dots,G_{n}\\}$, where $F$ is a
flip-flop monoid, which may be excluded when $A$ is a nontrivial permutation
automaton.

Conversely, let $A_{1}\ltimes\dots\ltimes A_{n}$ be a semiautomata cascade
that homomorphically represents the automaton $A$. If a subsemigroup $S$ of a
flip-flop monoid $F$ or a simple group $S$ is a homomorphic image of a
subsemigroup of $\operatorname{\mathbf{S}}(A)$, then $S$ is a homomorphic
image of a subsemigroup of $\operatorname{\mathbf{S}}(A_{i})$ for some $1\leq
i\leq n$.

An immediate implication is that prime automata with an input function suffice
to express every semiautomaton, and hence to build cascades that capture the
regular languages. A second implication is that group-free semiautomata can be
expressed as cascades of flip-flops with an input function. Group-free
automata are important because they capture _noncounting automata_ , c.f. (?),
whose expressivity is the _star-free regular languages_ (?)—i.e., the
languages that can be specified by regular expressions without using the
Kleene star but using complementation.

######  Theorem 2.

The expressivity of cascades of prime automata with an input function is the
regular languages. The expressivity of cascades of flip-flop automata with an
input function is the star-free regular languages.

##  6 The Krohn-Rhodes Logics

We propose a family of temporal logics of the past. They are logic programs
where operators are specified by automata. We will show they have a close
correspondence with cascades, and hence they are supported by the Krohn-Rhodes
theory.

Syntax. A _static rule_ is

$\displaystyle p\,\colonminus\,\alpha$ (1)

where $p$ is a propositional variable, and $\alpha$ is a static formula. A
_delay rule_ is

$\displaystyle p\,\colonminus\,\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}q$ (2)

where $p$ and $q$ are propositional variables. An _operator automaton_
$\mathcal{A}$ is a semiautomaton on assignments, with indexes as states, and
with an initial state. Specifically,
$\mathcal{A}=\langle\Sigma,Q,\delta,q_{\mathrm{init}}\rangle$ where
$\Sigma=\mathbb{B}^{m}$ and $Q=[1,n]$. We call $m$ the input arity of
$\mathcal{A}$, and $n$ its output arity. A _dynamic rule_ is

$\displaystyle p_{1},\dots,p_{n}\,\colonminus\,\mathcal{A}(a_{1},\dots,a_{m})$
(3)

where $q_{1},\dots,q_{n},a_{1},\dots,a_{m}$ are variables, and $\mathcal{A}$
is an operator automaton with input arity $m$ and output arity $n$. A
_(temporal) rule_ is a static, delay, or dynamic rule. In a rule, the
expression on the left of ‘$\,\colonminus\,$’ is called the _head_ of the
rule, and the expression on the right is called the _body_. A _(temporal)
program_ is a finite set of rules. We require programs to be _nonrecursive_ ,
i.e., to have an acyclic dependency graph. The _dependency graph_ of a program
consists of one node for each variable in the program, and it has a directed
edge from $a$ to $b$ if there is a rule where $a$ is in the body and $b$ is
the head. We also require programs to be _definitorial_ , i.e., every variable
$p$ occurs at most once in head position; if $p$ occurs in the head of a rule
$r$, we say that $r$ _defines_ $p$. In a given program, a variable is a
_defined variable_ if there is a rule in the program that defines it, and it
is an _input variable_ otherwise.

Semantics. An _interpretation_ for a (temporal) program $P$ is a non-empty
sequence finite non-empty sequence of subsets of the input variables of $P$.
The semantics of programs is defined in terms of the following satisfiability
relation, which extends the one for formulas by taking the program into
account. Given a program $P$, an interpretation $I=I_{1},\dots,I_{\ell}$ for
$P$, a time point $t$, and formula $\alpha$, the _satisfiability relation_
$(P,I,t)\models\alpha$ is defined following the structural definition of
programs and formulas:

  1. 1.

$(P,I,t)\models\top$, $(P,I,t)\not\models\bot$,

  2. 2.

$(P,I,t)\models a$ with $a$ an input variable iff $a\in I_{t}$,

  3. 3.

$(P,I,t)\models\neg\alpha$ iff $(P,I,t)\not\models\alpha$,

  4. 4.

$(P,I,t)\models\alpha\lor\beta$ iff $(P,I,t)\models\alpha$ or
$(P,I,t)\models\beta$,

  5. 5.

$(P,I,t)\models\alpha\land\beta$ iff $(P,I,t)\models\alpha$ and
$(P,I,t)\models\beta$.

  6. 6.

$(P,I,t)\models p$ with $p$ defined by (1) iff $(P,I,t)\models\alpha$,

  7. 7.

$(P,I,t)\models p$ with $p$ defined by (2) iff $(P,I,t-1)\models q$,

  8. 8.

$(P,I,0)\models p_{i}$ with $p_{i}$ defined by (3) iff $q_{\mathrm{init}}=i$,

  9. 9.

$(P,I,t)\models p_{i}$ with $p_{i}$ defined by (3) and $t>0$ iff, for some $j$
and some assignment $\sigma$ to variables $\\{a_{1},\dots,a_{m}\\}$,

$\displaystyle\delta(j,\sigma)=i,\quad(P,I,t-1)\models
p_{j},\quad(P,I,t)\models\sigma.$

This semantics extends the one for temporal formulas, by defining the
semantics of defined variables. For such variables, instead of checking
whether they are in the given interpretation, we check whether they are true
according to the rule that defines them (Points 7–10). The semantics of delay
rules (Point 8) follows the semantics of the before operator. The semantics of
dynamic rules (Points 9 and 10) follows the semantics of automata.
Intuitively, such rules pass assignments to the operator automaton, and
receive assignments for the head variables, that indicate the current
automaton state, in a one-hot encoding fashion. From Point 10 it might seem
that there is some nondeterminism, but there is not, as it will be clear later
from the correspondence with cascades, which are deterministic.

###  6.1 Notable Operators

We present some instances of automaton operators.

#### Flip-Flop Operator.

The _flip-flop operator_ $\mathcal{F}$ is

$\displaystyle\mathcal{F}=\langle\mathbb{B}^{2},\\{1,2\\},\delta,1\rangle,$
$\displaystyle\delta(q,00)=q,\quad\delta(q,10)=\delta(q,11)=2,\quad\delta(q,01)=1.$

Note that $\mathcal{F}$ is isomorphic to the composition of the canonical
flip-flop semiautomaton with the following input function:

$\displaystyle\phi(00)=\mathit{read},\quad\phi(10)=\phi(11)=\mathit{set},\quad\phi(01)=\mathit{reset}.$

This is the kind of encoding of input signals that is found in digital
circuits. In fact, the encoding above is the one of an _SR latch_ (where,
however, input $11$ is not allowed). Intuitively, it allows us to specify
flip-flops as a rule

$\displaystyle\mathit{low},\mathit{high}\,\colonminus\,\mathcal{F}(\mathit{set},\mathit{reset}),$

where here variable names are chosen to indicate a correspondence with the
canonical flip-flop semiautomaton.

#### Counter Operators.

These are operators based on the $n$-counter semiautomaton, and
subsemiautomata thereof. The _$n$ -counter operator_ $\mathcal{C}_{n}$ is

$\displaystyle\mathcal{C}_{n}=\langle\mathbb{B}^{n},[1,n],\delta,1\rangle,$
$\displaystyle\delta(i,b_{0}\dots b_{n-1})=i+j\,(\operatorname{mod}n),$
$\displaystyle j=\min\big{(}\\{1\\}\cup\\{k\mid b_{k}=1\\}\big{)}.$

When used in a rule

$\displaystyle
q_{0},\dots,q_{n-1}\,\colonminus\,\mathcal{C}_{n}(a_{0},\dots,a_{n-1}),$

the operator increases the value of the state by the minimum index of a
variable $a_{i}$ that is true, and $0$ if they are all false. The $n$ head
variables indicate the current state. So the index $i$ of the head variable
$q_{i}$ that is true corresponds to the current value of the counter. The
_simplified $n$-counter operator_ is

$\displaystyle\mathcal{C}^{\mathrm{s}}_{n}=\langle\mathbb{B},[1,n],\delta,1\rangle,\quad\text{
with }\delta(i,j)=i+j(\operatorname{mod}n).$

When used in a rule

$\displaystyle
p_{1},\dots,p_{n-1}\,\colonminus\,\mathcal{C}^{\mathrm{s}}_{n}(a),$

it increments by $1$ and $0$, when $a$ holds or not, respectively. The _parity
operator_ is $\mathcal{P}=\mathcal{C}^{\mathrm{s}}_{2}$. It checks whether the
input variable has been true an even number of times. It is exemplified by the
rules below:

$\displaystyle\mathit{even},\mathit{odd}$
$\displaystyle\,\colonminus\,\mathcal{P}(a),$
$\displaystyle\mathit{off},\mathit{on}$
$\displaystyle\,\colonminus\,\mathcal{P}(\mathit{toggle}).$

###  6.2 From Logic Programs to Automata Cascades

The logic programs we have introduced can be easily translated to cascades.
Note that the automata considered in this section are automata on assignments.

######  Lemma 1.

Every delay rule $r$ admits an equivalent automaton $A$ whose semiautomaton is
a flip-flop semiautomaton with an input function, i.e., $(r,I,t)\models h$ if
and only if $(A,I,t)\vdash h$.

###### Proof.

Let $r$ be a delay rule $h\colonminus\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$. We build the
corresponding automaton $A$ as follows. Letting $\Sigma=\mathbb{B}$, the
equivalent semiautomaton is defined as the automaton
$A=\langle\Sigma,Q,\delta_{\phi},q_{\mathrm{init}},\Gamma,\theta\rangle$
having a semiautomaton obtained as the composition of the canonical flip-flop
semiautomaton with the input function defined as $\phi(1)=\mathit{set}$ and
$\phi(0)=\mathit{reset}$, and output function defined as
$\theta(\mathit{high},\sigma)=1$ and $\theta(\mathit{low},\sigma)=0$. ∎

######  Lemma 2.

Every dynamic rule $r$ admits an equivalent automaton $A$, i.e.,
$(r,I,t)\models p_{i}$ if and only if $(A,I,t)\vdash p_{i}$.

###### Proof.

Consider a dynamic rule $r$ of the form (3). In particular let the operator
automaton be $\mathcal{A}=\langle\Sigma,Q,\delta,q_{\mathrm{init}}\rangle$
with $\Sigma=\mathbb{B}^{m}$ and $Q=[1,n]$. The equivalent automaton is
defined as the automaton
$A=\langle\Sigma,Q,\delta,q_{\mathrm{init}},\Gamma,\theta\rangle$ where
$\Gamma=\mathbb{B}^{n}$ and $\theta(q,\sigma)=\langle
b_{1},\dots,b_{n}\rangle$ where $b_{i}=1$ if $\delta(q,\sigma)=i$ and
$b_{i}=0$ otherwise—i.e., the output returns the one-hot encoding of the
state. ∎

######  Observation 1.

The automaton $A$ equivalent to $r$ has the same semiautomaton as the
automaton operator of $r$.

######  Lemma 3.

Every static rule $r$ admits an equivalent automaton $A$, i.e.,
$(r,I,t)\models p$ if and only if $(A,I,t)\vdash p$.

###### Proof.

Every static rule $r$ of the form $p\colonminus\alpha$ is equivalent to the
trivial automaton
$A=\langle\mathbb{B}^{m},\\{1\\},\delta,1,\mathbb{B},\theta\rangle$ where
$\theta(q,\sigma)=1$ iff $r,\sigma\models p$. ∎

######  Theorem 3.

Every program $P$ admits an equivalent cascade $C$, i.e., $(P,I,t)\models a$
if and only if $(C,I,t)\vdash a$.

###### Proof.

Consider a program $P$. Let us enumerate the rules $r_{1},\dots,r_{n}$ of $P$
such that $r_{i}$ does not depend on any rule $r_{j}$ with $j>i$—the
enumeration exists because the program is nonrecursive. In the base case
$n=1$, and the program consists of one rule $r_{1}$. Note that all variables
occurring in the body of $r_{1}$ are input variables. Rule $r_{1}$ admits an
equivalent automaton $A_{1}$ by the lemmas above. In the inductive case $n\geq
2$, and we assume that the subprogram $P^{\prime}=\\{r_{1},\dots,r_{n-1}\\}$
admits an equivalent cascade $A_{1}\ltimes\dots\ltimes A_{n-1}$. Rule $r_{n}$
admits an equivalent automaton $A_{n}$ by the lemmas above. The cascade
$A_{1}\ltimes\dots\ltimes A_{n-1}\ltimes A_{n}$ is equivalent to $P$. Note
that, in the cascade, the last component receives assignments to all variables
in $P^{\prime}$. ∎

######  Observation 2.

The cascade for a program has a number of components that is linear in the
number of rules. Static rules correspond to trivial automata, delay rules to
flip-flops with an input function, and dynamic rules to automata with the
semiautomaton of the operator of the rule.

###  6.3 From Automata Cascades to Logic Programs

Automata cascades can be easily translated into our logic programs. In
particular, rules allow for preserving the structure present in the cascade
architecture, and also the one within a single component. Namely, every
automaton is mapped to a program with one dynamic rule capturing its
semiautomaton, and static rules capturing its input and output functions.

######  Lemma 4.

Every automaton $A$ admits an equivalent program $P$, i.e., $(A,I,t)\vdash a$
if and only if $(P,I,t)\models a$.

###### Proof.

Consider an automaton

$\displaystyle
A=\langle\Sigma,Q,\delta_{\phi},q_{\mathrm{init}},\Gamma,\theta\rangle,$

whose semiautomaton is built as the composition of a semiautomaton
$\langle\Pi,Q,\delta\rangle$ and an input function $\phi$. In particular,
$\Sigma=\mathbb{B}^{m}$, $\Pi=\mathbb{B}^{k}$, and $\Gamma=\mathbb{B}^{h}$. We
constuct an equivalent program. Consider the operator automaton

$\displaystyle\mathcal{A}=\langle\Pi,Q^{\prime},\delta^{\prime},q^{\prime}_{\mathrm{init}},Q^{\prime},\delta^{\prime}\rangle,$

where $Q^{\prime}=[1,n]$, and $\delta^{\prime}(i,\pi)=j$ iff
$\delta(q_{i},\pi)=q_{j}$. Let us consider $Q=\\{q_{1},\dots,q_{n}\\}$ as
variables, and let us introduce fresh variables $V=\\{b_{1}\dots,b_{k}\\}$.
Let $r_{0}$ be the dynamic rule

$\displaystyle
q_{1},\dots,q_{n}\,\colonminus\,\mathcal{A}(b_{1},\dots,b_{k}).$

Let us introduce fresh variables
$Q^{\prime}=\\{q^{\prime}_{1},\dots,q^{\prime}_{n}\\}$, and let us define the
program $P_{\mathrm{state}}=\\{r_{0},r_{1},\dots,r_{n}\\}$ where rule $r_{i}$
for $1\leq i\leq n$ is defined as

$\displaystyle q_{i}^{\prime}\,\colonminus\,\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
Let $\phi_{i}$ be the projection of $\phi$ on its $i$-th component. Since
$\phi_{i}$ is a Boolean function, and the set $\\{\land,\lor,\neg\\}$ of
Boolean operators is universal, there exists a static formula $\varphi_{i}$ on
fresh variables $U=\\{a_{1},\dots,a_{m}\\}$ such that, for every
$\sigma\in\Sigma$, $\phi_{i}(\sigma)=1$ iff $\sigma\models\varphi_{i}$. Let us
define the program
$P_{\mathrm{in}}=\\{r^{\mathrm{in}}_{1},\dots,r^{\mathrm{in}}_{k}\\}$ where
rule $r^{\mathrm{in}}_{i}$ is defined as

$\displaystyle b_{i}\,\colonminus\,\varphi_{i}.$

Let $\theta_{i}$ be the projection of function $\theta$ on its $i$-th
component. There exists a static formula $\psi_{i}$ on variables
$Q^{\prime}\cup U$ such that, for every $q_{i}^{\prime}\in Q$ and every
$\sigma\in\Sigma$, $\theta_{i}(q_{i}^{\prime},\sigma)=1$ iff
$\\{q_{i}^{\prime}\\}\cup\sigma\models\psi_{i}$. Let us introduce fresh
variables $W=\\{c_{1},\dots,c_{h}\\}$, for the output of the automaton. Let us
define the program
$P_{\mathrm{out}}=\\{r^{\mathrm{out}}_{1},\dots,r^{\mathrm{out}}_{h}\\}$ where
rule $r^{\mathrm{out}}_{i}$ is defined as

$\displaystyle c_{i}\,\colonminus\,\psi_{i}.$

Then, the equivalent program is $P=P_{\mathrm{state}}\cup P_{\mathrm{in}}\cup
P_{\mathrm{out}}$. ∎

It is worth noting that a delay rule is required to capture an automaton. In
particular to capture the fact that the Mealy-style output function depends on
the before-update state. In particular, the following observation is
important.

######  Observation 3.

Program $P$ contains only one operator automaton, with a semiautomaton that is
isomorphic to the one of the given automaton.

######  Theorem 4.

Every cascade $C$ admits an equivalent program $P$, i.e., $(C,I,t)\vdash a$ if
and only if $(P,I,t)\models a$.

###### Proof.

Consider a cascade $C=A_{1}\ltimes\dots\ltimes A_{n}$. We proceed by induction
on $n$. In the base case $n=1$, $C=A_{1}$ and the program exists by Lemma 4.
In the inductive case $n\geq 2$, and we assume the cascade
$C^{\prime}=A_{1}\ltimes\dots\ltimes A_{n-1}$ admits an equivalent program
$P^{\prime}$, where variables $x_{1},\dots,x_{n}$ are input variables, and
variables $y_{i,1},\dots,y_{i,m_{i}}$ are for the output of automaton $A_{i}$.
By Lemma 4, automaton $A_{n}$ admits an equivalent program $P_{n}$, and we can
assume that the program has the former variables as input variables, and fresh
variables for the output. Thus, $P^{\prime}\cup P_{n}$ is equivalent to $C$. ∎

######  Observation 4.

The number of dynamic rules in the program is one, and the number of delay
rules equals the number of states of the automaton. The program has size
linear in the size of the automaton, if the input and output functions are
already represented by static programs in the automaton, or if we ignore their
representation.

###  6.4 Expressivity of the KR Logics

The correspondence with cascades allows us to apply the Krohn-Rhodes theory.
Here we use it to derive expressivity results about the KR Logics.

######  Definition 6.

Given a set $\mathbf{A}$ of operator automata, _the KR Logic with operators
from $\mathbf{A}$_ is the set of programs consisting of static rules, delay
rules, and dynamic rules with operators from $\mathbf{A}$. We write it as
$\mathcal{L}(\mathbf{A})$.

######  Definition 7.

A _prime operator_ is an operator automaton whose semiautomaton is the
composition of a surjective input function with a prime semiautomaton, called
its _core_. Two operators $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ are
_similar_ if their cores are isomorphic; we write
$\mathcal{A}_{1}\simeq\mathcal{A}_{2}$.

As a consequence of the correspondence with cascades, and of the Krohn-Rhodes
theorem, we obtain the following expressivity result.

######  Theorem 5.

The expressivity of the KR Logic with all prime operators is the regular
languages.

###### Proof.

The expressivity is within the regular languages since, by Theorem 3, every KR
Logic corresponds to an automata cascade, which is in particular an automaton,
and the expressivity of automata is the regular languages. Next we argue that
every regular language $L$ is recognised by a program with prime operators. By
Theorem 2, language $L$ is recognised by an acceptor $A$ that is a cascade of
prime semiautomata with an input function. Then, by Theorem 4, cascade $A$
admits an equivalent program $P$ with prime operators. Thus the expressivity
of such programs is the regular languages. ∎

######  Theorem 6.

The expressivity of the KR Logic $\mathcal{L}(\mathcal{F})$, with
$\mathcal{F}$ the flip-flop operator, is the star-free regular languages.

###### Proof.

By Theorems 3,4, programs of $\mathcal{L}(\mathcal{F})$ correspond to cascades
of flip-flops with an input function, whose expressivity is the star-free
regular languages (Theorem 2). ∎

######  Theorem 7.

For $\mathbf{A}_{1}$ and $\mathbf{A}_{2}$ sets of prime operators with
$\mathbf{A}_{1}\simeq\mathbf{A}_{2}$, we have
$\mathcal{L}(\mathbf{A}_{1})\equiv\mathcal{L}(\mathbf{A}_{2})$.

###### Proof.

We show $\mathcal{L}(\mathbf{A}_{1})\sqsubseteq\mathcal{L}(\mathbf{A}_{2})$,
and then $\mathcal{L}(\mathbf{A}_{2})\sqsubseteq\mathcal{L}(\mathbf{A}_{1})$
will be symmetric. By Theorem 3, every program $P$ of
$\mathcal{L}(\mathbf{A}_{1})$ admits an equivalent automaton $A$ whose
semiautomaton is a cascade $C=D_{1}\ltimes\dots\ltimes D_{n}$ where every
$D_{i}$ is the composition of an input function with a core of
$\mathbf{A}_{1}$. Such cores can be replaced with cores from $\mathbf{A}_{2}$,
since $\mathbf{A}_{1}\simeq\mathbf{A}_{2}$, so as to build an isomorphic
cascade $C^{\prime}=D_{1}^{\prime}\ltimes\dots\ltimes D_{n}^{\prime}$. Then,
by Proposition 1, there is an automaton $A^{\prime}$ that has semiautomaton
$C^{\prime}$ and it is equivalent to $A$. Then, by Theorem 4, there is a
program of $\mathcal{L}(\mathbf{A}_{2})$ that is equivalent to $A^{\prime}$,
hence to $A$, and hence to the program $P$ we initially considered. This
proves the theorem. ∎

Defining logics using operators that are not similar yields logics with
incomparable expressivity.

######  Theorem 8.

For $\mathbf{A}_{1}$ and $\mathbf{A}_{2}$ sets of prime operators with
$\mathbf{A}_{1}\not\simeq\mathbf{A}_{2}$, we have
$\mathcal{L}(\mathbf{A}_{1})\not\sqsubseteq\mathcal{L}(\mathbf{A}_{2})$ and
$\mathcal{L}(\mathbf{A}_{2})\not\sqsubseteq\mathcal{L}(\mathbf{A}_{1})$.

###### Proof.

We show
$\mathcal{L}(\mathbf{A}_{1})\not\sqsubseteq\mathcal{L}(\mathbf{A}_{2})$, and
then $\mathcal{L}(\mathbf{A}_{2})\not\sqsubseteq\mathcal{L}(\mathbf{A}_{1})$
will be symmetric. Let $\mathcal{A}$ be a prime operator in
$\mathbf{A}_{1}\setminus\mathbf{A}_{2}$. Consider the programs of
$\mathcal{L}(\mathbf{A}_{1})$ that have one dynamic rule with operator
$\mathcal{A}$. Assume by contradiction that every such program admits an
equivalent program in $\mathcal{L}(\mathbf{A}_{2})$. It implies, by Theorem 3,
that there is a semiautomaton $D$ isomorphic to a core of $\mathcal{A}$ such
that every language recognised by an acceptor with semiautomaton $D$ is also
recognised by an acceptor whose semiautomaton is a cascade
$C=A_{1}\ltimes\dots\ltimes A_{n}$ where every component $A_{i}$ is the
composition of an input function with a semiautomaton $D_{i}$ isomorphic to a
core of $\mathbf{A}_{2}$. In particular, $D$ and every $D_{i}$ are prime, and
every $A_{i}$ is a homomorphic image of $D_{i}$. By the contrapositive of
Proposition 2, we have that $C$ homomorphically represents $D$—in prime
semiautomata all states are reachable, as required by the proposition. Since
$D$ is prime, by the converse of the Krohn-Rhodes theorem, we have that $D$ is
a homomorphic image of a subsemigroup of $\operatorname{\mathbf{S}}(A_{i})$
for some $1\leq i\leq n$, and hence of $\operatorname{\mathbf{S}}(D_{i})$.
This is a contradiction, since $D_{i}$ is itself prime. ∎

Among others, the theorem allows us to establish hierarchies of KR Logics,
such as the one obtained by adding operators based on cyclic groups of prime
order.

######  Corollary 1.

$\mathcal{L}(\mathcal{C}_{2})\sqsubset\mathcal{L}(\mathcal{C}_{2},\mathcal{C}_{3})\sqsubset\mathcal{L}(\mathcal{C}_{2},\mathcal{C}_{3},\mathcal{C}_{5})\sqsubset\cdots$.

###  6.5 The Past LTL Fragment

In this section we discuss the relationship between Past LTL and the KR
Logics. In particular, Past LTL can be seen as a fragment of a KR Logic,
allowing us to transfer results from the previous sections to Past LTL.

We observe that the Boolean operators and the before operator are present both
in Past LTL and in the KR Logics. Thus, it suffices to show how the since
operator can be captured in KR Logics. It amounts to the operator automaton

$\displaystyle\mathcal{S}=\langle\mathbb{B}^{2},\\{1,2\\},\delta,1\rangle,$
$\displaystyle\delta(q,10)=q,\quad\delta(q,01)=\delta(q,11)=2,\quad\delta(q,00)=1.$

In fact, the Past LTL formula $\varphi=a\operatorname{\mathcal{S}}b$ is
equivalent to the dynamic rule $r$ defined as

$\displaystyle q_{1},q_{2}$
$\displaystyle\,\colonminus\,\operatorname{\mathcal{S}}(a,b).$

The operator automaton $\mathcal{S}$ can be expressed as having a flip-flop
semiautomaton as a core, then composed with the following input function:

$\displaystyle\phi(10)=\mathit{read},\quad\phi(01)=\phi(11)=\mathit{set},\quad\phi(00)=\mathit{reset}.$

Now can interpret $\mathcal{S}$ as a flip-flop on assingments to variables
$\\{a,b\\}$, that sets when $b$ holds, resets when $\neg b\land a$ holds, and
reads otherwise.

######  Theorem 9.

The operator $\mathcal{S}$ is a prime operator.

###### Proof.

Since $\mathcal{S}$ is the composition of a flip-flop semiautomaton with the
surjective input function $\phi$ given above. ∎

It also follows that the core of $\mathcal{S}$ is isomorphic to the core of
the flip-flop operator defined in the previous sections, and hence
$\mathcal{S}\simeq\mathcal{F}$. The only difference between the two operators
is in the way the input signals are encoded in binary. As a consequence of
this, we obtain the following expressivity result.

######  Theorem 10.

$\mathcal{L}(\operatorname{\mathcal{S}})\equiv\mathcal{L}(\mathcal{F})$.

###### Proof.

By Theorem 7, since $\mathcal{S}\simeq\mathcal{F}$. ∎

Now we turn to formulas. Past LTL formulas can be easily captured in
$\mathcal{L}(\mathcal{S})$, since programs are able to closely capture the
parse tree of a formula.

######  Theorem 11.

Every Past LTL formula admits an equivalent program of
$\mathcal{L}(\mathcal{S})$ of linear size.

###### Proof.

By induction on the structure of formulas, we introduce a static rule in the
case of a Boolean operator, a delay rule in the case of the before operator, a
dynamic rule with operator $\mathcal{S}$ in the case of the since operator. ∎

We have the following corollary of Theorems 3 and 11.

######  Corollary 2.

Every Past LTL formula admits an equivalent cascade with a linear number of
components, that are flip-flops with an input function or trivial automata.

Programs of $\mathcal{L}(\mathcal{S})$ can be unfolded into Past LTL formulas.

######  Theorem 12.

Every pair of a program $P$ of $\mathcal{L}(\mathcal{S})$ and variable $a$
admits an equivalent Past LTL formula $\varphi$ of size at most exponential.
Namely, $(P,I,t)\models a$ iff $(P,I,t)\models\varphi$.

###### Proof.

Since programs are nonrecursive, they can be unfolded into a single rule.
Unfolding consists in taking the rule that defines $a$ and iteratively
replacing its variables with the body of the rules that define them. In the
casese of a variable $q_{i}$ defined by a dynamic rule, of the form
$q_{1},q_{2}\colonminus\mathcal{S}(b,c)$, we replace it with
$\neg(b\operatorname{\mathcal{S}}c)$ if $q_{i}=q_{1}$, and with
$b\operatorname{\mathcal{S}}c$ otherwise. The body of the rule resulting from
the unfolding is the required Past LTL formula $\varphi$. In order to assess
its size, we note that unfolding can be visualised as a tree with nodes
labelled by variables. The root is labelled by $a$. Every node with label $v$
has one child for each variable $u$ in the body of the rule that defines $v$
(if any), and the child is labelled by $u$. The nodes of such tree correspond
to the variables in the unfolding, and hence its size is the size of the
unfolding. Since the program is nonrecursive, we do not encounter the same
variable twice along a branch. Thus the depth is bounded by the size of $P$.
The arity is also bounded by the size of $P$. Therefore the tree has size at
most exponential, and so does the formula $\varphi$, as claimed. ∎

We have the following corollary of Theorems 4 and 12.

######  Corollary 3.

Every acceptor that is a cascade of flip-flops with an input function admits
an equivalent Past LTL formula of size at most exponential.

######  Theorem 13.

The expressivity of Past LTL is the star-free regular languages.

###### Proof.

By Corollaries 2,3 and by Theorem 2. ∎

We briefly mention that the operators $\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{2.58333pt}\pgfsys@lineto{5.5972pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ and
$\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{2.58333pt}\pgfsys@lineto{4.95137pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ are can be seen as
operators whose core is a subsemiautomaton of the flip-flop semiautomaton—no
reset transition. In particular, they are not prime.

The correspondence with the KR Logics opens to the possibility of identifying
new operators for Past LTL. Every operator automaton can be included in Past
LTL, by designing an appropriate syntax that is suitable for inline notation.
Some operators may be more natural than others. For instance, the parity
operator $\mathcal{P}$ introduced in the previous sections can be easily seen
as a Boolean-valued operator, since it suffices it indicates whether the
automaton is in state $1$. Thus we can write formulas such as
$\mathcal{P}(a\lor\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}b)\land(d\operatorname{\mathcal{S}}e)$.
Since the parity operator is prime, we immediately obtain the following
expressivity result by Theorem 7.

######  Theorem 14.

The parity operator $\mathcal{P}$ properly extends the expressivity of Past
LTL.

###### Proof.

By Theorem 7 and 12, since $\mathcal{P}\not\simeq\mathcal{S}$ and
$\mathcal{P}$ is prime (its core is defined by $C_{2}$). ∎

##  7 Related Work

The Krohn-Rhodes Logics are a valuable addition to the rich set of temporal
and dynamic logics adopted in knowledge representation. Such logics include
propositional temporal logics of the past such as Past LTL, cf. (?), as well
as temporal logics of the future interpreted both on finite and infinite
traces (?; ?). They include first-order variants such as Past FOTL (?).
Finally, they include rule-based logics—i.e., logic programs—of several kinds:
propositional modal temporal logics such as Templog (?; ?); logics with first-
order variables where time occurs explicitly as an argument of a special sort
such as Datalog1S (?), and Temporal Datalog (?); propositional modal logics
specialised for reasoning on streams (?). Automata cascades have been used in
the context of temporal logics to prove complexity results for translations
between automata and logic (?; ?).

Identifying hierarchies of regular languages such as the one in our Corollary
1 follows the spirit of the pioneering work (?).

##  8 Conclusions

The KR Logics provide a general framework for temporal logics. The flexibility
given by operator automata allows for defining KR Logics with the expressivity
of many different classes of regular languages, with the guidance of the
Krohn-Rhodes theory, and of group theory. While the star-free regular
languages are well-known, sincce they are the expressivity of many well-
established formalisms, the fragments beyond them are less known. The KR
Logics provide a way to explore them.

## Acknowledgments

This work has been supported by the ERC Advanced Grant WhiteMech (No. 834228),
by the EU ICT-48 2020 project TAILOR (No. 952215), and by the PRIN project
RIPER (No. 20203FFYLK).

## References

  * Abadi and Manna 1989 Abadi, M., and Manna, Z.  1989\.  Temporal logic programming.  J. Symb. Comput. 8(3):277–295.
  * Bacchus, Boutilier, and Grove 1996 Bacchus, F.; Boutilier, C.; and Grove, A. J.  1996\.  Rewarding behaviors.  In AAAI, 1160–1167.
  * Baudinet 1995 Baudinet, M.  1995\.  On the expressiveness of temporal logic programming.  Inf. Comput. 117(2):157–180.
  * Beck, Dao-Tran, and Eiter 2018 Beck, H.; Dao-Tran, M.; and Eiter, T.  2018\.  LARS: A logic-based framework for analytic reasoning over streams.  Artif. Intell. 261:16–70.
  * Bietti, Venturi, and Bruna 2021 Bietti, A.; Venturi, L.; and Bruna, J.  2021\.  On the sample complexity of learning under geometric stability.  In NeurIPS, volume 34, 18673–18684.
  * Brafman and Giacomo 2019 Brafman, R. I., and Giacomo, G. D.  2019\.  Regular decision processes: Modelling dynamic systems without using hidden variables.  In AAMAS, 1844–1846.
  * Bronstein et al. 2021 Bronstein, M. M.; Bruna, J.; Cohen, T.; and Velickovic, P.  2021\.  Geometric deep learning: Grids, groups, graphs, geodesics, and gauges.  CoRR abs/2104.13478.
  * Camacho et al. 2019 Camacho, A.; Icarte, R. T.; Klassen, T. Q.; Valenzano, R. A.; and McIlraith, S. A.  2019\.  LTL and beyond: Formal languages for reward function specification in reinforcement learning.  In IJCAI, 6065–6073.
  * Cecconi et al. 2022 Cecconi, A.; Giacomo, G. D.; Ciccio, C. D.; Maggi, F. M.; and Mendling, J.  2022\.  Measuring the interestingness of temporal logic behavioral specifications in process mining.  Inf. Syst. 107:101920.
  * Chomicki and Imielinski 1988 Chomicki, J., and Imielinski, T.  1988\.  Temporal deductive databases and infinite objects.  In PODS, 61–73.
  * Chomicki 1995 Chomicki, J.  1995\.  Efficient checking of temporal integrity constraints using bounded history encoding.  ACM Trans. Database Syst. 20(2):149–186.
  * Cohen and Brzozowski 1971 Cohen, R. S., and Brzozowski, J. A.  1971\.  Dot-depth of star-free events.  J. Comput. Syst. Sci. 5(1):1–16.
  * De Giacomo and Vardi 2013 De Giacomo, G., and Vardi, M. Y.  2013\.  Linear temporal logic and linear dynamic logic on finite traces.  In IJCAI.
  * Dömösi and Nehaniv 2005 Dömösi, P., and Nehaniv, C. L.  2005\.  Algebraic theory of automata networks: An introduction.  SIAM.
  * Giacomo et al. 2020 Giacomo, G. D.; Iocchi, L.; Favorito, M.; and Patrizi, F.  2020\.  Restraining bolts for reinforcement learning agents.  In AAAI, 13659–13662.
  * Ginzburg 1968 Ginzburg, A.  1968\.  Algebraic Theory of Automata.  Academic Press.
  * Gorenstein, Lyons, and Solomon 2018 Gorenstein, D.; Lyons, R.; and Solomon, R.  2018\.  The Classification of the Finite Simple Groups, Number 8.  American Mathematical Soc.
  * Hopcroft and Ullman 1979 Hopcroft, J., and Ullman, J.  1979\.  Introduction to Automata Theory, Languages, and Computation.  Addison-Wesley.
  * Kleene 1956 Kleene, S. C.  1956\.  Representation of events in nerve nets and finite automata.  Automata studies 34:3–41.
  * Krohn and Rhodes 1965 Krohn, K., and Rhodes, J.  1965\.  Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines.  Trans. Am. Math. Soc. 116:450–64.
  * Maler and Pnueli 1990 Maler, O., and Pnueli, A.  1990\.  Tight bounds on the complexity of cascaded decomposition of automata.  In FOCS, 672–682.
  * Maler 1990 Maler, O.  1990\.  Finite Automata: Infinite Behaviour, Learnability and Decomposition.  Ph.D. Dissertation, The Weizmann Institute of Science.
  * Manna and Pnueli 1991 Manna, Z., and Pnueli, A.  1991\.  Completing the temporal picture.  Theor. Comput. Sci. 83(1):91–130.
  * Pnueli 1977 Pnueli, A.  1977\.  The temporal logic of programs.  In FOCS, 46–57.
  * Ronca et al. 2022 Ronca, A.; Kaminski, M.; Grau, B. C.; and Horrocks, I.  2022\.  The delay and window size problems in rule-based stream reasoning.  Artif. Intell. 306:103668.
  * Ronca, Knorozova, and De Giacomo 2023 Ronca, A.; Knorozova, N. A.; and De Giacomo, G.  2023\.  Automata cascades: Expressivity and sample complexity.  In AAAI.
  * Schützenberger 1965 Schützenberger, M. P.  1965\.  On finite monoids having only trivial subgroups.  Inf. Control. 8(2):190–194.

##  Appendix A Proofs

###  A.1 Proofs for Section 5

We provide a definition of state reachability, relevant to the propositions
below.

######  Definition 8.

Consider a semiautomaton $D=\langle\Sigma,Q,\delta\rangle$. A state $q\in Q$
is _reachable_ in $D$ from a state $q^{\prime}\in Q$ if there exists an input
string $\sigma_{1}\dots\sigma_{\ell}$ such that, for $q_{0}=q^{\prime}$ and
$q_{i}=\delta(q_{i-1},\sigma_{i})$, it holds that $q=q_{\ell}$.

See 1

###### Proof.

Let us consider semiautomata $D_{1}$ and $D_{2}$. Consider a subsemiautomaton
$D_{1}^{\prime}$ of $D_{1}$ such that there is a homomorphism
$\psi=\langle\psi_{1},\psi_{2}\rangle$ of $D_{1}^{\prime}$ onto $D_{2}$. Let
$D_{1}^{\prime}=\langle\Sigma_{1},Q_{1},\delta_{1}\rangle$ and
$D_{2}=\langle\Sigma_{2},Q_{2},\delta_{2}\rangle$, and consider an automaton

$\displaystyle
A_{2}=\langle\Sigma_{2},Q_{2},\delta_{2},q^{2}_{\mathrm{init}},\Gamma,\theta_{2}\rangle.$

We construct an automaton

$\displaystyle
A_{1}=\langle\Sigma_{2},Q_{1},\delta_{1}^{\prime},q^{1}_{\mathrm{init}},\Gamma,\theta_{1}\rangle,$

where $\delta_{1}^{\prime}(q,\sigma)=\delta_{1}(q,\psi_{1}(\sigma))$,
$\theta_{1}=\psi_{2}\circ\theta_{2}$, and $q_{1}^{\mathrm{init}}\in Q_{1}$ is
such that $\psi_{2}(q_{2}^{\mathrm{init}})=q_{1}^{\mathrm{init}}$—it exists
because $\psi_{2}$ is surjective. Then we show that $A_{1}$ and $A_{2}$
recognise the same language.

Let $\sigma_{1}\dots\sigma_{n}$ be an input string, and let
$q^{1}_{0},\dots,q^{1}_{n}$ and and $q^{2}_{0},\dots,q^{2}_{n}$ be the
corresponding sequence of states for $A_{1}$ and $A_{2}$, respectively.
Namely, $q^{1}_{0}=q^{1}_{\mathrm{init}}$ and
$q^{1}_{i}=\delta_{1}^{\prime}(q^{1}_{i-1},\sigma_{i})$ for $1\leq i\leq n$.
Similarly, $q^{2}_{0}=q^{2}_{\mathrm{init}}$ and
$q^{2}_{i}=\delta_{2}(q^{2}_{i-1},\sigma_{i})$ for $1\leq i\leq n$.

As an auxiliary result, we show that $q^{2}_{i}=\psi_{2}(q^{1}_{i})$ for every
$0\leq i\leq n$. We show the claim by induction on $i$.

In the base case $i=0$ and $q^{2}_{0}=\psi_{2}(q^{1}_{0})$ amounts to
$q^{2}_{\mathrm{init}}=\psi_{2}(q^{1}_{\mathrm{init}})$, which holds by
construction.

In the inductive case $i>0$ and we assume that
$q^{2}_{i-1}=\psi_{2}(q^{2}_{i-1})$. We have to show
$q^{2}_{i}=\psi_{2}(q^{2}_{i})$. By the definition of $q^{1}_{i}$ and
$q^{2}_{i}$ above, it can be rewritten as

$\displaystyle\delta_{2}(q^{2}_{i-1},\sigma_{i})=\psi_{2}(\delta_{1}^{\prime}(q^{1}_{i-1},\sigma_{i}))$
$\displaystyle\psi_{2}(\delta_{1}^{\prime}(q^{1}_{i-1},\sigma_{i}))=\delta_{2}(q^{2}_{i-1},\sigma_{i})$

Then, by the inductive hypothesis $q^{2}_{i-1}=\psi_{2}(q^{1}_{i-1})$, we have

$\displaystyle\psi_{2}(\delta_{1}^{\prime}(q^{1}_{i-1},\sigma_{i}))=\delta_{2}(\psi_{2}(q^{1}_{i-1}),\sigma_{i})$

which holds since $\langle\psi_{1},\psi_{2}\rangle$ is a homomorphism from
$D_{1}$ to $D_{2}$, This proves the auxiliary claim.

By definition, we have that $A_{1}$ accepts $\sigma_{1}\dots\sigma_{n}$ iff
$\theta_{1}(q^{1}_{n-1},\sigma_{n})=1$, and similarly $A_{2}$ accepts
$\sigma_{1}\dots\sigma_{n}$ iff $\theta_{2}(q^{2}_{n-1},\sigma_{n})=1$. We
have that

$\displaystyle\theta_{1}(q^{1}_{n-1},\sigma_{n})=\theta_{2}(q^{2}_{n-1},\sigma_{n})=\theta_{2}(\psi_{2}(q^{1}_{n-1}),\sigma_{n}).$

Finally, consider the semiautomaton
$D_{1}=\langle\Sigma_{1}^{\prime},Q_{1}^{\prime},\delta_{0}\rangle$, and let
us define the automaton

$\displaystyle
A_{1}^{\prime}=\langle\Sigma_{2},Q_{1}^{\prime},\delta_{0}^{\prime},q^{1}_{\mathrm{init}},\Gamma,\theta_{1}\rangle,$

where $\delta_{0}^{\prime}(q,\sigma)=\delta_{0}(q,\psi_{1}(\sigma))$. We have
that $A_{1}^{\prime}$ recognises the same language as $A_{1}$, since the
states $Q_{1}^{\prime}\setminus Q_{1}$ are not reachable from
$q^{1}_{\mathrm{init}}$ in $D_{1}$ when its inputs are restricted to
$\Sigma_{1}$. Automaton $A_{1}^{\prime}$ has a semiautomaton that corresponds
to the composition of $D_{1}$ and $\psi_{1}$ seen as an input function.
Furthermore, $A_{1}^{\prime}$ is similar to $D_{1}$. Thus, $A_{1}^{\prime}$ is
the required automaton, and hence the proposition is proved. ∎

See 2

###### Proof.

Assume that $D_{2}$ is a semiautomaton is not homomorphically represented by a
semiautomaton $D_{1}$, and $D_{2}$ admits a state from which all the other
states are reachable. The former assumption implies that $D_{1}$ has no
subsemiautomaton $D_{1}^{\prime}$ such that there is a homomorphism of
$D_{1}^{\prime}$ onto $D_{2}$. Let us assume by contradiction that every
language recognised by an acceptor with semiautomaton $D_{2}$ is also
recognised by an acceptor whose semiautomaton $D_{1}^{\prime}$ is the
composition of $D_{1}$ with an input function. Let $D_{1}^{\prime}$ and
$D_{2}$ be of the form

$\displaystyle D_{1}^{\prime}=\langle\Sigma,Q_{1},\delta_{1}\rangle,\quad
D_{2}=\langle\Sigma,Q_{2},\delta_{2}\rangle.$

Let us consider an enumeration of the states of $D_{2}$,
$Q_{2}=\\{q^{2}_{1},\dots,q^{2}_{n}\\}$. There exists a state
$q^{2}_{\mathrm{init}}\in Q_{2}$ such that every state in $Q_{2}$ is reachable
in $D_{2}$ from $q^{2}_{\mathrm{init}}$. For every $1\leq i\leq n$, let us
consider the system

$\displaystyle
A_{2}^{i}=\langle\Sigma,Q_{2},\delta_{2},q^{2}_{\mathrm{init}},\\{0,1\\},\theta_{2}^{i}\rangle,$

where $\theta^{i}_{2}(q,\sigma)=1$ if $q=q^{2}_{i}$ and
$\theta^{i}_{2}(q,\sigma)=0$ otherwise. Then, by our assumption, there exists
an automaton $A_{1}^{i}$ with dynamics $D_{1}^{\prime}$ that recognises the
same languages as $A_{2}^{i}$. Namely,

$\displaystyle
A_{1}^{i}=\langle\Sigma,Q_{1},\delta_{1},q^{1,i}_{\mathrm{init}},\\{0,1\\},\theta_{1}^{i}\rangle.$

Let $D_{1,i}=\langle\Sigma,Q_{1,i},\delta_{1,i}\rangle$ be the
subsemiautomaton of $D_{1}^{\prime}$ obtained by restricting to the states
$Q_{1,i}$ that are reachable in $A_{1}^{i}$ from the initial state
$q^{1,i}_{\mathrm{init}}$. Then, let

$\displaystyle
A_{1,i}=\langle\Sigma,Q_{1,i},\delta_{1,i},q^{1,i}_{\mathrm{init}},\\{0,1\\},\theta_{1,i}\rangle,$

where $\theta_{1,i}$ is the restriction of $\theta_{1}^{i}$ on $Q_{1,i}$.
Clearly, $A_{1,i}$ and $A_{1}^{i}$ recognise the same language.

First, we show that $\theta_{1,i}(q,\sigma)=\theta_{1,i}(q,\sigma^{\prime})$
for every $q\in Q_{1,i}$ and every $\sigma,\sigma^{\prime}\in\Sigma$. Consider
an input string $I=\sigma_{1}\dots\sigma_{\ell}$. We have that

$\displaystyle\theta_{2}^{i}(\delta_{2}(\sigma_{1}\dots\sigma_{\ell-1}),\sigma_{\ell})=\theta_{1,i}(\delta_{1,i}(\sigma_{1}\dots\sigma_{\ell-1}),\sigma_{\ell}).$

Since $\theta_{2}^{i}$ does not depend on $\sigma_{\ell}$, it must be that
$\theta_{1,i}$ does not either. Otherwise we can choose $\sigma^{\prime}$ such
that

$\displaystyle\theta_{2}^{i}(\delta_{2}(\sigma_{1}\dots\sigma_{\ell-1}),\sigma^{\prime})\neq\theta_{1,i}(delta_{1}(\sigma_{1}\dots\sigma_{\ell-1}),\sigma^{\prime}).$

Thus, we write $\theta_{1,i}(q,\sigma)$ simply as $\theta_{1,i}(q)$.

Let $H$ be the domain of one-hot encodings of arity $n$,

$\displaystyle H=\\{\langle b_{1},\dots,b_{n}\rangle\mid\exists
i.\,b_{i}=1\text{ and }\forall j\neq i.\,b_{j}=0\\}.$

Let $\psi^{\prime}:H\to Q_{2}$ be defined as
$\psi^{\prime}(b_{1},\dots,b_{n})=q^{2}_{i}$ when $b_{i}=1$. Let
$Q_{1}^{\prime}=\bigcup_{1\leq i\leq n}Q_{1,i}$. Let us define
$\psi:Q_{1}^{\prime}\to Q_{2}$ as

$\displaystyle(\theta_{1,i}\times\dots\times\theta_{1,n})\circ\psi^{\prime}.$

In other words, we have that $\psi(q)=q^{2}_{i}$ if $\theta_{1,i}(q)=1$. Note
that $\psi$ is well-defined since $\theta_{1,i}(q)=1$ implies
$\theta_{1,j}(q)=0$ for every $j\neq i$.

Let $D_{1}^{\prime\prime}$ be the union of the semiautomata $D_{1,i}$. In
particular, it
$D_{1}^{\prime\prime}=\langle\Sigma,Q_{1}^{\prime},\delta_{1}^{\prime\prime}\rangle$
where $Q_{1}^{\prime}$ is defined above. Note that $D_{1}^{\prime\prime}$ is a
subsemiautomaton of $D_{1}$.

We show that $\langle\mathbf{I},\psi\rangle$ is a homomorphism of
$D_{1}^{\prime}$ onto $D_{2}$, where $\mathbf{I}$ is the identity function.

First, we show that $\psi$ is surjective. We have that every state in $Q_{2}$
is reachable in $D_{2}$ from the initial state $q^{2}_{\mathrm{init}}$. Thus,
for every $1\leq i\leq n$, there exists an input sequence $I$ such that
$A_{2}^{i}$ accepts $I$, hence $A_{1,i}$ accepts $I$, hence
$\theta_{1,i}(q)=1$ for some $q\in Q_{1,i}$, and hence $\psi(q)=q^{2}_{i}$.
This shows that $\psi$ is surjective.

Second, we show that, for every $q\in Q_{1}^{\prime}$ and every
$\sigma\in\Sigma$, it holds that

$\displaystyle\psi(\delta_{1}^{\prime\prime}(q,\sigma))=\delta_{2}(\psi(q),\sigma).$

Consider an input string $\sigma_{1}\dots,\sigma_{\ell}$. For $0\leq
t\leq\ell$, let $q^{1,i}_{t},q^{2}_{t}$ be the state of $A_{1,i},A_{2}^{i}$,
respectively, upon reading $\sigma_{1}\dots,\sigma_{t}$. Note that states of
$A_{2}^{i}$ do not need to be indexed by $i$ since all automata $A_{2}^{i}$
have semiautomaton $D_{2}$. We have that, for every $1\leq i\leq n$,

$\displaystyle\psi(q^{1,i}_{\ell-1})$
$\displaystyle=\psi^{\prime}\big{(}\theta_{1,1}(q^{1,i}_{\ell-1},\sigma_{\ell}),\dots,\theta_{1,n}(q^{1,i}_{\ell-1},\sigma_{\ell})\big{)}$
$\displaystyle=\psi^{\prime}\big{(}\theta_{2}^{i}(q^{2}_{\ell-1},\sigma_{\ell}),\dots,\theta_{2}^{i}(q^{2}_{\ell-1},\sigma_{\ell})\big{)}$
$\displaystyle=q^{2}_{\ell-1},$

where the middle equality holds because $A_{1,i},A_{2}^{i}$ recognise the same
language. We also have that

$\displaystyle\psi(q^{1,i}_{\ell-2})$
$\displaystyle=\psi^{\prime}\big{(}\theta_{1,1}(q^{1,i}_{\ell-2},\sigma_{\ell-1}),\dots,\theta_{1,n}(q^{1,i}_{\ell-2},\sigma_{\ell-1})\big{)}$
$\displaystyle=\psi^{\prime}\big{(}\theta_{2}^{1}(q^{2}_{\ell-2},\sigma_{\ell-1}),\dots,\theta_{2}^{n}(q^{2}_{\ell-2},\sigma_{\ell-1})\big{)}$
$\displaystyle=q^{2}_{\ell-2}.$

Using the identities above, we derive two equivalent expressions for
$q^{2}_{\ell-1}$,

$\displaystyle q^{2}_{\ell-1}$
$\displaystyle=\delta_{2}(q^{2}_{\ell-2},\sigma_{\ell-1})$
$\displaystyle=\delta_{2}(\psi(q^{1,i}_{\ell-2}),u_{\ell-1})$

and

$\displaystyle q^{2}_{\ell-1}$ $\displaystyle=\psi(q^{1,i}_{\ell-1})$
$\displaystyle=\psi(\delta_{1}(q^{1,i}_{\ell-2},\sigma_{\ell-1}))$
$\displaystyle=\psi(\delta_{1}^{\prime\prime}(q^{1,i}_{\ell-2},\sigma_{\ell-1})).$

Therefore,

$\displaystyle\psi(\delta_{1}^{\prime\prime}(q^{1,i}_{\ell-2},\sigma_{\ell-1}))=\delta_{2}(\psi(q^{1,i}_{\ell-2}),\sigma_{\ell-1}).$

Since every state $q^{1,i}_{\ell-2}$ can be reached for some input sequence,
and also $\sigma_{\ell-1}$ is arbitrary, the equation above proves the
required condition on $\psi$. This a contradiction, since it shows that
$D_{2}$ is homomorphically represented by $D_{1}$, and hence the proposition
is proved. ∎

###  A.2 Proofs for Section 6.2

See 1

###### Proof (continued).

Here we prove correctness of the construction given in the main body of the
paper. Consider $r$ and $A$ as introduced there. Then, for every input string
$I=\sigma_{1}\dots\sigma_{t}$, it holds that the output of $A$ on $I$ is
$\theta(q_{t-1},\sigma_{t})=\sigma_{t-1}(a)$. Thus, $(A,I,t)\vdash h$ iff
$(r,I,t-1)\models a$ iff $(r,I,t)\models h$, as required. ∎

See 2

###### Proof (continued).

Here we prove correctness of the construction given in the main body of the
paper. Consider $r$ and $A$ as introduced there. Let
$I=\sigma_{1}\dots\sigma_{\ell}$ be an interpretation for the rule. For the
sake of induction, we show a (mildly) more general claim. Namely, for every
$t\geq 0$, $(r,I,t)\models p_{i}$ iff $A$ is in state $i$ upon reading
$\sigma_{1}\dots\sigma_{t}$. Then the lemma will follow by the definition of
$\theta$—note that $\theta$ returns the one-hot encoding of the state after
the update.

First we show that $(r,I,t)\models p_{i}$ implies that $A$ is in state $i$
upon reading $\sigma_{1}\dots\sigma_{t}$. We show it by induction on $t$. In
the base case $t=0$, and hence by Point 9 of the semantics we have that
$i=q_{\mathrm{init}}$, and hence the claim holds. In the inductive case $t\geq
1$, and we assume that $(r,I,t-1)\models p_{j}$ implies that $A$ is in state
$j$ upon reading $\sigma_{1}\dots\sigma_{t-1}$. By Point 10 of the semantics
of programs, we have that $(r,I,t)\models p_{i}$ implies that
$\delta(j,\sigma)=i$ where $j$ is an index such that $r,I,t-1\models p_{j}$,
and $\sigma$ is an assignment to variables $\\{a_{1},\dots,a_{m}\\}$ such that
$r,I,t\models\sigma$. By the inductive hypothesis, $r,I,t-1\models p_{j}$
implies that $A$ is in state $j$ upon reading $\sigma_{1}\dots\sigma_{t-1}$.
Since $\delta(j,\sigma)=i$, we have that $A$ is in state $i$ upon reading
$\sigma_{1}\dots\sigma_{t}$, as required.

Now we assume that $A$ is in state $i$ upon reading
$\sigma_{1}\dots\sigma_{t}$, and we show $(r,I,t)\models p_{i}$. We proceed by
induction on $t$. In the base case $t=0$, and we have that $A$ is in state
$i=q_{\mathrm{init}}$. We have that $(r,I,t)\models p_{i}$ by the semantics of
the rule. In the inductive case $t\geq 1$, and we assume that
$(r,I,t-1)\models p_{j}$ when $A$ is in state $j$ upon reading
$\sigma_{1}\dots\sigma_{t-1}$. There are $j$ and $\sigma$ such that
$\delta(j,\sigma)=i$ and $A$ is in state $j$ upon reading
$\sigma_{1}\dots\sigma_{t-1}$. Then, by the inductive hypothesis, we have
$(r,I,t-1)\models p_{j}$. Then $(r,I,t)\models p_{i}$ by the semantics of the
rule, as required. This concludes the proof. ∎

See 3

###### Proof (continued).

Here we prove correctness of the construction given in the main body of the
paper. Consider $r$ and $A$ as introduced there. We have that, for every
$I=\sigma_{1}\dots\sigma_{\ell}$, $(A,I,t)\vdash p$ iff
$\theta(1,\sigma_{t})=1$ iff $(r,\sigma_{t})\models p$ iff $(r,I,t)\models p$,
as required. ∎

###  A.3 Proofs for Section 6.3

See 4

###### Proof (continued).

Here we prove correctness of the construction given in the main body of the
paper. For the sake of induction, we show a (mildy) more general claim. Let
$I=\sigma_{1},\dots,\sigma_{\ell}$ be an input string over $\Sigma$, and let
$I_{t}$ be the substring $\sigma_{1}\dots\sigma_{t}$. We show that, for every
$q_{i}\in Q$, it holds that $(P,I,t)\models q_{i}$ iff $A$ is in state $q_{i}$
upon reading $I_{t}$. Then it will follow that, for every $q^{\prime}_{i}\in
Q^{\prime}$, it holds that $(P,I,t)\models q^{\prime}_{i}$ iff $A$ is in state
$q_{i}$ upon reading $I_{t-1}$. Then it will follow that, for every $c_{i}\in
W$, it holds that $(P,I,t)\models c_{i}$ iff $(A,I,t)\vdash c_{i}$, by the
rules in $P_{\mathrm{out}}$.

We first show that $(P,I,t)\models q_{i}$ implies that $A$ is in state $q_{i}$
upon reading $I_{t}$. We proceed by induction on $t$. In the base case $t=0$.
We have that $(P,I,t)\models q_{i}$ implies $q_{i}=q_{\mathrm{init}}$ as
required, by the dynamic rule and Point 9 of the semantics. In the inductive
case $t\geq 1$, and we assume that, for every $q_{j}\in Q$, $(P,I,t-1)\models
q_{j}$ implies that $A$ is in state $q_{j}$ upon reading $I_{t-1}$. We have
that $(P,I,t)\models q_{i}$ implies (by the dynamic rule, and Point 10 of the
semantics) that there are $j\in[1,n]$ and $\pi$ such that

$\displaystyle\delta^{\prime}(j,\pi)=i,\quad(P,I,t-1)\models
q_{j}\quad(P,I,t)\models\pi.$

Then it also follows, by the inductive hypothesis, that $j$ is such that $A$
is in state $q_{j}$ upon reading $I_{t-1}$. We have that $(P,I,t)\models\pi$
implies $\phi(\sigma_{t})=\pi$, by construction of $P$, in particular of
$P_{\mathrm{in}}$. Thus, the state of $A$ upon reading $I_{t}$ is
$\delta(q_{j},\phi(\sigma_{t}))=\delta(q_{j},\pi)$. It implies
$\delta(q_{j},\pi)=q_{i}$ as required, since $\delta^{\prime}(j,\pi)=i$.

Now we show that, if the state of $A$ upon reading $I_{t}$ is $q_{i}$, then
$(P,I,t)\models q_{i}$. We proceed by induction on $t$. In the base case
$t=0$, we have that the initial state of $A$ is $q_{\mathrm{init}}$, and we
have that $(P,I,t)\models q_{\mathrm{init}}$ as required, by the dynamic rule
in $P$. In the inductive case $t\geq 1$, and we assume that $A$ is in state
$q_{j}$ upon reading $I_{t-1}$, and $(P,I,t-1)\models q_{j}$. Let
$\pi=\phi(\sigma_{t})$. By the dynamic rule in $P$, in order to show
$(P,I,t)\models q_{i}$, it suffices to show the following three conditions:

$\displaystyle\delta^{\prime}(j,\pi)=i,\quad(P,I,t-1)\models
q_{j}\quad(P,I,t)\models\pi.$

First, we have $q_{i}=\delta(q_{j},\phi(\sigma_{t}))=\delta(q_{j},\pi)$, and
hence $\delta^{\prime}(j,\pi)=i$ by the definition of $\delta^{\prime}$.
Second, we have that $\pi=\phi(\sigma_{t})$ implies $(P,I,t)\models\pi$, by
the construction of $P$, in particular of $P_{\mathrm{in}}$. Third, we have
$(P,I,t-1)\models q_{j}$ by the inductive hypothesis. This concludes the
proof. ∎

###  A.4 Proofs for Section 6.5

Consider the Past LTL formula $\varphi=a\operatorname{\mathcal{S}}b$, and the
dynamic rule $r$

$\displaystyle q_{1},q_{2}$
$\displaystyle\,\colonminus\,\operatorname{\mathcal{S}}(a,b).$

######  Lemma 5.

We have $(I,t)\models\varphi$ if and only if $(r,I,t)\models q_{2}$.

###### Proof sketch.

By induction on $t$, making use of the recursive definition of the semantics
of the ‘since’ operator. ∎

###### Proof.

Let $I=\sigma_{1}\dots\sigma_{\ell}$ We proceed by induction on $t$. In the
base case $t=1$. We show the two implications separately. First, we show that
$(I,1)\models(a\operatorname{\mathcal{S}}b)$ implies $(r,I,1)\models q_{2}$.
We have that $(I,1)\models(a\operatorname{\mathcal{S}}b)$ implies
$\sigma_{1}(b)=1$, hence the operator automaton $\mathcal{S}$ is in state $2$
upon reading $\sigma_{1}$, and hence $(r,I,1)\models q_{2}$ as required.
Second, we show that $(r,I,1)\models q_{2}$ implies
$(I,1)\models(a\operatorname{\mathcal{S}}b)$. We have that $(r,I,1)\models
q_{2}$ implies (Point 10 of the semantics) that for some $j$ and some
assignment $\sigma$ to variables $\\{a,b\\}$, the following three conditions
hold

$\displaystyle\delta(j,\sigma)=2,\quad(r,I,0)\models
q_{j},\quad(r,I,1)\models\sigma.$

By the definition of $\delta$, we have that $\delta(j,\sigma)=2$ implies
$\sigma=01$ or $\sigma=11$. Thus, $(r,I,1)\models\sigma$ implies that
$\sigma_{1}(b)=1$, and hence $(I,1)\models(a\operatorname{\mathcal{S}}b)$.

In the inductive case $t\geq 2$, and we assume that
$(I,t-1)\models(a\operatorname{\mathcal{S}}b)$ iff $(r,I,t-1)\models q_{2}$.
We show the two implications separately. First, we show that
$(I,t)\models(a\operatorname{\mathcal{S}}b)$ implies $(r,I,t)\models q_{2}$.
We have that $(I,t)\models(a\operatorname{\mathcal{S}}b)$ implies (i)
$(I,t)\models b$ or (ii) $(I,t-1)\models(a\operatorname{\mathcal{S}}b)$ and
$(I,t)\models a$. The first case is analogous to the one in the base case. Let
us consider the second case, by assuming
$(I,t-1)\models(a\operatorname{\mathcal{S}}b)$ and $(I,t)\models a$. Hence, it
suffices to show, for some $\sigma=10$ or $\sigma=11$

$\displaystyle\delta(2,\sigma)=2,\quad(r,I,t-1)\models
q_{2},\quad(r,I,t)\models\sigma.$

The first condition holds by the definition of $\delta$. The second condition
holds by the inductive hypothesis since
$(I,t-1)\models(a\operatorname{\mathcal{S}}b)$. The third condition holds
since $(I,t)\models a$. Now we show the other implication, i.e.,
$(r,I,t)\models q_{2}$ implies $(I,t)\models(a\operatorname{\mathcal{S}}b)$.
We assume $(r,I,t)\models q_{2}$. It follows that there is $j$ and $\sigma$
such that

$\displaystyle\delta(j,\sigma)=2,\quad(r,I,t-1)\models
q_{j},\quad(r,I,t)\models\sigma.$

It suffices to show (i) $(I,t)\models b$ or (ii)
$(I,t-1)\models(a\operatorname{\mathcal{S}}b)$ and $(I,t)\models a$. We
consider the two possible cases separately. In the first case
$(r,I,t-1)\models q_{2}$. It follows that $j=2$, and hence $\sigma=00$ or
$\sigma=01$ or $\sigma=11$. If $\sigma=01$ or $\sigma=11$, then
$\sigma_{t}=01$ or $\sigma_{t}=11$, and hence $\sigma_{t}(b)=1$. Thus,
$(I,t)\models b$, and hence $(I,t)\models(a\operatorname{\mathcal{S}}b)$ by
(i). Otheriwse, $\sigma=00$, hence $\sigma_{t}=00$, hence $\sigma_{t}(a)=1$,
and hence $(I,t)\models(a\operatorname{\mathcal{S}}b)$ by (ii), since
$(I,t-1)\models(a\operatorname{\mathcal{S}}b)$ by the inductive hypothesis. In
the second case $(r,I,t-1)\not\models q_{2}$. Hence $(r,I,t-1)\models q_{1}$.
It follows that there is $\sigma$ such that

$\displaystyle\delta(1,\sigma)=2,\quad(r,I,t-1)\models
q_{1},\quad(r,I,t)\models\sigma.$

By the definition of $\delta$, we have that $\sigma=01$ or $\sigma=11$, and
hence $\sigma_{t}=01$ or $\sigma_{t}=11$. It follows that $I,t\models b$.
Hence $(I,t)\models(a\operatorname{\mathcal{S}}b)$ by (i).

This concludes the proof. ∎