Ph Schnoebelen

On flat lossy channel machines

We show that reachability, repeated reachability, nontermination and unboundedness are NP-complete for Lossy Channel Machines that are flat, i.e., with no nested cycles in the control graph. The upper complexity bound relies on a fine analysis of iterations of lossy channel actions and uses compressed word techniques for efficiently reasoning with paths of exponential lengths. The lower bounds already apply to acyclic or single-path machines.

-→ (q ′ 1 , ba) -→ (q ′ 0 , ε) .

Introduction

Lossy channel machines, aka LCMs, are FIFO automata, i.e., finite-state machines operating on buffers with FIFO read/write discipline, where the buffers are unreliable, or lossy, in the sense that letters (or "messages") in a buffer can be lost nondeterministically at any time.

LCMs were first introduced as a model for communication protocols designed to work properly in unreliable environments. They immediately attracted interest because, unlike FIFO automata with reliable buffers, they have decidable safety and termination problems [START_REF] Finkel | Decidability of the termination problem for completely specificied protocols[END_REF][START_REF] Abdulla | Verifying programs with unreliable channels[END_REF][START_REF] Cécé | Unreliable channels are easier to verify than perfect channels[END_REF][START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF]. It was later found that LCMs are a relevant computational model per se, useful for verifying timed automata [START_REF] Abdulla | Decidability and complexity results for timed automata via channel machines[END_REF][START_REF] Lasota | Alternating timed automata[END_REF], modal logics [START_REF] Gabelaia | Non-primitive recursive decidability of products of modal logics with expanding domains[END_REF], etc., and connected to other problems in computer science [START_REF] Karandikar | Generalized Post embedding problems[END_REF][START_REF] Chambart | Toward a compositional theory of leftist grammars and transformations[END_REF][START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF].

