# Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic

Paolo Felli, Marco Montali, Sarah Winkler This work is partially supported by
the UNIBZ projects DaCoMan, QUEST, SMART-APP, VERBA, and WineId.

###### Abstract

Combined modeling and verification of dynamic systems and the data they
operate on has gained momentum in AI and in several application domains. We
investigate the expressive yet concise framework of data-aware dynamic systems
(DDS), extending it with linear arithmetic, and provide the following
contributions. First, we introduce a new, semantic property of “finite
summary”, which guarantees the existence of a faithful finite-state
abstraction. We rely on this to show that checking whether a witness exists
for a linear-time, finite-trace property is decidable for DDSs with finite
summary. Second, we demonstrate that several decidability conditions studied
in formal methods and database theory can be seen as concrete, checkable
instances of this property. This also gives rise to new decidability results.
Third, we show how the abstract, uniform property of finite summary leads to
modularity results: a system enjoys finite summary if it can be partitioned
appropriately into smaller systems that possess the property. Our results
allow us to analyze systems that were out of reach in earlier approaches.
Finally, we demonstrate the feasibility of our approach in a prototype
implementation.

##  1 Introduction

The analysis of complex dynamic systems is a core research topic in AI. While
process analysis has long focused on the control-flow perspective, in recent
years a multi-perspective approach gained momentum, studying the interplay
between control flow and data (Reichert 2012; Calvanese, de Giacomo, and
Montali 2013; Calvanese et al. 2018; Deutsch et al. 2018). Verification in
this setting is challenging, as it must deal with potentially infinitely many
states.

This is aggravated in the presence of arithmetic, notwithstanding that it is
essential for practical applications (Deutsch et al. 2018): model checking of
transition systems operating over simple data with arithmetic constraints is
known to be undecidable, as it is easy to model a two-counter system. However,
restrictions on the transition system have been shown to render certain
verification tasks decidable. In particular, decidability has been obtained by
confining the constraint language, as in the case of _monotonicity_
constraints (Demri and D’Souza 2007) (e.g. $x\>{\leq}\>y$) and _gap-order_
constraints (Mayr and Totzke 2016; Bozzelli and Pinchinat 2014) (e.g.
$x\,{-}\,y\>{\geq}\>2$), or by limiting the control flow, as in the case of
_feedback freedom_ (Damaggio, Deutsch, and Vianu 2012).

In this work, we focus on the framework of data-aware dynamic systems (DDSs)
(de Leoni, Felli, and Montali 2020), an expressive yet concise model for
process analysis, which we enrich with linear arithmetic. We call the
resulting systems _DDSs with arithmetic (DDSAs)_ , and study the verification
problem for the linear-time, finite-trace temporal logic LTLf (de Giacomo and
Vardi 2013) extended with arithmetic constraints. The following is a
motivating example.

######  Example 1.1.

Consider the process of an auction at an online market place. Its data
variables are a timer $d$, the offer $o$ by the last bidder, identified by
$b$, a threshold price $t$ for which the item can be sold immediately, and the
sum $s$.
$\mathsf{sold}$$\mathsf{init}\colon[\,{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}{d^{w}\,{>}\,0}}\wedge{\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{t^{w}\,{>}\,0}}\,]$$\mathsf{bid}\colon[\,{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}{0<b^{w}}}\wedge{\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{o^{w}>o^{r}}}\,]$$\mathsf{check}\colon[\,{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}{d^{r}>0}}\,]$$\mathsf{dec}\colon[\,{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}{d^{r}\,{-}\,d^{w}\,{\geq}\,1}}\,]$$\mathsf{exp}\colon[\,{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}{d^{r}\leq
0}}\wedge{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}{b^{r}>0}}\,]$$\mathsf{sell\>now}\colon[\,{\color[rgb]{0,0,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8}{o^{r}>t^{r}}}\,]$$\mathsf{fee}\colon[\,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{s^{w}=o^{r}+10}}\,]$
The timer $d$ is initialized to a number of days, and $t$ is fixed (action
$\mathsf{init}$). Then, while the timer did not expire ($\mathsf{check}$),
bids are taken ($\mathsf{bid}$) or the timer may be decremented
($\mathsf{dec}$). The auction ends if the timer expires and a bid was set
($\mathsf{exp}$), or the offer exceeds $t$ ($\mathsf{sell\>now}$). Finally,
$\mathsf{fee}$ sets $s$ to the offer plus an auction fee. We will use our
approach to verify that $\psi=\Box(\mathsf{sold}\wedge d\,{>}\,0\to
o\,{>}\,t)$ holds, i.e., if the auction ends before the timer expires, the
offer exceeds the threshold. The meaning of the colors will be clarified
later.

Our contribution is as follows.  (1) First, we introduce the novel property of
_finite summary_ , and show that the above restrictions studied in the
literature (i.e. $(i)$ monotonicity constraints, $(ii)$ gap-order constraints,
$(iii)$ feedback freedom) are instances of this property. We further
generalize feedback freedom introducing a new, expressive property called
$(iv)$ _bounded lookback_.  (2) Second, we prove that finite summary
guarantees the existence of a _faithful, finite-state abstraction_ for a DDSA
by representing sets of states as logical constraints. This is used to show
that checking existence of a witness for an LTLf property is decidable.  (3)
Third, we illustrate a _modularity_ result: if a DDSA $\mathcal{B}$ represents
either the sequential, or parallel but variable-disjoint, execution of DDSAs
with finite summary (possibly according to the different criteria
$(i)$-$(iv)$), then also $\mathcal{B}$ enjoys this property and is thus
amenable to our verification technique.

To the best of our knowledge, LTLf model checking of such combinations of
$(i)-(iv)$ is shown decidable for the first time (and the result is new for
$(ii),(iv)$ individually).

To demonstrate feasibility, we implemented our approach in the tool ada, which
tests for finite summary using $(i)-(iv)$, computes finite-state abstractions,
and handles LTLf model checking using an SMT solver as backend.

Related Work. Verification of transition systems with arithmetic constraints
has been studied in many areas including formal methods, database theory, and
BPM. For monotonicity constraint (MC) systems, LTL model checking was proven
decidable in (Demri and D’Souza 2007), even comparing variables multiple steps
apart. An extended language is studied in (Demri 2006). DDSAs with MCs are
also considered in (Felli, de Leoni, and Montali 2019) from the perspective of
a finite-run semantics, giving an explicit procedure to compute finite,
faithful abstractions. For gap-order constraint (GC) systems, reachability was
shown decidable (Bozga, Gîrlea, and Iosif 2009). Also the existential fragment
of CTL∗ with GCs is decidable, while the universal one is not (Bozzelli and
Pinchinat 2014). A similar dichotomy was discovered for the EF and EG
fragments of CTL (Mayr and Totzke 2016). We here consider LTLf model checking,
a task suited to many applications (de Giacomo and Vardi 2013): For DDSAs with
a finite summary, we prove decidability of our verification task, i.e., to
check existence of a witness for an LTLf formula with constraints. Finite
summary is based on the notion of _history constraints_ from (Damaggio,
Deutsch, and Vianu 2012), and we show that it generalizes their feedback
freedom property, though their constraints may refer to a read-only database,
a feature that we leave for future work. DDSAs generalize timed automata, and
in fact our abstraction shares with the famous region graph the representation
of a “region” of reachable states by a formula (Alur and Dill 1994). The
finite summary property does not cover timed automata with multiple clocks,
whereas the one-clock-case is captured by MCs. Abstracting reachable states by
formulas is an approach that was also pursued in (Barrett, Demri, and Deters
2013). However, our results are incomparable to both of these works. Our
method can be seen as a form of predicate abstraction, subject to a long line
of research (e.g., (Clarke et al. 2004; Colón and Uribe 1998)); but in
contrast to most works there, our abstraction is _strongly_ preserving, i.e.,
our verification task is decidable.

Paper structure. In Sec. 2 we formalize DDSAs and our verification language
and task. In Sec. 3 we develop the notion of finite summary and show how it
yields finite state abstractions. Sec. 4 is devoted to our verification
technique. In Sec. 5 we demonstrate four concrete classes implying finite
summary, and in Sec. 6 we present modularity results. Sec. 7 describes our
tool ada and concludes with directions for future work. All proofs and further
examples can be found in an extended version (Felli, Montali, and Winkler
2021).

##  2 DDSs with Arithmetic

In this section we fix our model and verification language: we enrich _data-
aware dynamic systems (DDSs)_ from (de Leoni, Felli, and Montali 2020) with
linear arithmetic constraints, and extend the linear-time verification
language correspondingly.

Model. We start by defining the set of arithmetic constraints over a domain
$D$, which may be $\mathbb{Z}$, $\mathbb{Q}$, or $\mathbb{R}$:

######  Definition 2.1.

A _constraint_ $c$ over a set $V$ of variables is defined by the following
grammar, where $k\in D$ and $v\in V$:
$e$ := $v\ \mid\ k\ \mid\ e+e\ \mid\ e-e\ $ $c$ := $e=e\ \mid\ e\neq e\ \mid\
e<e\ \mid\ e\leq e\ \mid\ c\wedge c$

The set of all constraints over domain $D$ is denoted by $\mathcal{C}_{D}$.
E.g., $x\neq 1$, $x<y\,{-}\,z$, and $x\,{-}\,y=2$ are constraints over
$\\{x,y,z\\}$ for domain $\mathbb{Z}$, $\mathbb{Q}$, or $\mathbb{R}$. From now
on, $V$ will be a fixed, finite set of variables. Two disjoint copies $V^{r}$
and $V^{w}$ of $V$, called the _read_ and _write_ variables, denote the
variable values before and after a transition, respectively. We also write
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V$ for a vector that
contains the variables $V$ in an arbitrary but fixed order, and
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{r}$ and
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{w}$ for $V^{r}$ and
$V^{w}$ ordered in the same way. Throughout this paper, by a _formula_
$\varphi$ we mean a boolean formula whose atoms are either propositional or
constraints as in Def. 2.1. We are thus in the realm of SMT with linear
arithmetic, which is decidable and admits _quantifier elimination_ : if
$\varphi$ is a formula with free variables $X\cup\\{y\\}$, and atoms in
$\mathcal{C}_{D}$ (cf. Def. 2.1), there is some $\varphi^{\prime}$ with free
variables $X$ that is equivalent to $\exists y.\varphi$, i.e.,
$\varphi^{\prime}\,{\equiv}\,\exists y.\varphi$ (Presburger 1929). Here the
relation $\equiv$ denotes logical equivalence. For a set $C$ of constraints
and a formula $\varphi$, we sometimes write $\varphi\wedge C$ for the formula
$\varphi\wedge\bigwedge C$.

A _state variable assignment_ $\alpha$ is a total function $\alpha\colon
V\mapsto D$; we say that $\alpha$ _satisfies_ a constraint $c$ over $V$,
written $\alpha\models c$, if the evaluation of $c$ under $\alpha$ is true in
$D$.

######  Definition 2.2.

A _DDS with arithmetic (DDSA)_ is a labelled transition system $\langle
B,b_{0},\mathcal{A},T,F,V,\alpha_{0},guard\rangle$, where:

  * $\bullet$

$B$ is a finite set of _states_ , with $b_{0}\in B$ the initial one;

  * $\bullet$

$\mathcal{A}$ is a finite set of _actions_ ;

  * $\bullet$

$T\colon B\times\mathcal{A}\mapsto B$ is a _transition function_ ;

  * $\bullet$

$F\subseteq B$ is the set of _final states_ ;

  * $\bullet$

$\alpha_{0}$ is the _initial state variable assignment_ ; and

  * $\bullet$

$guard\colon\mathcal{A}\mapsto\mathcal{C}_{D}$ specifies _executability
constraints_ on actions over variables $V^{r}\cup V^{w}$.

In Def. 2.2 we restrict to conjunctive guards: disjunction can be captured by
multiple transitions between the same states. With this convention, the system
in Ex. 1.1 can be transformed into an equivalent DDSA, and Fig. 1 shows
further examples of DDSAs. Note that a guard simultaneously expresses a
condition on the read variables, and an update on the written ones: for
instance, $v^{r}<7$ requires the current value of $v$ to be less than $7$,
while $v^{w}-v^{r}\leq 7$ demands that the new value of $v$ exceeds the
current value by at most $7$.

We denote a transition from state $b$ to $b^{\prime}$ by executing an action
$a\,{\in}\,\mathcal{A}$ as
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$. A _configuration_
of $\mathcal{B}$ is a pair $(b,\alpha)$ where $b\,{\in}\,B$ and $\alpha$ is a
state variable assignment.

A _guard assignment_ $\beta$ is a function $\beta\colon V^{r}\cup V^{w}\mapsto
D$. As defined next, an action $a$ transforms a configuration $(b,\alpha)$
into a new configuration $(b^{\prime},\alpha^{\prime})$ by changing state as
defined by action $a$, and updating the state variable assignment in agreement
with the action guard. In the new assignment $\alpha^{\prime}$, variables that
are not written keep their previous value as per $\alpha$, whereas written
variables are updated according to the guard. Let $write(a)=\\{x\mid x^{w}\in
V^{w}\text{ occurs in }guard(a)\\}$.

######  Definition 2.3.

A DDSA $\mathcal{B}\,{=}\,\langle
B,b_{0},\mathcal{A},T,F,V,\alpha_{0},\mathit{guard}\rangle$ _admits a step_
from configuration $(b,\alpha)$ to $(b^{\prime},\alpha^{\prime})$ via action
$a$, denoted
$(b,\alpha)\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}(b^{\prime},\alpha^{\prime})$,
if $b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$ and the guard
assignment $\beta$ given by $\beta(v^{r})=\alpha(v)$ and
$\beta(v^{w})=\alpha^{\prime}(v)$ for all $v\in V$ satisfies the guard of $a$,
i.e., $\beta\models\mathit{guard}(a)$ holds.

A _run_ of length $n$ is a sequence of steps
$\smash{\rho\colon(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}}$
$\smash{(b_{1},\alpha_{1})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}(b_{n},\alpha_{n})}$,
and $\rho_{i}$ refers to $(b_{i},\alpha_{i})$. Note that a run always starts
in the initial state $(b_{0},\alpha_{0})$.

Specification language. For a constraint set $\mathcal{C}$ over $V$ and DDSA
$\mathcal{B}=\langle B,b_{0},\mathcal{A},T,F,V,\alpha_{0},guard\rangle$, let
$\mathcal{L}_{\mathcal{B}\mathcal{C}}$ be the language defined by the
following grammar:
$c\mid b\mid\psi{\wedge}\psi\mid\psi{\vee}\psi\mid\langle
a\rangle\psi\mid\langle\cdot\rangle\psi\mid\Diamond\psi\mid\Box\psi\mid\psi\mathrel{\mathsf{U}}\psi$
where $a\,{\in}\,\mathcal{A}$, $c\,{\in}\,\mathcal{C}$, and $b\,{\in}\,B$.
Note that $\mathcal{L}_{\mathcal{B}\mathcal{C}}$ does not support negation as
we will also consider fragments where decidability is lost if constraints can
be negated. However, if the set $\mathcal{C}$ is closed under negation,111Here
a constraint set $\mathcal{C}$ is _closed under negation_ if for all
$c\,{\in}\,\mathcal{C}$ there is some $c^{\prime}\,{\in}\,\mathcal{C}$ such
that $c^{\prime}\equiv\neg c$. $\mathcal{L}_{\mathcal{B}\mathcal{C}}$ can
express an arbitrary formula in negation normal form. We adapt LTLf semantics
(de Giacomo and Vardi 2013):

$\mathcal{B}_{1}$$\mathsf{1}$$\mathsf{2}$$\mathsf{a}_{1}\colon[x^{w}>y^{r}]$$\mathsf{a}_{2}\colon[y^{w}>x^{r}]$$\mathcal{B}_{2}$$\mathsf{1}$$\mathsf{2}$$\mathsf{3}$$[x^{w}>0]$$[y^{w}>x^{r}]$$[y^{r}\leq
x^{r}+7]$$\mathcal{B}_{3}$$\mathsf{1}$$\mathsf{2}$$[x^{w}-y^{r}\geq
2]$$[y^{w}-y^{r}\geq
3]$$\mathcal{B}_{4}$$\mathsf{1}$$\mathsf{2}$$\mathsf{3}$$[s^{w}=a^{r}]$$[s^{w}=s^{r}+b^{r}]$$[a^{w}=0\wedge
b^{w}=0]$$[a^{w}>0]$$[b^{w}>0]$

Figure 1: Simple DDSAs (with finite summary).

######  Definition 2.4.

