Nathalie Bertrand

Hugo Francon

Nicolas Markey

Synchronizing words under LTL constraints

Synchronizing a (deterministic, finite-state) automaton is the problem of finding a sequence of actions to be played in the automaton in order to end up in the same state independently of the starting state. We consider synchronization with LTL constraints on the executions leading to synchronization, extending the results of [Petra Wolf. Synchronization under dynamic constraints. FSTTCS'20] by showing that the problem is PSPACE-complete for LTL as well as for restricted fragments (involving only modality F or G), while it is NP-complete for constraints expressed using only modality X.

Introduction

Synchronizing an automaton. A synchronizing word for a deterministic finitestate automaton A is a finite word that always takes the automaton to the same state, independently of the state of A it starts from. When the automaton represents the behaviours of a computer system, a synchronizing word can be seen as a sequence of actions to perform on the system so as to take it to the same state (in a sense, to regain control) if we initially don't know which state it is in. yes no yes/no yes/no insert coin Example. Consider the coffee-vending machine whose behaviour is depicted in Fig. 1: it asks the user how much sugar they want, and whether they want milk; the user may insert coins at any time to get coffee with the last choices that have been recorded.

Unfortunately, the display is broken. You do not know what state the machine is in, but you want a coffee with milk and no sugar. By noticing that the sequence ⟨no, yes, no⟩ is a synchronizing word, always ending up in the milk state, you will get a beverage at your taste (by appending ⟨yes, no⟩ to the previous sequence to be sure you get milk and no sugar).

The problem of regaining control on a device dates back to Moore [START_REF] Moore | Gedanken-experiments on sequential machines[END_REF] and Ginsburg [START_REF] Ginsburg | On the length of the smallest uniform experiment which distinguishes the terminal states of a machine[END_REF], and was popularized in the early 1960's by Černý [ Čer64], who proposed a polynomial-time algorithm for deciding the existence of a synchronizing word. Černý's algorithm works by iteratively synchronizing states by pairs, based on the following fact: an automaton has a synchronizing word if, and only if, for any two states s and s ′ , there is a word w which, when read from s and from s ′ ends up in the same state. This way, the existence of a synchronizing word can even be decided in non-deterministic logarithmic space, and is actually NLOGSPACE-complete. Černý's result also entails that, if there is a synchronizing word for a given automaton, then there is one of size O(n 3 ) (where n is the number of states of the automaton). Černý conjectured that the upper bound on the size of synchronizing words is (n -1) 2 ; this is a long-standing open problem in automata theory. Pin and Frankl proved in the early 1980's that an upper bound is (n 3 -n)/6 [START_REF] Frankl | An extremal problem for two families of sets[END_REF][START_REF] Pin | On two combinatorial problems arising from automata theory[END_REF], and recently Szyku la and Shitov improved this bound to 0.1654n 3 + o(n 3 ) [START_REF] Szyku La | Improving the upper bound on the length of the shortest reset word[END_REF][START_REF] Shitov | An improvement to a recent upper bound for synchronizing words of finite automata[END_REF]. Additionally, the probability that an n-state deterministic complete automaton (chosen uniformly at random) has a synchronizing word of size O(n log 3 (n)) tends to 1 as n tends to +∞ [START_REF] Nicaud | The Černý conjecture holds with high probability[END_REF].

Another, more naive algorithm for deciding the existence of a synchronizing word consists in building the powerset automaton and looking for a path to a singleton state; however, the resulting automaton has exponential size, and this algorithm thus runs in polynomial space. It can be used to solve the subsetsynchronization-word problem, where the aim is to synchronize a subset of the set of states of the automaton; somewhat surprisingly, this problem can be proved to be PSPACE-complete [START_REF] Rystsov | Polynomial-complete problems in automata theory[END_REF]; as a side result, shortest synchronizing words may be of exponential size for subset synchronization. We refer to classical surveys [START_REF] Volkov | Synchronizing automata and the Černý conjecture[END_REF][START_REF] Sandberg | Homing and synchronizing sequences[END_REF] for more background and results about synchronizing words.

Synchronizability in other classes of automata. Synchronizability has been studied in a variety of contexts since then: for timed automata and integerweighted automata under energy constraints, synchronizability is PSPACEcomplete [DJL + 14]. The problem of synchronizing probabilistic automata is a bit more complex (conceptually): probabilistic automata generate infinite sequences of distributions over states; synchronizing a probabilistic automaton may then amount to reaching a distribution where the probability mass ultimately accumulates in a single state. The existence of a synchronizing word in that setting is PSPACE-complete [START_REF] Doyen | Infinite synchronizing words for probabilistic automata[END_REF][START_REF] Doyen | Infinite synchronizing words for probabilistic automata[END_REF]; several variants and extensions of this result are presented in [START_REF] Doyen | The complexity of synchronizing Markov decision processes[END_REF]. Synchronizability has also been studied in the context of register automata, where again the problem has been proven to be PSPACE-complete [START_REF] Quaas | Synchronizing data words for register automata[END_REF].

Our contributions. Recently, Wolf considered the problem of finding synchronizing words with additional dynamic constraints: this requires that all the paths generated by the considered synchronizing word from all the states of A satisfy some constraints on the order of the states being visited; an example of such a constraint is that the last occurrence of state p always precedes the last occurrence of some other state q. Deciding the existence of such synchronizing words is PSPACE-complete in most cases [START_REF] Wolf | Synchronization under dynamic constraints[END_REF].

In the present paper, we extend the results of Wolf by showing that the existence of synchronizing words with additional LTL constraints on all paths is also PSPACE-complete. Membership in PSPACE relies on the translation of the LTL constraint into a finite-state automaton, and on an algorithm similar to the powerset automaton described above. Hardness in PSPACE is actually proved for very simple, fixed formulas involving only LTL modalities F or G. When X is the only allowed modality, we show that the problem is NP-complete.

Definitions

Linear-time Temporal Logic (LTL)

The linear-time temporal logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] over the set AP of atomic propositions is the set of formulas built along the following grammar:

LTL ∋ ϕ, ψ ::= p | ϕ ∨ ψ | ¬ϕ | Xϕ | ϕ U ψ
where p ranges over AP ⊎ {true}. The size of an LTL formula ϕ, denoted with |ϕ|, is the size of its derivation tree.

A finite trace over AP is a sequence ρ = (v i ) 0≤i≤n with n ≥ 0 and v i ⊆ AP for all 0 ≤ i ≤ n. We may equivalently see each v i as a mapping AP → {0, 1}. The size of ρ, denoted with |ρ|, is n + 1.

For our purposes, we interpret LTL formulas over finite traces. For any finite trace ρ = (v i ) 0≤i≤n and any index 0 ≤ j ≤ n, we inductively define:

ρ, j |= true ρ, j |= p ⇐⇒ v j (p) = 1 ρ, j |= ϕ ∨ ψ ⇐⇒ ρ, j |= ϕ or ρ, j |= ψ ρ, j |= ¬ϕ ⇐⇒ ¬(ρ, j |= ϕ) ρ, j |= Xϕ ⇐⇒ j < n and ρ, j + 1 |= ϕ ρ, j |= ϕ U ψ ⇐⇒ ∃0 ≤ k < n -j. ρ, j + k |= ψ and ∀0 ≤ l < k. ρ, j + l |= ϕ .
Intuitively, X means "next" while U stands for "until". We write ρ |= ϕ as a shorthand for ρ, 0 |= ϕ.

Example. Formula ϕ U ψ demands that ψ be true at some point along the path. A weaker modality, called weak until, relaxes this condition by allowing ψ to never hold true. This modality can be defined as ϕ W ψ ≡ Gϕ ∨ ϕ U ψ.

We extend the syntax of LTL by defining false as the negation of true, conjunction as the dual of disjunction, and with the following extra constructs:

• ϕ R ψ ≡ ¬(¬ϕ U ¬ψ) is the dual of U: this modality is read "release". Its semantics is given by

ρ, j |= ϕ R ψ ⇐⇒ ∀0 ≤ k < n -j. ρ, j + k |= ψ or ∃0 ≤ l < k. ρ, j + l |= ϕ .
It can be checked that ϕ R ψ is equivalent to ψ W (ϕ ∧ ψ) in our setting.

• Xϕ ≡ ¬X¬ϕ is the dual of X: it holds true at position j of ρ if either j is the last position in ρ, or ϕ holds at position j + 1;

• Fϕ ≡ true U ϕ; then ρ, j |= Fϕ if there exists 0 ≤ k such that ρ, j + k |= ϕ; • Gϕ ≡ ¬F¬ϕ; then ρ, j |= Gϕ if for all 0 ≤ k ≤ |ρ| -j, it holds ρ, j + k |= ϕ. Notice that Gϕ ≡ false R ϕ.
Thanks to conjunction, X and R, any LTL formula can be turned into negation normal form, where negations are only allowed to apply to atomic propositions. Said differently, LTL can be defined as

LTL ∋ ϕ, ψ ::= p | ¬p | ϕ ∨ ψ | ϕ ∧ ψ | Xϕ | Xϕ | ϕ U ψ | ϕ R ψ. (1)
In the sequel, we will consider some sublogics of LTL defined by restricting the set of allowed modalities. For a subset M ⊆ {X, X, F, G, U, R}, we write L + (M) for the sublogic obtained by restricting the grammar of Eq. (1) to only allow the modalities in M [SC85]. In the sequel we will encounter the sublogics L + (F), L + (G) and L + (X). Notice that in those sublogics, negation is only allowed in front of atomic propositions, so that e.g. modality F cannot be used in L + (G).

Synchronizing words

Definition 1. Let Σ be a finite alphabet, and AP be a finite set of atomic propositions. An AP-labelled automaton over Σ is a tuple A = ⟨S, T, ℓ⟩ where S is a finite set of states, T ⊆ S × Σ × S is a set of transitions, and ℓ : S → 2 AP is a labelling function.

The size of such an automaton is defined as the cardinality of its state set S. In some situations, the AP-labelling of those automata will be useless; we will simply call them automata in that case; such automata will have no labelling function ℓ.

Pick a labelled automaton A = ⟨S, T, ℓ⟩, and a state s ∈ S. A (finite) path from s in A is a sequence π = (t i ) 1≤i≤n of transitions from T such that, writing

t i = ⟨s i , σ i , s ′ i ⟩ for all 1 ≤ i ≤ n, it holds s 1 = s and s ′ i = s i+1 for all 1 ≤ i < n.
We write first(π) and last(π) for the states s 1 and s ′ n when n > 0, with the special case first(π) = last(π) = s when n = 0 (i.e., when π is the empty sequence). The word associated with π is the finite sequence word(π) = (σ i ) 1≤i≤n ∈ Σ n .

An acceptor automaton over Σ is an automaton A = ⟨S, T ⟩ over Σ equipped with two subsets I and F of S, respectively containing initial and final states. A word σ ∈ Σ n is accepted by the acceptor automaton B = ⟨⟨S, T ⟩, I, F )⟩ whenever there exists a path π with first(π) ∈ I, last(π) ∈ F , and word(π) = σ. The language of B is the set of words it accepts. Given a state s ∈ S and a finite word w in Σ * , we define the set s ⊗ w of paths generated by reading w from s inductively as follows: for the empty word ϵ, the set s ⊗ ϵ only contains the empty path from s; for any non-empty word w, writing w = w ′ • σ with σ ∈ Σ, we have

s ⊗ (w ′ • σ) = {π • ⟨r, σ, r ′ ⟩ | π ∈ s ⊗ w ′ and r = last(π) and ⟨r, σ, r ′ ⟩ ∈ T }.
Finally, we let s ⊙ w = {last(π) | π ∈ s ⊗ w} for the set of states reached from s by reading w, and for any subset

