# Traversing automata with current state uncertainty
under LTLf constraints

Andrew Ryzhikov1, Petra Wolf2

(1Department of Computer Science, University of Oxford, UK
2 LaBRI, Université de Bordeaux, France)

###### Abstract

In this paper, we consider a problem which we call LTLf model checking on
paths: given a DFA $\mathcal{A}$ and a formula $\phi$ in LTL on finite traces,
does there exist a word $w$ such that every path starting in a state of
$\mathcal{A}$ and labeled by $w$ satisfies $\phi$? The original motivation for
this problem comes from the constrained parts orienting problem, introduced in
[Petra Wolf, “Synchronization Under Dynamic Constraints”, FSTTCS 2020], where
the input constraints restrict the order in which certain states are visited
for the first or the last time while reading a word $w$ which is also required
to synchronize $\mathcal{A}$. We identify very general conditions under which
LTLf model checking on paths is solvable in polynomial space. For the
particular constraints in the parts orienting problem, we consider PSPACE-
complete cases and one NP-complete case. The former provide very strong lower
bound for LTLf model checking on paths. The latter is related to (classical)
LTLf model checking for formulas with the until modality only and with no
nesting of operators. We also consider LTLf model checking of the power-set
automaton of a given DFA, and get similar results for this setting. For all
our problems, we consider the case where the required word must also be
synchronizing, and prove that if the problem does not become trivial, then
this additional constraint does not change the complexity.

##  1 Introduction

Synchronization is a classical and well-studied way of regaining control over
an automaton if its current state is unknown. Given a complete deterministic
finite automaton (complete DFA), we say that a finite word is synchronizing
for it, if it maps all its states to one particular state. Such a word can be
seen as a word resolving the current state uncertainty: if the structure of
the DFA is known, then after reading a synchronizing word the current state of
the DFA is also known. If a DFA admits a synchronizing word, it is also called
synchronizing.

#### Orienting parts.

One of the oldest applications of synchronizing automata is the problem of
designing parts orienters, which are simple robots or machines that get a
number of identical objects in various orientations and need to bring them all
in the same orientation, usually using conveyor belts with obstacles. This
approach is relatively cheap, since it does not require introducing any
sensors that register the orientation of each object, and instead just makes
sure that the final orientation is the same regardless of the initial
orientation of the object, see [AV04] for an example. In his pioneering work,
Natarajan [Nat86] modeled parts orienters as complete DFAs where states
correspond to possible orientations of a part and letters correspond to
applying different modifiers or obstacles. Because of their shape and design,
those modifiers can have different effect on the parts depending on the
orientation of the parts. In this context, he studied automata which were
later called _orientable_ [Vol08]. Many different classes of automata have
since been studied regarding their synchronization behavior. We refer to
[Vol08, BP16, TV19, KV21] for an overview.

Figure 1: Illustration of how different modifiers of a parts orienter can have
an impact on the part itself. Here, the part consists of a box with lids that
open when the box is rotated and need to be closed again by a different
modifier.

The original motivation of designing a parts orienter was revisited in [TY15]
where Türker and Yenigün modeled the design of an assembly line, which again
brings a part from an unknown orientation into a known orientation, with
different costs of modifiers. What has not been considered so far is that
different modifiers can have different impacts on a part, depending on the the
history of its orientations. For example, if the part is a box with a fold-out
lid, turning it upside-down will cause the lid to open as depicted in Figure
1. In order to close the lid, one might need another modifier such as a low
bar which brushes the lid and closes it again. To specify that a parts
orienter must deliver the box facing upward with a closed lid, one needs to
encode the property “when the box is in the state _facing down_ , it must
later be in the state _lid closed_ ”. But this does not stop us from opening
the lid again in the future, so we need to be more precise and instead encode
the property “after the last time the box was in the state _facing down_ , it
must visit the state _lid closed_ at least once”. In order to model these
types of constraints in the automaton abstraction of a parts orienter, we
associate with each word several different traversal relations describing how
it traverses the states of a DFA. We then implement the conditions mentioned
above by requiring the traveral relation associated with the word to agree
with a given binary relation $R$ on the states of the DFA. We consider two
different cases: restricting the traversal relation
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$, intuitively, requires
visiting the state _lid closed_ no matter what, restricting the traversal
relation $\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ only requires
closing the lid if it was opened before that.

To motivate the third traversal relation we consider,
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$, let us again picture the box
with a lid, but this time the box initially contains some water. We would like
to have the box in a specific orientation with the lid open but the water must
not be shed while orientating. We have a modifier that opens the lid and a
modifier which rotates the box. Clearly, we do not want the box to face
downwards after the lid has been opened. So, we encode the property “once the
state _lid open_ is reached, the state _facing downwards_ must never be
visited again”.

#### Controlling multiple automata sharing a common resource.

Consider now the scenario where several copies of the same DFA $\mathcal{A}$
are controlled by the same input, and we know precisely the set $S$ of current
states of these copies. If $S$ is synchronizing, that is, if there exists a
word bringing all the states of $S$ to one particular state, then after
applying a synchronizing word for it we know that the current state of all the
copies is the same. However, the DFAs can have some side effects on the
resources which are shared between all of them. As an example, let $p$ be a
state of $\mathcal{A}$ such that visiting it requests a shared resource and
marks it as busy for all DFAs, and $q$ be a state such that visiting it
releases the resource and marks it as free for all DFAs. It is natural to ask
that after the last moment of time when the resource was requested by at least
one copy of $\mathcal{A}$, it was released by a copy, not necessarily the same
one. In other words, it must not happen that some copy required the resource
and no copy released it afterwards. This restriction can be modeled by
considering sets of possible current states of $\mathcal{A}$, and is
formalized by including the pair $(p,q)$ in the binary relation restricting
the traversal relation $\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$ defined
in Section 2. We also consider a less strict traversal relation
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ where the last visits of $p$
and $q$ are allowed to happen at the same time. We show that checking whether
a word satisfying such requirements exists is PSPACE-complete, even if $S$ is
the set of all states of $\mathcal{A}$.

Another possible interpretation of this setting is that we are given a DFA
$\mathcal{A}^{\prime}$ and a constraint, and want to check if there exists a
word accepted by $\mathcal{A}^{\prime}$ such that the path labeled by it in
$\mathcal{A}^{\prime}$ satisfies this constraint. If $\mathcal{A}^{\prime}$ is
provided as a part of the input, this problem is solvable in polynomial time
for any fixed order constraint. However, we show that if
$\mathcal{A}^{\prime}$ is defined as the power-set automaton of a DFA
$\mathcal{A}$ provided in the input, the problem becomes PSPACE-complete, even
for a fixed constraint. Hence, with such a succinct representation the
complexity of the problem increases drastically, but it is still better than
the trivial approach of explicitly constructing the power-set automaton, which
takes exponential time and space.

The traversal relations $\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$,
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ and
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$ mentioned above also make sense
in the setting where we have a DFA whose structure is known to us, but its
current state is not. Constraining them ensures that whichever state we start
with, when applying the sequence of input commands the requirements are
satisfied. For example, if there is only one copy of a DFA releasing and
requesting a resource, and its current state is unknown, we can ask for a word
which does not request the resource after it is released no matter in which
state the DFA was, and which brings it to a known state.

For $\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$,
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$ and
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ it is also natural to ask
for a word which satisfies the conditions but is not necessarily
synchronizing. In this case, we only care that the resource is eventually
released, but do not require that all the copies are in the same state
afterwards. We prove that dropping the requirement that the word must be
synchronizing does not change the complexity of the problem. However,
satisfying the constraints imposed on
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ and
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$ with a word which is not required
to be synchronizing is trivial: they are satisfied by the empty word.

#### LTL on finite traces.

Linear temporal logic (LTL) is a popular and expressive formalism for
specifying properties of systems [BK08]. Classical LTL is defined on infinite
traces and is more suitable for describing the behavior of reactive systems.
Its variation, LTL on finite traces [GV13], denoted LTLf, is more suitable for
describing the behavior of systems performing tasks which eventually
terminate. The difference between LTL and LTLf is discussed in [DGDMM14]. All
the constraints on the traversal relations that we consider, as well as their
Boolean combinations, can be expressed as formulas of LTLf in a suitable
setting. Moreover, the constructions showing computational complexity lower
bounds for these constraints provide very strong lower bounds on the
complexity of model checking in our setting.

The classical LTLf model checking problem is, given an LTLf formula $\phi$ and
a transition system with a specified initial state $s$ and without any labels
of the transitions, check if there exists a path in the transition system
starting in $s$ and satisfying $\phi$. Our setting differs in that there is no
specified initial state, and the transitions are labeled by letters of the
alphabet. In more detail, we consider either a set of paths starting in each
state of the DFA and labeled by the same word (LTLf model checking on paths),
or a unique path in the power-set automaton labeled by this word (LTLf model
checking on sets). However, we show that the polynomial space algorithm for
the classical setting can be adapted to our settings without an increase in
its computational complexity. In particular, this provides polynomial space
upper bounds for the problem of satisfying all the restrictions discussed
above. On the other hand, in the classical setting model checking becomes
solvable in polynomial time if the LTLf formula is fixed. In contrast, we show
that there exist fixed formulas such that LTLf model checking on paths and on
sets, as well as their synchronized versions, remain PSPACE-complete, even for
DFAs over constant-size alphabet. For synchronized LTLf model checking on
sets, it follows from the PSPACE-completeness of synchronization with
constraints on $\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ for a
constraint relation of constant size, originally proved in [Wol20]. For LTLf
model checking on paths it was explicitly stated and proved in [BFM23] when
the alphabet size grows with the number of states. See the subsection
“Existing results and our contributions” below for a more detailed discussion
of the differences between the settings of [BFM23] and this paper.

#### Related work.

The problem of checking whether for a given DFA
$\mathcal{A}=(Q,\Sigma,\delta)$ there exists a synchronizing word can be
solved in time $\mathcal{O}(|Q|^{2}\cdot|\Sigma|)$ [Epp90, Vol08]. The problem
of finding such a word is solvable in time
$\mathcal{O}(|Q|^{3}+|Q|^{2}\cdot|\Sigma|)$. In comparison, if we only ask for
a subset of states $S\subseteq Q$ to be synchronized, the problem becomes
PSPACE-complete [San04]. These two problems have been investigated for several
restricted classes of automata involving orders on states. Here, we want to
mention the class of _oriented_ automata, whose states can be arranged in a
cyclic order which is preserved by all transitions. This model has been
studied among others in [Nat86, Epp90, AV04, RS18, Vol08]. If the order on the
states is linear instead of cyclic, we get the class of monotonic automata
which was studied in [AV04, RS18].