A run $\rho$ of length $n$ _satisfies_
$\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}$, denoted $\rho\models\psi$, iff
$\rho,0\models\psi$ holds, where for $0\leq i\leq n$:

$\rho,i\models c$ | iff $\rho_{i}=(b,\alpha)$ for some $b$ and $\alpha\models c$
---|---
$\rho,i\models b$ | iff $\rho_{i}=(b,\alpha)$ for some $\alpha$
$\rho,i\models\psi_{1}\wedge\psi_{2}$ | iff $\rho,i\models\psi_{1}$ and $\rho,i\models\psi_{2}$
$\rho,i\models\psi_{1}\vee\psi_{2}$ | iff $\rho,i\models\psi_{1}$ or $\rho,i\models\psi_{2}$
---|---
$\rho,i\models\langle a\rangle\psi$ | iff $i<n$, $\exists\beta$ $\smash{\rho_{i}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a,\beta}$}}\rho_{i{+}1}}$ and $\rho,i{+}1\models\psi$
$\rho,i\models\langle\cdot\rangle\psi$ | iff $i<n$ and $\rho,i{+}1\models\psi$
$\rho,i\models\Diamond\psi$ | iff $\rho,i\models\psi$ or ($i<n$ and $\rho,i{+}1\models\Diamond\psi$)
$\rho,i\models\Box\psi$ | iff $\rho,i\models\psi$ and ($i=n$ or $\rho,i{+}1\models\Box\psi$)
$\rho,i\models\psi_{1}\mathrel{\mathsf{U}}\psi_{2}$ | iff $\rho,i\models\psi_{2}$, or ($i\,{<}\,n$ and both
|  $\rho,i\models\psi_{1}$ and
$\rho,i{+}1\models\psi_{1}\mathrel{\mathsf{U}}\psi_{2}$)

Verification problem. We use $\mathcal{L}_{\mathcal{B}\mathcal{C}}$ to express
properties over the finite traces of a DDSA $\mathcal{B}$. A run $\rho$ is a
_witness_ for $\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}$ if $(i)$ $\rho$
ends in a final state of $\mathcal{B}$ and $(ii)$ $\rho\models\psi$.

######  Definition 2.5 (Verification task).

Given a DDSA $\mathcal{B}$ and $\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}$,
check whether there exists a witness $\rho$ for $\psi$ in $\mathcal{B}$.

If $\mathcal{C}$ is closed under negation, one can model check $\psi$ by
looking for a witness for $\neg\psi$, i.e., a counterexample.

Unsurprisingly, DDSAs can directly encode 2-counter Minsky machines, making
the verification task undecidable.

######  Remark 2.6.

It is undecidable to check whether there exists a witness for a property of
the form $\Diamond b$ in a DDSA, for $b\in B$.

##  3 DDSAs with Finite Summary

Instead of taming undecidability of verification by directly looking for
decidable fragments, we introduce a _semantic property_ called _finite
summary_ , and show that DDSAs with this property admit a faithful finite-
state abstraction that preserves all properties expressible in our
verification language. Throughout the section, we fix a DDSA
$\mathcal{B}=\langle B,b_{0},\mathcal{A},T,F,V,\alpha_{0},guard\rangle$ and a
finite constraint set $\mathcal{C}$. We first consider paths in $\mathcal{B}$,
called _symbolic runs_ :

######  Definition 3.1.

A _symbolic run_ $\sigma$ is a transition sequence
$\smash{b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}b_{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}b_{n}}$
where $b_{i}\,{\in}\,B$ and $a_{i}\,{\in}\,\mathcal{A}$; it _abstracts_ any
run of the form
$\smash{(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}(b_{1},\alpha_{1})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}}$
$\smash{\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}(b_{n},\alpha_{n})}$
i.e., a run with the same state and action sequence. The prefix of $\sigma$ of
$i$ steps is denoted $\sigma|_{i}$.

For instance, for the DDSA $\mathcal{B}_{1}$ in Fig. 1 the sequence
$\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}\mathsf{1}$
is a symbolic run. In this section, we aim to construct an abstract
representation of the reachable configurations of $\mathcal{B}$, where we
capture a set of configurations by a pair $(b,\varphi)$ of a system state
$b\,{\in}\,B$ and a formula $\varphi$ with free variables $V$ that describes
the current state of the data. Our aim is to find a _finite_ set of such pairs
that covers all reachable configurations while being precise enough to decide
our verification task. To that end, we next define the $\mathit{update}$
function as a uniform way to express how the current state, captured by a
formula $\varphi$, changes by executing an action.

First, we define the _transition formula_ $\Delta_{a}$ of action $a$ as
$\Delta_{a}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{r},\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{w})\>{=}\>\mathit{guard}(a)\wedge\bigwedge_{v\not\in
write(a)}v^{w}\,{=}\,v^{r}$. Intuitively, this formula states the conditions
on variables _before and after_ executing $a$: $\mathit{guard}(a)$ must be
true and the values of all variables that are not written are propagated by
inertia. Note that $\Delta_{a}$ has free variables
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{r}$ and
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{w}$; for variable
vectors $\makebox[0.0pt]{$\phantom{X}\overline{\phantom{X}}$}X$ and
$\makebox[0.0pt]{$\phantom{Y}\overline{\phantom{Y}}$}Y$ of the same length,
let
$\Delta_{a}(\makebox[0.0pt]{$\phantom{X}\overline{\phantom{X}}$}X,\makebox[0.0pt]{$\phantom{Y}\overline{\phantom{Y}}$}Y)$
be the formula obtained from $\Delta_{a}$ by replacing
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{r}$ by
$\makebox[0.0pt]{$\phantom{X}\overline{\phantom{X}}$}X$ and
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{w}$ by
$\makebox[0.0pt]{$\phantom{Y}\overline{\phantom{Y}}$}Y$.

######  Definition 3.2.

For a formula $\varphi$ with free variables $V$ and an action $a$, let
$\mathit{update}(\varphi,a)=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\Delta_{a}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U,\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)$,
where $\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U$ is a variable
vector of the same length as
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V$ such that $U$ is
disjoint from $V$ and variables in $\varphi$, to avoid variable capture.

For instance, for action $\mathsf{a}_{1}$ in DDSA $\mathcal{B}_{1}$ of Fig. 1,
$\Delta_{\mathsf{a}_{1}}=(x^{w}\,{>}\,y^{r})\wedge(y^{w}\,{=}\,y^{r})$; and
for $\varphi=(x\,{>}\,0)\wedge(y\,{>}\,x)$ we get
$\mathit{update}(\varphi,\mathsf{a}_{1})=\exists
x^{\prime}\,y^{\prime}.(x^{\prime}\,{>}\,0)\wedge(y^{\prime}\,{>}\,x^{\prime})\wedge(x\,{>}\,y^{\prime})\wedge(y\,{=}\,y^{\prime})$.
Using quantifier elimination, we get an equivalent, quantifier-free formula,
for instance $(y\,{>}\,0)\wedge(x\,{>}\,y)$.

A key notion for our approach are _history constraints_ : formulas that sum up
constraints collected along symbolic runs, possibly in combination with
additional constraints that are needed for verification (i.e., constraints
that occur in the property $\psi$ to be checked). To express the latter, we
consider _verification constraint sequences_ $\mathbf{C}$ over constraint set
$\mathcal{C}$, i.e., sequences $\mathbf{C}=\langle C_{0},\dots,C_{n}\rangle$
of sets $C_{i}\subseteq\mathcal{C}$. A prefix $\langle
C_{0},\dots,C_{m}\rangle$ of $\mathbf{C}$ is denoted by $\mathbf{C}|_{m}$.
Moreover, we denote by $C_{\alpha_{0}}=\\{v\,{=}\,\alpha_{0}(v)\mid
v\,{\in}\,V\\}$ the set of _initial constraints_ , to capture in a formula the
initial assignment.

######  Definition 3.3.

For a symbolic run $\sigma\colon
b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}b_{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}b_{n}$,
and verification constraint sequence $\mathbf{C}=\langle
C_{0},\dots,C_{n}\rangle$, the _history constraint_ $h(\sigma,\mathbf{C})$ is
inductively defined by setting
$h(\sigma,\mathbf{C})=\bigwedge(C_{\alpha_{0}}\cup C_{0})$ if $n\,{=}\,0$, and
$h(\sigma,\mathbf{C})=\mathit{update}(h(\sigma|_{n-1},\mathbf{C}|_{n-1}),a_{n})\wedge
C_{n}$ if $n>0$.

Informally, the history constraint of a symbolic run is a formula that
captures all variable constraints that must hold in the last state, i.e., it
is a _summary_ of the symbolic run, taking into account additional
verification constraints $\mathbf{C}$ that will become relevant in Sec. 4.
Note that symbolic runs may in fact feature a sequence of actions that is not
executable due to guard conditions. In these cases history constraints are
unsatisfiable. For simplicity, in what follows we do not rule out these
explicitly (as it does not affect our results), though it is possible and in
fact done in our implementation. We call $h(\sigma,\mathbf{C})$ a history
constraint _of_ $\mathcal{B}$ and $\mathcal{C}$ if $\sigma$ is a symbolic run
of $\mathcal{B}$ and $\mathbf{C}$ is a constraint sequence over $\mathcal{C}$.
If no verification constraints are needed, we write $h(\sigma)$ for
$h(\sigma,\langle\emptyset,\dots,\emptyset\rangle)$.

######  Example 3.4.

For $\mathcal{B}_{1}$ in Fig. 1 with domain $\mathbb{Q}$ and
$\alpha_{0}(x)=\alpha_{0}(y)=0$, let $\sigma_{k}$ be the (unique) symbolic run
of $k$ steps, e.g.
$\sigma_{2}\colon\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}\mathsf{1}$.
We get the history constraints

$\displaystyle h(\sigma_{0})$ $\displaystyle=x\,{=}\,0\wedge y\,{=}\,0$
$\displaystyle(\varphi_{0})$ $\displaystyle h(\sigma_{1})$
$\displaystyle=\exists x_{0}y_{0}.\>x_{0}\,{=}\,0\wedge y_{0}\,{=}\,0\wedge
x\,{>}\,y_{0}\wedge y\,{=}\,y_{0}$ $\displaystyle\equiv x\,{>}\,0\wedge
y\,{=}\,0$ $\displaystyle(\varphi_{1})$ $\displaystyle h(\sigma_{2})$
$\displaystyle=\exists x_{1}y_{1}x_{0}y_{0}.\>x_{0}\,{=}\,0\wedge
y_{0}\,{=}\,0\wedge x_{1}\,{>}\,y_{0}\wedge{}$ $\displaystyle\quad
y_{1}\,{=}\,y_{0}\wedge y\,{>}\,x_{1}\wedge x\,{=}\,x_{1}$
$\displaystyle\equiv x\,{>}\,0\wedge y\,{>}\,x$ $\displaystyle(\varphi_{2})$

where $x_{0}$, $y_{0}$, $x_{1}$, $y_{1}$ are fresh variables. The equivalence
steps are obtained by simplification and quantifier elimination. In a similar
way, we get for
$\sigma_{3}\colon\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}$
the constraint $h(\sigma_{3})\equiv(y\,{>}\,0)\wedge(x\,{>}\,y)$, and for
$\sigma_{4}\colon\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}\mathsf{1}$
we get $h(\sigma_{4})\equiv(x\,{>}\,0)\wedge(y\,{>}\,x)$. The fact that
$h(\sigma_{2})$ and $h(\sigma_{4})$ are equivalent reflects that $\sigma_{2}$
and $\sigma_{4}$ are equivalent in our finite-state abstraction.

Next we relate history constraints and assignments in runs.

######  Lemma 3.5.

For any symbolic run $\sigma$ of length $n$ and $\mathbf{C}=\langle
C_{0},\dots,C_{n}\rangle$, $\smash[t]{h(\sigma,\mathbf{C})}$ is satisfied by
assignment $\alpha$ iff there is a run
$\smash{(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}(b_{n},\alpha_{n})}$
that is abstracted by $\sigma$ such that $\alpha=\alpha_{n}$ and
$\alpha_{i}\models C_{i}$ for all $i$, $0\leq i\leq n$.