Q ⊆ S, we define Q ⊗ w = s∈Q s ⊗ w and Q ⊙ w = s∈Q s ⊙ w.
A labelled automaton is said deterministic (resp. complete) whenever for any s ∈ S and any σ ∈ Σ, the cardinality of s ⊙ σ is at most (resp. at least) 1.

A set of states Q ⊆ S of a complete deterministic labelled automaton A is said to admit a synchronizing word if there exists a word w such that Q ⊙ w is a singleton. A complete deterministic automaton is said synchronizable if its set of states S has a synchronizing word [ Čer64].

Example. Consider the automaton of Fig. 2 (borrowed from [START_REF] Wolf | Synchronization under dynamic constraints[END_REF]), over the 2-letter alphabet {a, b}. This automaton admits bab as a synchronizing word. With a path π = (t i ) 1≤i≤n in a labelled automaton A, writing t i = ⟨s i , σ i , s ′ i ⟩ for all 1 ≤ i ≤ n, we associate the sequence of states (q i ) 0≤i≤n defined as q 0 = s 1 and q i = s ′ i for all 1 ≤ i ≤ n. We then let trace(π) = (ℓ(q i )) 0≤i≤n . For a formula ϕ ∈ LTL, we write that π |= ϕ when trace(π), 0 |= ϕ.

In the sequel, we focus on the following problem:

Definition 2. Subset-synchronizability under LTL constraints is the problem of deciding, given a complete, deterministic AP-labelled automaton A = ⟨S, T, ℓ⟩ over Σ, a subset Q ⊆ S, and an LTL formula ϕ over AP, whether there exists a finite word w ∈ Σ * such that Q ⊙ w is a singleton and for all π ∈ Q ⊗ w, it holds π |= ϕ. Synchronizability under LTL constraints is the special case of subset-synchronizability where Q = S.

Example. Consider again the automaton of Fig. 2, and the property that the transition from state 5 to state 2 is never taken; this condition can be expressed as ϕ : G(5 ⇒ X¬2) (assuming that the names of the states are the atomic propositions). Obviously, bab is not a good candidate; actually, because of the path starting from state 5, any synchronizing word under LTL constraint ϕ has to start with an a; it turns out that abab is a valid solution. On the other hand, it can be checked that no synchronizing word can avoid the transition from state 2 to state 4.

Related work: synchronizing words under dynamic constraints

Our work can be seen as an extension of some of the results of [START_REF] Wolf | Synchronization under dynamic constraints[END_REF]. In that paper, Wolf considered the problem of synchronizing labelled automata under dynamic constraints, enforcing different kinds of constraints on the first or last occurrence of states of the automaton. Formally, with a (non-necessarily synchronizing) finite word, we can associate different orders on the states of the (deterministic complete) automaton: for instance, the order ∝ l<f p@w is defined as follows: for any two states p and q in S, it holds p ∝ l<f p@w q if, and only if, for all s ∈ S, along the path s ⊗ w, either p never occurs, or q never occurs, or the last occurrence of p occurs before the first occurrence of q. Synchronizability under ∝ l<f p@w then asks, given an automaton and a binary relation R ⊆ S 2 , whether there is a synchronizing word w for which R ⊆ ∝ l<f p@w ; in other terms, for all ⟨p, q⟩ ∈ R, the last occurrence of state p (if any) must occur before the first occurrence of state q (if any) along any path following w in A. This is easily expressed in LTL, e.g. as G(q ⇒ G¬p), assuming that AP = S and each state is labelled with (only) its name. It is proved in [START_REF] Wolf | Synchronization under dynamic constraints[END_REF] that synchronizability under ∝ l<f p@w is PSPACE-complete. Similarly, the order ∝ l≤l p@w requires that the last occurrence of the left-handside state should occur before or at the same time as the last occurrence of the right-hand-side state. Constraint p ∝ l≤l p@w q can be expressed in LTL as G(p ⇒ Fq). The associated synchronizability problem is shown NP-hard (and in PSPACE) in [START_REF] Wolf | Synchronization under dynamic constraints[END_REF]; it is PSPACE-complete when the constraint does not take into account the starting state of each path (equivalently, when the LTL constraint is prefixed by X).