A (complete or partial) DFA $\mathcal{A}=(Q,\Sigma,\delta)$ is called
_partially ordered_ [BF80] or _weakly acyclic_ [Ryz19] if there exists an
ordering of the states $q_{1},q_{2},\dots,q_{n}$ such that if
$\delta(q_{i},a)=q_{j}$ for some letter $a\in\Sigma$, then $i\leq j$. In other
words, all cycles in a partially ordered DFAs are self-loops. Each
synchronizing partially ordered complete DFA admits a synchronizing word of
linear length [Ryz19]. Going from complete DFAs to partial DFAs brings a jump
in complexity. For example, the so called _careful synchronization_ problem
for partial DFAs asks for a word that is defined on all states and that brings
all states to one particular state. This problem is PSPACE-complete for
partial DFAs, even over binary alphabets and with only one undefined
transition [Mar14, Mar12].

Linear temporal logic (LTL) was introduced as a formalism for verifying
properties of programs [Pnu77, Pnu81]. The LTL model checking problem is,
given a transition system and an LTL formula, check if there exists an
infinite path in the transition system satisfying the formula. This problem is
PSPACE-complete and becomes solvable in polynomial time if the formula is
fixed [BK08]. In [Mar04], the computational complexity of many fragments of
LTL was investigated. LTL on finite traces, denoted LTLf, was introduced in
[GV13] to describe properties of finite paths. The complexity of
satisfiability of formulas from different fragments in LTLf is studied in
[FG18], and a framework for LTLf satisfiability checking is proposed in
[LZP+14].

#### Existing results and our contributions.

The parts orienting problem and traversal constraints were introduced in
[Wol20], a preliminary conference version of this paper. See Section 2.2 for
the discussion on the differences of the notation between [Wol20] and the
current paper. In [Wol20], it was shown that checking the existence of a
synchronizing word with constraints on
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$,
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ and
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$ is PSPACE-complete over constant-
size alphabet, and for constraints on
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$ and
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ it stays PSPACE-complete
even for constraint relations of constant size. It was also shown that
checking the existence of a synchronizing word with constraints on
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$ is in NP, and with constraints
on $\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ is NP-hard.

This setting was later extended to arbitrary LTLf formulas on paths in
[BFM23]. There, is was proved that checking the existence of a synchronizing
word satisfying a given LTLf formula is solvable in polynomial space, and
there exist fixed formulas for which it stays PSPACE-complete. It was also
proved that synchronization with constraints on
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ is PSPACE-complete.
However, all the mentioned complexity lower bounds in [BFM23] require
alphabets of variable size, and atomic propositions that are more general than
just the names of the states.

In this paper, we generalize, unify and improve the results of [Wol20] and
[BFM23]. In Section 3, we recall the PSPACE upper bound for checking the
existence of a synchronizing word under LTLf constraints in [BFM23], and
discuss more general conditions where it can be applied. The most interesting
cases are what we call LTLf model checking on paths and sets, as well as their
synchronized versions. As an application, we show that this generalized
algorithm solves synchronization with constraints on
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$ and
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ in polynomial space.

In Section 4, we prove that for LTLf model checking on paths and sets, as well
as their synchronized versions, there exist fixed LTLf formulas for which they
remain PSPACE-hard, even for DFAs over constant-size alphabets (Theorem 4.2
and Theorem 4.4). Moreover, in all our complexity lower bounds in this paper,
we assume that the only atomic proposition which is true in a state is the
name of this state. Hence, the properties such as “the state $p$ belongs to a
set $S$” cannot be expressed by fixed LTLf formulas. The lower bounds in
Section 4 come from PSPACE-hardness of synchronization with constraints on
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$,
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$,
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$ and
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$.

In Section 5, we close an open problem stated in [Wol20] and show that
synchronization with constraints on
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$ is NP-complete (Theorem 5.7).
We show a connection of this problem to (classical) LTLf model checking where
the formula contains only the until modality without nesting, which we prove
to be NP-hard (Theorem 5.8). The expressivity of LTLf formulas with limited
nesting of until operators is studied in [TW04].

##  2 Main definitions

A _complete deterministic finite semi-automaton_
$\mathcal{A}=(Q,\Sigma,\delta)$, which we simply call a DFA in this paper,
consists of the finite set $Q$ of states, the finite alphabet $\Sigma$, and
the transition function $\delta:Q\times\Sigma\to Q$. The transition function
$\delta$ is generalized to finite words in the usual way. It is further
generalized to sets of states $S\subseteq Q$ as
$\delta(S,w)=\\{\delta(q,w)\mid q\in S\\}$. We sometimes refer to
$\delta(S,w)$ as $S.w$. We often talk about active states. Given a set $S$ of
previously active states, we say that $q$ is active after the application of
$w$ if $q\in S.w$. We denote by $|S|$ the size of the set $S$. We might
identify singleton sets with their elements. If for some $w\in\Sigma^{*}$ and
a set of states $S\subseteq Q$, $|S.w|=1$, we say that the word $w$
_synchronizes_ the set $S$. Given a word $w$, we denote by $|w|$ the length of
$w$, by $w[i]$ the $i^{\text{th}}$ letter of $w$ (or the empty word $\epsilon$
if $i=0$) and by $w[i..j]$ the factor of $w$ from letter $i$ to letter $j$.
For a state $q$, we call the sequence of active states $q.w[1..i]$ for $0\leq
i\leq|w|$ the _path_ induced by $w$ starting at $q$. A _DFA acceptor_
$\mathcal{A}=(Q,\Sigma,\delta,i,F)$ is a DFA with a chosen initial state $i\in
Q$ and a set of final state $F\subseteq Q$. The _language accepted by_
$\mathcal{A}$ is the set of words $w$ such that $i.w\in F$.

Let $w\in\Sigma^{*}$ and $q\in Q$. We define
$\operatorname{paths}_{\mathcal{A}}(q,w)$ to be the path in $\mathcal{A}$
starting in $q$ and labeled by $w$. Given $S\subseteq Q$, define
$\operatorname{paths}_{\mathcal{A}}(S,w)=\cup_{q\in
S}\\{\operatorname{paths}_{\mathcal{A}}(q,w)\\}$. Define the _power-set
automaton_ $\mathcal{P}(\mathcal{A})=(2^{Q},\Sigma,\delta^{\prime})$ of
$\mathcal{A}$ as usually: the set of states of $\mathcal{P}(\mathcal{A})$ is
the set $2^{Q}$ of all subsets of $Q$, and the transition function is defined
as $\delta^{\prime}(S,a)=\\{\delta(q,a)\mid q\in S\\}$. We define
$\operatorname{sets}_{\mathcal{A}}(S,w)$ to be the single path in
$\mathcal{P}(\mathcal{A})$ starting in the state $S$ and labeled by $w$.

A _partial DFA_ is a DFA $\mathcal{A}=(Q,\Sigma,\delta)$ where the transition
function $\delta$ is allowed to be partial, that is, undefined for some input
values. Its extensions to $Q\times\Sigma^{*}$ and further to
$2^{Q}\times\Sigma^{*}$ are defined in the same way as for complete DFAs. We
say that a word $w$ _carefully synchronizes_ $S\subseteq Q$ if the action of
$w$ is defined for every state in $S$ and $|\delta(S,w)|=1$. If $w$ carefully
synchronizes $Q$, we say that it _carefully synhronizes_ $\mathcal{A}$, and
then call both $w$ and $\mathcal{A}$ _carefully synchronizing_.

The _underlying digraph_ of a DFA $\mathcal{A}$ is obtained by forgetting the
labels of transitions in $\mathcal{A}$. Given a digraph $G=(V,E)$, we call a
_path_ a sequence of vertices interleaved with edges

$\rho=v_{1}\xrightarrow[]{e_{1}}v_{2}\xrightarrow[]{e_{2}}\dots\xrightarrow[]{e_{n}}v_{n+1}$

such that $e_{i}=(v_{i},v_{i+1})$ for $1\leq i\leq n$. We emphasize that a
path can have repeating vertices. We say that a vertex $v$ is reachable from a
vertex $u$ if there exists a path from $u$ to $v$. The relation “$u$ and $v$
are reachable from each other” is an equivalence relation, and a class of this
relation is called a _maximal strongly connected component_. A maximal
strongly connected component is called a _sink_ if only vertices belonging to
it are reachable from its vertices. A digraph is called _strongly connected_
if every its vertex is reachable from every other vertex. A DFA is called
_strongly connected_ if its underlying digraph is strongly connected.

We expect the reader to be familiar with basic concepts of automata theory,
computational complexity and model checking, and refer to the textbooks
[Sip97] and [BK08] as a reference.

###  2.1 LTLf model checking

Let $P$ be a finite set, which we call the set of _atomic propositions_. The
_linear temporal logic on finite traces (LTL f)_ over $P$ is the set of
formulas defined inductively as follows. The symbol $\top$ representing the
constant true, and every element of $P$ are in LTLf. Moreover, if $\phi,\psi$
are in LTLf, then
$\neg\phi,\phi\lor\psi,\phi\land\psi,\mathrm{X}\phi,\phi\mathrel{{\mathrm{U}}}\psi,\mathrm{F}\phi,\mathrm{G}\phi$,
as well as all Boolean combinations of this formulas are in LTLf. The
operators $\mathrel{{\mathrm{U}}},\mathrm{X},\mathrm{F},\mathrm{G}$ stand for
until, next, finally and globally, and their semantics is the standard
semantics on finite traces [GV13, BFM23], which are in our setting paths in a
DFA. The size $|\phi|$ of the formula $\phi$ is the length of a bit string
encoding it.

We also consider restricted formulas of LTLf. Namely, given a modality $T$, we
denote by $\mathrm{L}^{+}(T)$ the set of LTLf formulas where negation is
allowed only in front of atomic propositions, and the only allowed modality is
$T$.

We defined the following problems.

######  Problem.

LTLf model checking on paths
Input: A DFA $\mathcal{A}=(Q,\Sigma,\delta)$ and an LTLf formula $\phi$ over
the set $P=Q$.
Output: Yes, if and only if there exists a word $w$ such that for every
$\pi\in\operatorname{paths}(Q,w)$ we have $\pi\models\phi$.

######  Problem.