This shows that history constraints faithfully summarize accumulated
constraints in symbolic runs, and their satisfying assignments correspond to
the results of actual runs. Both directions are proven by straightforward
induction proofs. For instance, Lem. 3.5 states that since the assignment
$\alpha(x)=9$, $\alpha(y)=7$ satisfies $h(\sigma_{3})$ in Ex. 3.4, there is a
run abstracted by $\sigma_{3}$ ending with this assignment. This is true,
e.g., for $(\mathsf{1},\text{ \leavevmode\hbox to22.23pt{\vbox
to10.4pt{\pgfpicture\makeatletter\hbox{\hskip 11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{0}\\\ {y}&{0}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}(\mathsf{2},\text{
\leavevmode\hbox to22.23pt{\vbox to10.4pt{\pgfpicture\makeatletter\hbox{\hskip
11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{1}\\\ {y}&{0}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}(\mathsf{1},\text{
\leavevmode\hbox to22.23pt{\vbox to10.4pt{\pgfpicture\makeatletter\hbox{\hskip
11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{1}\\\ {y}&{7}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}(\mathsf{2},\text{
\leavevmode\hbox to22.23pt{\vbox to10.4pt{\pgfpicture\makeatletter\hbox{\hskip
11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{9}\\\ {y}&{7}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})$.

Our finite summary property will express that all (infinitely many) symbolic
runs can be faithfully described by a _finite_ set of states $(b,\varphi)$ of
a system state $b\in B$ and a formula $\varphi$ that summarizes accumulated
constraints. To that end, we first define a _history set_ as a set of such
states that contains a representative for every history constraint:

######  Definition 3.6.

A _history set_ $\Phi$ for $\mathcal{B},\mathcal{C}$ is a set of pairs
$(b,\varphi)$ of $b\,{\in}\,B$ and a formula $\varphi$ such that for every
history constraint $h(\sigma,\mathbf{C})$ of $\mathcal{B},\mathcal{C}$ where
$\sigma$ has final state $b$, there is a $(b,\varphi)\,{\in}\,\Phi$ with
$h(\sigma,\mathbf{C})\,{\equiv}\,\varphi$ and $\Phi$ contains no other pairs.

The next result turns out to be convenient in the sequel to characterize
history sets:

######  Lemma 3.7.

$\Phi$ is a history set iff (1) for all $C\subseteq\mathcal{C}$, there is some
$(b_{0},\varphi_{0})\in\Phi$ such that
$\varphi_{0}\equiv\bigwedge(C_{\alpha_{0}}\cup C)$, and (2) for all
$(b,\varphi)\in\Phi$,
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$, and
$C\subseteq\mathcal{C}$, there is some $(b^{\prime},\varphi^{\prime})\in\Phi$
such that $\varphi^{\prime}\equiv\mathit{update}(\varphi,a)\wedge C$.

We will show that some of the DDSA classes that we consider in this paper
admit a _finite_ history set—systems with monotonicity constraints and bounded
lookback—and this feature is sufficient to decide our verification problem.
For other systems (e.g., gap-constraint systems) it is not possible to find
finite history sets. However, we will prove that the verification problem is
still decidable if the more liberal property of _finite summary_ holds.
Basically, this property expresses that there exists a suitable equivalence
relation $\sim$ such that the _quotient_ of a history set with respect $\sim$
is finite. Here, $\sim$ is considered _suitable_ if it is preserved under
steps of $\mathcal{B}$ and implies equisatisfiability; for practicality we
also require decidability. These requirements are made formal in the following
definition.

######  Definition 3.8.

A _summary_ for $(\mathcal{B},\mathcal{C})$ is a pair $(\Phi,\sim)$ of a
history set $\Phi$ for $\mathcal{B}$, $\mathcal{C}$ and equivalence relation
$\sim$ s.t.

  1. (1)

$\sim$ contains $\equiv$ on $\Phi$ and is decidable,

  2. (2)

for all $(b,\varphi),(b,\psi)\in\Phi$ such that $\varphi\sim\psi$,  (a)
$\varphi$and $\psi$ are equisatisfiable, and  (b) for all transitions
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$ and
$C\subseteq\mathcal{C}$, $[\mathit{update}(\varphi,a)\wedge
C]\sim[\mathit{update}(\psi,a)\wedge C]$.

We say that $(\mathcal{B},\mathcal{C})$ _has finite summary_ if it admits a
summary $(\Phi,{\sim})$ where $\sim$ has finitely many equivalence classes.

Here, $[\cdot]$ is a _representative_ function for the given history set: if
for a pair $(b,\psi)$ there is some $(b,\varphi)\in\Phi$ with
$\psi\equiv\varphi$, we can assume that $[\psi]$ is such a formula $\varphi$.
A formula equivalent to $\mathit{update}(\varphi,a)\wedge C$ exists in $\Phi$
because of Lem. 3.7.

Intuitively, a DDSA has finite summary if it admits a finite-state abstraction
that is expressive enough to account for all possible evolutions of
$\mathcal{B}$ and properties in $\mathcal{C}$. We next show that
$(\mathcal{B},\mathcal{C})$ admits a finite summary if it has a finite history
set, so one can pick $\equiv$ as equivalence relation.

######  Lemma 3.9.

If $\mathcal{B}$ and $\mathcal{C}$ admit a finite history set $\Phi$ then
$(\mathcal{B},\mathcal{C})$ has finite summary $(\Phi,\equiv)$.

###### Proof.

Def. 3.8 (1) follows from decidability of linear arithmetic and finiteness of
$\Phi$. For Def. 3.8 (2), we have that (a) $\varphi\,{\equiv}\,\psi$ implies
equisatisfiability, and (b) we can write
$\mathit{update}(\varphi,a)\wedge\bigwedge
C=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi$
and $\mathit{update}(\psi,a)\wedge\bigwedge
C=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\psi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi$
for some $\chi$, and these two formulas are clearly again equivalent as
$\varphi\,{\equiv}\,\psi$. ∎

######  Example 3.10.

Continuing Ex. 3.4, it can be shown that $h(\sigma_{2i})\equiv\varphi_{2}$ and
$h(\sigma_{2i+1})\equiv\varphi_{3}$ for all $i>0$. Thus the set
$\Phi=\\{(\mathsf{1},\varphi_{0}),(\mathsf{2},\varphi_{1}),(\mathsf{1},\varphi_{2}),(\mathsf{2},\varphi_{3})\\}$
is a finite history set, and by Lem. 3.9 the tuple $(\Phi,\equiv)$ is a finite
summary for $(\mathcal{B}_{1},\emptyset)$. It can be visualized in a
constraint graph, as done in (Felli, de Leoni, and Montali 2019):

$\mathsf{1},\varphi_{0}$$\mathsf{2},\varphi_{1}$$\mathsf{1},\varphi_{2}$$\mathsf{2},\varphi_{3}$$\mathsf{a}_{1}$$\mathsf{a}_{2}$$\mathsf{a}_{1}$$\mathsf{a}_{2}$

We conclude this section with another example where the history set is not
finite but a finite summary can be found.

######  Example 3.11.

Consider the DDSA $\mathcal{B}_{3}$, and let $\sigma_{k}$ be the symbolic run
of $k$ steps (there is only one). We have e.g.
$h(\sigma_{1})\equiv(x\,{-}\,y\,{\geq}\,2)\wedge(y\,{=}\,0)$, and
$h(\sigma_{2})\equiv(x\,{\geq}\,2)\wedge(y\,{\geq}\,3)$. In general, we obtain
$h(\sigma_{2i})\equiv(x\,{\geq}\,3i-1)\wedge(y\,{\geq}\,3i)$ and
$h(\sigma_{2i+1})\equiv(x\,{-}\,y\,{\geq}\,2)\wedge(y\,{\geq}\,3i)$ for all
$i\geq 1$. Since $h(\sigma_{i})\not\equiv h(\sigma_{j})$ for $i\neq j$, the
history set $\Phi=\\{h(\sigma_{i})\mid i\geq 0\\}$ is not finite. However, in
Sec. 5 (subsection on gap-order constraints) we will show that
$\mathcal{B}_{3}$ admits a finite summary $(\Phi,\sim_{K})$, where $\sim_{K}$
is the _cutoff equivalence relation_ that considers formulas equivalent if
they are syntactically equal after replacing all constants larger than some
bound $K$ by $K$ itself.

##  4 Checking the Existence of Witnesses

In order to express the requirements on a run of a DDSA $\mathcal{B}$ to
satisfy an LTLf formula $\psi$, we next define a nondeterministic automaton
(NFA) ${\mathcal{N}}_{\psi}$. Then we combine ${\mathcal{N}}_{\psi}$ with
$\mathcal{B}$ in a kind of product construction to check for the existence of
witnesses for $\psi$.

To get the NFA, we perform a similar preprocessing step as in (de Leoni,
Felli, and Montali 2020), and replace first all occurrences of subformulas
$\langle a\rangle\psi^{\prime}$ in $\psi$ by
$\langle\cdot\rangle(a\wedge\psi^{\prime})$, adding a new proposition symbol
for each action. For a run $\rho$ of length $n$, we thus write $\rho,i\models
a$ if $0\,{<}\,i\,{<}\,n$ and $\rho,i-1\models\langle a\rangle\top$. This
modification allows us to consider fewer cases in the constructions and proofs
below.

Technically, given $\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}$ we build the
NFA ${\mathcal{N}}_{\psi}=(Q,\Sigma,\varrho,q_{0},Q_{F})$, where:  (i) the set
$Q$ of states is a set of quoted formulas;  (ii) $\Sigma\,{=}\,2^{S}$is the
alphabet, where $S=B\,{\cup}\,\mathcal{A}\,{\cup}\,\mathcal{C}$;  (iii)
$\varrho\subseteq Q\times\Sigma\times Q$is the transition relation;  (iv)
$q_{0}\in Q$is the initial state;  (v) $Q_{F}\subseteq Q$is the set of final
states.  Following (de Giacomo, de Masellis, and Montali 2014), we define
$\varrho$ using an auxiliary function $\delta$ and a new proposition $\lambda$
that marks the last element of the trace. The input of $\delta$ is a (quoted)
formula $\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}\cup\\{\top,\bot\\}$, and
its output a set of tuples
$(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\varsigma)$
where $\psi^{\prime}$ has the same type as $\psi$ and $\varsigma\in
2^{S\cup\\{\lambda,\neg\lambda\\}}$. For two sets of such tuples $R_{1}$,
$R_{2}$, and $\odot$ either $\wedge$ or $\vee$, let $R_{1}\odot
R_{2}=\\{(\text{\textgravedbl}\\!{\psi_{1}\odot\psi_{2}}\\!\text{\textacutedbl},\varsigma_{1}\cup\varsigma_{2})\mid(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl},\varsigma_{1})\,{\in}\,R_{1},(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl},\varsigma_{2})\,{\in}\,R_{2}\\}$,
where we simplify $\psi_{1}\odot\psi_{2}$ if possible. The function $\delta$
is as follows:

$\delta(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl})$ | = $\\{(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\emptyset)\\}\text{ and }\delta(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl})=\\{(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\emptyset)\\}$
---|---
$\delta(\text{\textgravedbl}\\!{p}\\!\text{\textacutedbl})$ | = $\\{(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{p\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\emptyset)\\}\text{ if $p\in\mathcal{C}\cup B\cup\mathcal{A}$}$
$\delta(\text{\textgravedbl}\\!{\psi_{1}\vee\psi_{2}}\\!\text{\textacutedbl})$ | = $\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})\vee\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$
$\delta(\text{\textgravedbl}\\!{\psi_{1}\wedge\psi_{2}}\\!\text{\textacutedbl})$ | = $\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})\wedge\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$
$\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\psi}\\!\text{\textacutedbl})$ | = $\\{(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},\\{\neg\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\lambda\\})\\}$
$\delta(\text{\textgravedbl}\\!{\Diamond\psi}\\!\text{\textacutedbl})$ | = $\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})\vee\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Diamond\psi}\\!\text{\textacutedbl})$
$\delta(\text{\textgravedbl}\\!{\Box\psi}\\!\text{\textacutedbl})$ | = $\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})\wedge(\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Box\psi}\\!\text{\textacutedbl})\vee\delta_{\lambda})$
$\delta(\text{\textgravedbl}\\!{\psi_{1}\mathrel{\mathsf{U}}\psi_{2}}\\!\text{\textacutedbl})$ | = $\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})\vee(\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})\wedge\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle(\psi_{1}\mathrel{\mathsf{U}}\psi_{2})}\\!\text{\textacutedbl}))$

where $\delta_{\lambda}$ abbreviates
$\smash{\\{(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\neg\lambda\\})\\}}$.
While the symbol $\lambda$ is needed for the construction, we can omit it from
the NFA, and define ${\mathcal{N}}_{\psi}$ as follows:

######  Definition 4.1.

Given a formula $\psi\,{\in}\,\mathcal{L}_{\mathcal{B}\mathcal{C}}$, let the
NFA ${\mathcal{N}}_{\psi}\,{=}\,(Q,\Sigma,\varrho,q_{0},\\{q_{f},q_{e}\\})$ be
given by $q_{0}\,{=}\,\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl}$,
$q_{f}\,{=}\,\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}$ and $q_{e}$
is an additional final state, and $Q$, $\varrho$ are the smallest sets such
that $q_{0},q_{f},q_{e}\in Q$ and whenever $q\in Q\setminus\\{q_{e}\\}$ and
$(q^{\prime},\varsigma)\in\delta(q)$ such that
$\\{\lambda,\neg\lambda\\}\not\subseteq\varsigma$ then $q^{\prime}\in Q$ and

  1. (i)

if $\lambda\not\in\varsigma$ then
$(q,\varsigma\setminus\\{\lambda,\neg\lambda\\},q^{\prime})\in\varrho$, and

  2. (ii)

if $\lambda\in\varsigma$ and
$q^{\prime}=\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}$ then
$(q,\varsigma\setminus\\{\lambda,\neg\lambda\\},q_{e})\in\varrho$.

This construction is similar to the one by (de Giacomo, de Masellis, and
Montali 2014), but reflects that our verification language does not include
negation. In fact it can be seen as a relaxation, in that
$\delta(\text{\textgravedbl}\\!{p}\\!\text{\textacutedbl})$ contains
$(\bot,\emptyset)$ rather than $(\bot,\\{\neg p\\})$, for any atom $p$. In
this way, ${\mathcal{N}}_{\psi}$ cannot explicitly require atoms to be false;
instead, the transition labels intuitively state _minimal requirements_ for
$\psi$ to hold.

######  Example 4.2.

Let $\psi=\Diamond c$ for a constraint $c=(y>5)$. By the definition of
$\delta$, we have $\delta(\text{\textgravedbl}\\!{\Diamond
c}\\!\text{\textacutedbl})=\delta(\text{\textgravedbl}\\!{c}\\!\text{\textacutedbl})\vee\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Diamond
c}\\!\text{\textacutedbl})=\\{(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{c\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\emptyset)\\}\vee\\{(\text{\textgravedbl}\\!{\Diamond
c}\\!\text{\textacutedbl},\\{\neg\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\lambda\\})\\}=\\{(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{c,\neg\lambda\\}),(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{c,\lambda\\}),(\text{\textgravedbl}\\!{\Diamond
c}\\!\text{\textacutedbl},\\{\neg\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\lambda\\})\\}$,
so the automaton ${\mathcal{N}}_{\psi}$ is as follows:
$\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl}$$\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl}$$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}$$\\{c\\}$$\emptyset$$\emptyset$$\emptyset$$\emptyset$
Due to our relaxation, the self-loop on
$\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl}$ is labeled $\emptyset$
rather than $\\{\neg c\\}$, but nonetheless ${\mathcal{N}}_{\psi}$ works as
expected: if $c$ is true an accepting path exists, and if $c$ is false no
further possibilities arise.

To express correctness of ${\mathcal{N}}_{\psi}$, we need some notions of
consistency to express that a word $w$ and a symbolic run are not
contradictory with respect to actions and states. First, we call a symbol
$\varsigma\,{\in}\,\Sigma$ _consistent_ with transition
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$ if $\varsigma$ is
disjoint from $\mathcal{A}\,{\setminus}\,\\{a\\}$ and
$B\,{\setminus}\,\\{b^{\prime}\\}$, namely if it contains no action symbol
other than $a$ nor state symbol other than $b^{\prime}$. Let
$\mathit{constr}(\varsigma)=\varsigma\cap\mathcal{C}$.

######  Definition 4.3.

A word $w=\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}\in\Sigma^{*}$ is
_consistent_ with  (a) a symbolic run $\sigma\colon
b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}b_{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}b_{n}$
if $\varsigma_{0}$ is disjoint from $B\setminus\\{b_{0}\\}$, and
$\varsigma_{i}$ is consistent with
$b_{i-1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{i}}$}}b_{i}$ for
$0\,{<}\,i\,{\leq}\,n$.  (b) a run $\rho$ if it is consistent with the
abstraction $\sigma$ of $\rho$ and $\alpha_{i}$ satisfies
$\bigwedge\mathit{constr}(\varsigma_{i})$, where
$\rho_{i}=(b_{i},\alpha_{i})$.

These notions allow us to express correctness of ${\mathcal{N}}_{\psi}$:

######  Lemma 4.4.

${\mathcal{N}}_{\psi}$ accepts a word that is consistent with a run $\rho$ iff
$\rho\models\psi$.

#### Product construction.

To check the existence of a witness for $\psi$ in DDSA $\mathcal{B}$, we
combine ${\mathcal{N}}_{\psi}$ with $\mathcal{B}$ to a cross-product automaton
$\smash{\mathcal{N}^{\psi}_{\mathcal{B}}}$, exploiting the notions from Sec.
3.

First, for technical reasons we add a dummy initial state $b_{0}^{\prime}$ to
$\mathcal{B}$ and update its states to $B^{\prime}=B\cup\\{b_{0}^{\prime}\\}$
and its transitions to $T^{\prime}=T\cup\\{(b_{0}^{\prime},a_{0},b_{0})\\}$
for a fresh action $a_{0}$ with $\mathit{guard}(a_{0})=\top$. We call the
resulting DDSA $\mathcal{B}^{\prime}$.

######  Definition 4.5.

Let $\mathcal{B}^{\prime}=\langle
B^{\prime},b_{0}^{\prime},\mathcal{A},T^{\prime},F,V,\alpha_{0},\mathit{guard}\rangle$
as above, $\mathcal{C}$ a constraint set, and $(\Phi,\sim)$ a summary for
$(\mathcal{B},\mathcal{C})$. For a formula
$\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}$ and ${\mathcal{N}}_{\psi}$ as
above, the _product automaton_
$\smash{\mathcal{N}^{\psi}_{\mathcal{B}}=(P,\Sigma,R,p_{0},P_{F})}$ is as
follows:

  * $\bullet$

States in $P$ are triples $(b,q,\varphi)$ s.t. $b\,{\in}\,B^{\prime}$,
$q\,{\in}\,Q$, $\varphi\in\Phi$;

  * $\bullet$

The initial state is $p_{0}=(b_{0}^{\prime},q_{0},\bigwedge C_{\alpha_{0}})$;

  * $\bullet$

There is a transition
$(b,q,\varphi)\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}(b^{\prime},q^{\prime},\varphi^{\prime})$
in $R$ iff $b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$ in
$T^{\prime}$, there is some $\varsigma\in\Sigma$ s.t.
$q\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\varsigma}$}}q^{\prime}$ in
${\mathcal{N}}_{\psi}$, and

    * $-$

formula $\chi=\mathit{update}(\varphi,a)\wedge constr(\varsigma)$ is
satisfiable, and $\varphi^{\prime}\sim\chi$; in this way, $\chi$ captures all
current constraints that are either inherited from $\mathcal{B}$ or stem from
the transition of ${\mathcal{N}}_{\psi}$, given by $constr(\varsigma)$,

    * $-$

$\varsigma$ is consistent with
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$, and

    * $-$

$(b^{\prime},q^{\prime},\varphi^{\prime})\in P_{F}$ iff $b^{\prime}\in F$,
$q^{\prime}\in Q_{F}$.

Note that $R$ is well-defined in the sense that for every such formula $\chi$
above, some $\varphi^{\prime}$ with $\varphi^{\prime}\sim\chi$ and
$(b^{\prime},\varphi^{\prime})\in\Phi$ exists, because $\Phi$ is a history set
(cf. Lem. 3.7). Thus, if $(\Phi,\sim)$ is a _finite_ summary, the construction
in Def. 4.5 terminates. The next result states properties of the product
construction, the induction proofs of both directions are straightforward.

######  Lemma 4.6.

Let $\sigma$ be a symbolic run of $\mathcal{B}$ and $w\in\Sigma^{*}$. There is
a path $\pi$ with $\sigma=\sigma(\pi)$ to a node $(b,q,\varphi)$ in
$\smash{\mathcal{N}_{\mathcal{B}}^{\psi}}$ such that $\varphi\sim h(\sigma,w)$
iff $w$ is accepted by $\mathcal{N}_{\psi}$, consistent with $\sigma$, and
$h(\sigma,w)$ is satisfiable.