Synchronizability under LTL constraints

Our main result can be stated as follows:

Theorem 3. Synchronizability under LTL constraints is PSPACE-complete, even for fixed formulas in L + (F) or L + (G).

Proof. We first prove membership in PSPACE, and start with an overview of the proof. Intuitively, given a formula ϕ over AP and an AP-labelled automaton A, the first step of the algorithm consists in building an acceptor automaton B ϕ over 2 AP accepting exactly the finite traces satisfying ϕ (following the classical transformation of LTL formula into automata [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF]). Identifying traces over AP with words over the alphabet 2 AP , we then construct the synchronized product C of A and B ϕ , which accepts the traces generated by A and satisfying ϕ. The existence of a synchronizing word for A with constraint ϕ is then equivalent to the existence of a word w which, when read from a set of initial states of C covering all states of A, reaches final states of C involving only one single state of A. Checking the existence of such a word can be performed by a non-deterministic algorithm, which guesses w letter by letter, and computes the set of states reached by reading the current prefix of w from each of the initial states considered, until reaching a final configuration as described above. While a naive implementation of this algorithm requires exponential space, we notice that we do not need to explicitely build the automata B ϕ and C, but only need to compute the successor of a state by a letter. Following this remark, we get a non-deterministic algorithm running in polynomial space; by Savitch's theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], this proves that synchronizability under LTL constraints is in PSPACE.

We now develop the details of this proof. For the sake of self-containment, we briefly sketch the construction of an acceptor automaton B ϕ = ⟨⟨V, R⟩, I, F ⟩ over 2 AP associated with an LTL formula [START_REF] Ch | Principles of Model-Checking[END_REF][START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF].

Fix a formula ϕ ∈ LTL; its set of subformulas subf(ϕ) is the smallest set of LTL formulas containing ϕ and true, and such that, for any two formulas α and β of LTL,

• if α ∨ β or α U β appears in subf(ϕ), then also α and β are in subf(ϕ);

• if Xα or ¬α appears in subf(ϕ), then α ∈ subf(ϕ);

• if α ∈ subf(ϕ) and α is not of the form ¬α ′ , then ¬α ∈ subf(ϕ).

Clearly enough, subf(ϕ) contains at most 2|ϕ| formulas. A subset C of subf(ϕ) is said to be maximally-consistent whenever it contains true and for all α and β in subf(ϕ),

• if ¬α ∈ subf(ϕ), then ¬α ∈ C if, and only if, α / ∈ C;

• if α ∨ β ∈ subf(ϕ), then α ∨ β ∈ C if, and only if, α ∈ C or β ∈ C; • if α U β ∈ subf(ϕ), then α U β ∈ C implies that α ∈ C or β ∈ C.
The number of maximally-consistent subsets of subf(ϕ) is at most 2 2|ϕ| . The states of automaton B ϕ are the maximally-consistent sets of subformulas of ϕ, together with an extra state f ; there is a transition ⟨v, l, v ′ ⟩ from state v ̸ = f to state v ′ ̸ = f labelled with l if, and only if, for any ψ ∈ subf(ϕ),

• if ψ = Xα, then ψ ∈ v if, and only if, α ∈ v ′ ; • if ψ = α U β, then ψ ∈ v if, and only if, β ∈ v or α ∈ v and ψ ∈ v ′ ; • l = v ∩ AP.
Additionally, for any v ̸ = f , there is a transition from v to f labelled with v ∩ AP whenever for all α U β ∈ subf(ϕ), if α U β ∈ v, then β ∈ v and for all Xα ∈ subf(ϕ), Xα ̸ ∈ v. Finally, all states containing ϕ are initial, and f is the unique final state. It can be proved inductively that the language accepted by B ϕ contains exactly the finite traces over AP that satisfy ϕ [START_REF] Ch | Principles of Model-Checking[END_REF][START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF].