LTLf model checking on sets
Input: A DFA $\mathcal{A}=(Q,\Sigma,\delta)$ and an LTLf formula $\phi$ over
the set $P=Q$.
Output: Yes, if and only if there exists a word $w$ such that for the path
$\pi=\operatorname{sets}(Q,w)$ we have $\pi\models\phi$.

The problems Synchronized LTLf model checking on paths (on sets) are defined
similarly with an additional requirement that $w$ must synchronize
$\mathcal{A}$. As discussed in Section 2.2, it is not necessarily the case
that an LTLf fomula which is true on paths is also true on sets, or vice
versa.

###  2.2 Traversal relations

We now describe different traversal relations $\mathrm{R}(w)$ which are
induced by the traversal of a word $w$ through the states of a DFA. The first
two relations are defined by the last visits of the states to each other,
while the third relation is defined by the connection between first and last
visits. Given a DFA $\mathcal{A}=(Q,\Sigma,\delta)$ and an arbitrary relation
$R\subseteq Q^{2}$ which we call a _constraint relation_ , we say that a
traversal relation $\mathrm{R}(w)$ _agrees_ with $R$ if and only if
$R\subseteq\mathrm{R}(w)$. We then consider the following problem for each
traversal relations $\mathrm{R}(w)$ introduced below.

######  Problem.

Constrained-$\mathrm{R}(w)$-Sync
Input: A DFA $\mathcal{A}=(Q,\Sigma,\delta)$ and a constraint relation
$R\subseteq Q^{2}$.
Output: Yes, if and only if there exists a word $w\in\Sigma^{*}$ such that
$R\subseteq\mathrm{R}(w)$ and $w$ synchronizes $\mathcal{A}$.

We also consider version of this problem where $w$ is not required to
synchronize $\mathcal{A}$. We call this variant
Constrained-$\mathrm{R}(w)$-Word. In [Wol20] and [BFM23], the problem
Constrained-$\mathrm{R}(w)$-Sync was called Sync-Under-$\lessdot_{w}$.

Given a DFA $\mathcal{A}=(Q,\Sigma,\delta)$, define
$\operatorname{first}(q,w,S)$ to be the minimum of the positions at which the
state $q$ appears as an active state over all paths induced by $w$ starting at
some state in $S$. Accordingly, let $\operatorname{last}(q,w,S)$ be the
maximum of those positions. Note that $\operatorname{first}(q,w,S)=0$ for all
states $q\in S$ and is strictly positive for $q\in Q\backslash S$. If $q$ does
not appear on a path induced by $w$ on $S$, we set
$\operatorname{first}(q,w,S):=+\infty$ and
$\operatorname{last}(q,w,S):=-\infty$. For any natural number $n$, we make
standard assumptions that $-\infty<n<+\infty$, and we also assume that
$-\infty\leq-\infty$, $+\infty\leq+\infty$, but the inequalities
$-\infty<-\infty$ or $+\infty<+\infty$ do not hold.

We remark that in [Wol20], the traversal relations $\mathrm{R}(w)$ (denoted
$\lessdot_{w}$ there) were called orders. However, in some cases they are not
transitive or reflective, and are thus not order relations. Instead, these
traversal relations describe the order in which $w$ traverses the DFA. The
traversal relations $\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}(w)$ and
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)$ defined below were
denoted as $\propto^{l<l}_{w@s}$ and $\propto^{l\leq l}_{w@s}$, and the
relations $\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(w)$,
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$ and
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}(w)$ were denoted there as
$\propto^{l<l}_{w@p}$, $\propto^{l\leq l}_{w@p}$ and $\propto^{l<f}_{w@p}$.
Finally, we mention that in [Wol20] the case where the configuration before
reading the first letter of the word is not included in the definitions of
$\operatorname{first}(q,w,S)$ and $\operatorname{last}(q,w,S)$ was also
considered. However, this variant does not change the complexity of the
problems that we consider, and hence we omit its discussion.

In the following definitions, let $\mathcal{A}=(Q,\Sigma,\delta)$ be a DFA and
let $p,q\in Q$ be two its distinct states. For all the traversal relations
defined below we do not include the pair $(p,p)$ for any $p\in Q$.

#### Traversal relations on sets.

Given a word $w\in\Sigma^{*}$, we define the following traversal relations
$\mathrm{R}(w)$:

$(p,q)\in\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}(w)\Leftrightarrow\operatorname{last}(p,w,Q)<\operatorname{last}(q,w,Q)\textmd{
(traversal relation $\ell<\ell$ on sets),}$
$(p,q)\in\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)\Leftrightarrow\operatorname{last}(p,w,Q)\leq\operatorname{last}(q,w,Q)\textmd{
(traversal relation $\ell\leq\ell$ on sets).}$

The second traversal relation differs from the first one in the sense that it
does not say that $q$ is active strictly after the moment when $p$ is active
for the last time, and instead they can disappear simultaneously. It is easy
to see that for any word $w$ we have
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}(w)\subseteq\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)$.

#### Traversal relations on paths.

So far, we only introduced traversal relations which are defined by the set of
active states as a whole. It did not matter which active state belongs to
which path and a state on a path $\tau$ could stand in a relation with a state
on some other path $\rho$. However, in most scenarios the fact that we start
with the active state set $Q$ only models the lack of knowledge about the
_actual_ current state, and in reality only one state $q$ is active at any
moment of time. Hence, any constraints on the ordering of traversed states
should apply to each path separately. Therefore, we introduce the variants of
the traversal relations above which are defined on paths rather than on series
of state sets:

$(p,q)\in\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(w)\Leftrightarrow\forall
r\in
Q\colon\operatorname{last}(p,w,\\{r\\})<\operatorname{last}(q,w,\\{r\\})\textmd{
(traversal relation $\ell<\ell$ on paths),}$
$(p,q)\in\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)\Leftrightarrow\forall
r\in
Q\colon\operatorname{last}(p,w,\\{r\\})\leq\operatorname{last}(q,w,\\{r\\})\textmd{
(traversal relation $\ell\leq\ell$ on paths).}$

The traversal relations $\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$ and
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ differ significantly. For
instance, for any pair
$(p,q)\in\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(w)$ every path labeled
by $w$ visits $q$, while for
$(p,q)\in\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$ a path labeled
by $w$ may not necessarily visit $q$ if it does not visit $p$ as well.
However, for any word $w$ we have
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(w)\subseteq\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$.

In a way, restricting the traversal relations described so far with a pair
$(p,q)$ in the constraint relation $R$ brings “positive” constraints on the
future transitions of a word, in the sense that the visit of a state $p$
demands for a later visit of the state $q$. For instance, opening the lid
demands closing the lid later in our example in the introduction. We now
introduce a traversal relation whose restrictions yield “negative”
constraints. The last kind of traversal relations demands for a pair of states
$(p,q)$ that the first visit of the state $q$ forbids any future visits of the
state $p$. Referring again to the example in the introduction, this might be
caused by the requirement to not turn the box after opening the lid. This
stands in contrast to the previous restrictions where we could make up for a
“forbidden” visit of the state $p$ by visiting $q$ again. The traversal
relation $\mathrm{R}^{\ell<f}$ will only be considered on paths, since the
corresponding definition on sets leads to the empty relation alreafy on the
state set $Q$. The definitions of $\mathrm{R^{\ell<f}_{\operatorname{paths}}}$
is as follows:

$(p,q)\in\mathrm{R^{\ell<f}_{\operatorname{paths}}}(w)\Leftrightarrow\forall
r\in
Q:\operatorname{last}(p,w,\\{r\\})<\operatorname{first}(q,w,\\{r\\})\textmd{
(traversal relation $\ell<f$ on paths).}$

Note that $\mathrm{R^{\ell<f}_{\operatorname{paths}}}$ is not transitive. For
example, for $R=\\{(p,q),(q,r)\\}$ a path is allowed to go from $r$ to $p$ if
it has not visited $q$.

There are very few connections between different introduced traversal
relations. For every DFA and every word $w$, besides the already mentioned
facts that
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}(w)\subseteq\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)$
and
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(w)\subseteq\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$,
we also have that
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}(w)\subseteq\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$.
No other inclusions hold true for every DFA and every $w$. Figure 2 provides
some examples on the differences between the behavior of various traversal
relations.

$p$$q$$r$$a$$a$$b,c$$b,d$$d$$c$$a,b,c,d$

| $\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$ | $\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ | $\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$ | $\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ | $\mathrm{R^{\ell<f}_{\operatorname{paths}}}$
---|---|---|---|---|---
$(p,q)\in\mathrm{R}(a)$ | ✗ | ✓ | ✗ | ✗ | ✗
$(p,q)\in\mathrm{R}(b)$ | ✗ | ✓ | ✗ | ✓ | ✓
$(p,q)\in\mathrm{R}(cd)$ | ✗ | ✗ | ✗ | ✓ | ✓
$(p,q)\in\mathrm{R}(dc)$ | ✓ | ✓ | ✗ | ✓ | ✓

Figure 2: Example of a DFA and a table showing which traversal relations
include the pair $(p,q).$

#### Connection to LTLf.

Take the set of states of $\mathcal{A}$ as the set of atomic propositions.
Then, for traversal relations on paths, each state on a path is labeled only
by itself, while for traversal relations on sets each state of
$\mathcal{P}(\mathcal{A})$ is labeled by all the states of $\mathcal{A}$ that
it includes. Then, all defined orders can be expressed in LTLf.

Indeed, let $R$ be the constraining relation, and let $(p,q)\in R$. Then for
$\mathrm{R}^{l\leq l}$ we take the formula $\mathrm{G}(p\to\mathrm{F}q)$,
since each occurrence of $p$ requires an occurrence of $q$ in the future. For
$\mathrm{R}^{l<l}$ we take $\mathrm{F}(q\land\mathrm{G}\neg p)$, since $q$
must occur at some point, and after the last of its occurrence, there must not
be any occurrence of $p$. Finally, for $\mathrm{R}^{l<f}$ we take
$\mathrm{G}(q\to\mathrm{G}\neg p)$, since after the first occurrence of $q$
there must be no occurrence of $p$. To combine the constraints induced by
multiple pairs in $R$, we take the conjunction of the corresponding formulas.