We next state our main result, where $h(\sigma,w)$ denotes
$h(\sigma,\langle\mathit{constr}(\varsigma_{0}),\dots,\mathit{constr}(\varsigma_{n})\rangle)$
for word $w=\varsigma_{0}\cdots\varsigma_{n}$.

######  Theorem 4.7.

Let $\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}$. The language of
$\smash{\mathcal{N}_{\mathcal{B}}^{\psi}}$ is non-empty iff there is a run of
$\mathcal{B}$ that is a witness for $\psi$.

###### Proof.

($\Longrightarrow$) Let $\pi$ be a path to a final state $p_{f}$ in
$\smash{\mathcal{N}_{\mathcal{B}}^{\psi}}$. By Lem. 4.6, there is an accepting
transition sequence in $\mathcal{N}_{\psi}$ labeled
$w=\varsigma_{0}\dots\varsigma_{n}$, and a symbolic run $\sigma(\pi)\colon
b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}b_{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{*}$}}b_{n}$
such that $h(\sigma(\pi),w)$ is satisfiable by some $\alpha$, and
$\varsigma_{i}$ is consistent with
$b_{i-1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{i}}$}}b_{i}$, for all $i$,
so $w$ is consistent with $\sigma$. By Lem. 3.5 (2), there is a run
$\rho\colon(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}(b_{n},\alpha_{n})$
abstracted by $\sigma$ such that $\alpha=\alpha_{n}$ and
$\alpha_{i}\models\bigwedge\mathit{constr}(\varsigma_{i})$ for all $i$,
$0\,{\leq}\,i\,{\leq}\,n$. Thus $w$ is consistent with $\rho$, and it follows
from Lem. 4.4 that $\rho$ is a witness. ($\Longleftarrow$) Let $\rho$ be a
witness for $\psi$, and $\sigma$ its abstraction. By Lem. 4.4,
$\mathcal{N}_{\psi}$ accepts a word $w$ that is consistent with $\rho$.
Consistency of $w$ with $\rho$ implies that $w$ is also consistent with
$\sigma$, and that $\alpha_{i}\models\bigwedge\mathit{constr}(\varsigma_{i})$
for all $i$, $0\,{\leq}\,i\,{\leq}\,n$. Thus $\alpha_{n}$ satisfies
$h(\sigma,w)$ by Lem. 3.5 (1). By Lem. 4.6, the run of $\mathcal{N}_{\psi}$
labeled $w$ and the symbolic run $\sigma$ give rise to a path $\pi$ in
$\smash{\mathcal{N}_{\mathcal{B}}^{\psi}}$ such that $w$ is consistent with
$\sigma$. As $\mathcal{N}_{\psi}$ accepts $w$, and the last state of $\sigma$
is final, also $\pi$ is accepting. ∎

We illustrate the product construction as well as the witness extraction on a
simple example.

######  Example 4.8.