We consider the synchronized product of A = ⟨S, T, ℓ⟩ with B ϕ = ⟨⟨V, R⟩, I, F ⟩, denoted with A ⋉ B ϕ , which is the automaton C = ⟨Q, R⟩ over Σ defined as:

• Q = {⟨s, v⟩ ∈ S × V | ℓ(s) = v ∩ AP} ⊎ {⟨s, f ⟩ | s ∈ S}; • R is the set of triples ⟨⟨s, v⟩, σ, ⟨s ′ , v ′ ⟩⟩ ∈ Q × Σ × Q such that there are transitions ⟨s, σ, s ′ ⟩ in A and ⟨v, v ∩ AP, v ′ ⟩ in B ϕ .
By construction, for any path π in A ⋉ B ϕ starting from some state ⟨s, v⟩ with v ∈ I and ending in some state ⟨s ′ , f ⟩, it holds π |= ϕ.

In order to decide synchronizability of A = ⟨S, T, ℓ⟩ under LTL constraint ϕ, we consider the cross-product P of |S| copies of A ⋉ B ϕ , and look for a path π from some state of the form

(⟨s i , v i ⟩) 1≤i≤|S| with {s i | 1 ≤ i ≤ |S|} = S and v i ∈ I for all 1 ≤ i ≤ |S|, to a state of the form (⟨s ′ i , f ⟩) 1≤i≤|S| where {s ′ i | 1 ≤ i ≤ |S|} is a singleton.
Clearly enough, any such path π is such that for all s ∈ S, the path s ⊗ word(π) in A satisfies ϕ, since it corresponds to some path from ⟨s i , v i ⟩ to ⟨s ′ i , f ⟩ in the product automaton A ⋉ B ϕ . Since the size of P is at most (|S| × 2 |ϕ| ) |S| , if such a path π exists, there must be one that never visits the same state twice, thus there is one of size at most (|S| × 2 |ϕ| ) |S| . As a consequence, synchronizability of A under LTL constraint ϕ can be decided by non-deterministically building such a path step-by-step, using space polynomial in both |ϕ| and |S| to store the current state of P being visited and a counter to stop the computation if no solution is found after (|S| × 2 |ϕ| ) |S| steps. Since PSPACE = NPSPACE [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], this proves that synchronizability under LTL constraints is in PSPACE.

Hardness in PSPACE is easily derived from the results of [START_REF] Wolf | Synchronization under dynamic constraints[END_REF], even for a fixed LTL formula in L + (G) (see Section 3). We propose an alternative PSPACEhardness proof for fixed formulas without nesting of modalities, and involving only modality G (i.e., in L + (G)), or only modality F (i.e., in L + (F)). Our proof is based on a reduction from the subset-synchronizability problem (with no LTL constraints), which is known to be PSPACE-complete [START_REF] Rystsov | Polynomial-complete problems in automata theory[END_REF].

Consider an automaton A = ⟨S, T ⟩ over alphabet Σ, and a non-empty subset Q ⊆ S of states that we want to synchronize. We define a labelled automaton