To express the fact that a word is synchronizing in LTLf, one can use the
following approaches. Pick any state $s$ in a sink maximal strongly connected
component of the DFA. On paths, it is enough to add the restriction
$\mathrm{F}\mathrm{G}s$. On sets, we can introduce an atomic proposition that
is true for all the states except $s$, and put $\mathrm{F}\neg s$ as a
restriction. We do not use either of these approaches, and instead add a
direct separate requirement of synchronizability to the problems, since this
allows us to get more precise results on the shape of formulas and the set of
atomic propositions. For all our complexity lower bounds we restrict to the
setting where the only atomic proposition that is true in a state is the name
of the state itself, thus strengthening the lower bounds in [BFM23], where the
same atomic proposition is allowed to be true in a set of states of non-
constant length.

##  3 Polynomial space upper bounds

#### Generic model checking algorithm.

In this section, we describe polynomial space algorithms for LTLf model
checking on paths (sets) and their synchronized versions. Synchronized LTLf
model checking on paths was proved to be in PSPACE in [BFM23]. While most of
the ideas are already present there, we need several tweaks of their
polynomial space algorithm, hence we choose to provide its brief description
in a way that is more convenient for our use. Then, we describe how to adapt
it to the three other problems defined in LABEL:subsec:\LTL{}-defs: LTLf model
checking on sets, LTLf model checking on paths, and Synchronized LTLf model
checking on sets. The main issue that the algorithm needs to overcome is that
the LTLf restrictions are defined on the product DFA (on paths) or the power-
set DFA (on sets), which are both of exponential size in terms of the input.
However, as we discuss, we do not have to construct them explicitly, and only
need to store one their state at a time.

The idea of the approach in [BFM23] is an extension of the classical automata-
based polynomial space algorithm for LTLf model checking. The main difference
is that the automaton defining the paths now has exponential size, and hence
has to be dealt with without constructing it. We provide only a brief
description of the algorithm of [BFM23], and we refer to the proof of Theorem
3 there for full details. We work in the following slightly more general
setting. Let $P$ be a set of atomic propositions and let
$\mathcal{C}=(Q_{\mathcal{C}},\Sigma,\delta_{\mathcal{C}},i,F)$ be a DFA
acceptor with a labelling function $L:Q_{\mathcal{C}}\to 2^{P}$. We think of
$\mathcal{C}$ and $L$ as defined implicitly by a much smaller DFA
$\mathcal{A}$ provided in the input, the precise constructions will be
specified later. The requirements for this implicit specification are that the
transition function of $\mathcal{C}$ and the labeling function $L$ must be
computable in polynomial space in the size of $\mathcal{A}$. In particular,
this means that every state of $\mathcal{C}$ and the set of labels must be of
polynomial size in the size of $\mathcal{A}$.

Given $\mathcal{C}$ defined in such a way, and an LTLf formula $\phi$ over the
set $P$ of atomic propositions, we want to decide if there exists a word
accepted by $\mathcal{C}$ and satisfying $\phi$. Given $\mathcal{C}$ and
$\phi$, one can construct a non-deterministic finite automaton $\mathcal{D}$
with the following property: the language accepted by $\mathcal{D}$ is non-
empty if and only if there exists a word $w\in\Sigma^{*}$ accepted by
$\mathcal{C}$ such that the path labeled by it in $\mathcal{C}$ satisfies
$\phi$. To build $\mathcal{D}$, we first construct the automaton
$\mathcal{B}_{\phi}$ over the alphabet $2^{P}$ which recognizes the set of
finite traces of $\mathcal{C}$ satisfying $\phi$, and take the synchronized
product of $\mathcal{C}$ and $\mathcal{B}_{\phi}$ as $\mathcal{D}$, please
refer to the proof of Theorem 3 of [BFM23] for technical details. We only need
the fact that each state of $\mathcal{B}_{\phi}$ is of size polynomial in
$\phi$, and its transition function is computable in polynomial time. If
$\mathcal{C}$ satisfies the restrictions described in the previous paragraph,
then, by the construction of synchronized product, each state of $\mathcal{D}$
also has polynomial size and the transition function of $\mathcal{D}$ is
computable in polynomial space. To check that the language accepted by
$\mathcal{D}$ is non-empty in non-deterministic polynomial space, it is enough
to non-deterministically guess a word $w$ accepted by $\mathcal{D}$ letter by
letter. Observe that for each guess we do not need the whole automaton
$\mathcal{D}$ to be constructed explicitly, since we only need to maintain the
current state and then compute one of the states obtained by taking a
transition labeled by a guessed letter. By Savitch theorem [Sip97],
PSPACE$=$NPSPACE, and hence this can be done in deterministic polynomial
space.

#### Implicitly represented DFAs.

Let now $\mathcal{A}=(Q,\Sigma,\delta)$ and $\phi$ be the input of the
Synchronized LTLf model checking on paths problem, and let $|Q|=n$. Take
$\mathcal{C}$ to be the product of $n$ copies of $\mathcal{A}$. As the initial
state of $\mathcal{C}$, we take an arbitrary $n$-tuple with pairwise different
states. The set of accepting states of $\mathcal{C}$ consists of all the
$n$-tuples with the same state at each position. Such automaton recognizes the
set of synchronizing words of $\mathcal{A}$, and its transition function is
computable in polynomial time. As the set of labels, we take a separate label
$q_{i}^{(j)}$ for each state $q_{i}$ of the $j$th copy of $\mathcal{A}$. The
labeling function $L$ is then defined as
$L((q_{i_{1}},\ldots,q_{i_{n}}))=\\{q_{i_{1}}^{(1)},\ldots,q_{i_{n}}^{(n)}\\}$.
Finally, for each $j$, define $\phi_{j}$ to be $\phi$ where each state $q_{i}$
is substituted with $q_{i}^{(j)}$, and let $\phi^{\prime}$ be the conjunction
of all $\phi_{j}$. It is then easy to see that a word $w\in\Sigma^{*}$
accepted by $\mathcal{C}$ labels in it a path satisfying $\phi^{\prime}$ if
and only if for every $\pi\in\operatorname{paths}(Q,w)$ we have
$\pi\models\phi$. By using the algorithms described above, we get that
Synchronized model checking on path is in PSPACE, which was originally proved
in [BFM23].

We now discuss the modifications for other problems. First, we observe that if
we make all the states of $\mathcal{C}$ accepting in the above construction,
we get a polynomial space algorithm for LTLf model checking on paths.

######  Proposition 3.1.

LTLf model checking on paths and its synchronized version are in PSPACE.

Now, take $\mathcal{C}$ to be the power-set automaton
$\mathcal{P}(\mathcal{A})$. Take the set $Q$ of all the states of
$\mathcal{A}$ as the initial state of $\mathcal{P}(\mathcal{A})$, take $P=Q$
and define the labeling function $L$ as
$L(\\{q_{1},\ldots,q_{k}\\})=\\{q_{1},\ldots,q_{k}\\}$ for
$q_{1},\ldots,q_{k}\in Q$. By defining the set of accepting states of
$\mathcal{P}(\mathcal{A})$ as, respectively, the set $2^{Q}$ of all its
states, or the set of singletons, we get the following result.

######  Proposition 3.2.

LTLf model checking on sets and its synchronized version are in PSPACE.

In particular, as explained in Section 2.2, the constraints on all considered
traversal relations are expressible as LTLf formulas. Hence, we get a uniform
proof of Theorem 11 from [Wol20]. Moreover, this theorem is true for arbitrary
Boolean combination of constraints on different traversal relations.

######  Theorem 3.3 ([Wol20]).

For all traversal relations
$\mathrm{R}(w)\in\\{\mathrm{R^{\ell<\ell}_{\operatorname{sets}}},\mathrm{R^{\ell<\ell}_{\operatorname{paths}}},\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}},\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}},\mathrm{R^{\ell<f}_{\operatorname{paths}}}\\}$,
the problem Constrained-$\mathrm{R}(w)$-Sync is contained in PSPACE.

Moreover, the described algorithm can be easily adapted to require the word we
are looking for to have given rank, or bring the whole set of states to a
particular subset (or a family of subsets), or even come from a given fixed
regular language. It is also easy to see that all these restrictions can be
implemented in the setting where we are also given a subset $S\subseteq Q$ in
the input, and we need to check if there exists a word $w$ that for every
$\pi\in\operatorname{paths}(S,w)$ we have $\pi\models\phi$ (respectively, for
the path $\pi=\operatorname{sets}(S,w)$ we have $\pi\models\phi$). This word
$w$ can be additionally required to synchronize $S$, that is, to have
$|S.w|=1$. Finally, we remark that even if $\mathcal{A}$ is not deterministic,
without any changes, the described polynomial space algorithm still finds a
word satisfying the given LTLf constraints on paths or on sets.

##  4 PSPACE-complete constraints

In this section, we give two constructions which provide PSPACE-hardness for
most of the constraints that we introduced, one for traversal relations on
sets and one for traversal relations on paths. As discussed at the end of
Section 2.2, these constraints can be expressed by LTLf formulas, hence as a
consequence we get PSPACE-hardness of model checking on path and sets, as well
as of their synchronized versions.

###  4.1 Constraints on sets

We start with a reduction from the PSPACE-complete problem Careful Sync
[Mar12, Mar14] to
Constrained-$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$-Sync, and then
extend the construction to other traversal constraints.

######  Problem.

Careful Sync
Input: A partial DFA $\mathcal{A}=(Q,\Sigma,\delta)$.
Output: Yes, if and only if there exists a word $w\in\Sigma^{*}$, such that
$w$ is defined for all $q\in Q$ and $|Q.w|=1$.

######  Theorem 4.1.

Constrained-$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$-Sync and
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$-Sync are PSPACE-
complete, even for $|R|=1$ and $|\Sigma|=2$.
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$-Word is PSPACE-
complete, even for $|R|=2$ and $|\Sigma|=3$.

###### Proof.

Membership in PSPACE comes from Proposition 3.2 and the fact that constraints
on $\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ and
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$ can be expressed in LTLf. We
first show PSPACE-hardness of
Constrained-$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$-Sync. Let
$\mathcal{A}=(Q,\Sigma,\delta)$ be a partial DFA in the input of Careful Sync.
We construct a complete DFA
$\mathcal{A}^{\prime}=(Q^{\prime},\Sigma,\delta^{\prime})$ with
$Q^{\prime}=Q\cup\\{q_{\circleddash},r\\}$ such that $q_{\circleddash},r\notin
Q$. We define the constraint relation $R$ as $R=\\{(q_{\circleddash},r)\\}$.
The idea is to define the transition function of $\mathcal{A}^{\prime}$ so
that after reading any non-empty word, it is no longer possible to visit the
state $r$, and since $(q_{\circleddash},r)\in R$, it is also not possible to
visit $q_{\circleddash}$. We then define all the transitions undefined in
$\mathcal{A}$ to go to $q_{\circleddash}$ in $\mathcal{A}^{\prime}$. Thus we
get that for every word $w$ we have that
$\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)$ agrees with $R$ and $w$
is synchronizing for the $\mathcal{A}^{\prime}$ if and only if $w$ is
carefully synchronizing for the original automaton $\mathcal{A}$. See Figure 3
for an illustration.