Consider the DDSA $\mathcal{B}_{1}$ from Fig. 1 and a formula
$\psi=\Diamond(y>5)$. We use the NFA $\mathcal{N}_{\psi}$ obtained in Ex. 4.2,
removing the leftmost deadlock state for compactness. Then, the product
automaton is as follows:
$\mathsf{0}$$\psi$$x\,{=}\,y\,{=}\,0$$\mathsf{1}$$\psi$$x\,{=}\,y\,{=}\,0$$\mathsf{2}$$\psi$$x\,{>}\,y\wedge
y\,{=}\,0$$\mathsf{1}$$\psi$$x\,{>}\,0\wedge
y\,{>}\,x$$\mathsf{2}$$\psi$$x\,{>}\,y\wedge
y\,{>}\,0$$\mathsf{1}$$\top$$x\,{>}\,0\wedge y\,{>}\,x\wedge
y\,{>}\,5$$\mathsf{2}$$\top$$x\,{>}\,y\wedge
y\,{>}\,5$$\mathsf{1}$$\top$$x\,{>}\,5\wedge
y\,{>}\,x$$\mathsf{a_{0}}$$\mathsf{a_{1}}$$\mathsf{a_{2}}$$\mathsf{a_{1}}$$\mathsf{a_{2}}$$\mathsf{a_{2}}$$y\,{>}\,5$$\mathsf{a_{2}}$$y\,{>}\,5$$\mathsf{a_{1}}$$y\,{>}\,5$$\mathsf{a_{1}}$$\mathsf{a_{2}}$$\mathsf{a_{1}}$
Since $\mathcal{N}_{\mathcal{B}}^{\psi}$ has a final state (shown shaded), by
Thm. 4.7 a witness for $\psi$ exists. We obtain a witness from the accepting
path drawn in red: This path corresponds to the word
$w=\langle\emptyset\>\emptyset\>\\{y\,{>}\,5\\}\>\emptyset\rangle\in\Sigma^{*}$
accepted by $\mathcal{N}_{\psi}$, and the symbolic run
$\sigma\colon\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}\mathsf{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}\mathsf{2}$
of $\mathcal{B}_{1}$. The formula $\varphi$ in the final state is satisfiable
and equivalent to $h(\sigma,w)$, and for any satisfying assignment of
$\varphi$ we obtain a witness run for $\psi$ according to Lem. 3.5. For
instance for $\alpha(x)=9$, $\alpha(y)=7$, one possible solution is
$(\mathsf{1},\text{ \leavevmode\hbox to22.23pt{\vbox
to10.4pt{\pgfpicture\makeatletter\hbox{\hskip 11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{0}\\\ {y}&{0}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}(\mathsf{2},\text{
\leavevmode\hbox to22.23pt{\vbox to10.4pt{\pgfpicture\makeatletter\hbox{\hskip
11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{1}\\\ {y}&{0}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{2}}$}}(\mathsf{1},\text{
\leavevmode\hbox to22.23pt{\vbox to10.4pt{\pgfpicture\makeatletter\hbox{\hskip
11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{1}\\\ {y}&{7}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\mathsf{a}_{1}}$}}(\mathsf{2},\text{
\leavevmode\hbox to22.23pt{\vbox to10.4pt{\pgfpicture\makeatletter\hbox{\hskip
11.11469pt\lower-5.20004pt\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{
}{{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6}{0.0}{0.0}{0.6}{-11.11469pt}{-3.70003pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\left[\begin{array}[]{@{\,}l@{=}l@{\,}}{x}&{9}\\\ {y}&{7}\\\
\end{array}\right]$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}})$.

##  5 Conditions for Finite Summary

Thanks to Thm. 4.7 we can check for witnesses over DDSAs that admit a finite
summary. Unfortunately, however:

######  Lemma 5.1.

The finite summary property is undecidable.

###### Proof (sketch).

Consider a DDSA $\mathcal{B}$ encoding a Minsky machine. $\mathcal{B}$ admits
a finite summary iff the counter configurations are bounded, which is
undecidable. ∎

In this section we identify relevant, sufficient conditions for finite
summary. In short, these are the following (the equivalence relation used in
Def. 3.8 is given in parentheses).

  1. C1:

$\mathcal{B}$ is over _monotonicity constraints_ ($\equiv$) Thm. 5.2

  2. C2:

$\mathcal{B}$ is over _gap-order constraints_ ($\sim_{K}$) Thm. 5.5

  3. C3:

$\mathcal{B}$ is _feedback free_ ($\equiv$) Thm. 5.8

  4. C4:

$\mathcal{B}$ has _bounded lookback_ ($\equiv$) Thm. 5.10

While C1 and C2 restrict the constraint language, C3 and C4 restrict the
control flow (i.e., the shape of the DDSA). C4 generalizes C3 as well as the
case where $\mathcal{B}$ is acyclic.

Before explaining these conditions, we point out that the DDSAs in Fig. 1
admit a finite summary. $\mathcal{B}_{1}$ can be seen as a monotonicity
constraint (MC) system over $\mathbb{Q}$, or a gap-order constraint (GC)
system over $\mathbb{Z}$, but C3 and C4 do not apply. $\mathcal{B}_{2}$ is
feedback free and it can be shown to have also 2-bounded lookback.
$\mathcal{B}_{3}$ is a GC system over $\mathbb{Z}$ but no other condition
applies. $\mathcal{B}_{4}$ models a shopping process where two products with
prices $a$ and $b$ are chosen by a customer, and the sum is computed in the
variable $s$. $\mathcal{B}_{4}$ has 3-bounded lookback, but due to the self-
reference of $s$ in $s^{w}=s^{r}+b$, C3 does not apply, and neither do C1 or
C2.

Monotonicity constraints (MCs) restrict Def. 2.1 as follows: MCs over
variables $V$ and domain $D$ have the form $p\odot q$ where
$p,q\in{D\,{\cup}\,V}$ and $\odot$ is one of $=,\neq,\leq,<,\geq$, or $>$. For
MCs, we consider $D$ to be $\mathbb{R}$ or $\mathbb{Q}$. An _MC-formula_ is a
boolean formula whose atoms are MCs. A DDSA is an MC-DDSA whose guards are
conjunctions of MCs.

It is known that if $\varphi$ is an MC-formula over constants ${\mathcal{K}}$
and variables $V\cup\\{x\\}$, then for a formula $\exists x.\,\varphi$, we can
find a formula $\varphi^{\prime}\equiv\exists x.\,\varphi$ such that
$\varphi^{\prime}$ is an MC-formula over constants ${\mathcal{K}}$ and
variables $V$, using a quantifier elimination procedure á la Fourier-Motzkin
(Kroening and Strichman 2016, Sec. 5.4). In particular the set of constants
${\mathcal{K}}$ remains the same. This fact is crucial for the next result:

######  Theorem 5.2.

If $\mathcal{B}$ is an MC-DDSA and $\mathcal{C}$ a set of MCs then
$(\mathcal{B},\mathcal{C})$ admits a finite summary.

###### Proof.

Let ${\mathcal{K}}$ be the set of constants in $\mathcal{C}$, ${\alpha_{0}}$,
and guards of $\mathcal{B}$, and $\textup{MC}_{\mathcal{K}}$ the set of
quantifier-free formulas whose atoms are MCs over $V$, ${\mathcal{K}}$, so
$\textup{MC}_{\mathcal{K}}$ is finite up to equivalence. We use Lem. 3.7 to
show that $\Phi_{\textup{MC}}:=B\times\textup{MC}_{\mathcal{K}}$ is a finite
history set. First, for all $C\,{\subseteq}\,\mathcal{C}$,
$\bigwedge(C_{\alpha_{0}}\cup C)\in\textup{MC}_{\mathcal{K}}$. If
$(b,\varphi)\in\Phi_{\textup{MC}}$ and
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$ then
$\mathit{update}(\varphi,a)\wedge
C=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi$
for some MC-formula $\chi\in\textup{MC}_{\mathcal{K}}$. From quantifier
elimination one obtains some $\varphi^{\prime}$ in $\textup{MC}_{\mathcal{K}}$
such that
$\varphi^{\prime}\equiv\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi$.
Thus $(\Phi_{\textup{MC}},\equiv)$ is a finite summary by Lem. 3.9. ∎

This result explains why the history set in Ex. 3.10 is finite. MCs over
$\mathbb{Q}$ and $\mathbb{R}$ are closed under negation, so Thms. 4.7 and 5.2
imply decidability of LTLf model checking. Note that the proof of Thm. 5.2
fails for domain $\mathbb{Z}$, as MCs over $\mathbb{Z}$ are _not_ closed under
quantifier elimination. Instead, they are covered by gap-order constraints,
discussed next.

Gap-order constraints. Let $X$ be a set of variables and
${\mathcal{K}}\subseteq\mathbb{Z}$ a finite set of constants such that
$0\in{\mathcal{K}}$. A _gap-order constraint_ (GC) over $X$ and
${\mathcal{K}}$ restricts Def. 2.1 to constraints of the form $x-y\geq k$ for
$x,y\in X\cup{\mathcal{K}}$ and $k\,{\in}\,\mathbb{N}$. We call a _GC-formula_
a quantifier-free formula whose atoms are GCs, and a GC-DDSA a DDSA where all
guards are conjunctions of GCs. GC-DDSAs are known to generalize MC-DDSAs over
$\mathbb{Z}$ (Bozzelli and Pinchinat 2014): for instance, $x=3$ is expressible
by $x\,{-}\,3\geq 0\wedge 3\,{-}\,x\geq 0$. However, it is known that relaxing
the GC definition to allow also $x-y\leq k$ (or $k<0$ in $x-y\geq k$) renders
reachability in GC-DDSAs undecidable (Bozzelli and Pinchinat 2014).

In order to show that GC-DDSAs allow for a finite summary, we use the concept
of a bounded approximation: Given the set of constants ${\mathcal{K}}$ and
$K:=max\\{|c-c^{\prime}|+1\mid c,c^{\prime}\in{\mathcal{K}}\\}$, the _$K$
-bounded approximation_ $\lfloor\varphi\rfloor_{K}$ of a GC-formula $\varphi$
is obtained from $\varphi$ by replacing all constraints $x\,{-}\,y\geq k$
where $k\geq K$ by $x-y\geq K$. The next lemma rephrases (Bozzelli and
Pinchinat 2014, Props. 6 and 7):

######  Lemma 5.3.

(1) A GC formula $\varphi$ over variables $X$ and constants ${\mathcal{K}}$ is
satisfiable iff $\lfloor\varphi\rfloor_{K}$ is.  (2) GC formulas $\varphi$
over variables $U$ and ${\mathcal{K}}$, and $\psi$ over $U\cup V$ and
${\mathcal{K}}$ satisfy
$\smash{\lfloor\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi\wedge\psi\rfloor_{K}\equiv\lfloor\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\lfloor\varphi\rfloor_{K}\wedge\lfloor\psi\rfloor_{K}\rfloor_{K}}$.

In the remainder of this section, let $\mathcal{B}$ be a GC-DDSA and
$\mathcal{C}$ a constraint set, such that $C_{\alpha_{0}}$ and $\mathcal{C}$
consist of GCs over variables $V$ and constants ${\mathcal{K}}$, and all
guards of $\mathcal{B}$ are GCs over $V^{r}\cup V^{w}$ and ${\mathcal{K}}$,
with the bound $K$ as above. Below we use the fact that GC formulas are closed
under quantifier elimination: if $\varphi$ is a GC formula over variables
$V\cup\\{x\\}$ and constants ${\mathcal{K}}$, we can find a GC formula
$\varphi^{\prime}$ that is equivalent to $\exists x.\,\varphi$, quantifier-
free, and over the variables $V$ (though the constants in $\varphi^{\prime}$
need not be ${\mathcal{K}}$). For details, see (Revesz 1993), (Bozga, Gîrlea,
and Iosif 2009, Thm. 2).

Let $\textup{GC}_{\mathcal{K}}$ be the set of quantifier-free formulas whose
atoms are GCs over $V$ and ${\mathcal{K}}$ and
$\Phi_{\textup{GC}}=B\times\textup{GC}_{\mathcal{K}}$. As
$\textup{GC}_{\mathcal{K}}$ may be infinite, we consider finite summary w.r.t.
the equivalence relation $\sim_{K}$ defined as $\varphi\sim_{K}\psi$ iff
$\lfloor\varphi\rfloor_{K}\equiv\lfloor\psi\rfloor_{K}$.

######  Example 5.4.

For $\mathcal{B}_{3}$ from Fig. 1 we have ${\mathcal{K}}=\\{0,2,3\\}$, so
$K=4$ (if $\mathcal{C}=\emptyset$, otherwise constraints in $\mathcal{C}$ need
to be included). The history constraints
$h(\sigma_{4})\equiv(x\,{\geq}\,5)\wedge(y\,{\geq}\,6)$ and
$h(\sigma_{6})\equiv(x\,{\geq}\,8)\wedge(y\,{\geq}\,9)$ from Ex. 3.11 hence
satisfy $h(\sigma_{4})\sim_{K}h(\sigma_{6})$ because their cutoff is equal,
namely $\lfloor h(\sigma_{4})\rfloor_{K}=\lfloor
h(\sigma_{6})\rfloor_{K}=(x\,{\geq}\,4)\wedge(y\,{\geq}\,4)$.

######  Theorem 5.5.

$(\Phi_{\textup{GC}},\sim_{K})$ is a finite summary for $\mathcal{B}$ and
$\mathcal{C}$.

###### Proof (sketch).

We use Lem. 3.7 to show that $\Phi_{\textup{GC}}$ is a history set: first, for
all $C\,{\subseteq}\,\mathcal{C}$, $\bigwedge(C_{\alpha_{0}}\cup C)$ is in
$\textup{GC}_{\mathcal{K}}$. Next, for $(b,\varphi)\in\Phi_{\textup{GC}}$ and
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$, there is some GC-
formula $\chi$ over $U\cup V$ and ${\mathcal{K}}$ such that
$\smash{\mathit{update}(\varphi,a)\wedge
C=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi}$.
From quantifier elimination we get a GC-formula $\varphi^{\prime}$ over $V$
and ${\mathcal{K}}$ with
$\varphi^{\prime}\equiv\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi$,
so $\varphi^{\prime}\in\textup{GC}_{\mathcal{K}}$. It remains to check Def.
3.8: Suppose $\varphi\sim_{K}\psi$, so
$\lfloor\varphi\rfloor_{K}\equiv\lfloor\psi\rfloor_{K}$. Equisatisfiability of
$\varphi$ and $\psi$ follows from Lem. 5.3 (1). We can write
$\mathit{update}(\varphi,a)\wedge
C=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi$
and $\mathit{update}(\psi,a)\wedge
C=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\psi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi$
for some GC-formula $\chi$ over $U\cup V$ and ${\mathcal{K}}$. Then
$\lfloor\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi\rfloor_{K}\equiv\lfloor\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\psi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi\rfloor_{K}$
follows using Lem. 5.3 (2). Finally, $(\Phi_{\textup{GC}},\sim_{K})$ has
finitely many equivalence classes as the number of $K$-bounded GCs is finite.
∎

With Thm. 4.7 it follows that model checking of a formula $\psi$ is decidable
if $\neg\psi$ is expressible in $\mathcal{L}_{\mathcal{B}\mathcal{C}}$.
However, the latter is not guaranteed for GC-DDSAs since GCs are not closed
under negation. For instance, $\Box(x\,{\geq}\,y)$ can be checked as its
negation is expressible as $\Diamond(y\,{-}\,x\,{\geq}\,1)$; but
$\Box(x\,{-}\,y\,{\geq}\,2)$ cannot as its negation is not expressible in
$\mathcal{L}_{\mathcal{B}\mathcal{C}}$ with GCs.

Feedback freedom (Damaggio, Deutsch, and Vianu 2012) achieves decidability by
forbidding variable updates that depend on an unbounded history: it requires
that for every dependency between two instances $x_{i}$, $x_{j}$ of a variable
$x$ in a run, another “guard” variable $y$, keeps its value for the time span
$[i,j]$ of the dependency. More precisely, let $\sigma$ be a symbolic run of
length $n$ whose $k$-th action is $a_{k}$, and $\mathcal{C}$ a constraint set.
The _computation graph_ $G_{\sigma,\mathcal{C}}$ is the undirected graph with
nodes $\mathcal{V}=\\{v_{i}\mid v\in V\text{ and }0\,{\leq}\,i\,{\leq}\,n\\}$
and an edge from $x_{i}$ to $y_{j}$ iff $x_{i}$ and $y_{j}$ occur in a common
literal of
$\Delta_{a_{k}}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V_{k-1},\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V_{k})\wedge
C(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V_{k})$, for some
$C\subseteq\mathcal{C}$ and $i,j,k\leq n$. The subgraph of
$G_{\sigma,\mathcal{C}}$ of all edges corresponding to equality literals
$x_{i}=y_{j}$ for $x_{i},y_{j}\in\mathcal{V}$ is denoted
$E_{\sigma,\mathcal{C}}$.

Let $\equiv_{E}$ be the smallest equivalence relation on $\mathcal{V}$
containing $E_{\sigma,\psi}$, so that the equivalence classes of $\equiv_{E}$
are the connected components of $E_{\sigma,\psi}$. The equivalence class of
$x_{i}\in\mathcal{V}$ is denoted $\llbracket{x_{i}}\rrbracket$, and the _span_
of $\llbracket{x_{i}}\rrbracket$ is the set of affected instants, i.e.,
$span(\llbracket{x_{i}}\rrbracket)=\\{j\mid\exists v\,{\in}\,V\text{ with
}v_{j}\in\llbracket{x_{i}}\rrbracket\\}$.

######  Definition 5.6.

For a DDSA $\mathcal{B}$ and constraint set $\mathcal{C}$, the pair
$(\mathcal{B},\mathcal{C})$ is _feedback-free_ if for every symbolic run
$\sigma$, every path in $G_{\sigma,\mathcal{C}}$ from $x_{i}$ to $x_{j}$
contains a node $y$ such that $span(\llbracket{x_{i}}\rrbracket)\cup
span(\llbracket{x_{j}}\rrbracket)\subseteq span(\llbracket{y}\rrbracket)$.

The next example illustrates this concept.

######  Example 5.7.

For runs $\sigma_{2}$ of $\mathcal{B}_{2}$ and $\sigma_{4}$ of
$\mathcal{B}_{4}$ (cf. Fig. 1) and $\mathcal{C}=\\{x\,{>}\,5,s\,{>}\,0\\}$, we
get the following graphs $G_{\sigma_{i},\mathcal{C}}$:
$x$$y$$\sigma_{2}\colon$0$\mathsf{1}$1$\mathsf{2}$2$\mathsf{2}$3$\mathsf{2}$4$\mathsf{3}$$a$$s$$b$$\sigma_{4}\colon$0$\mathsf{1}$1$\mathsf{1}$2$\mathsf{2}$3$\mathsf{2}$4$\mathsf{3}$5$\mathsf{1}$
where edges in $E_{\sigma_{i},\mathcal{C}}$ are drawn solid and others dotted.
For $\sigma_{2}$, we have $span(\llbracket{y_{2}}\rrbracket)\allowbreak\cup
span(\llbracket{y_{3}}\rrbracket)\subseteq span(\llbracket{x_{1}}\rrbracket)$.
The graph is similar for other runs, so that $\mathcal{B}_{2}$ is feedback
free; but $\mathcal{B}_{4}$ is not, as witnessed by the path from $s_{3}$ to
$s_{4}$.

We postpone the proof of the next theorem, to show below that feedback freedom
is a special case of _bounded lookback_.

######  Theorem 5.8.

Feedback freedom implies finite summary.

Bounded lookback. We next show that a DDSA $\mathcal{B}$ has finite summary
if, intuitively, at any point of a run of $\mathcal{B}$ the values of $V$
depend on a bounded number of earlier steps. Throughout this section, we
consider a DDSA $\mathcal{B}$ and constraint set $\mathcal{C}$. Moreover, we
denote by $\llbracket{G_{\sigma,\mathcal{C}}}\rrbracket$ the graph obtained
from $G_{\sigma,\mathcal{C}}$ by collapsing all edges in
$E_{\sigma,\mathcal{C}}$.

######  Definition 5.9.

The pair $(\mathcal{B},\mathcal{C})$ has _bounded lookback_ if there is some
$K$ such that for all symbolic runs $\sigma$ of $\mathcal{B}$, all acyclic
paths in $\llbracket{G_{\sigma,\mathcal{C}}}\rrbracket$ have length at most
$K$.

For instance, after collapsing all solid (i.e., $E_{\sigma_{4},\mathcal{C}}$)
edges of $G_{\sigma_{4},\mathcal{C}}$ in Ex. 5.7, the longest path has length
3. In fact, one can show that $(\mathcal{B}_{4},\mathcal{C})$ has bounded
lookback for $K=3$.

######  Theorem 5.10.

Bounded lookback implies finite summary.

###### Proof (sketch).

Let $\Psi$ be the set of formulas with free variables $V$, quantifier depth at
most $K\cdot|V|$, and vocabulary $\mathcal{C}$, $C_{\alpha_{0}}$, and guards
of $\mathcal{B}$. As the quantifier depth is bounded and the set of atoms in
the vocabulary is finite, $\Psi$ is finite up to equivalence. Induction on
$\sigma$ shows that $B\times\Psi$ is a history set: If $\sigma$ is empty,
$h(\sigma,\mathbf{C})$ is quantifier free and has all atoms in
$C_{\alpha_{0}}$, hence it is in $\Psi$. Otherwise, by induction hypothesis,
$h(\sigma|_{n},\mathbf{C}|_{n})$ is equivalent to some $\varphi\in\Psi$, so
$h(\sigma,\mathbf{C})\equiv\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\chi=:\varphi^{\prime}$
for some quantifier free $\chi$. Let $\llbracket{\varphi^{\prime}}\rrbracket$
be the formula that is obtained from $\varphi^{\prime}$ by eliminating all
equality literals $x\,{=}\,y$, and substituting all variables in an
equivalence class by a representative. As
$\llbracket{\varphi^{\prime}}\rrbracket$ encodes
$\llbracket{G_{\sigma,\mathcal{C}}}\rrbracket$ and $(\mathcal{B},\mathcal{C})$
has $K$-bounded lookback, $\llbracket{\varphi^{\prime}}\rrbracket$ is
equivalent to a formula that has quantifier depth at most $K\cdot|V|$. Hence,
$\Psi$ must contain a formula equivalent to
$\llbracket{\varphi^{\prime}}\rrbracket$. ∎

Note that all acyclic DDSAs have bounded lookback, for $K$ the number of
states. For feedback-free systems, (Damaggio, Deutsch, and Vianu 2012, Lem.
5.4) shows that $\llbracket{G_{\sigma,\mathcal{C}}}\rrbracket$ is a tree of
depth at most $|V|$, so that Thm. 5.8 follows from:

######  Lemma 5.11.

If $(\mathcal{B},\mathcal{C})$ is feedback-free then it has $2|V|$-bounded
lookback.

For a fixed $K$, bounded lookback is decidable in a similar way as feedback
freedom (Damaggio, Deutsch, and Vianu 2012, Sec. 4.4), by enumerating all
possible variable dependencies in symbolic runs of $\mathcal{B}$. While
(Damaggio, Deutsch, and Vianu 2012) discovered that LTL model checking is
decidable for feedback-free systems, the respective result—implied by Thms.
4.7 and 5.10—for the larger class of DDSAs with bounded lookback is new.

##  6 Modularity

In this section we show that a DDSA admits a finite summary if it is suitably
decomposable into smaller systems that enjoy this property. As finite summary
of the subsystems may be due to different criteria C1–C4, modularity results
substantially extend applicability of our approach. As an arbitrary splitting
of a DDSA $\mathcal{B}$ into subsystems with finite summary does not imply
that $\mathcal{B}$ inherits the property, we consider two specific ways of
decomposition for a DDSA $\mathcal{B}=\langle
B,b_{0},\mathcal{A},T,F,V,\alpha_{0},\mathit{guard}\rangle$:

######  Definition 6.1.

Suppose $B=B_{1}\cup B_{2}$, $B_{1}\cap B_{2}=\\{b\\}$, and $T$ contains
neither edges from $B_{2}$ to $B_{1}$, nor from $B_{1}\setminus\\{b\\}$ to
$B_{2}\setminus\\{b\\}$; Let $T_{1}$ and $T_{2}$ be the projections of $T$ to
$B_{1}\times\mathcal{A}$ and $B_{2}\times\mathcal{A}$, respectively. Then
$\mathcal{B}$ is _sequentially decomposable_ into the DDSAs
$\mathcal{B}_{1}=\langle
B_{1},b_{0},\mathcal{A},T_{1},\\{b\\},V,\alpha_{0},\mathit{guard}\rangle$ and
$\mathcal{B}_{2}=\langle B_{2},b,\mathcal{A},T_{2},F,V\cup
U,\alpha_{U},\mathit{guard}\rangle$, where $\alpha_{U}$ is the assignment such
that
$\alpha_{U}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)=\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U$,
for some set of variables $U$ such that $|U|=|V|$ and $U$ is disjoint from
$V$.

######  Definition 6.2.

Let $V=V_{1}\,{\uplus}\,V_{2}$ such that all constraints in
$\\{\mathit{guard}(a)\mid a\,{\in}\,\mathcal{A}\\}\cup\mathcal{C}$ are over
$V_{1}$ or $V_{2}$.
Then $(\mathcal{B},\mathcal{C})$ is _variable-decomposable_ into
$(\mathcal{B}_{1},\mathcal{C}|_{V_{1}})$ and
$(\mathcal{B}_{2},\mathcal{C}|_{V_{2}})$ where $\mathcal{B}_{i}=\langle
B,b_{0},\mathcal{A},T,F,V_{i},\alpha_{0}|_{V_{i}},guard_{i}\rangle$, and
$\mathit{guard}_{i}(a)$ is $\mathit{guard}(a)$ if it is over $V_{i}$, and
$\top$ otherwise.

Both ways of decomposition give rise to a modularity result:

######  Theorem 6.3.

Let $\mathcal{B}$ be a DDSA admitting a decomposition into $\mathcal{B}_{1}$
and $\mathcal{B}_{2}$ that is either $(a)$ sequential and so that
$(\mathcal{B}_{i},\mathcal{C})$ has finite summary $(\Phi_{i},\equiv)$, or
$(b)$ variable and so that $(\mathcal{B}_{i},\mathcal{C}|_{V_{i}})$ has finite
summary $(\Phi_{i},\sim_{i})$, for some $\mathcal{C}$ and both
$i\in\\{1,2\\}$. Then $(\mathcal{B},\mathcal{C})$ admits a finite summary.

###### Proof (sketch).

$(a)$ For
$\Phi=\Phi_{1}\cup\\{\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\>\varphi_{1}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\varphi_{2}\mid\varphi_{1}\in\Phi_{1}\text{
and }\varphi_{2}\in\Phi_{2}\\}$, the pair $(\Phi,\equiv)$ is a finite summary.
$(b)$ We show that
$\Phi=\\{\varphi_{1}\wedge\varphi_{2}\mid\varphi_{1}\in\Phi_{1}\text{ and
}\varphi_{2}\in\Phi_{2}\\}$ with $\sim_{1}$ and $\sim_{2}$ combined is a
finite summary. ∎

We conclude this section by showing that Thm. 6.3 allows us to handle our
motivating example Ex. 1.1. Note that decidability does not follow by any of
the criteria C1–C4 alone.

######  Example 6.4.

The system $\mathcal{B}$ of Ex. 1.1 is variable decomposable into a red GC-
DDSA $\mathcal{B}_{1}$ over $\\{b,d\\}$, and a blue/green system
$\mathcal{B}_{2}$ over $\\{o,s,t\\}$. $\mathcal{B}_{2}$ can in turn be
sequentially split into a blue MC-DDSA $\mathcal{B}_{21}$, and the green
single-step system $\mathcal{B}_{22}$ having 1-bounded lookback. By Thm. 6.3,
$\mathcal{B}$ has finite summary because so do $\mathcal{B}_{1}$,
$\mathcal{B}_{21}$, and $\mathcal{B}_{22}$. Then Thm. 4.7 applies to check
that there is no witness for $\Diamond(\mathsf{sold}\wedge d\,{>}\,0\wedge
o\,{\leq}\,t)$ (so property $\psi$ in Ex. 1.1 holds). On the other hand, we
can obtain a witness for $\Diamond(b\,{=}\,1\wedge
o\,{>}\,t\wedge\Diamond(\mathsf{sold}\wedge b\,{\neq}\,1))$, showing that a
bid above the threshold $t$ need not win.

##  7 Conclusion

Implementation. We implemented our approach in the prototype ada (arithmetic
DDS analyzer), available via a web interface (https://ltl.adatool.dev) where
also source code and examples can be found. ada takes a DDSA $\mathcal{B}$ and
an LTLf formula $\psi$ and checks whether $\mathcal{B}$ and the constraints
$\mathcal{C}$ in $\psi$ admit a finite summary according to C1–C4, or if
$\mathcal{B}$, $\mathcal{C}$ is suitably decomposable (cf. Sec. 6). If finite
summary is detected, ada visualizes the constraint graph, the NFA
$\mathcal{N}_{\psi}$, and $\smash{\mathcal{N}_{\mathcal{B}}^{\psi}}$, then
extracts a witness for $\psi$ if it exists (cf. Thm. 4.7). In the extended
version (Felli, Montali, and Winkler 2021) we show results for relevant
examples, including Ex. 1.1 and processes converted from Petri nets with data
(Mannhardt et al. 2016). ada is written in Python and uses the Z3 SMT solver
(de Moura and Bjørner 2008).

Future work. We see many possibilities for extensions: we expect finite
summary to cover further known decidable cases, e.g. DDSAs with integer
periodicity constraints (Demri 2006); and flat systems with Presburger-
definable loop effects (Barrett, Demri, and Deters 2013). For the criteria
C1–C4, it would be interesting to investigate the complexity bounds implied by
our method. Further decomposition results would be useful, too, e.g. forms of
parallel execution. Next, we want to study whether our techniques apply to
branching-time properties, as well as transition systems with full-fledged
relational databases in the vein of (Deutsch et al. 2018; Calvanese et al.
2020).

## References

  * Alur and Dill (1994) Alur, R.; and Dill, D. 1994.  A theory of timed automata.  _Theor. Comput. Sci._ , 126(2): 183–235.
  * Barrett, Demri, and Deters (2013) Barrett, C.; Demri, S.; and Deters, M. 2013.  Witness Runs for Counter Machines.  In _Proc. 10th FroCoS_ , volume 8152 of _LNCS_ , 120–150.
  * Bozga, Gîrlea, and Iosif (2009) Bozga, M.; Gîrlea, C.; and Iosif, R. 2009.  Iterating Octagons.  In _Proc. 15th TACAS_ , volume 5505 of _LNCS_ , 337–351.
  * Bozzelli and Pinchinat (2014) Bozzelli, L.; and Pinchinat, S. 2014.  Verification of gap-order constraint abstractions of counter systems.  _Theor. Comput. Sci._ , 523: 1–36.
  * Calvanese, de Giacomo, and Montali (2013) Calvanese, D.; de Giacomo, G.; and Montali, M. 2013.  Foundations of data-aware process analysis: a database theory perspective.  In _Proc. 32nd PODS_ , 1–12.
  * Calvanese et al. (2018) Calvanese, D.; de Giacomo, G.; Montali, M.; and Patrizi, F. 2018.  First-order _$\mu$_ -calculus over generic transition systems and applications to the situation calculus.  _Inf. Comput._ , 259(3): 328–347.
  * Calvanese et al. (2020) Calvanese, D.; Ghilardi, S.; Gianola, A.; Montali, M.; and Rivkin, A. 2020.  SMT-based verification of data-aware processes: a model-theoretic approach.  _Math. Struct. Comput. Sci._ , 30(3): 271–313.
  * Clarke et al. (2004) Clarke, E. M.; Kroening, D.; Sharygina, N.; and Yorav, K. 2004.  Predicate Abstraction of ANSI-C Programs Using SAT.  _Formal Methods Syst. Des._ , 25(2-3): 105–127.
  * Colón and Uribe (1998) Colón, M.; and Uribe, T. E. 1998.  Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures.  In _Proc. 10th CAV_ , volume 1427 of _LNCS_ , 293–304.
  * Damaggio, Deutsch, and Vianu (2012) Damaggio, E.; Deutsch, A.; and Vianu, V. 2012.  Artifact systems with data dependencies and arithmetic.  _ACM Trans. Database Syst._ , 37(3): 22:1–22:36.
  * de Giacomo, de Masellis, and Montali (2014) de Giacomo, G.; de Masellis, R.; and Montali, M. 2014.  Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness.  In _Proc. 28th AAAI_ , 1027–1033.
  * de Giacomo and Favorito (2021) de Giacomo, G.; and Favorito, M. 2021.  Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata.  In _Proc. 31st ICAPS_ , 122–130. AAAI Press.
  * de Giacomo and Vardi (2013) de Giacomo, G.; and Vardi, M. Y. 2013.  Linear Temporal Logic and Linear Dynamic Logic on Finite Traces.  In _Proc. 23rd IJCAI_ , 854–860.
  * de Leoni, Felli, and Montali (2020) de Leoni, M.; Felli, P.; and Montali, M. 2020.  Strategy Synthesis for Data-Aware Dynamic Systems with Multiple Actors.  In _Proc. 17th KR_ , 315–325.
  * de Moura and Bjørner (2008) de Moura, L.; and Bjørner, N. 2008.  Z3: An Efficient SMT Solver.  In _Proc. 14th TACAS_ , volume 4963 of _LNCS_ , 337–340.
  * Demri (2006) Demri, S. 2006.  LTL over integer periodicity constraints.  _Theor. Comput. Sci._ , 360(1-3): 96–123.
  * Demri and D’Souza (2007) Demri, S.; and D’Souza, D. 2007.  An automata-theoretic approach to constraint LTL.  _Inform. Comput._ , 205(3): 380–415.
  * Deutsch et al. (2018) Deutsch, A.; Hull, R.; Li, Y.; and Vianu, V. 2018.  Automatic verification of database-centric systems.  _ACM SIGLOG News_ , 5(2): 37–56.
  * Felli, de Leoni, and Montali (2019) Felli, P.; de Leoni, M.; and Montali, M. 2019.  Soundness Verification of Decision-Aware Process Models with Variable-to-Variable Conditions.  In _Proc. 19th ACSD_ , 82–91. IEEE.
  * Felli, Montali, and Winkler (2021) Felli, P.; Montali, M.; and Winkler, S. 2021.  Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic (extended version).  Available from https://tinyurl.com/adasoundness/downloads/arithdpnLTLf.pdf.
  * Kroening and Strichman (2016) Kroening, D.; and Strichman, O. 2016.  _Decision Procedures – An Algorithmic Point of View, Second Edition_.  Springer.
  * Mannhardt (2018) Mannhardt, F. 2018.  _Multi-perspective Process Mining_.  Ph.D. thesis, Technical University of Eindhoven.
  * Mannhardt et al. (2016) Mannhardt, F.; de Leoni, M.; Reijers, H.; and van der Aalst, W. 2016.  Balanced multi-perspective checking of process conformance.  _Computing_ , 98(4): 407–437.
  * Mayr and Totzke (2016) Mayr, R.; and Totzke, P. 2016.  Branching-Time Model Checking Gap-Order Constraint Systems.  _Fundam. Informaticae_ , 143(3-4): 339–353.
  * Presburger (1929) Presburger, M. 1929.  Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.  In _Comptes Rendus du I congres de Mathematiciens des Pays Slaves_ , 92–101.
  * Reichert (2012) Reichert, M. 2012.  Process and Data: Two Sides of the Same Coin?  In _OTM 2012_ , volume 7565 of _LNCS_ , 2–19.
  * Revesz (1993) Revesz, P. Z. 1993.  A Closed-Form Evaluation for Datalog Queries with Integer (Gap)-Order Constraints.  _Theor. Comput. Sci._ , 116(1): 117–149.
  * Xiao et al. (2021) Xiao, S.; Li, J.; Zhu, S.; Shi, Y.; Pu, G.; and Vardi, M. Y. 2021.  On-the-fly Synthesis for LTL over Finite Traces.  In _Proc. 35th AAAI_ , 6530–6537. AAAI Press.

##  Appendix A Proofs

### DDSAs with Finite Summary

The next result relates history constraints and symbolic runs to actual runs.
For a run $\rho$ of length $n$ and $i<n$, let $\rho|_{i}$ denote the $i$-step
prefix of $\rho$, for $i\leq n$.

######  Lemma 3.5.

For any symbolic run $\sigma\colon
b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}b_{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}b_{n}$
and $\mathbf{C}=\langle C_{0},\dots,C_{n}\rangle$,

  1. (1)

If $\sigma$ abstracts a run
$\rho\colon(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}(b_{n},\alpha_{n})$
and $\alpha_{i}\models C_{i}$ for all $i$, $0\,{\leq}\,i\,{\leq}\,n$, then
$\alpha_{n}$ satisfies $\smash[t]{h(\sigma,\mathbf{C})}$;

  2. (2)

If $\smash[t]{h(\sigma,\mathbf{C})}$ is satisfied by assignment $\alpha$ then
there is a run
$\rho\colon(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}(b_{n},\alpha_{n})$
that is abstracted by $\sigma$ such that $\alpha=\alpha_{n}$ and
$\alpha_{i}\models C_{i}$ for all $i$, $0\,{\leq}\,i\,{\leq}\,n$.

###### Proof.

  1. (1)

By induction on $n$. If $n\,{=}\,0$ then $\sigma$ and $\rho$ must be empty. As
$\alpha\,{=}\,\alpha_{0}$ satisfies $C_{0}$ by assumption, $\alpha$ also
satisfies $h(\sigma,\langle C_{0}\rangle)=\bigwedge(C_{\alpha_{0}}\cup
C_{0})$. Otherwise, suppose $\sigma$ is a symbolic run $\sigma\colon
b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{*}$}}b_{n}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b_{n+1}$
that abstracts
$\rho\colon(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{*}$}}(b_{n},\alpha_{n})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}(b_{n+1},\alpha_{n+1})$,
and let $\mathbf{C}\,{=}\,\langle C_{0},\dots,C_{n},C_{n+1}\rangle$. Then
$\sigma|_{n}$ also abstracts $\rho|_{n}$, so by the induction hypothesis
$\alpha_{n}$ satisfies $h(\sigma|_{n},\mathbf{C}|_{n})$. By definition of a
step, the guard assignment $\beta$ given by
$\beta(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{r})=\alpha_{n}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)$
and
$\beta(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{w})=\alpha_{n+1}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)$
satisfies $\mathit{guard}(a)$. For $X=V\setminus\mathit{write}(a)$,
$g=\mathit{guard}(a)$, and the formula
$\varphi=h(\sigma|_{n},\mathbf{C}|_{n})$, we thus have

$\displaystyle h(\sigma,\mathbf{C})$
$\displaystyle=\mathit{update}(\varphi,a)\wedge C_{n+1}$
$\displaystyle=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\>\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\Delta_{a}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U,\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)\wedge
C_{n+1}$
$\displaystyle=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.\>\varphi(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge(g\wedge\\!\bigwedge_{v\in
X}\\!v^{w}\,{=}\,v^{r})(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U,\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)\wedge
C_{n+1}$

Since $\alpha_{n+1}\models C_{n+1}$ by assumption, it follows that
$\alpha_{n+1}$ satisfies $h(\sigma,\mathbf{C})$, using the values
$\alpha_{n}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)$ as
witnesses for the existentially quantified variables
$\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U$.

  2. (2)

By induction on $n$. For $n\,{=}\,0$ we have
$h(\sigma,\mathbf{C})=\bigwedge(C_{\alpha_{0}}\cup C_{0})$, which is only
satisfied by $\alpha_{0}$ since $\alpha_{0}$ fixes all variables in $V$. Any
empty run has variable assignment $\alpha_{0}$, and $\alpha_{0}$ satisfies
$C_{0}$, so the claim holds. Now consider a symbolic run $\sigma\colon
b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{*}$}}b_{n}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b_{n+1}$
and $\mathbf{C}=\langle C_{0},\dots,C_{n},C_{n+1}\rangle$ such that
$h(\sigma,\mathbf{C})$ is satisfied by an assignment $\alpha$. Since

$\displaystyle h(\sigma,\mathbf{C})$
$\displaystyle=\mathit{update}(h(\sigma|_{n},\mathbf{C}|_{n}),a)\wedge
C_{n+1}$
$\displaystyle=\exists\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U.h(\sigma|_{n},\mathbf{C}|_{n})(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)\wedge\Delta_{a}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U,\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)\wedge
C_{n+1}$