A ′ = ⟨S ′ , T ′ , ℓ ′ ⟩ over Σ ′ by letting S ′ = S ⊎ {s # , s 0 , s ′ 0 , s f , s ′ f }, Σ ′ = Σ ⊎ {#} ⊎ S,
and T ′ = T ⊎ U where U contains the following transitions:

• ⟨s 0 , #, s # ⟩, ⟨s ′ 0 , #, s # ⟩, and ⟨s 0 , σ, s ′ 0 ⟩ and ⟨s ′ 0 , σ, s ′ 0 ⟩ for all σ ∈ Σ ⊎ S. Since s 0 will have no incoming transitions, the automaton cannot synchronize in s 0 , so that any synchronizing word must contain #. Using an LTL constraint, we will enforce that any synchronizing word begins with #;

• all transitions from s f and s ′ f go to s ′ f ; this way, if synchronization is possible, the synchronized runs will end in s ′ f ;

• ⟨s, #, s # ⟩ for all s ∈ {s # } ∪ S \ Q, and ⟨q, #, q⟩ for all q ∈ Q. This way, when reading the first letter # of a synchronizing word, all states in Q take a self-loop, states s f and s ′ f move to s ′ f , while the other states (in particular those in S \ Q) all go to s # ;

• ⟨s, s, s f ⟩ for all s ∈ S, and ⟨s, s ′ , s # ⟩ for all s and s ′ in S with s ′ ̸ = s.

Additionally, U also contains ⟨s # , s, s ′ f ⟩ for all s ∈ S. An LTL constraint will forbid the runs originating from Q to ever visit s # , so that these runs can only leave S by reading a letter from S, and they must have synchronized before doing so;

• finally, ⟨s # , σ, s # ⟩ for all σ ∈ Σ.

The construction is depicted on Fig. 3. In that figure, ⋆-transitions represent all labels that do not already appear on other transitions leaving the same state (so that the automaton is deterministic and complete). We let AP ′ = {Q, s # , s 0 , s ′ 0 }, with ℓ ′ (q) = {Q} for all q ∈ Q, and ℓ ′ (s) = s for s ∈ {s # , s 0 , s ′ 0 }. Finally, we let ϕ = [s 0 ⇒ G(¬s ′ 0 )] ∧ [Q ⇒ G(¬s # )]; the first conjunct forces the synchronizing word (if any) to start with a #-transition, while the second one forbids the states in Q to ever visit s # , as required above.

q 1 q 2 q 3 s 1 s 2 s 3 Q S \ Q ⇝ q 1 q 2 q 3 s 1 s 2 s 3 Q S \ Q s ′ 0 s 0 s # s ′ f
We prove that Q can be synchronized in A if, and only if, S ′ can be synchronized in A ′ under LTL constraint ϕ. First, if w is a synchronizing word for Q in A, then w ′ = # • w • q w • # is a synchronizing word in A ′ satisfying ϕ, where q w is such that Q ⊙ w = {q w }: reading w ′ from states in Q first loops on the states in Q, then synchronizes to q w , and finally goes to s f and then s ′ f , thereby satisfying ϕ; reading w ′ from s f or s ′ f eventually loops in s ′ f , trivially satisfying ϕ; reading w ′ from any other state first goes to s # , loops there while reading w, and finally moves to s ′ f , thereby also satisfying ϕ. Conversely, consider a synchronizing word w ′ in A ′ under constraint ϕ. As argued above, it must start with # as otherwise reading w ′ from s 0 would visit s ′ 0 and falsify ϕ; states in Q then take their self-loops, while s f and s ′ f both go to s ′ f , and all other states go to s # . As argued above, synchronization can only happen in s ′ f , and since the runs originating from Q cannot visit s # , they cannot leave S by reading #; hence some letter in S must eventually occur in order to achieve synchronization. But this may only occur when all paths originating from the states in Q have synchronized in S, as otherwise some of those runs would visit s # . This proves our result.

This proof easily extends to fixed formulas in L + (F): the construction of the labelled automaton is almost unchanged, except that we swap the transitions from s 0 : we have ⟨s 0 , #, s ′ 0 ⟩ and ⟨s 0 , σ, s

# ⟩ for all σ ∈ Σ ′ \ {#}. Formula ϕ = [s 0 ⇒ Fs ′ 0 ] ∧ [Q ⇒ Fs f ]
achieves the same constraints as above: the first conjunct forces to start with #, and the second one prevents the synchronizing runs originating from Q to visit s # .

Remark 1. Notice that our algorithm is readily adapted to subset-synchronizability with LTL constraints, which is thus also in PSPACE (hence PSPACE-complete).

Remark 2. The last part of the hardness proof (for L + (F)) implies that the problem SYNC-UNDER-0-∝ l≤l w@p , which is proven to be NP-hard in [Wol20, Theorem 16], is actually PSPACE-hard (hence PSPACE-complete). Indeed, the L + (F) constraint can be encoded by requiring that the last occurrence of s 0 precedes the last occurrence of s ′ 0 , and that the last occurrence of each state in Q precedes the last occurrence of s f . Theorem 4. Synchronizability under L + (X)-constraints is NP-complete. It is NLOGSPACE-complete when the L + (X) formula is fixed.

Proof. Membership in NP can be proven in two steps: first, we have to check that all states can be synchronized, using the pairwise-synchronization algorithm. If so, in order to prove that there is a synchronizing word whose traces satisfy ϕ, we guess a prefix of size d of this synchronizing word, where d is the maximal number of nested X modality in ϕ; since the whole automaton can be synchronized, the set of states reached after reading this prefix can also be synchronized.

When the formula is fixed, the second part of the algorithm runs in NLOGSPACE: it guesses and stores the prefix (using space O(1)), and checks from each state of A that the resulting path satisfies ϕ, which can be achieved in LOGSPACE. Since the classical synchronizability problem is NLOGSPACE-complete, the first part of the algorithm can be performed in NLOGSPACE (and hardness for fixed L + (X) formulas follows).

NP-hardness for non-fixed formulas follows from the NP-hardness of model checking for L + (X) [START_REF] Markey | Past is for free: On the complexity of verifying linear temporal properties with past[END_REF]: given an AP-labelled automaton A, a state s 0 of A, and a formula ψ ∈ L + (X), deciding whether there is a path from s 0 satisfying ψ is NP-complete. This problem is easily reduced to our synchronizability problem with constraints in L + (X): we add two extra states t and t ′ , and two extra letters # and $ in Σ; all #-transitions go to t, except for a #-self-loop on s 0 , and all non-#-transitions from t and t ′ go to t ′ ; all $-transitions go to t ′ . Finally, we label s 0 , t and t ′ with their names, seen as two extra atomic propositions.

We consider the formula ϕ defined as (Xt ∧ X 2..d+1 ¬t) ∨ (Xs 0 ∧ Xψ ∧ X 1..d+1 (¬t ∧ ¬t ′ ))

where again d is the maximal number of nested X in ψ, and X a..b ϕ is a shorthand for the conjunction of all X j ϕ for j ranging from a to b.

Assume that there is a synchronizing word satisfying ψ. From t, the resulting path cannot satisfy Xs 0 , hence it has to satisfy the first disjunct, so that this word has to start with #, and cannot involve # in the next d steps. From s 0 , Xt cannot be fulfilled, so that the second conjunct has to be satisfied, and the synchronizing word gives rise to a path satisfying ψ and visiting only states of A for the first d steps; since the truth value of ψ only depends on the first d steps, this shows the existence of a path in A satisfying ψ.

Conversely, if there is a path from s 0 satisfying ψ, then we can build a synchronizing word satisfying ϕ by prepending # and appending $ to the corresponding word. The resulting word is easily checked to satisfy ϕ and, thanks to the last $, to synchronize all paths to t ′ .

Figure 1 :

 1 Figure 1: A coffee-vending machine

Figure 2 :

 2 Figure 2: A synchronizable automaton with Σ = {a, b} and AP = {1, 2, 3, 4, 5}.

Figure 3 :

 3 Figure 3: Reduction of subset-synchronizability to LTL-synchronizability

s f ⋆ ⋆ # # ⋆ ⋆ S ⋆ # # # s= s ̸ = #

Acknowledgement

We thank the anonymous reviewers for their very careful reading of earlier versions of this article, which helped us improve its writing.