Flat LCMs. In this paper we consider the case of flat LCMs, i.e., LCMs where the control graph has no nested cycles. In the area of infinite-state systems verification, flat systems were first considered in [START_REF] Fribourg | A decompositional approach for computing least fixed-points of datalog programs with Z-counters[END_REF][START_REF] Comon | Multiple counters automata, safety analysis, and Presburger arithmetic[END_REF] for counter systems1 . In addition, some earlier "loop acceleration" results, e.g. [START_REF] Boigelot | Symbolic verification with periodic sets[END_REF], where one can compute reachability sets along a cycle, can often be generalised to flat systems. Positive results on flat counter systems can be found in [LS05, BIL09, DFGvD10, BIK14, LPS14, DDS15], and in [START_REF] Ganty | Interprocedural reachability for flat integer programs[END_REF] for counter systems with recursive calls. Regarding flat FIFO automata, verification was shown decidable by Bouajjani and Habermehl [START_REF] Bouajjani | Symbolic reachability analysis of FIFOchannel systems with nonregular sets of configurations[END_REF] who improved on earlier results by Boigelot [START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using QDDs[END_REF], and the main verification problems were only recently proven to be NP-complete [START_REF] Esparza | A perfect model for bounded verification[END_REF][START_REF] Finkel | Verification of flat FIFO systems[END_REF]. These results have applications beyond flat systems in the context of bounded verification techniques, where one analyses a bounded subset of the runs of a general system [START_REF] Esparza | A perfect model for bounded verification[END_REF]. Flat LCMs have not been explicitly considered in the literature. They are implicit in forward analysis methods based on loop acceleration, starting with [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF], but these works do not address the overall complexity of the verification problem, only the complexity of elementary operations.

It is not clear whether one should expect flat LCMs to be simpler than flat FIFO automata (on account of unrestricted LCMs being simpler than the Turing powerful, unrestricted FIFO automata), or if they could be more complex since message losses introduce some nondeterminism that does not occur when one follows a fixed cycle in a FIFO system. Indeed, message losses can be seen as hidden implicit loops that disrupt the apparent flatness of the LCM.

Our contribution. We analyse the behaviour of the backward-reachability algorithm on cycles of lossy channel actions and establish a bilinear upper bound on its complexity. As a consequence, reachability along runs of the form ρ 1 σ * 1 ρ 2 σ * 2 . . . ρ m σ * m where the ρ i , σ i are sequences of channel actions, can be decided in time n O(m) . While shortest reachability witnesses can be exponentially long when the number m of cycles is not bounded, techniques based on SLP-compressed words allow handling and checking these witnesses in polynomial time, leading to an NP algorithm for flat LCMs. This easily translates into NP algorithms for nontermination, repeated reachability, and unboundedness, and in fact all four problems are NP-complete. Thus the restriction to flat systems really brings some simplification when compared to the very high complexity -sometimes undecidability as is the case for unboundedness-of verification for unrestricted LCMs [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF][START_REF] Schmitz | Multiply-recursive upper bounds with Higman's lemma[END_REF][START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF].

Remark 1.1 (Lossy channel machines vs. lossy channel systems). In line with most works on loop acceleration and verification of flat systems, we consider lossy channel "machines" instead of the more usual lossy channel "systems", i.e., systems where several independent concurrent machines communicate via shared channels. This is because a combination of individually flat machines does not lead to a "flat" system. Additionally, finite-state concurrent systems typically have PSPACE-hard verification problems already when they have no channels and run synchronously, or when they only synchronise via bounded channels that can hold at most one message [START_REF] Demri | A parametric analysis of the state explosion problem in model checking[END_REF].

Outline. After some technical preliminaries (Section 2), we present our main technical contribution (Section 3): we analyse the computation of predecessors (of some given configuration) through a cycle iterated arbitrarily many times. In particular we show that the backward-reachability analysis of a single cycle reaches its fixpoint after a bilinear number of iterations. This leads to an effective bound on the length of the shortest runs between two configurations. In Section 4 we show how the previous analysis can be turned into a nondeterministic polynomial-time algorithmic via the use of SLP-compressed words for efficiently computing intermediary channel contents along a run. In Section 5 we show how our main results also apply to termination, repeated reachability, and boundedness. Finally Appendix C presents reductions showing how the problems we considered are NP-hard, even for acyclic LCMs or single-path LCMs.

Related work. After we circulated our draft proof, we became aware that a related NPmembership result will be found in [START_REF] Finkel | Verification of flat FIFO systems[END_REF]. There the authors adapt the powerful technique from [START_REF] Esparza | A perfect model for bounded verification[END_REF] and encode front-lossy channel systems into multi-head pushdown automata, from which an NP-algorithm for control-state reachability in flat machines ensue. Our approach is lower level, providing a tight bilinear bound on the number of times a cycle must be visited in the backward-reachability algorithm. Once these bounds are established, our NP algorithm only needs to guess the number of times each cycle is visited.

Preliminaries

We consider words u, v, w, x, y, z, . . . over a finite alphabet Σ = {a, b, . . .}. We write |u| for the length of a word and ε for the empty word. The set of letters that occur in u is written alph(u). For a n-letter word u = a 1 • • • a n and some index ℓ ∈ {0, 1, . . . , n}, we write

u ≤ℓ def = a 1 • • • a ℓ and u >ℓ def = a ℓ+1 • • • a n
for the ℓ-th prefix and the ℓ-th suffix of u. We write

u (ℓ) def = u >ℓ • u ≤ℓ for the ℓ-th cyclic shift of u.
Exponents are used to denote the concatenation of multiple copies of a same word, i.e., u 3 denotes uuu. A fractional exponent p ∈ Q can be used for u p if p•|u| is a natural number. E.g., when a, b, c are letters, (abc) 11 3 , or equivalently (abc) 3+2 3 , denotes abc abc abc ab. We write u v to denote that u is a (scattered) subword of v, i.e., there exist 2m + 1 words u 1 , . . . , u m , x 0 , x 1 , . . . , x m such that u

= u 1 • • • u m and v = x 0 u 1 x 1 . . . u m x m . It is well-known that
is a well-founded partial ordering. For a word x ∈ Σ * , we write

↑ x def = {y ∈ Σ * |x
y} to denote the upward-closure of x, i.e., the set of all words that contain x as a (scattered) subword.

LCMs. In this paper we consider channel machines with a single communication channel 2 . A lossy channel machine (LCM) is a tuple S = Q, Σ, ∆ where Q = {p, q, . . .} is a finite set of control locations, or just "locations", Σ = {a, b, . . .} is the finite message alphabet, and ∆ ⊆ Q × ({!, ?} × Σ * ) × Q is a finite set of transition rules. A rule δ = q, (d, w), q ′ has a start location q, an end location q ′ and a channel action (d, w). We write Act Σ def = {!, ?}×Σ * for the set of channel actions over Σ, and often omit the Σ subscript when it can be inferred from the context. We use θ, θ ′ , . . . to denote actions and σ, ρ, . . . to denote sequences of channel actions.

We'll constantly refer to the written part and the read part of some channel action (or sequence of such). These are formally defined via

wri(!w) def = w , rea(!w) def = ε , wri(?w) def = ε , rea(?w) def = w , wri(θ 1 • • • θ m ) def = wri(θ 1 ) • • • wri(θ m ) , rea(θ 1 • • • θ m ) def = rea(θ 1 ) • • • rea(θ m ) .
(1)

Semantics. The operational semantics of LCMs is given via transition systems. Fix some

LCM S = Q, Σ, ∆ . Actions in Act Σ induce a ternary relation -→ ⊆ Σ * × Act Σ × Σ * on channel contents: x ! w -→ y def ⇐⇒ y x w , x ? w -→ y def ⇐⇒ w y x . (2)
Observe how Equation (2) includes the subword relation in the definition of the operational semantics. This models the fact that messages in the channel can be lost nondeterministically during any single computation step. A consequence is the following monotonicity property: if x ′ x and y y ′ then x θ -→ y implies x ′ θ -→ y ′ .

Flat LCMs. An elementary cycle of length m in a LCM S is a non-empty set C = { p i , θ i , q i |i = 1, . . . , m} of rules from ∆ such that q m = p 1 and p i = q i-1 when 2 ≤ i ≤ m, and such that the p i 's are all distinct. A cycle of length 1 is a self-loop. The set {p 1 , . . . , p m } is the set of locations visited by C. Note that two distinct cycles may have the same visited set if they use different transition rules. We say that S is flat if no control location is visited by two different elementary cycles. An extreme case of flat machines are the machines having no cycles whatsoever, called acyclic machines. 3When S is flat, there is (at most) one cycle around any location q and we write σ q for the sequence of actions along this cycle, making sure that σ q starts with the action leaving q (so that if q, q ′ are two locations visited by the same cycle, σ q ′ will be a cyclic shift of σ q ). When there is no cycle visiting q we let σ q = ε by convention. NP-hardness. It is known that reachability and other verification problems are NP-hard for (reliable) FIFO automata: see [EGM12, App. C] and [START_REF] Finkel | Verification of flat FIFO systems[END_REF]. We strengthen these results in Appendix C with the following theorems that cover reliable and unreliable channels indifferently.

Theorem 2.1 (Hardness for acyclic channel machines). Reachability, nontermination and unboundedness are NP-hard for acyclic channel machines, with reliable or with unreliable channels. Hardness already holds for a single channel and a binary alphabet. It also holds for a unary alphabet (i.e., for acyclic VASSes, reliable or lossy) provided one allows several channels (or counters).

NP-hardness for acyclic machines uses the nondeterminism allowed in channel machines. It is thus interesting to consider single-path machines where the control graph is a single line possibly carrying cycles on some locations, as is done in [START_REF] Kuhtz | Weak Kripke structures and LTL[END_REF] or [START_REF] Demri | Taming past LTL and flat counter systems[END_REF]. In such a machine, nondeterminism only occurs in choosing how many times a cycle is visited (and what messages are lost in unreliable systems). This is equivalent to considering reachability (or nontermination or unboundedness) along a given bounded path scheme of the form

q 1 C * 1 q 2 C * 2 • • • q m C * m .
Theorem 2.2 (Hardness for single-path channel machines). Reachability, nontermination and unboundedness are NP-hard for single-path channel machines, with reliable or with unreliable channels. Hardness already holds for a single channel. It also holds for singlepath VASSes, reliable or lossy, provided one allows several counters.

The above NP-hardness does not apply to bounded path schemes with a fixed number of cycles and indeed we show in Section 3 that reachability along path schemes with m cycles can be verified in polynomial-time n O(m) .

Backward reachability in flat LCMs

In this section we consider a generic flat single-channel LCM S with channel alphabet Σ and investigate the complexity of backward-reachability analysis.

Computing predecessors

The classical approach to deciding reachability in LCMs is the backward-reachability algorithm proposed by Abdulla and Jonsson. They first developed it for lossy channel systems [START_REF] Abdulla | Verifying programs with unreliable channels[END_REF] before generalising it to the larger class of Well-Structured Systems [A ČJT00,[START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

For backward reachability, we write Pre[σ](x) for {y ∈ Σ * | y σ -→ x}, the set of σpredecessors of x, and Pre[σ](↑ x) for {y ∈ Σ * | ∃x ′ ∈ ↑ x : y σ -→ x ′ }, the set of σ-predecessors of x "and larger contents". A consequence of the monotonicity of steps is that Pre[σ](↑ x) is upward-closed set and, unless σ is the empty sequence, coincides with Pre[σ](x). Definition 3.1 (pr[σ](x)). For a channel contents x ∈ Σ * and a sequence σ of channel actions, we write pr[σ](x) = y when Pre[σ](↑ x) = ↑ y.

In the case of lossy channels, Pre[σ](↑ x) always has a single minimal element, hence pr[σ](x) is always defined. We now explain how to compute it.

For two words x, v we define x/v as the prefix of x that remains when we remove from x its longest suffix that is a subword of v. This operation is always defined and can be computed using the following rules where a, b are letters:

x/ε = x , ε/v = ε , (x a)/(v b) = x/v if a = b, (x a)/v if a = b. (4) This immediately entails (x/v)/v ′ = x/(v ′ v).
We'll also use the following properties:

if x ′ /v = ε then x(x ′ /v) = (x x ′ )/v , if |x ′ | > |v| then x ′ /v = ε . (5)
We may now compute pr[σ](x) with:

pr[?u](x) = u • x , pr[!v](x) = x/v , pr[ε](x) = x , pr[σ 1 • σ 2 ](x) = pr[σ 1 ] pr[σ 2 ](x) . (6)
W.r.t. subword ordering, the / operation is monotonic in its first argument and contramonotonic in the second : u u ′ implies u/v u ′ /v and x/u x/u ′ . Concatenation too is monotonic. This generalises to the following useful lemma: Lemma 3.2. Assume pr[σ](x) = y and pr[σ](x ′ ) = y ′ where σ is some sequence of actions. Then x x ′ implies y y ′ . Proof. By induction on σ, using eqs. ( 4) and (6).

Cycles: repeating a given sequence of actions

We now focus on computing pr[σ k ](x) for σ a sequence of actions and some k ∈ N.

Without any loss of generality, σ can be written in the general form ?a 1 !b 1 ?a 2 !b 2 • • •?a r !b r where each a i and b i is a letter or the empty word ε. Then rea

(σ) = a 1 a 2 • • • a r and wri(σ) = b 1 b 2 • • • b r .
To fix notation, we define "the small-step sequence for pr[σ](x)", or just "the SSS ", as the sequence y r , y ′ r , y r-1 , y ′ r-1 , . . ., y 1 , y ′ 1 , y 0 of 2r + 1 words given by

y r = x , y ′ i = y i /b i , y i-1 = a i y ′ i . (7)
Clearly, the SSS lists all the intermediary steps in the computation of pr[σ](x) as dictated by eq. ( 6), and thus it yields y 0 = pr[σ](x).

Our first lemma handles the special case where x is made of copies of rea(σ).

Lemma 3.3. Let u = rea(σ). (i) If x is a fractional power u p of u, then y = pr[σ](x) is also a fractional power of u, written y = u m . (ii) Furthermore, if m > 1, then pr[σ](u p+n ) = u m+n for all n ∈ N. (iii) Finally, for all n ∈ N, if m > n + 1, then pr[σ](u p-n ) = u m-n .
Proof. The lemma holds spuriously if u = ε, so we assume |u| > 0. Let us write σ in the general form ?

a 1 !b 1 ?a 2 !b 2 • • •?a r !b r , so that u = a 1 a 2 • • • a r .
To simplify notation we will write u (i) for the shift

a i+1 • • • a r • a 1 . . . a i that really should be written u (|a 1 •••a i |) (remember that a j = ε is possible).
We now claim that, in the SSS (y i , y ′ i ) i for σ and x, each y i and y ′ i is a fractional power of u (i) , written

y i = u p i (i) and y ′ i = u p ′ i (i) .
The proof is by induction on r -i. For y i , there are two cases: (1) y r = x is a power of u by assumption, hence of u (r) , with p r = p; (2) y i-1 is a i y ′ i , i.e., a i u

p ′ i (i) by ind. hyp., hence a power of u (i-1) with p i-1 = p ′ i + |a i | |u| .
For y ′ i the proof is simpler: by ind. hyp. it is u p i (i) /b i and, as a prefix of a power of u (i) , is itself a power of u (i) , albeit with a perhaps smaller exponent, i.e., p i -

|b i | |u| ≤ p ′ i ≤ p i .
(i) Since y coincide with y 0 , we obtain y = u m as required by letting m = p 0 .

(ii) Equation (8) gathers the (in)equalities we just established:

p r = p , p i-1 = p ′ i + |a i | |u| , max 0, p i - |b i | |u| ≤ p ′ i ≤ p i , p 0 = m . (8)
Thus the assumption m > 1 entails p ′ i > 0, i.e. y ′ i = ε, for all i = r, r -1, . . . , 2, 1. Let us now consider the SSS (z i , z ′ i ) i for pr[σ](u p+1 ). We claim that for all i, z i = u (i) y i and

z ′ i = u (i) y ′ i ,
as is easily proven by induction on r -i. The crucial case is z ′ i , defined as z i /b i and equal to (u (i) y i )/b i by ind. hyp. Since y i /b i = y ′ i = ε as just observed, we deduce (u (i) y i )/b i = u (i) (y i /b i ) from eq. ( 5). This is u (i) y ′ i as required. Finally we end up with pr[σ](u p+1 ) = z 0 = u (0) y 0 = uu m = u m+1 , and this generalises to pr[σ](u p+n ) = u m+n .

(iii) With eq. ( 8), the assumption m > n + 1 now entails p i , p

′ i ≥ n + 1 |u| for all i. We claim that the SSS (z i , z ′ i ) i for pr[σ](u p-n ) satisfies u n (i) z i = y i and u n (i) z ′ i = y ′
i for all i, as can be proved by induction on r -i. The base case 5) applies and we deduce

u n z r = u n u p-n = u p = y r is clear. Let us now consider u n (i) z ′ i . It is u n (i) (z i /b i ), that is u n (i) (u p i -n (i) /b i ) since u n (i) z i = y i by ind. hyp. and y i = u p i (i) by (i). Now |u p i -n (i) | = |u|(p i -n) ≥ 1 ≥ |b i |, so eq. (
u n (i) (z i /b i ) = (u n (i) z i )/b i = y i /b i (by ind. hyp.) = y ′ i . We have proved u n (i) z ′ i = y ′ i as required. Finally, proving u n (i) z i = y i is handled in a similar way.
Note that m > 1 is required for part (ii) of the Lemma. For example, with σ =?a!b?c!c!a one has u = rea(σ) = a c and pr[σ](u

1 2 ) = u 1 . However one can check that pr[σ](u 3 2 ) = a c a = u 3 2 .
Equipped with Lemma 3.3, we turn to the general case for pr[σ k ](x).

Theorem 3.4. Let σ ∈ Act * Σ be a sequence of actions and write u for rea(σ). Let x ∈ Σ * be some channel contents and write y k for pr[σ k ](x). (i) For every k ∈ N, y k has the form u p k •x <ℓ k for some fractional power p k and some length ℓ k ∈ {0, 1, . . . , |x|}. (ii) Furthermore, computing p k and ℓ k can be done in time poly(|σ| + |x| + log k).

Proof. (i) Write v for wri(σ) and consider the sequence (x k ) k∈N given by x 0 def = x and

x k+1 def = x k /v. Note that |x k+1 | ≤ |x k |
for all k and write κ for the largest index with x κ = ε. We let κ = -1 if already we started with x = ε, and κ = ω if all x k 's are non-empty, which happens iff alph(x) ⊆ alph(v).

If

k ≤ κ, pr[σ k ](x) = u k • x k and x k is a prefix of x, so taking p k = k and ℓ k = |x k | works. If k = κ + 1, y k is pr[σ](u κ • x <ℓκ ). Since x <ℓκ /v = ε, the result is a prefix of u κ+1
, so has the form u p κ+1 for some p κ+1 . One also lets l κ+1 = 0.

Finally, if k > κ + 1, we have If k = κ + 1, we need to compute pr[σ](u κ x <κ ) in order to extract p κ+1 . This uses eq. (6) for O(|σ|) small steps. Note that we do not build u κ explicitly: once x has been consumed, we work on some u p (i) and just update p and i when applying some pr[?a], or only update p when applying some pr[!b], for which we only need to know where are the occurrences of b in u. For each small step, the updates can be computed in time O(|u|+|x|), hence p κ+1 is computable in quadratic time.

y k = pr[σ k-κ-1 ](y κ+1 ) = pr[σ k-κ-1 ](u p κ+1
If k > κ + 1, we set q 0 = p κ+1 , k ′ = kκ -1 and aim for pr σ k ′ (x ′ ), starting from x ′ = u q 0 . We need to compute u q k ′ in the sequence u q 0 , u q 1 , . . . , defined by u q i+1 def = pr[σ](u q i ). Let us first compute q 1 and consider the three possibilities:

(1) If q 0 = q 1 , y p is a fixpoint for pr[σ] and we know p k = p.

(2) If q 0 < q 1 , the exponents increase under pr[σ] and after computing at most |u| + 1 consecutive values, we'll find two indexes 1 ≤ i < j ≤ |u| + 1 such that q i and q j have the same fractional parts, i.e., differ by some natural number. We can then use Lemma 3.3.(ii) and compute q j+ k ′ -j j-i = q j + k ′ -j j-i . From there, we're just at most |u| steps from q k ′ , i.e., p k .

(3) Finally, if q 0 > q 1 a similar technique, now relying on Lemma 3.3.(iii), will let us compute q k ′ in polynomial time.

The next step is to compute Pre[σ * ](↑ x), that is, ↑ x ∪ Pre[σ](↑ x) ∪ Pre[σ 2 ](↑ x) ∪ • • • . Like Pre[σ](↑ x)
, this set is upward-closed. However it may have several minimal elements and one needs to collect all of them in order to represent the set faithfully. Definition 3.5 (Iteration number). The iteration number L(σ, x) associated with a sequence of actions σ and a channel contents x is the smallest integer such that there exists

ℓ ≤ L(σ, x) with pr[σ ℓ ][x]
pr[σ L(σ,x)+1 ](x). Note that, by Higman's Lemma, such an integer always exists.

The point of Definition 3.5 is that it captures the number of iterations that are sufficient to compute Pre[σ * ](↑ x).

Lemma 3.6. Pre[σ * ](↑ x) = L(σ,x) i=0 ↑ pr[σ i ](x).
Proof. Write y k for pr[σ k ](x) and L for L(σ, x). By definition there is some ℓ ≤ L with y ℓ y L+1 . By Lemma 3.2, this continues into y ℓ+1 y L+2 , y ℓ+2 y L+3 , etc., implying ↑ y ℓ ⊇ ↑ y L+1 , ↑ y ℓ+1 ⊇ ↑ y L+2 , ↑ y ℓ+2 ⊇ ↑ y L+3 , . . . Finally Pre[σ * ](↑ x), which is i∈N ↑ y i coincides with the finite union

L(σ,x) i=0 ↑ y i .
Theorem 3.7 (Bounding iteration numbers). L(σ, x) ≤ |x|(| rea(σ)| + 1) for any action sequence σ and channel contents x.

Proof. We write u for rea(σ). Using Theorem 3.4, we write y k = pr[σ k ](x) = u p k • x <ℓ k and observe that p i ≤ p j and ℓ i ≤ ℓ j imply y i y j . Recall from the proof of Theorem 3.4 that

|x| = ℓ 0 ≥ ℓ 1 ≥ • • • ≥ ℓ i ≥ • • • is a decreasing sequence and that p k = k when ℓ k > 0.
There are two cases: (1) If (ℓ k ) k stabilises with some limit value ℓ ∞ that is strictly positive, then ℓ |x|-1 = ℓ |x| and we deduce y |x|-1 y |x| , entailing L(σ, x) < |x|.

(2) If ℓ ∞ = 0 then, writing k 0 for the first index with ℓ k 0 = 0, we know that k 0 ≤ |x| and

p k 0 = k 0 . If p k 0 +1 ≥ p k 0 then y k 0 y k 0 +1 . Otherwise p k 0 > p k 0 +1
and as a consequence of Lemma 3.2 the suffix sequence The bound given by Theorem 3.7 is tight as the next simple example shows.

p k 0 > p k 0 +1 ≥ p ko+2 ≥ p k 0 +3 ≥ • • • is

Bounding runs

Assume that a flat LCM S is such that (q ′ , y) ∈ Post * (q, x). Since S is flat, the run (q, x) * -→ (q ′ , y) has the following shape:

(q, x) = (q 0 , z 0 )

σ n 0 0 --→ (q 0 , z ′ 0 ) θ 1 -→ (q 1 , z 1 ) σ n 1 1 --→ (q 1 , z ′ 1 ) θ 2 -→ (q 2 , z 2 ) σ n 2 2 --→ • • • • • • (q m-1 , z ′ m-1 ) θm -→ (q m , z m ) σ nm m --→ (q m , z ′ m ) = (q ′ , y) . (9)
In eq. ( 9), the control locations (q =)q 0 , q 1 , . . . , q m (= q ′ ) are all distinct, σ i is the sequence of actions performed along the (unique) cycle on q i , and n i is the number of times this cycle has been traversed along the run. We use σ i = ε when there is no cycle on q i , and we use n i = 0 when the cycle is not traversed at all. For i = 1, . . . , m, θ i is the sequence of actions that labels the transition from q i-1 to q i .

We say that the run in eq. ( 9) is minimal if for all i = 1, . . . , m, z i is a minimal element in Pre[σ * i ](↑ z ′ i ) and n i is the smallest such z i = pr[σ n i i ](z ′ i ), and if z i = pr[σ n i i ](z ′ i ) for i = 0, . . . , m. By allowing z 0 x, it is always possible to associate a minimal run with some reachability statement "(q, x) * -→ (q ′ , y)" and use the tuple

q 0 , z 0 , n 0 , z ′ 0 , q 1 , z 1 , n 1 , z ′ 1 , . . . , q m , z m , n m , y (10)
as a witness of reachability. We now try to bound the size of such a witness. One has

|z ′ m | = |y| , |z i | ≤ |z ′ i | + n i | rea(σ i )| , |z ′ i-1 | ≤ |z i | + | rea(θ i )| , (11)
for all i. We further know from Theorem 3.7, that Unfortunately, as Example 3.9 shows, these bounds cannot be much improved upon.

n i ≤ |z ′ i |(1 + | rea(σ i )|) for i =
Example 3.9. Consider the flat LCM S depicted in fig. 1. In S, (q 0 , ε) * -→ (q ′ 0 , ε) is witnessed by the following run schema Figure 1: A flat LCM where (q 0 , ε) * -→ (q ′ 0 , ε) requires exponential-sized configurations.

(q 0 , ε) -→ (q 1 , ab) * -→ (q 1 , ba 2 ) -→ (q 2 , a 2 b) * -→ (q 2 , ba 4 ) -→ (q 3 , a 4 b) * -→ • • • * -→ (q n , ba 2 n ) - → (q ′ n , a 2 n b) * -→ (q ′ n , ba 2 n-1 ) -→ (q ′ n-1 , a 2 n-1 b) q0 q1 q2 q3 • • • qn q ′ n q ′ n-1 • • • q ′ 1 q ′ 0 ?a
In fact, there is only one run witnessing (q 0 , ε) * -→ (q ′ 0 , ε) and this run necessarily visits (q n , ba 2 n ), a configuration of exponential size, iterating 2 n-1 times the cycle on q n . Observe that, starting from (q 0 , ε), any message loss will prevent ever reaching q ′ 0 .

SLP-compressed words and an NP algorithm for reachability

In this section we explain how the exponentially long minimal runs analysed in Section 3.3 can be handled efficiently using SLP-compressed words. This provides witnesses of polynomial size that can be validated in polynomial time, thus showing that reachability in flat LCMs is in NP.

SLP-compressed words

Compressed words are data structures used to represent long words via succinct encodings. If a long word is rather repetitive, it can have a succinct encoding of logarithmic size. Since several operations on long words or decision tests about them can be performed efficiently on the succinct representation, compressed words have been used to provide efficient solutions to algorithmic problems involving exponential-size (but rather repetitive) words, see [START_REF] Lohrey | Algorithmics on SLP-compressed strings: A survey[END_REF] for a survey. The most studied encoding is the SLP, for Straight-Line Program, which is in effect an acyclic context-free grammar that generates a single word, called its expansion.

From now on, we always use small letters x, y, u, v for usual words, and capital letters X, Y, U, V for SLPs expanding to the corresponding words. Since SLPs are interpreted as plain words, we will use them freely in places where words can be used. It will always be clear when we consider the SLP as a data structure and then we use it to denote its expansion. The main situation where we want to distinguish between the two usages is when reasoning about size and algorithmic complexity: for this we write |X| for the length |x| of the expansion, while we write X for the size of the SLP as a data structure. For example, if X expands to x then for any fractional power of the form x p , there is an SLP

X p with |X p | = |x p | = p|x| and X p = O( X + log p).
In the rest of this section we will use well-known, or easy to prove, algorithmic results on SLP. In particular, all the following problems can be solved in polynomial time: length: Given a SLP X, compute |X|.

factor: Given a SLP X and two positions 0 ≤ i ≤ j ≤ |X|, construct a SLP of size O( X ) for the factor X[i : j].

concatenation: Given two SLPs X and Y , construct a SLP for X • Y .

Theorem 4.3. Deciding whether (q, x) * -→ (q ′ , y) in a flat LCM S is NP-complete.

Proof. NP-hardness is proven in Appendix C and we just provide a NP decision algorithm. As expected, the algorithm just guesses a SLP-based witness and checks that it is indeed a valid witness. For a positive instance of the problem, a witness exists and has polynomial size as shown in Lemma 4.2. Now checking that it is valid, i.e., that each Z i is indeed pr[σ n i ](Z ′ i ) etc., can be done in polynomial time as shown with Proposition 4.1.4

NP algorithms for liveness properties

We show in this section how, for flat LCMs, liveness properties like nontermination, unboundedness, and existence of a Büuchi run, effectively reduce to reachability. This only requires characterising and computing the set of configurations from which infinite runs are possible but Section 3 provides all the necessary tools.

With any sequence of channel actions σ we associate The set I σ , represented via pr[σ ω ](ε), is interesting because it characterises the configurations from which a σ-labelled cycle can be traversed infinitely many times, i.e., it characterises nontermination.

I σ def = k=0,1,2,... Pre[σ k ](Σ * ).
Indeed, the following lemma reduces nontermination to reachability:

Lemma 5.3 (Existence of infinite runs). (i) There exists an infinite sequence

x = x 0 σ -→x 1 σ -→x 2 • • • starting from x if,

and only if, pr[σ ω ](ε) x.

(ii) There exists an infinite run in S that starts from (q, x) and visits a given q ′ ∈ Q infinitely many times if, and only if, q ′ is on an elementary cycle of S and (q, x) * -→ (q ′ , pr[σ ω q ′ ](ε)).

Proof.

-→ x 1 σ -→ x 2 σ -→ • • • satisfies x 0 pr[σ k ](x k ) pr[σ k ](ε) for all k ∈ N. Thus pr[σ ω ](ε) = ⊥ and x = x 0 pr[σ ω ](ε).
(ii) is an immediate consequence of (i).

By combining the above lemmas with Theorem 4.3 and the NP-hardness results proven in Appendix C, one now obtains: Theorem 5.4. Nontermination and existence of a Büchi run are NP-complete for flat LCMs.

Remark 5.5 (Repeated coverability is NP-complete). Let us define more generally I σ (x) as k=0,1,2,... Pre[σ k ](↑ x), so that I σ really is shorthand for I σ (ε). For a location q on a σ qlabelled cycle, I σq (x) characterises a form of repeated coverability since y ∈ I σq (x) iff there is an infinite run from (q, y) such that the channel contains a superword of x every time q is (re)visited. Using some temporal logic, this could be written under the form

y ∈ I σq (x) ⇐⇒ (q, y) |= ∃ GFq ∧ G(q =⇒ chan ≥ x) .
The proof of Lemma 5.2 can be extended to the computation of I σ (x). One obtains

I σq (x) = ↑ y 0 ∩ ↑ y 1 ∩ • • • ∩ ↑ y K for some K in O(|σ| • |x|).
We deduce that the repeated coverability problem is in NP for flat LCMs, and is indeed NP-complete.

Note however that now the (y k ) k sequence does not necessarily satisfies y 0 y 1 , so that I σ (x) will have in general several minimal elements, and possibly exponentially many. In fact already ↑ y 0 ∩ ↑ y 1 may have exponentially many minimal elements (see [GLHK + 20, § 6.3]). Thus the NP-algorithm for repeated coverability represents I σ (x) as a conjunction of subword constraints, not via a set of minimal elements, but this is sufficient for its purposes.

Unboundedness reduces to reachability in a very similar way. We say that a sequence of actions σ is increasing if u ℓv v ℓv-1 (and (ii) There exists an infinite unbounded sequence

ℓ v > 0) for u def = rea(σ), v def = wri(σ)
x σ * -→ x 1 σ * -→ x 2 σ * -→ • • • with |x 1 | < |x 2 | < • • • . (iii) σ is increasing and x pr[σ ω ](ε).
Lemma 5.7 (Existence of unbounded runs). In a flat LCM, t.f.a.e. (i) The reachability set Post * (q, x) is infinite. (ii) There is an unbounded run starting from (q, x). (iii) (q, x) * -→ (q ′ , pr[σ ω q ′ ](ε)) for some control location q ′ with an increasing σ q ′ . Proof (sketch).

(ii =⇒ iii): In an unbounded run, there must be a control location q ′ that is visited infinitely many times with associated channel contents that are unbounded. Since from q ′ one can only return to q ′ by running through the cycle around q ′ , hence performing σ q ′ some number of times, the first visit of q ′ is some (q ′ , x ′ ) satisfying case (ii) of Lemma 5.6. We deduce that σ ′ q is increasing and that x ′ pr[σ ω q ′ ](ε) as in case (iii) of the Lemma. (iii =⇒ ii): by Lemma 5.6 there exists an unbounded run starting from (q ′ , pr[σ ω q ′ ](ε)). Hence there is one starting from (q, x). (i ⇐⇒ ii): is an application of Kőnig's Lemma, not specific to LCMs, see e.g. [START_REF] Ph | Lossy counter machines decidability cheat sheet[END_REF]§6].

We can thus reduce unboundedness to reachability of an increasing cycle. With the NP-hardness results proven in Appendix C, one now obtains: Theorem 5.8. Unboundedness for flat LCMs is NP-complete.

Conclusion

We analysed the behaviour of the backward-reachability algorithm for lossy channel machines when a cycle of channel actions can be performed arbitrarily many times. This provides complexity bounds on the size of runs that follow a bounded path scheme of the form σ * 1 ρ 1 σ * 2 ρ 2 . . . σ * m ρ m , with applications in the verification of flat systems, or in bounded verification for general systems. The main result is an NP upper bound for reachability and, by reduction, several other verification problems like unboundedness or existence of a Büchi run.

Natural directions for future work include extending our approach to deal with richer verification problems, like temporal logic model checking. It would also be interesting to consider more expressive models, like the partially lossy channel systems from [START_REF] Ch | Reachability problems on partially lossy queue automata[END_REF] or the higher-order lossy channel systems and priority channel systems from [START_REF] Ch | The power of priority channel systems[END_REF].

A Some SLP algorithms

We describe here some SLP algorithms that are not readily available in the literature (as far as we know). Formally, by "an SLP X" we mean a grammar (Σ, N, X, P ) where X ∈ N is the axiom (a non terminal), where Σ is the set of terminal letters, and where the production rules in P are either A i → a or A i → A j A k for some a ∈ Σ and some nonterminals A i , A j , A k with i < j, k. There exactly one production rule for each A i ∈ N , so that each A i defines a unique word L(A i ) ∈ Σ * .

A.1 Deciding X v n

Deciding X Y between SLPs is a difficult problem, PP-hard as show in [START_REF] Lohrey | Algorithmics on SLP-compressed strings: A survey[END_REF]. When x (or y) is a plain word, the problem has polynomial-time solutions [START_REF] Markey | A PTIME-complete matching problem for SLP-compressed words[END_REF][START_REF] Cégielski | Window subsequence problems for compressed texts[END_REF][START_REF] Yamamoto | Faster subsequence and don't-care pattern matching on compressed texts[END_REF].

Here we consider the special case where Y is some v n .

Proposition A.1. Deciding whether X v n , where X is an SLP, v is a plain word, and n is a fractional exponent, can be done in time O( X

• |v| + |v| 2 + log n).
Proof. For v = ε and some word x such that alph(x) ⊆ alph(v), let us define p(x, v) as the smallest fractional power such that x v p . Now p(x, v) satisfies the following equalities:

p(ε, v) = 0 p(a, v) = i |v| , if the first occurrence of a in v is at position i, p(x y, v) = p(x, v) + p(y, v (j) ), if p(x, v) is some q + j |v| with q ∈ N. (12)
Using eq. ( 12) leads to a dynamic programming algorithm computing p(X, v) for an SLP X. After checking that alph(X) ⊆ alph(v), one computes the values of all p(A, v (i) ) for i = 1, . . . , |v| and A a nonterminal in SLP X. Each of these O( X • |u|) values is computed in time O(1) if one precomputes the first occurrences of letters in the cyclic shifts of v, say in time O(|v| 2 ). Finally, one only has to compare p(X, v) with n.

A.2 Computing X/v k Proposition A.2. Building a SLP for X/v k , where X is an SLP, v is a plain word, and k ∈ N, can be done in time poly( X + |v| + log n).

Proof. For given ℓ, deciding whether X/v k has length at least ℓ is easy: One just applies the definition, builds an SLP X ′ for the suffix of length |X| -ℓ of X, and checks that it is a subword of v k with proposition A.1. Thus one can computes |X/v k | by finding the length of the result via dichotomic search, repeating the previous process log |X|, i.e., O( X ), times.5

B Forward reachability techniques

We collect in this section some proofs relying on forward-reachability analysis.

Let us reuse notations from [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF] and define a partial function x⊖u between channel contents as follows:

x ⊖ u def =            x if u = ε, undefined if x = ε and u = ε, x ′ ⊖ u ′ if x = ax ′ and u = au ′ for some a ∈ Σ, x ′ ⊖ u if x = ax ′ and u = bu ′ for some a = b ∈ Σ. ( 13
)
Observe that x ⊖ u is defined if, and only if, u x. Note also that, when x ⊖ u is defined, we can use monotonicity and commutation with concatenation:

if u x then for all x ′ :

x x ′ implies x ⊖ u x ′ ⊖ u , (x ⊖ u) • x ′ = (xx ′ ) ⊖ u . (14)
Now x ⊖ u captures the forward effects of ?u actions in LCMs:

Lemma B.1. x ?u -→ y iff y x ⊖ u.
We can also use ⊖ to characterise the outcome of arbitrary sequences of actions.

Lemma B.2. Let σ ∈ Act * Σ be an arbitrary sequence of actions.

x ′ σ -→ y for some x ′ x iff x σ -→ and y x • wri(σ) ⊖ rea(σ) .

Proof. By induction on the length of σ. The existential quantification on some x ′ x accounts for the case where σ = ε is the empty sequence.

For the inductive step, we consider two cases:

1. σ = !w • σ ′ : For the "=⇒" direction, x σ -→ y implies x ′ σ ′ -→ y for some x ′ xw, which implies

y x ′ w • wri(σ ′ ) ⊖ rea(σ ′ ) by ind. hyp., = x ′ • wri(σ) ⊖ rea(σ) since σ = !w • σ ′ , x • wri(σ) ⊖ rea(σ) by monotonicity.
For the "⇐=" direction, we know that y x. wri(σ) ⊖ rea(σ) = xw. wri(σ ′ ) ⊖ rea(σ ′ ), so the ind. hyp. tells us that x ′ σ ′ -→ y for some x ′ xw. We deduce

x !w -→ x ′ σ ′ -→ y.
2. σ = ?w • σ ′ : For the "=⇒" direction, x ′ σ -→ y implies x ′ ?w -→ x ′′ σ ′ -→ y for some x ′′ x ′ ⊖ w. We have

y x ′′ . wri(σ ′ ) ⊖ rea(σ ′ ) by ind. hyp., [x ⊖ w] • wri(σ ′ ) ⊖ rea(σ ′ ) by monotonicity, = x • wri(σ ′ ) ⊖ w • rea(σ ′ ) by (14), = (x • wri(σ)) ⊖ rea(σ) since σ = ?w • σ ′ .
For the "⇐=" direction, we know that x σ -→ hence in particular x ⊖ w is defined. We also know that y

x. wri(σ) ⊖ rea(σ) = x. wri(σ ′ ) ⊖ (w • rea(σ ′ )) = (x ⊖ w). wri(σ ′ ) ⊖ rea(σ ′ ), so by ind. hyp. there is some x ′ x ⊖ w with x ′ σ ′ -→ y for some

x ′ xw. We deduce x ?w -→ x ′ σ ′ -→ y.
B.1 Proof of Lemma 5.6

Write u, v for rea(σ), wri(σ).

(ii =⇒ iii): we only have to prove that σ q is increasing since Lemma 5.3 entails x pr[σ ω ](ε) already.

By assumption, there is a sequence x 1 , x 2 , . . . of channel contents of increasing length, and some numbers n 1 , n 2 , . . . in N such that x

σ n i --→x i . W.l.o.g. we can assume n 1 < n 2 < • • • . With Lemma B.2 we deduce x i (x v n i ) ⊖ u n i , hence u n i x i x v n i
, for all i = 1, 2, . . . If u = ε, σ is trivially increasing, so assume |u| > 0 and write m = |x|: we get u n i -m x i v n i for all i such that n i ≥ m. Now take i such that |x i | ≥ (m+1)|v| (and such that n i > m): we get u n i -m v n i -m-1 . We now applies Lemma 6.2 from [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF]: "if there is some k ≥ 1 such that w k 1 w k-1 2 (for two words w 1 , w 2 ), then in particular one can choose k = |w 2 |". This yields u |v| v |v|-1 , i.e., σ is increasing.

(iii =⇒ i): we assume that σ is increasing, i.e., u |v| v |v|-1 , and that x pr[σ ω q ](ε). The second assumption entails that x C NP-hardness for flat LCMs and flat FIFO machines LCMs are derived from FIFO automata [START_REF] Vauquelin | Automates à file[END_REF][START_REF] Brand | On communicating finite-state machines[END_REF] and our NP-hardness results apply to both models. FIFO automata, sometimes called queue automata, or communicating finite state machines, are reliable channel machines where messages are never lost. Their operational semantics is based on a reliable notion of steps, formally given by x For this S ϕ has to choose the line corresponding to one of the three literals in C 1 , in fact choose one literal made true by the valuation. During this check, the valuation is written back on the channel. Then S ϕ checks that the remaining clauses, C 2 to C m , are satisfied by the valuation, each time reading the valuation and writing it back on the channel. Finally, the last leg from V b to V e checks that no message has been lost during all this run.

I b 1 2 3 4 n I e • • • !0 !1 !0 !1 !0 !1 !0 !1 !0 !1 !0 !1 !$ C b 1 • • • ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?$ !$ • • • ?0 !0 ?1 !1 ?0 !0 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?$ !$ C e 1 • • • ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?$ !$ C b 2 C e m ?$ !$ • • • V b V e • • • ?0 ?1 ?0 ?1 ?0 ?1 ?0 ?1 ?0 ?1 ?0 ?1 ?$ Write some valuation v Check v |= C 1 (≡ v 1 ∨ ¬v 2 ∨ v 4 ) Check v |= C 2 ∧ • • • ∧ C m Check no losses occurred Figure 2: LCM S ϕ for satisfiability of ϕ = (v 1 ∨ ¬v 2 ∨ v 4 ) ∧ C 2 • • • ∧ C m .
It is now clear that (I b , ε) * -→ (V e , ε) in S ϕ if, and only if, ϕ is satisfiable. The reasoning holds for lossy LCMs and for reliable FIFO automata. We have thus reduced SAT to the reachability problem for both types of acyclic machines.

Remark C.1. The construction of S ϕ can be simplified at the cost of making the reduction perhaps less obviously correct: one can either omit the end-marker symbol $ since in the end the machine checks that no message was lost (thus a binary alphabet suffices), or one can stop the machine at C e m , getting rid of the V b to V e part, since the markers ensure that the valuation read while checking a clause C i is indeed the full valuation written at the previous stage.

For hardness of nontermination and unboundedness we adapt the previous reduction by adding a single cycle V e !$ -→ V e on the last control location. Starting from (I b , ε), the modified S ϕ has an infinite run iff it has an unbounded run iff ϕ is satisfiable.

The above reductions adapt to flat VASSes and lossy VASSes, i.e., channel machines with unary alphabet, provided that we allow 2n channels (or counters) for a valuation on n Boolean variables.

C.2 Proof of Theorem 2.2: NP-hardness for single-path machines

We first show hardness for reachability. For this we reduce from SAT. So let us consider a 3CNF formula ϕ with Boolean variables among

V = {v 1 , . . . , v n }. Let us say ϕ = (v 2 ∨ ¬v 3 ∨ ¬v n ) ∧ C 2 ∧ • • • ∧ C m , with m clauses.
With ϕ we associate S ϕ , the single-path flat LCM described in Figure 3. This LCM has O(mn 2 ) control locations6 , and is organised as a series of distinct operations on the channel contents. The operations are grouped in lines and we describe them informally.

0 start 0, 1 0, 2 0, n • • • !v 1 0v 2 0 • • • v n 0 ?v 1 !v 1 ?v 2 !v 2 ?v n !v n ?0 !0 ?0 !1 ?0 !0 ?0 !1 ?0 !0 ?0 !1 1, 1 1, 2 1, 3 1, 4 1, n • • • ?v 1 !v 1 ?v 2 !v 2 ?v 3 !v 3 ?v 4 !v 4 ?v n !v n ?0 !0 ?1 !1 ?0 !0 ?1 !1x ?0 !0x ?1 !1 ?0 !0x ?1 !1 2, 1 2, 2 2, n • • • ?x !x ?v 1 !v 1 ?v 1 x !xv 1 ?0 !0 ?0x !x0 ?1 !1 ?1x !x1 ?v 2 !v 2 ?v 2 x !xv 2 ?0 !0 ?0x !x0 ?1 !1 ?1x !x1 ?v n !v n ?v n x !xv n ?0 !0 ?0x !x0 ?1 !1 ?1x !x1 3, 1 3, 2 3, n • • • ?x ?v 1 !v 1 ?v 2 !v 2 ?v n !v n ?0 !0 ?1 !1 ?0 !0 ?1 !1 ?0 !0 ?1 !1 L 0 L 1 L 2,1 L 3 . . . f . . . • • • Repeat line above 2n -1 times • • • • • • Repeat lines L 1 to L 3 (2n + 2 lines each time) for remaining clauses C 2 , . . . , C m • • • Figure 3: Single-path LCM for satisfiability of ϕ = (v 2 ∨ ¬v 3 ∨ ¬v n ) ∧ C 2 • • • ∧ C m .
L 0 , choosing a valuation nondeterministically: S ϕ first write v 1 0v 2 0 . . . v n 0 on the channel. This is our encoding for the valuation that is 0 for all variables. Then S ϕ reads the valuation and write it back, possibly changing any 0 value with a 1 (this happens at the red-coloured actions), and thus picking an arbitrary valuation nondeterministically. Here we see how the v 1 , . . . , v n markers are used to check positions inside the valuation.

L 1 , marking where clause C 1 is validated: S ϕ now checks whether the valuation stored on the channel makes C 1 true. In this example, we assume that C 1 is v 2 ∨ ¬v 3 ∨ ¬v n . Again S ϕ reads the valuation and writes it back. However, if it reads v 2 1 or v 3 0 or v n 0, it writes it back followed by a special checkmark symbol x that "means C 1 has been validated" (see red actions). Note that as many as 3 occurrences of x can be inserted in the encoding of the valuation.

L 2,1 , pushing x to the head of the valuation encoding: S ϕ now pushes any checkmark symbol to the left. This is done along the L 2,1 line. While the valuation is read and written back as usual (black actions), any symbol preceding a x can swap position with it (red actions).

L 2,2 , . . . , L 2,2n , more pushing x to the left: this behaviour is repeated 2n times in total, so that any x can be pushed completely to the left of the valuation. In case of multiple occurrences of x, we just need one of them to reach the head of the valuation so we assume that the other ones will just be lost.

L 3 , checking that clause C 1 has been validated: Now S ϕ knows where to expect x.

The machine can only proceed if indeed a x is present in the channel, in front of the valuation, and thus if the valuation on the channel satisfies C 1 . The rest of the line reads and writes back the valuation, clearing it of any remaining x's.

Same treatment for the remaining clauses C 2 , . . . , C m : S ϕ now continues with similar locations and rules checking that the remaining clauses are validated.

Note that, once the valuation has been picked nondeterministically (in L 1 ), it cannot be modified. Also note that the machine will block if one of the v i markers is lost before the last clause has been validated. If one of the 0/1 values of the valuation is lost, this value cannot be used any more for checkmarking a validated clause. Such message losses do not lead to any incorrect behaviour, they can only hinder the validation of a clause.

Finally, starting from (0, ε), S ϕ can reach its final location f iff ϕ is satisfiable. Now the reduction extends to show prove NP-hardness of unboundedness for single-path LCMs with exactly the same adaptation as in the proof for acyclic LCMs. For hardness of nontermination a little more work is needed since every cycle where S ϕ reads the valuation and writes it back could become a nonterminating cycle if all but one letter are lost. One possible trick to overcome this is to have two copies of the alphabet, say of two different colours, and to ensure that in all its phases the machine reads in one colour and writes back in the other, so that the valuation is always read and written in alternating colours. Once this is implemented, the system cannot have infinite runs as is. Adding a single loop on f, the final control location, as we did for acyclic LCMs, now provides a correct reduction from SAT to nontermination for single-path LCMs.

The idea behind this reduction can easily be adapted so that it applies to single-path VASSes and lossy VASSes, or equivalently, to channel machines with a unary alphabet. One uses 2n channels (or counters) for storing the valuation and m distinct counters for marking the clauses that have been validated.

Restricting to a binary alphabet on a single channel is equally easy for reliable FIFO automata, but more difficult when message losses have to be taken care of. Therefore we won't attempt it in this preliminary version.

D Multiple channels

The analysis we conducted in Section 3 carries over without any difficulty to systems with multiple channels. Lemma 3.3 and Theorem 3.4 remain valid since, once σ and k have been fixed, computing pr[σ k ]( x 1 , . . . , x c ) for a system with c channels can be done independently for each of the c channels: one only needs to distribute the actions on σ to their corresponding channel, so that rea(σ) now is some tuple u 1 , . . . , u c . In particular the bound in Theorem 3.7 becomes L σ, x 1 , . . . , x c ≤ max c i=1 |x i | • (|u i | + 1) , where rea(σ) = u 1 , . . . , u c .

  ) and we just have to invoke Lemma 3.3 (and set l k = 0). (ii) Computing κ takes time O(|x| + |σ|). If k ≤ κ, comparing k with κ and computing p k and ℓ k takes additional time O(|x| + |σ| + log k).

  decreasing. Since the p k fractions are multiples of 1 |u| , the sequence (p k ) k≥k 0 can only take 1 + |u|k 0 different values and eventually yield p k = p k+1 for some k ≤ k 0 + k 0 |u| ≤ |x|(|u| + 1), entailing L(σ, x) ≤ |x|(|u| + 1) as claimed.

  Example 3.8 (Bounds for L(σ, x) are tight.). For σ = !ab 5 ?b 4 and x = a 4 , the (y k ) k sequence withy k def = pr[σ k ](x) is: |x|=l 0 >l 1 >•••>l 4 =0 k 0 =4=p k 0 ∧p 4 ≥p 5 ≥p 6 •••Since y 20 y 21 is the earliest increasing pair, Definition 3.5 gives L(!ab 5 ?b 4 , a 4 ) = 20. This generalises to L(!ab n+1 ?b n , a m ) = m(n + 1) for any n, m ∈ N, which is exactly the |x|(| rea(σ)| + 1) bound given by Theorem 3.7.

  0, . . . , m. Thus, writing n for the size |S| + |x| + |y| of the instance (so that m ≤ n, and | rea(σ i )|, | rea(θ i )| ≤ n for all i), we have quadratic bounds O(n 2 ) for n m and |z m |, cubic bounds O(n 3 ) for n m-1 and |z m-1 |, . . . , etc., so that the witness has size O(n m ), hence 2 O(n) .

  Lemma 5.1. I σ ⊆ Σ * is an upward-closed set of channel contents. It has a single minimal element or is empty. Proof. Write (y k ) k∈N for the sequence y 0 def = ε and y k+1 = pr[σ](y k ). Then Pre[σ k ](Σ * ) = ↑ y k for all k ∈ N (Definition 3.1) andI σ = k∈N Pre[σ k ](Σ * ) = k ↑ y k . From y 0 y 1 and monotonicity of pr (Lemma 3.2) we obtain y 0 y 1 y 2 • • • and ↑ y 0 ⊇ ↑ y 1 ⊇ ↑ y 2 ⊇ • • • . Thus we have I σ = k∈N ↑ y k = ↑ y K if y K = y K+1 for some K, ∅ if the (y k ) k∈N sequence is strictly increasing. We write pr[σ ω ](ε) = y if I σ = ↑ y,and pr[σ ω ](ε) = ⊥ if I σ is empty. Lemma 5.2. pr[σ ω ](ε) can be computed in time O(|σ| 3 ). Proof (sketch). We start computing the elements y 0 , y 1 , y 2 , . . . of the (y k ) k sequence. If two consecutive values y K and y K+1 coincide, we have found pr[σ ω ](ε). Otherwise we continue while the sequence is strictly increasing until eventually |y k | > | rea(σ)| for some k (indeed, some k ≤ 1 + |σ|). In this case we can invoke Lemma 3.3.(ii) and conclude that the (y k ) k sequence will remain strictly increasing, hence pr[σ ω ](ε) = ⊥. For complexity, we note that each y k+1 is obtained in time O(|σ| + |y k |) and has length in O(|σ| 2 ) since |y k+1 | ≤ |y k | + | rea(σ)| for all k.

  (i) Write y for pr[σ ω ](ε). The proof of Lemma 5.2 shows that, unless y = ⊥, y = pr[σ](y) and thus y σ -→ y. (⇐=): Since x y, we have x σ • • if σ = ε, and x σ • • in the degenerate case where σ = ε. (=⇒): We assume σ = ε since otherwise x ε = pr[σ ω ](ε) holds trivially. The infinite sequence x 0 σ

and ℓ v def =

 def |v|. Now pr[σ ω ](ε) and increasingness of σ characterise unbounded reachability sets. Lemma 5.6 (Proof in Appendix B.1). Let x ∈ Σ * be some channel contents and σ a sequence of channel actions. T.f.a.e.: (i) For all k ∈ N there exists x k with x σ * -→ x k and |x k | ≥ k.

  all n. The first assumption entails v k xv k|v| ⊖u k|v| , hence x σ k|v| --→ v k by Lemma B.2, for all k ∈ N.(i =⇒ ii): is an application of Kőnig's Lemma, not specific to LCMs, see e.g.[START_REF] Ph | Lossy counter machines decidability cheat sheet[END_REF] §6].

  y def ⇐⇒ wy = x, to be compared with Equation (2). This is extended to x σ -→ rel y, c * -→ rel c ′ , etc., as for LCMs. C.1 Proof of Theorem 2.1: NP-hardness for acyclic machines We first show hardness for reachability and reduce from SAT. Let ϕ = C 1 ∧ • • • ∧ C m be a 3CNF with Boolean variables among V = {v 1 , . . . , v n }. With ϕ we associate a machine S ϕ as illustrated below in fig. 2. Let us explain informally how S ϕ operates. Starting from I b it first reaches I e while writing in the channel a word of the form w $ with w ∈ {0, 1} n . This word encodes a valuation of the Boolean variables and carries an end marker $. Then S ϕ crosses from C b 1 to C e 1 : this requires reading the valuation on the channel and checking that it satisfies C 1 .

Flatness remains relevant with finite-state systems, see e.g.,[START_REF] Kuhtz | Weak Kripke structures and LTL[END_REF]. This is especially true when one is considering the verification of properties expressed in a rich logic as in, e.g., [DHL + 17]. In language theory, flat finite-state automata correspond to regular languages of polynomial density, sometimes called sparse languages, or also bounded languages.

See Appendix D for a generalisation of our results to multi-channel machines.

In the finite-automata literature, "acyclic automata" sometimes allow self-loops.

In fact, it is sufficient to guess the exponents n1, . . . , nm for the σi's since the Zi, Z ′ i 's can be computed from them.

A better, dynamic programming, algorithm exists but here we aim for the simplest feasability proof.

Our reduction insists on using only one channel. With multiple channels the same idea would use O(n + m) control locations.

Acknowledgements

We thank A. Finkel who raised the issue of flatness in lossy channel systems. We also thank J. Leoux and S. Halfon for useful comments that helped improve this paper.

matching: Given two SLPs X and Y , decide if X is a factor (or a prefix, or a suffix) of Y .

To this list we add results tailored to our needs:

(scattered) subword with a power word: Given a SLP X, a plain word v and some power k ∈ N, decide if X v k . This special case of the fully compressed subsequence test can be done in time poly( X + |v| + log k), see Proposition A.1 in the Appendix.

iterated LCM predecessor: Given a SLP X, a plain word v, and some power k ∈ N, compute a SLP for X/v k , i.e., for pr[(!v) k ](X). This can be done in time poly( X + |v| + log k), see Proposition A.2 in the Appendix.

With the above results, we are ready to lift the computation of pr[σ k ](x) from plain words to SLPs: Proposition 4.1. Given an SLP X, a sequence of actions σ, and some k ∈ N, it possible to compute an SLP Y for pr[σ k ](X) in time poly( X + |σ| + log k).

Proof (sketch). We follow the construction described in the proof of Theorem 3.4, now using SLPs. So again let us write u and v for rea(σ) and wri(σ).

The first step is to compute κ. This is done by dichotomic search, since we can decide in polynomial time whether a candidate n leads to X/v n = ε. We then build X <ℓκ as X/v κ .

If k ≤ κ, we build a SLP Y for u k • (X/v k ) and we are done.

If k ≥ κ + 1, we compute a SLP for y κ+1 = u p κ+1 by applying pr[σ] on a SLP for y κ = u κ •x <ℓκ : this involves computing a SSS involving at most 2m operations like prefixing by a i or computing Y /b j . This is done in polynomial time and the exponent in u p κ+1 can be computed by dividing the length of a SLP with the length of u. From there we continue as in the proof of Theorem 3.4. This involves performing a polynomial number of simple pr operations and some simple reasoning on the exponents.

Reachability for flat LCMs is in NP

We now explain how eq. ( 10) can be replaced by an SLP-based witness of the form

Lemma 4.2. If q 0 , z 0 , n 0 , z ′ 0 , q 1 , n 1 , z 1 , z ′ 1 , . . . , q m , z m , n m , y is a minimal witness for (q, x) * -→(q ′ , y) in S, then there exist SLPs Z 0 , Z ′ 0 , Z 1 , . . . , Z m , Y representing z 0 , z ′ 0 , z 1 , . . . , z m , y that have size polynomial in |S| + |y|.

Proof. By induction on m -i. We start with Y for y which does not need any compression (and let Z ′ m = Y for the inductive reasoning). Then any Z i has the shape

) and is easily obtained from Z i and θ i according to eq. ( 6). One can ensure that Z ′ i is in O( Z i + |S|). Finally, and since each SLP has size linearly bounded in the size of the following one (the bounds propagate from right to left), we have a quadratic bound on the individual sizes for the Z i and Z ′ i , hence a cubic bound on the SLP witness overall (recall that the n i , written in binary, have size O(|S|)).