we have $\alpha\models C_{n+1}$ and there must be an assignment
$\alpha^{\prime}$ with domain $U$ such that $\alpha^{\prime}\cup\alpha$
satisfies
$h(\sigma|_{n},\mathbf{C}|_{n})(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)$
and
$\Delta_{a}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U,\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)$.
Let $\alpha_{n}$ be the assignment with domain
$\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V$ such that
$\alpha_{n}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)=\alpha^{\prime}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)$,
so $\alpha_{n}$ satisfies $h(\sigma|_{n},\mathbf{C}|_{n})$. Therefore, by the
induction hypothesis $\sigma|_{n}$ abstracts a run
$\rho\colon(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}(b_{1},\alpha_{1})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}(b_{n},\alpha_{n})$
with final assignment $\alpha_{n}$, and such that $\alpha_{i}\models C_{i}$
for all $i$, $0\,{\leq}\,i\,{\leq}\,n$. Let $\beta$ be the guard assignment
such that
$\beta(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{r})=\alpha_{n}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)=\alpha^{\prime}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U)$
and
$\beta(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{w})=\alpha(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)$.
Since $\alpha^{\prime}\cup\alpha$ satisfies
$\Delta_{a}(\makebox[0.0pt]{$\phantom{U}\overline{\phantom{U}}$}U,\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V)$,
$\beta$ satisfies
$\Delta_{a}(\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{r},\makebox[0.0pt]{$\phantom{V}\overline{\phantom{V}}$}V^{w})$
and hence $guard(a)$. Thus $\rho$ can be extended with a step
$(b_{n},\alpha_{n})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}(b_{n+1},\alpha_{n+1})$.
By definition of a step the assignment $\alpha_{n+1}$ coincides with $\alpha$.
Moreover, as $\alpha$ satisfies $C_{n+1}$, $\alpha_{i}$ satisfies $C_{i}$ for
all $i$, $0\,{\leq}\,i\,{\leq}\,{n+1}$. This proves the claim. ∎

######  Lemma 3.7.

$\Phi$ is a history set iff (1) for all $C\subseteq\mathcal{C}$, there is some
$(b_{0},\varphi_{0})\in\Phi$ such that
$\varphi_{0}\equiv\bigwedge(C_{\alpha_{0}}\cup C)$, and (2) for all
$(b,\varphi)\in\Phi$,
$b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$, and
$C\subseteq\mathcal{C}$, there is some $(b^{\prime},\varphi^{\prime})\in\Phi$
such that $\varphi^{\prime}\equiv\mathit{update}(\varphi,a)\wedge C$.

###### Proof.

($\Longleftarrow$) Suppose $\Phi$ satisfies (1) and (2). We show that for
every history constraint $h(\sigma,\mathbf{C})$ of $\mathcal{B}$ and
$\mathcal{C}$ where $\sigma$ has final state $b$ there is some
$(b,\varphi)\in\Phi$ with $h(\sigma,\mathbf{C})\equiv\varphi$, by induction on
$\sigma$. If $\sigma$ is empty and $\mathbf{C}=\langle C_{0}\rangle$ then by
Condition (1) there is some $(b_{0},\varphi_{0})\in\Phi$ such that
$\varphi_{0}\equiv\bigwedge(C_{\alpha_{0}}\cup C_{0})$. Otherwise, $\sigma$ is
of the form
$b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{*}$}}b_{n}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b_{n+1}$,
and $\mathbf{C}=\langle C_{0},\dots,C_{n},C_{n+1}\rangle$. By the induction
hypothesis there is some $(b_{n},\varphi)\in\Phi$ such that
$h(\sigma|_{n},\mathbf{C}|_{n})\equiv\varphi$. By Condition (2), there is
hence some $(b_{n+1},\varphi^{\prime})\in\Phi$ such that
$\varphi^{\prime}\equiv\mathit{update}(\varphi,a)\wedge C_{n+1}\equiv
h(\sigma,\mathbf{C})$.

($\Longrightarrow$) Suppose $\Phi$ is a history set. We verify that Conditions
(1) and (2) hold. For (1), let $\sigma$ be the empty run. For all
$C\subseteq\mathcal{C}$, there must be some $(b_{0},\varphi_{0})\in\Phi$ such
that $h(\sigma,\langle C\rangle)=\bigwedge(C_{\alpha_{0}}\cup
C)\equiv\varphi_{0}$, so Condition (1) is satisfied. Next, let
$(b,\varphi)\in\Phi$. By the assumption that every pair in $\Phi$ corresponds
to a history constraint of $\mathcal{B}$ and $\mathcal{C}$, there must be some
$h(\sigma,\mathbf{C})$ such that $\sigma$ ends in $b$ and
$h(\sigma,\mathbf{C})\equiv\varphi$. Let $\sigma^{\prime}$ be $\sigma$
extended with $b\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a}$}}b^{\prime}$, and
$\mathbf{C}^{\prime}$ be $\mathbf{C}$ with $C$ appended. As $\Phi$ is a
history set, there must be some $(b^{\prime},\varphi^{\prime})\in\Phi$ such
that $h(\sigma^{\prime},\mathbf{C}^{\prime})\equiv\varphi^{\prime}$. Since
$h(\sigma^{\prime},\mathbf{C}^{\prime})=\mathit{update}(h(\sigma,\mathbf{C}),a)\wedge
C\equiv\mathit{update}(\varphi,a)\wedge C$, also Condition (2) holds. ∎

### Checking the Existence of Witnesses

Before proving correctness of our approach in Thm. 4.7, we establish relevant
properties of our NFA construction (Def. 4.1). To that end, we define more
precise consistency notions. Let
$\Sigma^{\prime}=2^{S\cup\\{\lambda,\neg\lambda\\}}$.

######  Definition A.1.

  1. 1.

$\varsigma\,{\in}\,\Sigma$ is _consistent with step $i$_ of a symbolic run
$\sigma\colon
b_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}b_{2}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{n}}$}}b_{n}$
if either $i=0$ and $\varsigma$ is disjoint from $B\setminus\\{b_{0}\\}$, or
$\varsigma$ is consistent with
$b_{i-1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{i}}$}}b_{i}$.

  2. 2.

$\varsigma\,{\in}\,\Sigma$ is _consistent with step $i$_ of a run