Formally, the transition function $\delta^{\prime}$ is defined as follows. We
take $\delta^{\prime}(q,a)=\delta(q,a)$ for all the pairs $q\in Q,a\in\Sigma$
where $\delta$ is defined. For those pairs $(q,a)$ where $\delta$ is not
defined, we set $\delta^{\prime}(q,a)=q_{\circleddash}$. Further, fix some
arbitrary state $t\in Q$ and for all $a\in\Sigma$ set
$\delta^{\prime}(q_{\circleddash},a)=\delta^{\prime}(t,a)$ (note that this can
be the state $q_{\circleddash}$ itself) and
$\delta^{\prime}(r,a)=\delta^{\prime}(t,a)$.

$t$$\hat{t}$$s$$q_{\oplus}^{1}$$q_{\oplus}^{2}$$q_{\circleddash}$$r$$\hat{r}$$b$$b$$b$$a$$a$$a$$c$$c$$a,b$$a,b,c$$c$$c$$c$
Figure 3: Illustration of the constructions in the proof of Theorem 4.1. The
construction for $\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}$ is depicted
by solid lines, its extension to
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$ by dotted lines, and the
further extension to drop the synchronizability requirement by dashed lines.
For every state $q$ except $q_{\circleddash}$, we have a dotted state
$\hat{q}$, some of them are omitted in the picture for simplicity. Unmarked
states and transitions are only drawn for illustrative purposes and their
labels do not matter for the proof.

Assume that there exists a word $w\in\Sigma^{*}$, $|w|=n$, such that for all
states $q\in Q$, $\delta(q,w)$ is defined, and $|\delta(Q,w)|=1$. In
particular, $\delta(q,w[1])$ is defined for all states $q\in Q$. Let us
consider how the letter $w[1]$ acts on the states of $\mathcal{A}^{\prime}$.
First,
$\delta^{\prime}(r,w[1])=\delta^{\prime}(q_{\circleddash},w[1])=\delta(t,w[1])$,
and $\delta(t,w[1])$ is defined by our assumption. Second,
$\delta^{\prime}(Q,w[1])\subseteq Q$ since $\delta(q,w[1])$ is defined for all
states $q\in Q$. Hence, $\delta^{\prime}(Q^{\prime},w[1])\subseteq Q$.
Furthermore, by construction of $\delta^{\prime}$, we have
$\delta^{\prime}(Q^{\prime},w[1])=\delta(Q,w[1])$. Let $w=w[1]w^{\prime}$. By
our assumption, $\delta(q,w^{\prime})$ is defined for every
$q\in\delta(Q,w[1])$, and by construction
$\delta^{\prime}(q,w^{\prime})=\delta^{\prime}(q,w^{\prime})$ for every
$q\in\delta(Q,w[1])$. In particular, this means that while reading
$w^{\prime}$ in $\mathcal{A}^{\prime}$ starting from the states in
$\delta^{\prime}(Q^{\prime},w[1])$, the state $q_{\circleddash}$ is not
visited, and $\delta^{\prime}(Q^{\prime},w)=\delta(Q,w)$. Therefore, $w$ also
synchronizes the automaton $\mathcal{A}^{\prime}$. The state
$q_{\circleddash}$ is only active in the start configuration where no letter
of $w$ is read yet, and after that it is not active anymore while reading $w$.
The same is true for $r$, hence $R=\\{(q_{\circleddash},r)\\}\subseteq\
\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)$.

In the opposite direction, assume there exists a word $w\in\Sigma^{*}$,
$|w|=n$, that synchronizes $\mathcal{A}^{\prime}$ with
$(q_{\circleddash},r)\in\mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)$.
The only position of $w$ in which $r$ is active in $\mathcal{A}^{\prime}$ due
to the definition of $\delta^{\prime}$ is before any letter of $w$ is read. As
$(q_{\circleddash},r)\in\ \mathrm{R^{\ell\leq\ell}_{\operatorname{sets}}}(w)$,
it holds for all $i$, $1\leq i\leq n$, that
$q_{\circleddash}\notin\delta^{\prime}(Q^{\prime},w[1..i])$. Hence,
$\delta^{\prime}(q,w)$ is defined for every state $q\in Q$. Since
$\delta^{\prime}$ and $\delta$ agree on the definition range of $\delta$, it
follows that $w$ also synchronizes the state set $Q$ in $\mathcal{A}$ without
using an undefined transition.

To adapt the construction for $\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$,
we introduce a copy $\hat{q}$ of every state $q\in Q\cup\\{r\\}$ and set
$\delta^{\prime}(\hat{q},a)=q$ for every $a\in\Sigma$, $q\in Q\cup\\{r\\}$. We
keep $R=\\{(q_{\circleddash},r)\\}$. Since for any word $w\in\Sigma^{*}$ with
$|w|\geq 2$, we have that $r$ is no longer active after reading $w[2]$, in
order for $\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}(w)$ to agree with $R$,
the state $q_{\circleddash}$ needs to never be active after reading $w[1]$ in
$w$. Note that the state $q_{\circleddash}$ was not copied.

Denote the modified DFA (used for
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$) as $\mathcal{A}^{\prime}$
again. To show that
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$-Word is PSPACE-
complete, we further modify this construction so that the requirement on the
word to be synchronizing for $\mathcal{A}^{\prime}$ can be dropped. Add a new
letter $c$ to the alphabet $\Sigma$, and add two new states
$q^{1}_{\oplus},q^{2}_{\oplus}$ to $Q^{\prime}$. Observe that if $\mathcal{A}$
is carefully synchronizing, then every carefully synchronizing word maps all
the states of $\mathcal{A}$ to the same maximal strongly connected component
of the underlying digraph of $\mathcal{A}$. More generally, if $\mathcal{A}$
is carefully synchronizing, then the underlying digraph of $\mathcal{A}$ can
only contain one maximal strongly connected component $C\subseteq Q$ that is a
sink. For the sake of contradiction, assume that the underlying digraph of
$\mathcal{A}$ contains two maximal strongly connected components $C_{1}$ and
$C_{2}$ that are both sinks. Then, no word can synchronize the set $C_{1}\cup
C_{2}$ as no state outside of $C_{1}\cup C_{2}$ is reachable from any state in
$C_{1}\cup C_{2}$, and the states in $C_{1}$ cannot be mapped into $C_{2}$ and
vice versa. Observe that for a digraph, all the maximal strongly connected
components that are sinks can be found in polynomial time.

Let $C$ be the single maximal strongly connected component of $\mathcal{A}$
that is a sink. Pick a state $s$ in this component. Define all the letters in
$\Sigma$ to act as the identity on $q^{1}_{\oplus}$ and $q^{2}_{\oplus}$.
Furthermore, define $\delta^{\prime}(s,c)=q^{1}_{\oplus}$,
$\delta^{\prime}(q^{1}_{\oplus},c)=q^{2}_{\oplus}$,
$\delta^{\prime}(q^{2}_{\oplus},c)=q^{2}_{\oplus}$ and
$\delta^{\prime}(q,c)=q_{\circleddash}$ for all $q\in
Q^{\prime}\setminus\\{s,q^{1}_{\oplus},q^{2}_{\oplus}\\}$. Define
$R^{\prime}=R\cup\\{(q^{1}_{\oplus},q^{2}_{\oplus})\\}$. As shown above, if
$R^{\prime}$ is respected, the state $q_{\circleddash}$ is never active after
reading the first letter of any word. Observe that since
$(r,q_{\circleddash})\in R^{\prime}$, letter $c$ cannot be applied if any
state in $Q^{\prime}$ other than $s$ is active. However, it has to be applied
since $(q^{1}_{\oplus},q^{2}_{\oplus})\in R^{\prime}$, and applying any letter
in $\Sigma$ preserves the fact that both $q^{1}_{\oplus}$ and $q^{2}_{\oplus}$
are active. Hence, for a word $w\in\Sigma^{*}$,
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}(wcc)$ agrees with $R^{\prime}$
if and only if $w$ is synchronizing for $\mathcal{A}^{\prime}$ and
$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}(wcc)$ agrees with $R$. Hence, we
proved that Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{sets}}}$-Word is
PSPACE-complete. ∎

Together with Proposition 3.2, we get the following.

######  Theorem 4.2.

Model checking on sets and its synchronized version are PSPACE-complete, even
for a fixed LTLf formula and a DFA over constant-size alphabet.

An example of a fixed formula for which Model checking on sets is PSPACE-
complete is $\mathrm{G}(q_{1}\to\mathrm{F}q_{2})$. For Synchronized model
checking on sets an example of such a formula is
$\mathrm{G}(q_{1}\to\mathrm{F}q_{2})\land\mathrm{G}(q_{3}\to\mathrm{F}q_{4})$.

###  4.2 Constraints on paths

Observe that $\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ and
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$ express similar properties: in
both cases, if $(p,q)\in R$, then every path visiting $p$ must visit $q$
later. This allows us to use almost the same construction to show PSPACE-
hardness for both of them. For
Constrained-$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$-Sync, this was
already proved in [BFM23], but the alphabet in their construction grows with
the number of states of the DFA. We show, in particular, that for constant-
size alphabet this problem remains PSPACE-hard.

######  Theorem 4.3.

Constrained-$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$-Sync,
Constrained-$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$-Sync and
Constrained-$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$-Word are
PSPACE-complete, even over a constant-size alphabet.

###### Proof.

Membership in PSPACE comes from Proposition 3.1 and the fact that constraints
on $\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$ and
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}$ can be expressed in LTLf. To show
PSPACE-hardness, we reduce from the Finite Automata Intersection problem,
which is PSPACE-complete, even for binary alphabets [Koz77].

######  Problem.

Finite Automata Intersection
Input: A set of $m$ DFA acceptors
$\mathcal{A}_{i}=(Q_{i},\Sigma,\delta_{i},s_{i},F_{i}),1\leq i\leq m$.
Output: Yes, if and only if there exists a word in $\Sigma^{*}$ which is
accepted by all $\mathcal{A}_{i},1\leq i\leq m$.