$\rho\colon(b_{0},\alpha_{0})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{1}}$}}(b_{1},\alpha_{1})\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{2}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{}$}}(b_{n},\alpha_{n})$
(1)

if $\alpha_{i}$ satisfies $constr(\varsigma)$, and $\varsigma$ is consistent
with step $i$ of the abstraction $\sigma$ of $\rho$.

  3. 3.

$\varsigma\,{\in}\,\Sigma^{\prime}$ is _$\lambda$ -consistent with step $i$_
of a run $\rho$ if $\varsigma$ is consistent with step $i$ of $\rho$, if $i<n$
then $\lambda\not\in\varsigma$, and if $i=n$ then
$\neg\lambda\not\in\varsigma$.

By definition, a word
$\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}\in\Sigma^{*}$ is consistent
with a symbolic run $\sigma$ (run $\rho$) if $\varsigma_{i}$ is consistent
with step $i$ of $\sigma$ ($\rho$) for all $i$, $0\,{\leq}\,i\,{\leq}\,n$.

We first note that the function $\delta$ is total in the sense that its result
set contains an entry that is consistent with any pair of an assignment
$\alpha$ and a run $\sigma$:

######  Lemma A.2.

For every run $\rho$ of the form (1), every $i$, $0\leq i\leq n$, and
$\varphi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}\cup\\{\top,\bot\\}$, there is
some
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma)\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})$
such that $\varsigma$ is $\lambda$-consistent with step $i$ of $\rho$.

###### Proof.

By induction on the structure of $\varphi$. The claim is easy to check for
every base case of the definition of $\delta$, and in all other cases it
follows from the induction hypothesis. ∎

We next show a crucial feature of the $\delta$ function, namely that it
preserves and reflects the property of a run satisfying a formula. Both
directions are proven by laborious but straightforward induction proofs on the
formula structure.

######  Lemma A.3.

Let $\varphi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}\cup\\{\top,\bot\\}$,
$\rho$ a run of the form (1), and $0\,{\leq}\,i\,{\leq}\,n$. Then
$\rho,i\models\varphi$ holds if and only if there is some
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma)\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})$
such that
$(a)$ $\varsigma$ is $\lambda$-consistent with step $i$ of $\rho$, $(b)$
either $i<n$ and $\rho,i{+}1\models\varphi^{\prime}$, or $i\,{=}\,n$ and
$\varphi^{\prime}=\top$.

###### Proof.

($\Longrightarrow$) We first note that if $\varphi^{\prime}=\top$ then $(b)$
holds for both $i<n$ and $i=n$ ($\star$). The proof is by induction on
$\varphi$.

  * •

If $\varphi=\top$, we can choose
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma)=(\top,\emptyset)$.

  * •

If $\rho,i\models p$ for some $p\,{\in}\,\mathcal{A}\cup B$, we must have
either $p=b_{i}$, or $p=a_{i}$ and $i>0$. By choosing
$(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{p\\})\in\delta(\text{\textgravedbl}\\!{p}\\!\text{\textacutedbl})$,
consistency holds and we use ($\star$) for $(b)$.

  * •

If $\rho,i\models c$ for some $c\in\mathcal{C}$, we may take
$(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{c\\})\in\delta(\text{\textgravedbl}\\!{c}\\!\text{\textacutedbl})$.
As $\rho,i\models c$, $\alpha_{i}$ satisfies $c$, so consistency holds and we
use ($\star$) for $(b)$.

  * •

Suppose $\rho,i\models\langle\cdot\rangle\varphi$, so that $i\,{<}\,n$ and
$\rho,i{+}1\models\varphi$. For
$(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl},\\{\neg\lambda\\})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\varphi}\\!\text{\textacutedbl})$,
part $(a)$ holds since $\neg\lambda\in\varsigma$ and $i\,{<}\,n$, and $(b)$
because of $\rho,i{+}1\models\varphi$.

  * •

Suppose $\varphi=\varphi_{1}\wedge\varphi_{2}$. By assumption
$\rho,i\models\varphi_{1}\wedge\varphi_{2}$, and hence
$\rho,i\models\varphi_{1}$ and $\rho,i\models\varphi_{2}$. By the induction
hypothesis, there are
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\varphi_{1}}\\!\text{\textacutedbl})$
and
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\varphi_{2}}\\!\text{\textacutedbl})$
such that for both $k\in\\{1,2\\}$, $(a^{\prime})$ $\varsigma_{k}$ is
consistent with step $i$ of $\rho$ and $(b^{\prime})$ either
$\rho,i{+}1\models\varphi_{k}^{\prime}$, or $i\,{=}\,n$ and
$\varphi_{k}^{\prime}=\top$. By definition of $\delta$, we can choose
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}\wedge\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}\cup\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\varphi_{1}\wedge\varphi_{2}}\\!\text{\textacutedbl})$.
Then $(a)$ follows from $(a^{\prime})$ and
$\varsigma=\varsigma_{1}\cup\varsigma_{2}$, and $(b)$ if $i=n$ then
$(b^{\prime})$ implies $\varphi^{\prime}=\top$, and otherwise
$\rho,i{+}1\models\varphi_{1}^{\prime}\wedge\varphi_{2}^{\prime}$.

  * •

Suppose $\varphi=\varphi_{1}\vee\varphi_{2}$. By assumption
$\rho,i\models\varphi_{1}\vee\varphi_{2}$, and hence
$\rho,i\models\varphi_{1}$ or $\rho,i\models\varphi_{2}$. We assume the
former. By the induction hypothesis, there is some
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\varphi_{1}}\\!\text{\textacutedbl})$
such that $(a^{\prime})$ $\varsigma_{1}$ is consistent with step $i$ of
$\rho$, and $(b^{\prime})$ $\rho,i{+}1\models\varphi_{1}^{\prime}$, or
$i\,{=}\,n$ and $\varphi_{1}^{\prime}=\top$. As $\delta$ is total (Lem. A.2),
there must be some
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\varphi_{2}}\\!\text{\textacutedbl})$
such that $\varsigma_{2}$ is $\lambda$-consistent with step $i$ of $\rho$. By
definition of $\delta$, we can choose
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma)$
as
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}\vee\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}\cup\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\varphi_{1}\vee\varphi_{2}}\\!\text{\textacutedbl})$.
Then $(a)$ follows from $(a^{\prime})$ and $\varsigma_{2}$ being
$\lambda$-consistent with step $i$ of $\rho$, and $(b)$ if $i\,{=}\,n$ then
$(b^{\prime})$ implies $\varphi_{1}^{\prime}\,{=}\,\top$, hence
$\varphi^{\prime}\,{=}\,\top$; otherwise
$\rho,i{+}1\models\varphi_{1}^{\prime}\vee\varphi_{2}^{\prime}$.

  * •

Suppose $\rho,i\models\Diamond\varphi$, so either (1) $\rho,i\models\varphi$,
or (2) $i\,{<}\,n$ and $\rho,i{+}1\models\Diamond\varphi$. We have
$\delta(\text{\textgravedbl}\\!{\Diamond\varphi}\\!\text{\textacutedbl})=\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})\vee\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Diamond\varphi}\\!\text{\textacutedbl})$.
In case (1), by the induction hypothesis there is some
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma^{\prime})\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})$
such that $(a_{1})$ $\varsigma^{\prime}$ is $\lambda$-consistent with step $i$
of $\rho$, and $(b_{1})$ $\rho,i{+}1\models\varphi^{\prime}$, or $i\,{=}\,n$
and $\varphi^{\prime}=\top$. In case (2), let
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma^{\prime})$
be
$(\text{\textgravedbl}\\!{\Diamond\varphi}\\!\text{\textacutedbl},\\{\neg\lambda\\})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Diamond\varphi}\\!\text{\textacutedbl})$,
so that $(a_{2})$ $\varsigma^{\prime}$ is $\lambda$-consistent with step $i$
of $\rho$ because $i<n$, and $(b_{2})$ $\rho,i{+}1\models\varphi$. In either
case, the claim follows from $(a_{k})$ and $(b_{k})$ by a similar reasoning as
in the case for disjunction.

  * •

Suppose $\rho,i\models\Box\varphi$, so $\rho,i\models\varphi$ and either (1)
$i=n$, or (2) $\rho,i{+}1\models\Box\varphi$. We have
$\delta(\text{\textgravedbl}\\!{\Box\varphi}\\!\text{\textacutedbl})=\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})\wedge(\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Box\varphi}\\!\text{\textacutedbl})\vee\delta_{\lambda})=(\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})\wedge\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Box\varphi}\\!\text{\textacutedbl}))\vee(\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})\wedge\delta_{\lambda})$.
In either case, by the induction hypothesis there is some
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma^{\prime})\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})$
such that $(a^{\prime})$ $\varsigma^{\prime}$ is $\lambda$-consistent with
step $i$ of $\rho$, and $(b^{\prime})$ $\rho,i{+}1\models\varphi^{\prime}$, or
$i\,{=}\,n$ and $\varphi^{\prime}=\top$.

(1) Let
$(\text{\textgravedbl}\\!{\varphi_{1}}\\!\text{\textacutedbl},\varsigma_{1})$
be
$(\text{\textgravedbl}\\!{\varphi^{\prime}\wedge\top}\\!\text{\textacutedbl},\varsigma^{\prime}\cup\\{\lambda\\})\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})\wedge\delta_{\lambda}$.
We have $(a_{1})$ $\varsigma_{1}$ is $\lambda$-consistent with step $i$ of
$\rho$ because of $(a^{\prime})$ and $i\,{=}\,n$, and $(b_{1})$
$\rho,i{+}1\models\varphi_{1}=\top$ by $(b^{\prime})$.

(2) Let
$(\text{\textgravedbl}\\!{\varphi_{2}}\\!\text{\textacutedbl},\varsigma_{2})$
be
$(\text{\textgravedbl}\\!{\varphi^{\prime}\wedge\Box\varphi}\\!\text{\textacutedbl},\varsigma^{\prime}\cup\\{\neg\lambda\\})\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})\wedge\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Box\varphi}\\!\text{\textacutedbl})$.
Then $(a_{2})$ $\varsigma_{2}$ is $\lambda$-consistent with step $i$ of $\rho$
by $(a^{\prime})$ and $i<n$, and $(b_{2})$
$\rho,i{+}1\models\varphi_{2}=\varphi^{\prime}\wedge\Box\varphi$, using
$(b^{\prime})$ and $\rho,i{+}1\models\Box\varphi$. Thus the two cases can be
combined as in the case for disjunction, using $(a_{1})$, $(b_{1})$ and
$(a_{2})$, $(b_{2})$.

  * •

The case for the $\mathrel{\mathsf{U}}$ operator is similar.

($\Longleftarrow$) Note that the assumptions exclude $\varphi^{\prime}=\bot$.
We apply induction on $\varphi$, and use the definition of $\delta$ for each
case.

  * •

If $\varphi=\top$ then
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma)\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})$
implies $\varphi^{\prime}=\top$, and $\rho,i\models\top$ holds.

  * •

If $\varphi\,{=}\,c\in\mathcal{C}$, we must have $\varphi^{\prime}=\top$ and
$\varsigma=\\{c\\}$. As $\alpha_{i}$ satisfies $constr(\varsigma)$ by
$\lambda$-consistency, $\rho,i\models c$.

  * •

If $\varphi=p$ for $p\in B\cup\mathcal{A}$, we must have
$\varphi^{\prime}=\top$ and $\varsigma=\\{p\\}$. By consistency, either $i=0$
and $\varsigma$ is disjoint from $B\setminus\\{b_{0}\\}$, or $i>0$ and
$\varsigma$ is consistent with
$b_{i-1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{a_{i}}$}}b_{i}$. In the
former case, we must have $p=b_{0}$, so $\rho,0\models p$. Otherwise, by
consistency either $p=b_{i}$ or $p=a_{i}$. In the former case $\rho,i\models
b_{i}$ clearly holds. If $p=a_{i}$, this occurrence of $a_{i}$ must be the
result of replacing a subformula $\langle a_{i}\rangle\psi^{\prime}$ in $\psi$
by $\langle\cdot\rangle(a_{i}\wedge\psi^{\prime})$, for some $\psi^{\prime}$.
We have $\rho,i\models a_{i}$, equivalent to $\rho,i-1\models\langle
a_{i}\rangle\psi^{\prime}$.

  * •

Let $\varphi=\langle\cdot\rangle\chi$. As $\varphi^{\prime}=\top$ or
$\rho,i{+}1\models\varphi^{\prime}$, by definition of $\delta$ the only
possibility is
$\varphi^{\prime}=\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl}$ and
$\varsigma=\\{\neg\lambda\\}$. As $\varsigma$ is consistent with step $i$ of
$\rho$ and $\neg\lambda\in\varsigma$, we must have $i\,{<}\,n$, so
$\rho,i{+}1\models\varphi^{\prime}$ and hence $\rho,i\models\varphi$ by Def.
2.4.

  * •

If $\varphi=\varphi_{1}\wedge\varphi_{2}$ then by
$(\text{\textgravedbl}\\!{\varphi^{\prime}}\\!\text{\textacutedbl},\varsigma)\in\delta(\text{\textgravedbl}\\!{\varphi}\\!\text{\textacutedbl})$
and the definition of $\delta$ there are $\varphi_{1}^{\prime}$ and
$\varphi_{2}^{\prime}$ such that
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}^{\prime})\in\delta(\text{\textgravedbl}\\!{\varphi_{1}}\\!\text{\textacutedbl})$
and
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\varphi_{2}}\\!\text{\textacutedbl})$,
and $\varphi^{\prime}=\varphi_{1}^{\prime}\wedge\varphi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$. Therefore,
either $i=n$ and
$\varphi^{\prime}=\varphi_{1}^{\prime}=\varphi_{2}^{\prime}=\top$, or $i<n$
and $\rho,i{+}1\models\varphi^{\prime}$, which implies
$\rho,i{+}1\models\varphi_{1}^{\prime}$ and
$\rho,i{+}1\models\varphi_{2}^{\prime}$. In either case,
$\rho,i\models\varphi_{1}$ and $\rho,i\models\varphi_{2}$ hold by the
induction hypothesis, so $\rho,i\models\varphi_{1}\wedge\varphi_{2}$.

  * •

Similarly, if $\varphi=\varphi_{1}\vee\varphi_{2}$ then there are
$\varphi_{1}^{\prime}$ and $\varphi_{2}^{\prime}$ such that
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}^{\prime})\in\delta(\text{\textgravedbl}\\!{\varphi_{1}}\\!\text{\textacutedbl})$
and
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\varphi_{2}}\\!\text{\textacutedbl})$,
$\varphi^{\prime}=\varphi_{1}^{\prime}\vee\varphi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$. If $i=n$ and
$\varphi^{\prime}=\top$, then $\varphi_{1}^{\prime}=\top$ or
$\varphi_{2}^{\prime}=\top$. If otherwise $i<n$ then
$\rho,i{+}1\models\varphi^{\prime}$ implies
$\rho,i{+}1\models\varphi_{1}^{\prime}$ or
$\rho,i{+}1\models\varphi_{2}^{\prime}$. From the induction hypothesis we
obtain in either case $\rho,i\models\varphi_{1}$ or
$\rho,i\models\varphi_{2}$, so $\rho,i\models\varphi_{1}\vee\varphi_{2}$.

  * •

If $\varphi=\Diamond\chi$ then by the definition of $\delta$, there are
$\varphi_{1}^{\prime}$ and $\varphi_{2}^{\prime}$ such that
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1}^{\prime})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$,
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Diamond\chi}\\!\text{\textacutedbl})$,
$\varphi^{\prime}=\varphi_{1}^{\prime}\vee\varphi_{2}^{\prime}$, and
$\varsigma=\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$. If $i=n$ and
$\varphi^{\prime}=\top$, we must have $\varphi_{1}^{\prime}=\top$, and by the
induction hypothesis, $\rho,i\models\chi$. If $i<n$, since
$\rho,i{+}1\models\varphi^{\prime}=\varphi_{1}^{\prime}\vee\varphi_{2}^{\prime}$,
by Def. 2.4 either (1) $\rho,i{+}1\models\varphi_{1}^{\prime}$ or (2)
$\rho,i{+}1\models\varphi_{2}^{\prime}$. In case (1), by the induction
hypothesis, $\rho,i\models\chi$. In case (2),
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Diamond\chi}\\!\text{\textacutedbl})$
and $\rho,i{+}1\models\varphi_{2}^{\prime}$ implies
$\varphi_{2}^{\prime}=\Diamond\chi$ and we have $i<n$, so
$\rho,i\models\langle\cdot\rangle\Diamond\chi$ by Def. 2.4. Either way,
$\rho,i\models\Diamond\chi$ holds.

  * •

If $\varphi=\Box\chi$ then we can distinguish two cases:

(1) There are $\varphi_{1}$ and $\varphi_{2}$ such that
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$,
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta_{\lambda}$,
$\varphi^{\prime}=\varphi_{1}^{\prime}\wedge\varphi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}\cup\varsigma_{2}$. As
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta_{\lambda}$,
we must have $\varphi_{2}^{\prime}=\top$ and $\varsigma_{2}=\\{\lambda\\}$
(otherwise, we would have $\varphi^{\prime}=\bot$). By consistency,
$\lambda\in\varsigma$ implies $i=n$, so $\varphi^{\prime}=\top$ by assumption
and therefore we must have $\varphi_{1}^{\prime}=\top$. From the induction
hypothesis and
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$
we conclude $\rho,i\models\chi$, so by Def. 2.4 $\rho,i\models\Box\chi$.

(2) There are $\varphi_{1}^{\prime}$ and $\varphi_{2}^{\prime}$ such that
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$,
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Box\chi}\\!\text{\textacutedbl})$,
$\varphi^{\prime}=\varphi_{1}^{\prime}\wedge\varphi_{2}^{\prime}$ and
$\varsigma=\varsigma_{1}\cup\varsigma_{2}$. We have
$\neg\lambda\in\varsigma_{2}$, so by consistency $i<n$. As
$\rho,i{+}1\models\varphi^{\prime}=\varphi_{1}^{\prime}\wedge\varphi_{2}^{\prime}$,
by Def. 2.4 $\rho,i{+}1\models\varphi_{1}^{\prime}$ and
$\rho,i{+}1\models\varphi_{2}^{\prime}$. By the induction hypothesis,
$(\text{\textgravedbl}\\!{\varphi_{1}^{\prime}}\\!\text{\textacutedbl},\varsigma_{1})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$
and $\rho,i{+}1\models\varphi_{1}^{\prime}$ imply $\rho,i\models\chi$.
Moreover,
$(\text{\textgravedbl}\\!{\varphi_{2}^{\prime}}\\!\text{\textacutedbl},\varsigma_{2})\in\delta(\text{\textgravedbl}\\!{\langle\cdot\rangle\Box\chi}\\!\text{\textacutedbl})$
and $\rho,i{+}1\models\varphi_{2}^{\prime}$ imply
$\varphi_{2}^{\prime}=\Box\chi$ by Def. 2.4, so we have
$\rho,i\models\langle\cdot\rangle\Box\chi$. Thus $\rho,i\models\Box\chi$.

  * •

The case for $\mathrel{\mathsf{U}}$ is similar. ∎

Let a word $\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}\in\Sigma^{\prime*}$
be _well-formed_ if $\lambda\not\in\varsigma_{i}$ for all $0\leq i<n$, and
$\neg\lambda\not\in\varsigma_{n}$.

######  Lemma A.4.

A well-formed word $w\in\Sigma^{\prime*}$ that is consistent with a run $\rho$
satisfies
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w)$
iff $\rho\models\psi$.

###### Proof.

($\Longrightarrow$) Let $w=\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}$ and
$\chi_{0},\chi_{1},\dots,\chi_{n+1}$ be the sequence of formulas witnessing
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w)$,
so that $\chi_{0}=\psi$, $\chi_{n+1}=\top$, and
$(\text{\textgravedbl}\\!{\chi_{i{+}1}}\\!\text{\textacutedbl},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\chi_{i}}\\!\text{\textacutedbl})$
for all $i$, $0\leq i\leq n$. As $w$ is well-formed and consistent with
$\rho$, by definition $\varsigma_{i}$ is $\lambda$-consistent with $\rho$ at
$i$ for all $i$, $0\leq i\leq n$. In order to show that $\rho$ is a witness
for $\psi$, we verify that $\rho,i\models\chi_{i}$ for all $i$,
$0\,{\leq}\,i\,{\leq}\,n$, by induction on $n-i$. In the base case
$i\,{=}\,n$. We have $\chi_{n+1}=\top$ and
$(\text{\textgravedbl}\\!{\chi_{n{+}1}}\\!\text{\textacutedbl},\varsigma_{n})\in\delta(\text{\textgravedbl}\\!{\chi_{n}}\\!\text{\textacutedbl})$,
and from Lem. A.3 ($\Longrightarrow$) it follows that $\rho,n\models\chi_{n}$.
If $i<n$, we assume by the induction hypothesis that
$\rho,i{+}1\models\chi_{i{+}1}$. We have
$(\text{\textgravedbl}\\!{\chi_{i{+}1}}\\!\text{\textacutedbl},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\chi_{i}}\\!\text{\textacutedbl})$,
so $\rho,i\models\chi_{i}$ follows again from Lem. A.3 ($\Longrightarrow$),
which concludes the induction step. Finally, the claim follows for the case
$i\,{=}\,0$ because $\chi_{0}=\psi$.

($\Longleftarrow$) Let $\rho$ be of the form (1). We show that for all $i$,
$0\leq i\leq n$, and every formula $\chi$, if $\rho,i\models\chi$ then there
is a word $w_{i}=\varsigma_{i}\varsigma_{i+1}\cdots\varsigma_{n}$ of length
$n-i+1$ such that
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl},w_{i})$,
and $\varsigma_{j}$ is $\lambda$-consistent with step $j$ of $\rho$ for all
$j$, $i\leq j\leq n$. The proof of is by induction on $n-i$.

In the base case where $i=n$, we assume that $\rho,n\models\chi$. By Lem. A.3
($\Longleftarrow$) there is some $\varsigma_{n}$ such that
$(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\varsigma_{n})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$,
and $\varsigma_{n}$ is $\lambda$-consistent with step $n$ of $\rho$. For the
induction step, assume $i\,{<}\,n$ and $\rho,i\models\chi$. By Lem. A.3
($\Longleftarrow$) there is some
$(\text{\textgravedbl}\\!{\chi^{\prime}}\\!\text{\textacutedbl},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl})$
such that $\rho,i{+}1\models\chi^{\prime}$, and moreover $\varsigma_{i}$ is
$\lambda$-consistent with $\rho$ at step $i$. By the induction hypothesis,
there is a word $w_{i+1}=\varsigma_{i+1}\cdots\varsigma_{n}$ such that
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\chi^{\prime}}\\!\text{\textacutedbl},w_{i+1})$,
and $\varsigma_{j}$ is $\lambda$-consistent with $\rho$ at instant $j$ for all
$j$, $i\,{<}\,j\,{\leq}\,n$. Thus, we can define
$w_{i}=\varsigma_{i}\varsigma_{i+1}\cdots\varsigma_{n}$, which satisfies
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\chi}\\!\text{\textacutedbl},w_{i})$
and $\varsigma_{j}$ is $\lambda$-consistent with $\rho$ at instant $j$ for all
$j$, $i\,{\leq}\,j\,{\leq}\,n$. This concludes the induction step.

By assumption, $\rho,0\models\psi$ holds. From the case $i=0$ of the above
statement, we obtain a word $w=w_{0}$ such that
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w)$
and $w$ is $\lambda$-consistent with all steps of $\rho$, i.e., $w$ is well-
formed and consistent with $\rho$. ∎

######  Lemma A.5.

Let $\psi\in\mathcal{L}_{\mathcal{B}\mathcal{C}}$ and
$(\chi,\varsigma)\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$.

  1. (1)

If $\lambda\in\varsigma$ and $\neg\lambda\not\in\varsigma$ then $\chi=\top$ or
$\chi=\bot$.

  2. (2)

Suppose $\neg\lambda\in\varsigma$, $\lambda\not\in\varsigma$, and $\chi=\top$,
and $\varsigma$ is consistent with some step $i$ of some run $\rho$. Then
there is some
$(\top,\varsigma^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
such that $\neg\lambda\not\in\varsigma^{\prime}$ and $\varsigma^{\prime}$ is
consistent with step $i$ of $\rho$ as well.

  3. (3)

If $\chi$ is not $\top$ or $\bot$ then $\varsigma$ contains $\lambda$ or
$\neg\lambda$.

###### Proof.

All three statements are shown simultaneously by induction on $\psi$.

  * •

If $\psi$ is $\top$, $\bot$, or an atom $p$ then $\chi$ is $\top$ or $\bot$,
so (1) and (3) hold, and $\neg\lambda\not\in\varsigma$, so also (2) is
satisfied.

  * •

If $\psi=\langle\cdot\rangle\psi^{\prime}$ then
$\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})=\\{(\text{\textgravedbl}\\!{\psi^{\prime}}\\!\text{\textacutedbl},\\{\neg\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\lambda\\})\\}$.
(1) is satisfied by
$(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\lambda\\})$, (2)
holds because $\psi^{\prime}$ cannot be $\top$ since $\top$ does not occur in
$\mathcal{L}_{\mathcal{B}\mathcal{C}}$, and (3) is satisfied anyway.

  * •

If $\psi=\psi_{1}\vee\psi_{2}$ then we must have $\chi=\chi_{1}\vee\chi_{2}$
such that
$(\chi_{i},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\psi_{i}}\\!\text{\textacutedbl})$
for both $i\in\\{1,2\\}$, and $\varsigma=\varsigma_{1}\cup\varsigma_{2}$.

(1) Suppose $\lambda\,{\in}\,\varsigma$ and $\neg\lambda\not\in\varsigma$.
First, assume $\lambda\in\varsigma_{1}$, $\neg\lambda\not\in\varsigma_{1}$,
and $\neg\lambda\not\in\varsigma_{2}$. By the induction hypothesis (1),
$\chi_{1}$ is either $\top$ or $\bot$. In the former case, $\chi=\top$, so the
claim holds. Otherwise, $\chi=\chi_{2}$. Then, if $\lambda\in\varsigma_{2}$ we
can again use the induction hypothesis to conclude that $\chi=\chi_{2}$ is
$\top$ or $\bot$. Otherwise, we have $\lambda\not\in\varsigma_{2}$ and
$\neg\lambda\not\in\varsigma_{2}$, so $\chi_{2}$ must be $\top$ or $\bot$ by
the induction hypothesis (3).

(2) Suppose $\neg\lambda\,{\in}\,\varsigma$, $\lambda\not\in\varsigma$, and
$\chi=\top$, and $\varsigma$ is consistent with step $i$ of $\rho$. W.l.o.g.,
we can assume $\neg\lambda\in\varsigma_{1}$, $\lambda\not\in\varsigma_{1}$,
$\lambda\not\in\varsigma_{2}$, and $\chi_{1}=\top$. By the induction
hypothesis (2) applied to $\chi_{1}$, there is some
$(\top,\varsigma_{1}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{1}}\\!\text{\textacutedbl})$
such that $\neg\lambda\not\in\varsigma_{1}^{\prime}$ and
$\varsigma_{1}^{\prime}$ is consistent with step $i$ of $\rho$. By Lem. A.2,
there is some
$(\chi_{2}^{\prime},\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{2}}\\!\text{\textacutedbl})$
such that $\varsigma_{2}^{\prime}$ is consistent with step $i$ of $\rho$, and
such that $\neg\lambda\not\in\varsigma_{2}^{\prime}$. Thus
$(\top,\varsigma^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
with $\varsigma^{\prime}=\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$
satisfies the claim.

(3) If $\chi$ is not $\top$ or $\bot$ then at least one of $\chi_{1}$ or
$\chi_{2}$ is not $\top$ or $\bot$, so by the induction hypothesis (3),
$\varsigma_{1}$ or $\varsigma_{2}$ contains $\lambda$ or $\neg\lambda$, hence
so does $\varsigma$.

  * •

If $\psi=\psi_{1}\wedge\psi_{2}$ then we must have
$\chi=\chi_{1}\wedge\chi_{2}$ such that
$(\chi_{i},\varsigma_{i})\in\delta(\text{\textgravedbl}\\!{\psi_{i}}\\!\text{\textacutedbl})$
for both $i\in\\{1,2\\}$.

(1) Suppose $\lambda\in\varsigma$ and $\neg\lambda\not\in\varsigma$. W.l.o.g.,
we can assume $\lambda\in\varsigma_{1}$, $\neg\lambda\not\in\varsigma_{1}$,
and $\neg\lambda\not\in\varsigma_{2}$. By the induction hypothesis (1),
$\chi_{1}$ is either $\top$ or $\bot$. In the latter case, $\chi=\bot$, so the
claim holds. Otherwise, $\chi=\chi_{2}$, and due to the assumption that
$\neg\lambda\not\in\varsigma_{2}$, by the induction hypothesis (3), $\chi_{2}$
must be $\top$ or $\bot$.

(2) Suppose $\neg\lambda\in\varsigma$, $\lambda\not\in\varsigma$, and
$\chi=\top$, and $\varsigma$ is consistent with step $i$ of $\rho$. We can
assume $\lambda\not\in\varsigma_{1}$, $\lambda\not\in\varsigma_{2}$ and
$\chi_{1}=\chi_{2}=\top$. We must have $\lambda\in\varsigma_{1}$,
$\lambda\in\varsigma_{2}$, or both. However, for each $i\in\\{1,2\\}$ such
that $\lambda\in\varsigma_{i}$, by the induction hypothesis (2) there is some
$(\top,\varsigma_{i}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi_{i}}\\!\text{\textacutedbl})$
such that $\lambda\not\in\varsigma_{i}^{\prime}$ and $\varsigma_{i}^{\prime}$
is consistent with step $i$ of $\rho$. If $\lambda\not\in\varsigma_{i}$, set
$\varsigma_{i}^{\prime}=\varsigma_{i}$. Hence
$(\top,\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime})\in\delta(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl})$
such that $\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$ is consistent
with step $i$ of $\rho$ and
$\neg\lambda\not\in\varsigma_{1}^{\prime}\cup\varsigma_{2}^{\prime}$.

(3) If $\chi$ is not $\top$ or $\bot$ then at least one of $\chi_{1}$ or
$\chi_{2}$ is not $\top$ or $\bot$, so by the induction hypothesis (3),
$\varsigma_{1}$ or $\varsigma_{2}$ contains $\lambda$ or $\neg\lambda$, hence
so does $\varsigma$.

  * •

For $\psi=\Box\psi^{\prime}$, note that
$\delta_{\lambda}=\\{(\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl},\\{\lambda\\}),(\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl},\\{\neg\lambda\\})\\}$
satisfies the properties. The result then follows from the cases for $\vee$
and $\wedge$.

  * •

All other cases follow from the cases for $\vee$ and $\wedge$. ∎

######  Lemma 4.4.

${\mathcal{N}}_{\psi}$ accepts a word $w$ that is consistent with a run $\rho$
iff $\rho\models\psi$.

###### Proof.

($\Longrightarrow$) Let $w=\varsigma_{0}\varsigma_{1}\cdots\varsigma_{n}$, and
$q_{0}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\varsigma_{0}}$}}q_{1}\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\varsigma_{1}}$}}\dots\mathrel{\raisebox{-2.0pt}{$\xrightarrow{\varsigma_{n}}$}}q_{n+1}$
($\star$) be the respective accepting run of ${\mathcal{N}}_{\psi}$. By Def.
4.1, there are $\varsigma_{i}^{\prime}$, such that
$\varsigma_{i}=\varsigma_{i}^{\prime}\setminus\\{\lambda,\neg\lambda\\}$ and
$\\{\lambda,\neg\lambda\\}\not\subseteq\varsigma_{i}^{\prime}$ for all $i$,
$0\leq i\leq n$. Let $w^{\prime}$ be the word
$w^{\prime}=\varsigma_{0}^{\prime}\varsigma_{1}^{\prime}\cdots\varsigma_{n}^{\prime}$.
Then $w^{\prime}$ is consistent with $\rho$ because so is $w$. Moreover, by
Lem. A.5 (2) we can choose $\varsigma_{n}^{\prime}$ such that
$\neg\lambda\not\in\varsigma_{n}^{\prime}$, and $\varsigma_{n}^{\prime}$ is
consistent with $\rho$ at $n$. Then $w^{\prime}$ is well-formed: indeed, since
edges to $\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}$ labeled
$\lambda$ are redirected to $q_{e}$ and
$\text{\textgravedbl}\\!{\bot}\\!\text{\textacutedbl}$ cannot occur in
($\star$), by Lem. A.5 (1) we have $\lambda\not\in\varsigma_{i}^{\prime}$ for
$i<n$. Thus by Def. 4.1 we have
$\text{\textgravedbl}\\!{\top}\\!\text{\textacutedbl}\in\delta^{*}(\text{\textgravedbl}\\!{\psi}\\!\text{\textacutedbl},w^{\prime})$.