The idea is as follows. We construct a single DFA which is a union of all the
DFA acceptors together with three new states $y,n,f$. We add a letter $r$
which makes only the initial state of each DFA acceptor active. Then, the
synchronizability requirement will force all these initial states to be
brought to the same state $f$ by a new letter $t$, and the constraints on
traversal relations will force them to go through the state $y$ instead of $n$
on the way to $f$, thus guaranteeing that every synchronizing word satisfying
the constraints corresponds to a word accepted by every DFA acceptor.

Formally, given an instance of Finite Automata Intersection, we construct the
following DFA $\mathcal{B}=(Q^{\prime},\Sigma\cup\\{r,t\\},\delta^{\prime})$.
We take $Q^{\prime}=\cup_{i=1}^{m}Q_{i}\cup\\{y,n,f\\}$. For each $1\leq i\leq
m$, we define $\delta^{\prime}(q,a)=\delta_{i}(q,a)$ for all $q\in Q_{i}$,
$a\in\Sigma$. For the states $y,n,f$ we set every letter of $\Sigma$ to induce
a self-loop. It remains to define $\delta^{\prime}$ for the new letters $r$
and $t$. For each $1\leq i\leq m$, the letter $r$ sends all the states in
$Q_{i}$ to $s_{i}$, and the letter $t$ takes all the states in $F_{i}$ to $y$,
all the states in $Q_{i}\setminus F_{i}$ to $n$, and sends the states $n$ and
$y$ to $f$. All yet unspecified transitions induce self-loops. The part of the
constructed DFA corresponding to $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ is
depicted in Figure 4 (note that the states $y,n,f$ are shared by all such
gadgets).

$s_{1}$$n$$y$$f$$F_{1}$$Q_{1}$$\ldots$$Q_{2}$rr$t$$t$$t$$t$$\Sigma\cup\\{r,t\\}$$r$$t$$t$
Figure 4: Illustration of the construction in the proof of Theorem 4.3.

Finally, we take $R_{1}=\\{(s_{i},y)\mid 1\leq i\leq m\\}$ and
$R_{2}=\\{(n,s_{i})\mid 1\leq i\leq m\\}$. We claim that there exists a
synchronizing word $w$ for $\mathcal{B}$ such that
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$ (respectively,
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}(w)$) agrees with $R_{1}$
(respectively, $R_{2}$) if and only if all the DFAs
$\mathcal{A}_{1},\ldots,\mathcal{A}_{m}$ accept the same word.

In one direction, if there is a word $w$ accepted by
$\mathcal{A}_{1},\ldots,\mathcal{A}_{m}$, then $rwtt$ is a synchronizing word
for $\mathcal{B}$ such that
$R_{1}\subseteq\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(rwtt)$ and
$R_{2}\subseteq\mathrm{R^{\ell<f}_{\operatorname{paths}}}(rwtt)$. Indeed,
since for each $1\leq i\leq m$ the word $w$ is accepted by $\mathcal{A}_{i}$,
we have that $\delta(q,rwt)=y$ for each $q\in Q_{i}$. After that, the
application of $t$ sends $y$ to $f$ without visiting $n$. Hence, for each
$1\leq i\leq m$ the path labeled by $rwtt$ and staring in $s_{i}$ visits $y$
and then ends in $f$, so it visits $y$ for the last time after its last visit
of $s_{i}$. Hence $rwtt$ is a synchronizing word such that
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(rwtt)$ agrees with $R_{1}$.
Moreover, such path never visits $n$ and hence
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}(rwtt)$ agrees with $R_{2}$.

In the other direction, assume that $w$ is a synchronizing word for
$\mathcal{B}$ such that $\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$
(respectively, $\mathrm{R^{\ell<f}_{\operatorname{paths}}}(w)$) agrees with
$R_{1}$ (respectively, with $R_{2}$). By construction of $\mathcal{B}$, since
$w$ is synchronizing, for each $1\leq i\leq m$ the word $w$ sends $s_{i}$ to
$f$, as $f$ is a sink. Observe that the word $w$ must contain at least one
occurrence of $t$. Take $w=w_{1}tw_{2}$, where $w_{1}$ does not contain any
occurrences of $t$. If $w_{1}$ contains at least one occurrence of $r$, let
$w=w_{3}rw_{4}$, where $w_{4}$ does not contain any occurrences of $r$.
Otherwise, take $w_{4}=w_{1}$. Since
$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$ (respectively,
$\mathrm{R^{\ell<f}_{\operatorname{paths}}}(w)$) agrees with $R_{1}$
(respectively, $R_{2}$), for each $1\leq i\leq m$ the word $w_{4}$ must map
$s_{i}$ to $y$, because otherwise the path labelled by $w$ starting at $s_{i}$
would visit $n$ instead of $y$, and the states $y$ and $n$ cannot be visited
by the same path in $\mathcal{B}$. Hence, the word $w_{4}$ maps the initial
state of each $\mathcal{A}_{i}$, $1\leq i\leq m$, to its final state, and thus
it is accepted by each DFA acceptor.

The constraint relation $R_{1}$ can be extended to force $w$ to be
synchronizing. Indeed, add the pairs $(p,f)$ for all states $p\in
Q^{\prime}\setminus\\{f\\}$ to $R_{1}$. It is easy to see that in this case
every word $w$ such that $\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}(w)$
agrees with $R_{1}$ is synchronizing. Hence,
Constrained-$\mathrm{R^{\ell\leq\ell}_{\operatorname{paths}}}$-Word is also
PSPACE-complete. ∎

Finally, the same arguments as in the proof of Theorem 4.3 show that
satisfying the LTLf formula $\mathrm{F}f\land((\neg n\land\neg
f)\to\mathrm{F}y)$ is equivalent to the requirement for a word to be accepted
by all the DFA acceptors. This is also true for every synchronizing word
satisfying $\neg n\to\mathrm{G}\neg n$. Hence, together with Proposition 3.1,
we get the following.

######  Theorem 4.4.

LTLf model checking on paths and its synchronized version are PSPACE-complete,
even for a fixed $\mathrm{L}^{+}(\mathrm{F})$ LTLf formula. Synchronized LTLf
model checking on paths is also PSPACE-complete for a fixed
$\mathrm{L}^{+}(\mathrm{G})$ LTLf formula. All these complexity lower bounds
remain true even for DFAs over a constant-size alphabet.

##  5 NP-complete constraints

In this section, we prove NP-completeness of
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync, and explore
the connections of the traversal relation
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$ with (classical) LTLf model
checking. Let us describe the intuition of the proof. Observe that in
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync only last
visits of states matter, and for each $(p,q)\in R$ every path must visit $q$,
even if it does not visit $p$. Hence, in some sense not visiting $p$ does not
help with satisfying the restrictions. One can thus first find a synchronizing
word for the DFA, forcing the paths starting from every its state to end in a
particular state $f$, and then extend this word to satisfy all the
restrictions on the order of last visits starting only from $f$. The latter is
captured by a graph-theoretic problem Last-Visits Traversal. To show that this
problem is NP-complete, and hence
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync is NP-
complete too, we look at the equivalent First-Visits Traversal problem, which
is obtained by reversing all transitions and all restrictions of Last-Visits
Traversal. This problem has a more intuitive nature, since now we are dealing
with first visits of states, so it is more easier to control at every moment
of time which states can already be visited, and which cannot yet be visited.

We start by formally defining Last-Visits Traversal and relating it to
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync. This idea
was already present in [Wol20].

######  Problem.

Last-Visits Traversal
Input: A digraph $G=(V,E)$ and a relation $R\subseteq V\times V$.
Output: Does there exist a path in $G$ such that for each $(v,u)\in R$

  * •

this path visits $u$,

  * •

and if it also visits $v$, then it must visit $u$ after the last time it
visits $v$?

######  Lemma 5.1.

The problem Last-Visits Traversal for strongly connected digraphs can be
reduced in polynomial time to
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync for strongly
connected synchronizing DFAs.

###### Proof.

Given an instance of Last-Visits Traversal, construct the following DFA
$\mathcal{A}=(Q,\Sigma,\delta)$. Take $Q=V$, and take $\Sigma$ large enough to
define $\delta$ in such a way that $G$ is the underlying digraph of
$\mathcal{A}$ (by possibly duplicating some edges of $G$ to ensure that the
outdegrees of all the vertices are equal). Since $G$ is strongly connected, it
has a subgraph $T$ on the whole set $V$ of its vertices such that $T$ is an
oriented tree directed towards its root $r$. Add a fresh letter $s$ to
$\Sigma$ and define its action according to the edges in $T$, and make it act
induce a self-loop for $r$.

Since $G$ is strongly connected, thus obtained automaton $\mathcal{A}$ is also
strongly connected. It is also synchronizing, since the word $s^{|Q|}$ is
synchronizing for it. We claim that there exists a path satisfying the
requirements of Last-Visits Traversal if and only if there exists a
synchronizing word $w$ for $\mathcal{A}$ such that
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(w)$ agrees with $R$.

Indeed, if $w$ is a synchronizing word for $\mathcal{A}$ such that
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(w)$ agrees with $R$, then it is
enough to take the path labelled by $w$ and starting in an arbitrary state of
$\mathcal{A}$. Since for every transition from a state $q$ to a state
$q^{\prime}$ in $\mathcal{A}$ there is an edge $(q,q^{\prime})$ in $G$, this
path satisfies all the restrictions of Last-Visits Traversal. In the other
direction, consider a path $\rho$ in $G$ satisfying all the restrictions of
Last-Visits Traversal. For each edge $(q,q^{\prime})$ of this path, there is a
transition from $q$ to $q^{\prime}$ in $\mathcal{A}$. By concatenating all the
letters labelling these transitions in the order of how they appear along the
path, we obtain a word $w^{\prime}$. Let $w$ be a synchronizing word for
$\mathcal{A}$ mapping all its states the starting state of $\rho$. Since
$\mathcal{A}$ is strongly connected, such a word exists. Then $ww^{\prime}$ is
a synchronizing word for $\mathcal{A}$ such that
$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}(ww^{\prime})$ agrees with $R$.
∎

To show that Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync
is in NP, we will also need a reduction in the opposite direction.

######  Lemma 5.2.

The problem Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync
can be reduced in polynomial time to Last-Visits Traversal for strongly
connected digraphs.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,\delta)$ and $R\subseteq Q\times Q$ be the input of
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync. First, we
can assume that $\mathcal{A}$ is synchronizing, since it can be checked in
polynomial time [Vol08]. We can also assume that $R$ is non-empty. Observe
that for every $(p,q)\in R$, the path starting in every state of $\mathcal{A}$
must visit $q$. Hence, $q$ must be reachable from every state of
$\mathcal{A}$, so the underlying digraph of $\mathcal{A}$ can have only one
maximal strongly connected component $C$ that is a sink, and this component
must contain all the states occurring as second elements in the pairs in $R$.
Let $w_{1}$ be a synchronizing word for $\mathcal{A}$. This word necessarily
sends all the states to a state in $C$, call this state $f$.

We take the underlying digraph of $C$ and the restriction of $R$ to its set of
vertices as the input of Last-Visits Traversal. Assume that there exists a
required path $\rho$ for this problem, and let $g$ be the vertex where it
begins. Let further $w_{2}$ be a word mapping $f$ to $g$, and $w_{3}$ be a
word labeling the path $\rho$ in $\mathcal{A}$. Then the word
$w_{1}w_{2}w_{3}$ is clearly a required word for
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync. In the other
direction, if there exists a word $w$ required in
Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync, then the
path labeled by $w$ and starting in any vertex of $C$ satisfies the conditions
of Last-Visits Traversal. ∎

To prove that Last-Visits Traversal is NP-complete, we consider a polynomially
equivalent problem First-Visits Traversal. This problem is obtained by simply
reversing all the edges of the digraph and changing all requirements for the
required path accordingly. In other words, it is obtained by looking at the
path in the reversed order, from the end to the beginning.

######  Problem.

First-Visits Traversal
Input: A digraph $G=(V,E)$ and a relation $R\subseteq V\times V$.
Output: Yes, if and only if there exist a path in $G$ such that for every
$(u,v)\in R$

  * •

this path visits $u$,

  * •

and if it also visits $v$, then it must visit $u$ before visiting $v$.

######  Proposition 5.3.

In the First-Visits Traversal problem, if there exists a required path, then
there is such a path of length at most $(|V|-1)^{2}$.

###### Proof.

Let $\rho$ be a shortest path with the required properties. Let $S$ be the set
of vertices $u$ such that for some vertex $v$ we have $(u,v)\in R$. Then $S$
is the set of vertices this path must visit. Assume that $\rho$ visits for the
first time the vertices in $S$ in the order $v_{1},v_{2},\ldots,v_{|S|}$.
Represent $\rho$ as a concatenation of path $\rho_{i}$, $1\leq i\leq|S|-1$, so
that $\rho_{i}$ is the segment of $\rho$ between the first visit of $v_{i}$
and the first visit of $v_{i+1}$. We then can assume that for each $i$ the
path $\rho_{i}$ does not have any cycles, since removing such cycles does not
decrease the set of vertices $\rho$ can visit in the future. Hence, $\rho$ is
a concatenation of at most $|V|-1$ paths in $G$ containing no cycles, and so
its length is at most $(|V|-1)^{2}$. ∎

######  Corollary 5.4.

First-Visits Traversal is in NP.

If for each vertex $v$ there is at most one vertex $u$ with $(u,v)\in R$
(which will be the case in the construction in the proof of Proposition 5.5),
First-Visits Traversal has the following natural interpretation. By visiting a
vertex $u$, we “unlock” all vertices $v$ such that $(u,v)\in R$, which are not
allowed to be visited before $u$. Hence, the problem asks if, starting from
some vertex, it is possible to visit a given set of vertices (defined as
$\\{u\mid\text{ there is }v\text{ such that }(u,v)\in R\\}$) in a graph where
more and more vertices become available for visiting every time a new vertex
in $S$ is visited. The proof of the following proposition uses this intuition.

######  Proposition 5.5.

The problem First-Visits Traversal is NP-hard for strongly connected digraphs.

###### Proof.

We reduce from the NP-compete CNF-SAT problem [Kar72].

######  Problem.

CNF-SAT
Input: A set $C=\\{c_{1},\ldots,c_{m}\\}$ of clauses over Boolean variables
$x_{1},\ldots,x_{n}$.
Output: Does there exist an assignment which satisfies all the clauses?

The intuition behind the reduction is as follows, see Example 5.6 and Figure 5
for an illustration. With the traversal constraints, we force the path to
start in the leftmost vertex. Then, in the left half of Figure 5, every choice
of a vertex corresponds to assigning the value $0$ or $1$ to a variable. The
right half of Figure 5 corresponds to the clauses of the CNF-SAT formula. With
the traversal constraints, we make sure that the vertex $c^{\prime}_{i}$
corresponding to a clause $c_{i}$ can be reached if and only if the picked
value of at least one of the variables in $c_{i-1}$ satisfies the clause
$c_{i-1}$. In this case, the path can visit the vertex corresponding to this
occurrence and proceed to the next clause. The same is true for $f_{1}$ and
$c^{\prime}_{m}$. After reaching the vertex $f_{1}$ in Figure 5, the path
visits the vertices in the leftmost half that assign the values to the
variables that are opposite to the values picked at the beginning.

Formally, given an instance of CNF-SAT, we construct the following graph
$G=(V,E)$. For each variable $x_{i}$, $1\leq i\leq n$, we add three vertices
$x^{\prime}_{i},x_{i}^{0},x_{i}^{1}$ to $V$. For $1\leq i\leq n-1$, we add to
$E$ the edges

$(x^{\prime}_{i},x_{i}^{0}),(x^{\prime}_{i},x_{i}^{1}),(x_{i}^{0},x^{\prime}_{i+1}),(x_{i}^{1},x^{\prime}_{i+1}).$

For each clause $c_{j}$, $1\leq j\leq m$, we add a set of vertices
$\\{c^{\prime}_{j}\\}\cup\\{c_{j}^{k}\mid x_{k}\in c_{j}\text{ or
}\overline{x_{k}}\in c_{j}\\}$ to $V$. For each $j$, $1\leq j\leq m-1$, we add
to $E$ the edges

$\\{(c^{\prime}_{j},c_{j}^{k})\mid x_{k}\in c_{j}\text{ or
}\overline{x_{k}}\in c_{j}\\}\cup\\{(c_{j}^{k},c^{\prime}_{j+1})\mid x_{k}\in
c_{j}\text{ or }\overline{x_{k}}\in c_{j}\\}.$

We add to $V$ new vertices $f_{1},f_{2}$. Finally, we add to $E$ the edges

$(x_{n}^{0},c^{\prime}_{1}),(x_{n}^{1},c^{\prime}_{1}),\\{(c_{m}^{k},f_{1})\mid
x_{k}\in c_{j}\text{ or }\overline{x_{k}}\in
c_{j}\\},(f_{1},f_{2}),(f_{2},x^{\prime}_{1}),$

and observe that thus constructed digraph $G$ is strongly connected.

The relation $R$ is constructed as follows. For each clause $c_{j}$, we add to
$R$ the pair $(x_{i}^{1},c^{i}_{j})$ if $x_{i}$ occurs in $c_{j}$, and the
pair $(x_{i}^{0},c^{i}_{j})$ if $\overline{x_{i}}$ occurs in $c_{j}$. We also
add the pairs $(x^{\prime}_{1},f_{1})$ and $(f_{1},f_{2})$ to $R$. Example 5.6
below illustrates this construction. We claim that there exists a path in $G$
satisfying the constraints $R$ if and only if the input of the CNF-SAT problem
has a satisfying assignment.

In one direction, let $a_{1},\ldots,a_{n}\in\\{0,1\\}$ be an assignment
satisfying $C$. Consider the path
$\rho_{1}=x^{\prime}_{1},x_{1}^{a_{1}},x^{\prime}_{2},x_{2}^{a_{2}},x^{\prime}_{3},\ldots,x^{\prime}_{n},x_{n}^{a_{n}}$.
By construction of $R$, $c_{j}^{k}$ can be visited only after $x_{k}^{h}$ is
visited, where $h=0$ if $\overline{x_{k}}\in c_{j}$, and $h=1$ if $x_{k}\in
c_{j}$. Hence, since $a_{1},\ldots,a_{n}$ satisfies $C$, any path starting
with $\rho_{1}$ has now, for each $1\leq j\leq m$, at least one vertex
$c_{j}^{k}$ that it can visit. Let $\rho_{2}$ be such a path starting in
$c^{\prime}_{1}$ and ending in $f_{2}$. It now remains to complete
$\rho_{1}\rho_{2}$ with a path $\rho_{3}$ starting in $x^{\prime}_{1}$ that
visits the vertices $x_{i}^{h_{i}}$, $1\leq i\leq n$ and $h_{i}\in\\{0,1\\}$,
that were not visited by $\rho_{1}\rho_{2}$. The path
$\rho_{1}\rho_{2}\rho_{3}$ then satisfies the requirements of First-Visits
Traversal.

In the other direction, let $\rho$ be a path in $G$ which satisfies the
requirements of First-Visits Traversal. Since $(f_{1},f_{2})\in R$, state
$f_{1}$ must be visited, but since $(x^{\prime}_{1},f_{1})\in R$,
$x^{\prime}_{1}$ must be visited first. This means that $\rho$ must start in
$x^{\prime}_{1}$, since otherwise it is not possible to visit $x^{\prime}_{1}$
before $f_{1}$. Let $\rho_{1}\rho_{2}$ be the prefix of $\rho$ such that
$\rho_{1}$ ends in $x_{n}^{h}$ for $h\in\\{0,1\\}$ and does not visit
$c^{\prime}_{1}$, and $\rho_{2}$ starts in $c^{\prime}_{1}$, ends in $f_{1}$
and does not visit $f_{2}$. For each $j$, $1\leq j\leq m$, the path $\rho_{2}$
must visit one of the vertices $c_{j}^{k}$. By construction of $R$, this means
that $\rho_{1}$ must first visit the vertex $x_{k}^{1}$ if $x_{k}\in c_{j}$,
and $x_{k}^{0}$ if $\overline{x_{k}}\in c_{j}$. For $1\leq i\leq n$, take
$a_{i}=0$ if $\rho_{1}$ visits $x_{i}^{0}$, and $a_{i}=1$ if $\rho_{1}$ visits
$x_{i}^{1}$. We get that $a_{1},\ldots,a_{n}$ is a satisfying assignment for
the input of CNF-SAT. ∎

$x^{\prime}_{1}$$x_{1}^{0}$$x_{1}^{1}$$x^{\prime}_{2}$$x_{2}^{0}$$x_{2}^{1}$$c^{\prime}_{1}$$c_{1}^{1}$$c_{1}^{2}$$c^{\prime}_{2}$$c_{2}^{1}$$c_{2}^{2}$$f_{1}$$f_{2}$
Figure 5: Illustration for Example 5.6.

######  Example 5.6.

Consider the CNF formula $(\overline{x}_{1}\lor
x_{2})\land(x_{1}\lor\overline{x}_{2})$. The digraph from the reduction in the
proof of Proposition 5.5 is depicted in Figure 5. The set $R$ consists of the
following pairs:

$(x_{1}^{0},c_{1}^{1}),(x_{2}^{1},c_{1}^{2}),(x_{1}^{1},c_{2}^{1}),(x_{2}^{0},c_{2}^{2}),(x^{\prime}_{1},f_{1}),(f_{1},f_{2}).$

The path $\rho_{1}\rho_{2}$ corresponding to the assignment $x_{1}=0,x_{2}=0$
is depicted by dashed edges. To satisfy the conditions, the extension of
$\rho_{1}\rho_{2}$ must visit $x_{1}^{1}$ and $x_{2}^{1}$.

Since CNF-SAT remains NP-complete if every clause contains only three
literals, we get that the digraph in the proof of Proposition 5.5 has at most
three edges outgoing from each vertex. By combining Lemma 5.1, Lemma 5.2,
Corollary 5.4 and Proposition 5.5, we thus obtain the main result of this
section.

######  Theorem 5.7.

The problem Constrained-$\mathrm{R^{\ell<\ell}_{\operatorname{paths}}}$-Sync
is NP-complete, even for strongly connected DFAs over a constant-size
alphabet.

Finally, observe that in First-Visits Traversal the requirement on the path
induced by $(u,v)\in R$ can be expressed in LTLf as $\neg
v\mathrel{{\mathrm{U}}}u$. The LTLf model checking problem can be stated as
follows. Given a digraph $G=(V,E)$ with a selected vertex $v$ and an LTLf
formula $\phi$ over the set of atomic propositions $V$, does there exist a
path in $G$ starting in $v$ that satisfies $\phi$? We get the following result
from Corollary 5.4 and Proposition 5.5.

######  Theorem 5.8.

LTLf model checking is NP-complete for strongly connected digraphs and
formulas which are conjunctions of formulas $\neg v\mathrel{{\mathrm{U}}}u$
with $u,v\in V$.

For formulas in $\mathrm{L}^{+}(\mathrel{{\mathrm{U}}})$, LTL model checking
is PSPACE-complete [Mar04], and hence it is PSPACE-complete for such formulas
in LTLf by the construction in the proof of Theorem 1 in [GV13]. Hence, our
much stronger constraints, including completely forbidding the nesting of
until operators, drop the complexity for
$\mathrm{L}^{+}(\mathrel{{\mathrm{U}}})$, but only to NP-complete.

##  6 Conclusions and open problems

In this paper, we considered the problems of finding a word $w$ labeling paths
satisfying a certain LTLf formula $\phi$ in a DFA $\mathcal{A}$. We
concentrated on two cases: paths labeled by $w$ and starting in every state of
$\mathcal{A}$, and the unique path in the power-set automaton of $\mathcal{A}$
labeled by $w$. We showed that both cases are solvable in polynomial space,
and remain PSPACE-complete even for very strong restrictions, e.g., for some
fixed formulas.

One of the most natural questions is to find cases where these problems become
tractable. This might be done by either considering a combination of
restrictions on the DFA and the formula, or by considering different
parameters and investigating the parameterized complexity of the problem. For
example, observe that no PSPACE lower bound in Section 4 works for strongly
connected DFAs. In combination with the requirement that the constraint
relation has constant size, this might lead to polynomial time solvability.

Another direction is to consider fragments of LTLf with limited modalities
(such as $\mathrm{L}^{+}(\mathrm{G})$) and limited nesting (such as the
fragment considered in Theorem 5.8). Section 4.2 provides such results for
model checking on paths with formulas from $\mathrm{L}^{+}(\mathrm{F})$ and
$\mathrm{L}^{+}(\mathrm{G})$, but for model checking on sets the effect of
such restrictions remains open.

Finally, there could be other natural ways to succinctly define DFAs. Section
3 provides necessary conditions to perform model checking for them in PSPACE,
but it would be interesting to find some general conditions when the
complexity of model checking over such succinctly defined DFAs drops below
PSPACE.

### Acknowledgements

We thank Antonio Di Stasio and Przemysław Wałȩga for useful remarks and
fruitful conversations. Andrew Ryzhikov is supported by the European Research
Council (ERC) under the European Union’s Horizon 2020 research and innovation
programme (Grant agreement No. 852769, ARiAT). Petra Wolf is supported by the
French ANR, project ANR-22-CE48-0001 (TEMPOGRAL).

## References

  * [AV04] Dimitry S. Ananichev and Mikhail V. Volkov.  Synchronizing monotonic automata.  Theoretical Computer Science, 327(3):225–239, 2004.
  * [BF80] J.A. Brzozowski and Faith E. Fich.  Languages of R-trivial monoids.  Journal of Computer and System Sciences, 20(1):32–49, 1980.
  * [BFM23] Nathalie Bertrand, Hugo Francon, and Nicolas Markey.  Synchronizing words under LTL constraints.  Information Processing Letters, 182:106392, 2023.
  * [BK08] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT press, 2008.
  * [BP16] Marie-Pierre Béal and Dominique Perrin.  Synchronised automata.  In Combinatorics, Words and Symbolic Dynamics, Encyclopedia of Mathematics and its Applications, pages 213–240. Cambridge University Press, 2016\.
  * [DGDMM14] Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali.  Reasoning on LTL on finite traces: Insensitivity to infiniteness.  In Carla E. Brodley and Peter Stone, editors, AAAI 2014, Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada, pages 1027–1033. AAAI Press, 2014.
  * [Epp90] David Eppstein.  Reset sequences for monotonic automata.  SIAM Journal on Computing, 19(3):500–510, 1990.
  * [FG18] Valeria Fionda and Gianluigi Greco.  LTL on finite and process traces: Complexity results and a practical reasoner.  Journal of Artificial Intelligence Research, 63:557–623, 2018.
  * [GV13] Giuseppe De Giacomo and Moshe Y. Vardi.  Linear temporal logic and linear dynamic logic on finite traces.  In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 854–860. IJCAI/AAAI, 2013.
  * [Kar72] Richard M. Karp.  Reducibility among combinatorial problems.  In Raymond E. Miller, James W. Thatcher, and Jean D. Bohlinger, editors, Complexity of Computer Computations: Proceedings of a symposium on the Complexity of Computer Computations, held March 20–22, 1972, pages 85–103. Springer US, Boston, MA, 1972.
  * [Koz77] Dexter Kozen.  Lower bounds for natural proof systems.  In FOCS 1977, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 254–266. IEEE Computer Society, 1977.
  * [KV21] Jarkko Kari and Mikhail V. Volkov.  Černý’s conjecture and the road colouring problem.  In Handbook of Automata Theory, pages 525–565. EMS Press, 2021\.
  * [LZP+14] Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He.  LTLf satisfiability checking.  In Torsten Schaub, Gerhard Friedrich, and Barry O’Sullivan, editors, ECAI 2014, Proceedings of 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), volume 263 of Frontiers in Artificial Intelligence and Applications, pages 513–518. IOS Press, 2014.
  * [Mar04] Nicolas Markey.  Past is for free: on the complexity of verifying linear temporal properties with past.  Acta Informatica, 40:431–458, 2004.
  * [Mar12] Pavel V. Martyugin.  Synchronization of automata with one undefined or ambiguous transition.  In Nelma Moreira and Rogério Reis, editors, Implementation and Application of Automata - 17th International Conference, CIAA 2012, Porto, Portugal, July 17-20, 2012. Proceedings, volume 7381 of Lecture Notes in Computer Science, pages 278–288. Springer, 2012.
  * [Mar14] Pavel Martyugin.  Computational complexity of certain problems related to carefully synchronizing words for partial automata and directing words for nondeterministic automata.  Theory of Computing Systems, 54(2):293–304, 2014.
  * [Nat86] Balas K. Natarajan.  An algorithmic approach to the automated design of parts orienters.  In 27th Annual Symposium on Foundations of Computer Science, Toronto, Canada, 27-29 October 1986, pages 132–142. IEEE Computer Society, 1986.
  * [Pnu77] Amir Pnueli.  The temporal logic of programs.  In FOCS 1977, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46–57. IEEE Computer Society, 1977.
  * [Pnu81] Amir Pnueli.  The temporal semantics of concurrent programs.  Theoretical Computer Science, 13(1):45–60, 1981.
  * [RS18] Andrew Ryzhikov and Anton Shemyakov.  Subset synchronization in monotonic automata.  Fundamenta Informaticae, 162(2-3):205–221, 2018.
  * [Ryz19] Andrew Ryzhikov.  Synchronization problems in automata without non-trivial cycles.  Theoretical Computer Science, 787:77–88, 2019.
  * [San04] Sven Sandberg.  Homing and synchronizing sequences.  In Model-Based Testing of Reactive Systems, Advanced Lectures, pages 5–33, 2004.
  * [Sip97] Michael Sipser.  Introduction to the Theory of Computation.  PWS Publishing Company, 1997.
  * [TV19] Bianca Truthe and Mikhail V. Volkov.  Essays to commemorate the 55th anniversary of the Černý conjecture.  Journal of Automata, Languages and Combinatorics, 24(2-4):119–386, 2019.
  * [TW04] Denis Thérien and Thomas Wilke.  Nesting until and since in linear temporal logic.  Theory of Computing Systems, 37(1):111–131, 2004.
  * [TY15] Uraz Cengiz Türker and Hüsnü Yenigün.  Complexities of some problems related to synchronizing, non-synchronizing and monotonic automata.  International Journal of Foundations of Computer Science, 26(1):99–122, 2015.
  * [Vol08] Mikhail V. Volkov.  Synchronizing automata and the Černý conjecture.  In Carlos Martín-Vide, Friedrich Otto, and Henning Fernau, editors, Language and Automata Theory and Applications, Second International Conference, LATA 2008, Tarragona, Spain, March 13-19, 2008. Revised Papers, volume 5196 of Lecture Notes in Computer Science, pages 11–27. Springer, 2008.
  * [Wol20] Petra Wolf.  Synchronization under dynamic constraints.  In Nitin Saxena and Sunil Simon, editors, Proceedings of the 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, December 14-18, 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference), volume 182 of LIPIcs, pages 58:1–58:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.