Stéphane Demri

Arnaud Sangnier

When Model-Checking Freeze LTL over Counter Machines Becomes Decidable

We study the decidability status of model-checking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable (reversal-bounded counter machines, vector additions systems with states, flat counter machines, one-counter machines). In freeze LTL, a register can store a counter value and at some future position an equality test can be done between a register and a counter value. Herein, we complete an earlier work started on one-counter machines by considering other subclasses of counter machines, and especially the class of reversal-bounded counter machines. This gives us the opportuniy to provide a systematic classification that distinguishes determinism vs. nondeterminism and we consider subclasses of formulae by restricting the set of atomic formulae or/and the polarity of the occurrences of the freeze operators, leading to the flat fragment.

Introduction

Counter machines. Counter machines are ubiquitous computational models that provide a natural class of infinite-state transition systems, suitable for modeling various applications such as broadcast protocols [START_REF] Esparza | On the verification of broadcast protocols[END_REF], time granularities [START_REF] Lago | On the equivalence of automaton-based representations of time granularities[END_REF] and programs with pointer variables [START_REF] Bouajjani | Programs with lists are counter automata[END_REF], to quote a few examples. They are also known to be closely related to data logics for which decision procedures can be designed relying on those for counter machines, see e.g. remarkable examples in [START_REF] Bojańczyk | Two-variable logic on words with data[END_REF][START_REF] Björklund | Bounded depth data trees[END_REF]. When dealing with this class of models, most interesting reachability problems are undecidable but subclasses leading to decidability have been designed including reversal-bounded counter machines [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], onecounter machines [START_REF] Ibarra | Restricted one-counter machines with undecidable universe problems[END_REF], flat counter machines [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF] and vector addition systems with states (see e.g. [START_REF] Reutenauer | The Mathematics of Petri nets[END_REF]). Model-checking with Freeze LTL. In order to verify properties on counter machines, we aim at comparing counter values and we shall use the so-called freeze operator. The freeze quantifier in real-time logics has been introduced in the logic TPTL, see e.g. [START_REF] Alur | A really temporal logic[END_REF]. The formula x • φ(x) binds the variable x to the time t of the current state: x • φ(x) is semantically equivalent to φ(t). This variable-binding mechanism, quite natural when rephrased in first-order logic, is present in various logical formalisms including for example hybrid logics [START_REF] Goranko | Hierarchies of modal and temporal logics with references pointers[END_REF][START_REF] Areces | A road-map on complexity for hybrid logics[END_REF], freeze LTL [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF] and predicate λ-abstraction [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF]. Freeze LTL is a powerful extension of LTL that allows to store counter values in registers. Infinitary satisfiability restricted to one register is already undecidable [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF] just as modelchecking for nondeterministic one-counter machines [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF], which is quite unexpected since one-counter machines seem to be harmless operational models. Moreover, there is some hope that model-checking happens to be more tractable than satisfiability since more constraints are requested on models viewed as runs. Our contribution. We carry on with the quest started in [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF] to determine which classes of counter machines admit decidable model-checking with freeze LTL. In the paper, we consider the above-mentioned classes of counter machines for which the reachability problem is decidable. We provide an exhaustive analysis completing [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF]; some results are obtained by adequately adapting known results to our framework or by designing simple reductions. However, at each position, we may have to deal with more than one counter values. Our main technical contributions allow us to establish the following results with a special focus on reversal-bounded counter machines.

-Model-checking freeze LTL (written MC ω (LTL ↓ )) over deterministic vector addition systems with states and deterministic reversal-bounded counter machines is decidable (see Corollary 11). However, MC ω (LTL ↓ ) over reversal-bounded counter machines is undecidable, even when restricted to one register (see Theorem 7). -MC ω (LTL ↓ ) restricted to flat formulae over reversal-bounded counter machines is decidable (see Corollary 17) as well as the restriction to positively flat formulae over one-counter machines (see Theorem 18), partly by taking advantage of recent results about parameterized one-counter machines [START_REF] Haase | Reachability in succinct and parametric one-counter automata[END_REF].

A complete summary can be found in Section 8. As a nice by-product of the classification we made, we show a tight relationship between reachability problems for parameterized counter machines and model-checking counter machines over the flat fragment of freeze LTL (see Section 7.2). Besides, we believe that the principles underlying our undecidability proof for MC ω (LTL ↓ ) over reversal-bounded counter machines could be reused for other problems on such counter machines. Because of lack of space, omitted proofs can be found in [START_REF] Demri | When Model-Checking Freeze LTL over Counter Machines Becomes Decidable[END_REF].

Standard Classes of Counter Machines

In this section, we recall standard definitions about various classes of counter machines. We write N [resp. Z] for the set of natural numbers [resp. integers]. Given a dimension n ≥ 1 and k ∈ Z, we write k to denote the vector with all values equal to k and e i to denote the unit vector for i ∈ {1, . . . , n}. We recall that a semilinear set of N n is a finite union of linear sets. We often refer to Presburger arithmetic which consists of first-order logic over the structure N, 0, ≤, + (and more generally over Z, 0, ≤, + ) [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]. It is known that a subset of N k is semilinear if and only if it is definable by a formula in Presburger arithmetic [START_REF] Ginsburg | Semigroups, presburger formulas, and languages[END_REF].

Counter machines

A counter machine M is defined as a tuple n, Q, ∆, q 0 where n

≥ 1 is the dimension of M , Q is a finite set of control states, ∆ ⊆ Q × G × A × Q is a finite set of transitions
where G = {zero, true} n is the finite set of guards and A = {-1, 0, 1} n is the finite set of actions, and q 0 ∈ Q is the initial control state. Given a counter machine M , we introduce the transition system T S(M

) = Q × N n , - → where Q × N n is the set of configurations and - →⊆ (Q × N n ) × (Q × N n ) is the transition relation: for q, v , q , v ∈ Q × N n , we have q, v - → q , v def
⇔ there exists a transition t = q, g, a, q ∈ ∆ such that: v = v + a and for 1 ≤ c ≤ n, g(c) = zero implies v(c) = 0. We write * -→ to denote the reflexive and transitive closure of -→ and the reachability set of M is Reach(M )

def = { q, v | q 0 , 0 * - → q, v }.
Observe that this reachability set implicitly depends on the initial configuration q 0 , 0 : this is all what we need in the sequel. A finite (resp. infinite) run in T S(M ) is a finite (resp. infinite) sequence ρ = q 0 , 0 -→ q 1 , v 1 -→ . . .. A counter machine M is deterministic (also known as single-path) whenever for each q, v ∈ Reach(M ), there is at most one configuration q , v such that q, v -→ q , v . In the sequel, we shall use Minsky machines that form a special class of deterministic 2-counter machines.

We present below two types of decision problems when C is a class of counter machines. The reachability problem for the class C is defined as follows: given a machine M ∈ C and a configuration q, v , does q 0 , 0 * -→ q, v ? Similarly, the generalized repeated reachability problem for the class C is defined as follows: given a counter machine M ∈ C and N sets F 1 , . . . , F N of control states, is there a run of M such that for 1 ≤ i ≤ N , there is a control state in F i that is repeated infinitely often? 1CM. One-counter machines are naturally defined as counter machines of dimension one. Various logical formalisms have been introduced to specify the behavior of onecounter machines, including Freeze LTL [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF] and EF logic [START_REF] Göller | On the computational complexity of verifying one-counter processes[END_REF]. When one-counter machines are enriched by a finite alphabet (so that transitions are labelled), the universality problem is undecidable [START_REF] Ibarra | Restricted one-counter machines with undecidable universe problems[END_REF], witnessing that this simple operational model can lead to natural undecidable problems. VASS. Vector addition systems with states (a.k.a. VASS) are known to be equivalent to Petri nets, see e.g. [START_REF] Reutenauer | The Mathematics of Petri nets[END_REF], and they correspond to counter machines without zero-tests, i.e. each guard has no component equal to zero. To be precise, we are a bit less liberal than the usual definition since we only consider actions in {-1, 0, 1} n (instead of Z n ) but this does not make a real difference for all the developments made in this paper. Flat counter machines. A directed graph G = V, E (with V ⊆ E × E) is said to be flat whenever each vertex belongs to at most one cycle (path for which the initial and final vertices coincide). A counter machine n, Q, ∆, q 0 is flat whenever (1) between two control states there is at most one transition and (2) the directed graph Q, { q, q ∈ Q 2 : q, g, a, q ∈ ∆} is flat. Reachability problems have been considered for flat counter machines in [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF]; for instance it is proved that flat counter machines have an effectively computable semilinear set [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF], see also [START_REF] Bozga | Flat parametric counter automata[END_REF].

Reversal-bounded counter machines

The class of reversal-bounded counter machines has been introduced in [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] by considering the following restriction: each counter performs only a bounded number of alternations between increasing and decreasing mode. This class of counter machines is particularly interesting because it has been shown that each reversal-bounded counter ma-chine has a semilinear reachability set which can be effectively computed. We present now a more general class of counter machines proposed in [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF]. Given a bound b ∈ N, we consider the number of alternations between increasing and decreasing mode when the value of the considered counter is above b; if for each counter this number of alternations is bounded by a constant k ∈ N, we say that the counter machine is k-reversalb-bounded. From now on, we say that a counter machine M is reversal-bounded if there exist k, b ∈ N such that M is k-reversal-b-bounded and in the sequel, when reversalbounded counter machines are part of the instances of some decision problems, we assume that they come with their k and b. As mentioned in [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF], the above-defined class of reversal-bounded counter machines contains those defined in [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] and it also contains the counter machines for which the set of reachable configurations is finite. To make the distinction, we will call the machines introduced in [25] Ibarra reversalbounded counter machines. In [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF], the authors prove that the reachability problem is decidable for reversal-bounded counter machines (in fact their reachability set is also an effectively computable semilinear set) and in [START_REF] Sangnier | Vérification de systèmes avec compteurs et pointeurs[END_REF] it is proved that the generalized repeated reachability problem for this class of machines is also decidable when considering only one set of control states to be repeated infinitely often. The proof of this last result relies on the fact that this problem is decidable for Ibarra reversal-bounded counter machines [START_REF] Dang | Liveness verification of reversal-bounded multicounter machines with a free counter[END_REF]. Note that we can easily reduce the generalized reachability problem with N ≥ 1 sets of control states to its restriction to only one set (the same way the emptiness problem for generalized Bûchi automata can be reduced to the emptiness problem for Büchi automata).

Theorem 1. The generalized repeated reachability problem for reversal-bounded counter machines is decidable.

LTL with the Freeze Operator

In this section, we present a variant of temporal logic LTL with registers (also known as Freeze LTL) in order to reason about runs from counter machines. In [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF], LTL with registers is used to specify properties about one-counter machines. The datum stored in a register is the current counter value and equality tests are performed between a register value and the current counter value. When dealing with counter machines, a register can store the value of a counter c and test it later against the value of counter c with possibly c = c . Below, we present different ways to restrict the equality tests between registers and counters.

Given a finite set Q of control states (possibly empty) and n ≥ 1, the formulae of the logic LTL ↓ [Q, n] are defined as follows:

φ ::= q | ↑ c r | ¬φ | φ ∧ φ | φ ∨ φ | φUφ | φRφ | Xφ | ↓ c r φ
where q ∈ Q, c ∈ {1, . . . , n} and r ∈ (N \ {0}). Intuitively, the modality ↓ c r is used to store the value of the counter c into the register r; the atomic formula ↑ c r holds true if the value stored in the register r is equal to the current value of the counter c. An occurrence of ↑ c r within the scope of some freeze quantifier ↓ c r is bound by it; otherwise it is free. A sentence is a formula with no free occurrence of any ↑ c r .

Models of LTL ↓ [Q, n] are runs of transition systems from counter machines of dimension n and with a set of control states containing Q. Given a counter machine n, Q , ∆, q 0 with Q ⊆ Q and a run ρ, we write |ρ| to denote its length in ω + 1 and the ith configuration (0 ≤ i < |ρ|) is denoted by q i , v i . A counter valuation f is a finite partial map from N \ {0} to N. Note that whenever f (r) is undefined, the atomic formula ↑ c r is interpreted as false. Given a run ρ and a position 0 ≤ i < |ρ|, the satisfaction relation |= is defined as follows (Boolean clauses are omitted):

ρ, i |= f q def ⇔ q i = q ρ, i |= f ↑ c r def ⇔ r ∈ dom(f ) and f (r) = v i (c) ρ, i |= f Xφ def ⇔ i + 1 < |ρ| and ρ, i + 1 |= f φ ρ, i |= f φ 1 Uφ 2 def ⇔ for some i ≤ j < |ρ|, ρ, j |= f φ 2
and for all i ≤ j < j, we have ρ, j

|= f φ 1 ρ, i |= f φ 1 Rφ 2 def ⇔ for all i ≤ j < |ρ|, ρ, j |= f φ 2 or for some i ≤ j < |ρ|, ρ, j |= f φ 1 and for all i ≤ k ≤ j, ρ, k |= f φ 2 ρ, i |= f ↓ c r φ def ⇔ ρ, i |= f [r →vi(c)] φ f [r → v i (c)]
denotes the register valuation equal to f except that the register r is mapped to v i (c). In the sequel, we omit the subscript "f " in |= f when sentences are involved. We use the standard abbreviations for the temporal operators (G, F, . . . ) and for the Boolean operators and constants (⇒, , ⊥, . . . ). We defined below fragments of LTL ↓ [Q, n] by restricting the use of the freeze operators. The strict fragment, written LTL ↓,s [Q, n], consists in associating a unique counter to each register (to store and to test). More precisely, a formula φ in LTL ↓,s [Q, n] verifies the following syntactic property: if ↓ c r ψ is a subformula of φ, then φ has not subformulae of the form either ↑ c r or ↓ c r ψ with c = c . We also write LTL[Q] to denote the fragment of LTL ↓ [Q, n] in which the atomic formulae of the form ↑ c r are forbidden (and therefore ↓ c r becomes also useless). Model-checking problems. The infinitary (existential) model-checking problem over counter machines, written MC ω (LTL ↓ [•, •]), is defined as follows: given a counter machine M = n, Q , ∆, q 0 and a sentence φ

∈ LTL ↓ [Q, n] with Q ⊆ Q , is there an infinite run ρ such that ρ, 0 |= φ? If the answer is "yes", we write M |= ω φ. The subproblem of MC ω (LTL ↓ [•, •]) with formulae restricted to LTL ↓,s [Q, n] is written MC ω (LTL ↓,s [•, •]). Given n ≥ 1, we write MC ω (LTL ↓ [•, n]) to denote the subprob- lem of MC ω (LTL ↓ [•, •]) with counter machines of dimension at most n. Similarly, we write MC ω (LTL ↓ [∅, •]) to denote the subproblem of MC ω (LTL ↓ [•, •]
) with no atomic formula made of control states. Similar notations are used with other fragments of

LTL ↓ [Q, n].
In this existential version of model checking, this problem can be viewed as a variant of satisfiability in which satisfaction of a formula can be only witnessed within a specific class of data words, namely the runs of the counter machine. Note that results for the universal version of model checking will follow easily from those for the existential version when considering fragments closed under negation or deterministic counter machines.

Flat formulae. We say that the occurrence of a subformula in a formula is positive if it occurs under an even number of negations, otherwise it is negative. Let L be a fragment of LTL ↓ [Q, n]. The flat fragment of L, written flat-L, is the restriction of L where, for any occurrence of φ 1 Uφ 2 [resp. φ 2 Rφ 1 ], if it is positive then the freeze operator ↓ does not occur in φ 1 , and if it is negative then the freeze operator ↓ does not occur in φ 2 . A formula is positively flat when it is flat and no occurrence of the freeze operator ↑ occurs in the scope of an odd number of negations. For example, the formula below belongs to the positively flat fragment and it states that sometimes there is a value of the counter 1 such that (1) infinitely often counter 2 takes that value if and only if infinitely often counter 3 takes that value and (2) from some future position, the counter 4 has always that value:

F ↓ 1 1 [(GF ↑ 2 1 ⇔ GF ↑ 3 1 ) ∧ FG ↑ 4 1 ].
Considering flat fragments remains a standard means to regain decidability: for instance flat fragments of LTL variants have been studied in [START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Bouyer | The cost of punctuality[END_REF] (see also in [START_REF] Ibarra | On removing the stack from reachability constructions[END_REF]Section 5] the design of a flat logical temporal language for model-checking pushdown machines). Section 7 shall illustrate that flatness can lead to decidability but this is not always the case.

Preliminary Results

In this section, we present preliminary results that will be helpful to strenghten forthcoming results and we present results for flat counter machines and one-counter machines based on existing works. We shall study the effects of restricting the set of atomic formulae, for instance by allowing only atomic formulae that are control states [resp. that are of the form ↑ c r ].

Purification, or how to get rid of control states

Control states can be viewed as an internal piece of information about the counter machines and therefore, it is interesting to understand whether the absence of control states among the set of atomic formulae (called herein purification) makes a difference. Lemma 2 below roughly shows that control states can be always encoded by patterns for various classes of counter machines.

Lemma 2.

Given a counter machine M = n, Q, ∆, q 0 and a sentence φ in LTL ↓ [Q, n], one can build in logspace a counter machine M P = n + 1, Q P , ∆ P , q 0 and a formula

φ P ∈ LTL ↓ [∅, n + 1] such that M |= ω φ iff M P |= ω φ P . Moreover, M is deterministic [resp. reversal-bounded, flat] iff M P is deterministic [resp. reversal-bounded, flat] and φ ∈ LTL ↓,s [Q, n] iff φ P ∈ LTL ↓,s [∅, n + 1].
The proof consists in introducing an additional counter whose behavior in M P encodes the control states from M . The reduction in the proof of Lemma 2 does not preserve the number of counters; however, a purification lemma can be also established for the class of one-counter machines as shown in [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF]. By the way, the construction in [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF] could be also adapted to encode control states by patterns however, it does not preserve reversal-boundedness.

Restricting the atomic formulae to control states

Before considering decidability issues with the freeze operator, it is legitimate to wonder what happens when the atomic formulae are restricted to control states. We show below that for all subclasses of counter machines considered in this paper, this restriction leads to decidability (for flat counter machines, the proof is postponed to the next subsection). Basically, the proof is a consequence of the two following properties: LTL formulae can be translated into equivalent Büchi automata (see e.g. [START_REF] Vardi | Reasoning about infinite computations[END_REF]) and repeated reachability problem is decidable for the concerned subclasses of counter machines.

Theorem 3. MC ω (LTL[•]
) restricted to one-counter machines, VASS, and reversalbounded counter machines is decidable.

Existing results for two subclasses

In this paper, we wish to provide a complete classification with respect to the abovementioned subclasses. The two following results are known results recasted in our context. First, we observe that LTL ↓ [Q, n] can be viewed as a fragment of the temporal logic FOCTL (Pr) [START_REF] Demri | Towards a model-checker for counter systems[END_REF] which extends the logic CTL by allowing the use of Presburger formulae as atomic propositions to describe sets of configurations for a counter machine. Since model-checking FOCTL (Pr) over flat counter machines is decidable [START_REF] Demri | Towards a model-checker for counter systems[END_REF], we establish the following theorem.

Theorem 4. MC ω (LTL ↓ [•, •]) restricted to flat counter machines is decidable.
Moreover, in [START_REF] Demri | Model checking freeze LTL over one-counter automata[END_REF], the authors obtain the following results concerning the model-checking of LTL with registers over one-counter machines.

Theorem 5. [15] (I) MC ω (LTL ↓ [•, 1]) is undecidable. (II) MC ω (LTL ↓ [•, 1]
) restricted to deterministic one-counter machines is PSPACE-complete.

Nondeterministic Counter Machines

Herein, we consider the model-checking problems over LTL ↓ [Q, n] for nondeterministic counter machines. We have seen that for the class of one-counter machines the problem is undecidable (see Theorem 5(I)) whereas it is decidable for flat counter machines (see Theorem 4). First, we observe that zero-tests can be easily encoded in LTL ↓ [Q, n] by first storing the initial value of counters in some register r 0 and then performing a zero-test on counter c with the atomic formula ↑ c r0 .

Theorem 6. MC ω (LTL ↓ [•, •]) restricted to VASS and to positively flat formulae with at most one register is undecidable.

The proof is based on a simple encoding of zero-tests. For what concerns reversalbounded counter machines, we have the following result:

Theorem 7. MC ω (LTL ↓ [•, 4]
) restricted to reversal-bounded counter machines and to formulae with at most one register is undecidable.

To prove this result, we present a reduction from the halting problem for Minsky machines; note that a similar reduction is used in [START_REF] Ibarra | Counter machines and verification problems[END_REF] in order to prove that in reversalbounded counter machines extended with equality tests between distinct counters, the reachability problem is undecidable.

Proof. (sketch) Let M = 2, Q, ∆, q 0 be a Minsky machine (deterministic counter machine with two counters) and q F ∈ Q be a final control state with no transition from it. Without any loss of generality, we can assume that if q, g, a, q ∈ ∆ performs a decrementation, then the transition is of the form q, true, -e c , q for some c ∈ {1, 2}. Moreover, for q, q ∈ Q, the set { g, a : q, g, a, q ∈ ∆} contains at most one element. Let us build the reversal-bounded counter machine M = 4, Q , ∆ , (q 0 ) ∅ as follows:

-Q = {q X : q ∈ Q, X ⊆ {1, 2}} (X records on which counter of M zero-test is needed next), -∆ is the smallest set of transitions satisfying the conditions below:

• for X ⊆ {1, 2}, (q 0 ) ∅ , true, 0, (q 0 ) X ∈ ∆ ,

• for all q, g, a, q ∈ ∆, we have q 1 , true, a , q 1 ∈ ∆ assuming that * q 1 = q X with X = {c ∈ {1, 2} :

g(c) = zero}, * for c ∈ {1, 2}, • a(c) = 1 implies a (c) = 1 and a (c + 2) = 0, • a(c) = -1 implies a (c) = 0 and a (c + 2) = 1, • a(c) = 0 implies a (c) = a (c + 2) = 0. • for X ⊆ {1, 2}, (q F ) X , true, 0, (q F ) X ∈ ∆ (final loops).
By construction, the counter machine M is reversal-bounded since the four counters only increase. The idea behind this construction is that the first [resp. second] and the third [resp. fourth] counters of M respectively count the number of incrementations and decrementations of the first [resp. second] counter of M . No zero-test is performed in M ; in order to simulate a zero-test in M , we would need to test equality between two counters, which is not allowed in our models. Consequently, we encode these equality tests by formulae.

Let us build a formula φ in LTL ↓ [Q , 4] such that M |= ω φ iff the control state q F can be reached from the initial configuration of M . We consider the following auxiliary formulae (c ∈ {1, 2}):

φ c def = q∈Q {c}⊆X⊆{1,2} q X and φ q def = X⊆{1,2} q X .
We are now in position to define φ:

φ def = Fφ q F ∧ c∈{1,2} G(φ c ⇒↓ c 1 ↑ c+2 1 ) ∧ c∈{1,2} G( q,true,-ec,q ∈∆ q ∅ ∧ Xφ q ⇒↓ c 1 ¬ ↑ c+2 1 )
It remains to show that M |= ω φ iff the control state q F can be reached in M .

The result of Theorem 7 can be refined by showing the undecidability of the strict fragment MC ω (LTL ↓,s [•, 4]) restricted to reversal-bounded counter machines. Observe that we shall modify the above developments while we are dealing with a strict fragment for which each register is associated with a unique counter.

Theorem 8. MC ω (LTL ↓,s [•, 4]) restricted to reversal-bounded counter machines is undecidable.

The proof takes advantage of a refinement in the contruction of the counter machine M from the proof of Theorem 7 and it is interesting for its own sake. So far, it is still open whether the problem is Σ 1 1 -hard since we are "only" able to reduce the halting problem to it.

Deterministic Counter Machines

In this section, we restrict ourselves to classes of deterministic counter machines. A class C of deterministic counter machines has the PA-property def ⇔ for each counter machine M ∈ C, one can effectively build a formula φ M (x 0 , . . . , x n+1 ) in Presburger arithmetic such that for all j 0 , . . . , j n+1 ∈ N, j 0 , j 1 , . . . , j n is the j n+1 th configuration of the unique run of M iff j 0 , . . . , j n+1 |= φ M (x 0 , . . . , x n+1 ) (assuming that M has dimension n and its set of control states is viewed as a finite subset of N).

We show below that model-checking restricted to counter machines can be sometimes reduced to the decidable satisfiability problem for Presburger arithmetic. Checking whether a VASS is deterministic can be decided by using instances of the covering problem (the problem is actually PSPACE-complete [START_REF] Howell | Completeness results for single-path Petri nets[END_REF]). Checking whether a reversal-bounded counter machine is deterministic is also decidable adding a counter which counts each step and using the fact that the reachability set can be expressed in Presburger arithmetic. By contrast, checking whether a counter machine is reversalbounded is undecidable [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF].

Flat Freeze LTL

In this section, we consider the restriction of the model-checking problem to flat formulae only. By Theorem 4, we already know that MC ω (flat -LTL ↓ [•, •]) restricted to flat counter machines is decidable and that MC ω (flat -LTL ↓ [•, •]) restricted to VASS is undecidable (the proof of Theorem 6 involves only flat formulae). It is worth observing that flat LTL ↓ [Q, n] strictly contains LTL[Q], and therefore we refine below decidability results from Section 4.2.

A detour to counter machines with parameterized tests

We introduce here parameterized counter machines in order to solve later model-checking problems restricted to flat formulae. First, let us fix some definitions. A counter machine with parameterized tests (shortly parameterized counter machine) is defined as a counter machine M = n, Q, ∆, q 0 , Z extended with a finite set Z of integer variables such that the guards g are among ({zero, true} ∪ {=(z), =(z),

>(z), <(z) | z ∈ Z}) n . A concretization C of M is a map C : Z → N.
Given a parameterized counter machine M and a concretization C, we introduce the transition system

T S(M, C) = Q × N n , - → where - →⊆ (Q × N n ) × (Q × N n ) is defined as follows: for q, v , q , v ∈ Q × N n , we have q, v - → q , v def
⇔ there exists a transition t = q, g, a, q ∈ ∆ such that v = v + a, and for

1 ≤ c ≤ n, g(c) equals zero implies v(c) = 0, g(c) is equal to =(z) implies v(c) = C(z), g(c) is equal to =(z) implies v(c) = C(z), g(c) is equal to >(z) implies v(c) > C(z) and, g(c) is equal to <(z) implies v(c) < C(z). A finite [resp. infinite] run in T S(M, C) is a finite [resp. infinite] sequence ρ = q 0 , 0 - → q 1 , v 1 - → .
. .. The parameterized reachability problem for counter machines is defined as follows: given a parameterized counter machine M and a configuration q, v , is there a concretization C such that q 0 , 0 * -→ q, v in T S(M, C)? Even if the parameterized reachability problem is obviously undecidable, we will see in this section that some restrictions lead to decidability. We will say that a parameterized counter machine is Ibarra reversal-bounded if the classical counter machine obtained by replacing each parameterized test by true is Ibarra reversal-bounded. We have then the following result. Theorem 12. [START_REF] Ibarra | Counter machines and verification problems[END_REF] The parameterized reachability problem for Ibarra reversal-bounded parameterized counter machines is decidable.

If a parameterized counter machine has no guard of the form either =(z) or <(z), we say it is restricted. In [START_REF] Haase | Reachability in succinct and parametric one-counter automata[END_REF], parametric one-counter machines are defined as extensions of one-counter machines extended with actions consisting in incrementing or decrementing the unique counter with some parameterized integer constants. In [START_REF] Haase | Reachability in succinct and parametric one-counter automata[END_REF], it is shown that the reachability problem for this class of one-counter machines is decidable. Here is a corollary. Lemma 13. The parameterized reachability problem for restricted parameterized onecounter machines is decidable.

The proof of Lemma 13 consists in substituting each test of the form =(z) by the following sequence of instructions: decrement by z, perform a zero-test and increment by z. In order to encode the test >(z), we use the same technique except that we do not introduce a zero-test between the decrementation (in fact we also add a decrementation by 1 and an incrementation by 1) and the incrementation. Note that this method does not work if we allow guards of the form either =(z) or <(z), because the value of the counter cannot be negative, hence the decidability of the parameterized reachability problem for one-counter machines remains an open problem.

We introduce here a new problem which is needed to reduce the considered modelchecking problem. The parameterized generalized repeated reachability problem for parameterized counter machines is defined as follows: given a parameterized counter machine M , N sets F 1 , . . . , F N of control states, are there a concretization C and an infinite run of T S(M, C) such that for 1 ≤ i ≤ N , one control state in F i is repeated infinitely often?

From the previous theorem and lemma, we deduce the following corollary.

Corollary 14. The parameterized generalized repeated reachability problem is decidable when considering Ibarra reversal-bounded parameterized counter machines and restricted parameterized one-counter machines.

Flat formulae and parameterized counter machines

For MC ω (LTL ↓ [•, •]) restricted to flat formulae, we have the following result.

Theorem 15. There is a reduction from MC ω (LTL ↓ [•, •]) restricted to flat formulae to the parameterized generalized repeated reachability problem for counter machines.

Proof. (sketch) Let M = n, Q, ∆, q 0 be a counter machine and φ be a flat sentence belonging to LTL ↓ [Q, n]. Without any loss of generality, we can assume that φ is in negation normal form (which means that all the occurrences of negation appear only in front of atomic formulae). Moreover, we can assume that if ↓ c r ψ and ↓ c r ψ are distinct occurrences of subformulae in φ, then r = r (this may just linearly increase the number of registers). Consequently, if ψ 1 Uψ 2 [resp. ψ 1 Rψ 2 ] is a subformula of φ, then the freeze operator ↓ cannot occur in ψ 1 [resp. ψ 2 ]. We shall effectively build a parameterized counter machine M = n, Q , ∆ , q 0 , Z and sets F 1 , . . . , F N ⊆ Q for which there is a concretization C and an infinite run of T S(M , C) such that for 1 ≤ i ≤ N , one control state in F i is repeated infinitely often iff M |= ω φ. Let us fix some notations. As usual, the formula φ can be encoded as a finite tree whose leaves are labelled by atomic formulae and internal nodes are labelled by (Boolean, temporal or freeze) connectives. Each node of the formula tree corresponds naturally to a subformula and the set of nodes can be viewed as a finite prefix-closed subset occ(φ) ⊆ (N \ {0}) * (finite sequence of natural numbers). Each element in occ(φ) corresponds to the occurrence of a subformula in φ; hence two occurrences may correspond to the same subformula. The use of occurrences instead of subformulae is motivated by the need to provide formal and clear statements in which occurrences are crucial. For each occurrence u ∈ occ(φ), we write φ(u) to denote the corresponding subformula in φ; for instance φ( ) = φ. Moreover, when u is a prefix of u , written u ≤ pre u , we know that φ(u ) is a subformula of φ(u). We write occ ↓ (φ) [resp. occ ↑ (φ)] to denote the set of occurrences corresponding to formulae whose outermost connective is of the form

↓ c r [resp. ↑ c r ]. Let m = card(occ ↓ (φ)).
Observe that if m = 0, then we are in the case of MC ω (LTL[•]) which has been treated in Section 4.2. In the sequel, we assume that m > 0. Given u ∈ occ ↑ (φ) with φ(u) =↑ c r , we write bind(u) to denote the longest prefix of u (with respect to ≤ pre ) in occ ↓ (φ) such that φ(bind(u)) is of the form ↓ c r ψ (i.e., with the same register). An atom X is a subset of occ(φ) satisfying the conditions below (we abusively use subformulae to denote occurrences corresponding to formulae with the appropriate outermost connective):

(1) if ψ 1 ∧ ψ 2 ∈ X, then ψ 1 , ψ 2 ∈ X; (2) for all atomic formulae ψ ∈ X, {ψ, ¬ψ} ⊆ X; (3) if ψ 1 ∨ ψ 2 ∈ X, then either ψ 1 ∈ X or ψ 2 ∈ X; (4) if ↓ c r ψ ∈ X, then ψ ∈ X.
The set of atoms of φ is denoted by AT(φ). A pair of atoms X, X is said to be one-step consistent iff the conditions below hold true:

(I) if ψ 1 Uψ 2 ∈ X, then either ψ 2 ∈ X or (ψ 1 ∈ X and ψ 1 Uψ 2 ∈ X ); (II) if ψ 1 Rψ 2 ∈ X, then ψ 2 ∈ X and (ψ 1 ∈ X or ψ 1 Rψ 2 ∈ X ); (III) if Xψ ∈ X, then ψ ∈ X ; (IV)
No atom X strictly included in X satisfies the conditions (I)-(III) (by replacing X by X ). We will now describe the construction of the parameterized counter machine M which will use m integer variables z 1 , . . . , z m . Intuitively, each integer variable will be used to store the value of a register. In order to make explicit this dependancy, we shall use a one-to-one map reg : occ ↓ (φ) → {1, . . . , m}. We define also a function counter : occ ↓ (φ) ∪ occ ↑ (φ) → {1, . . . , n} that indicates the counter involved in the subformula. Given u ∈ occ ↓ (φ) such that φ(u) =↓ c r ψ, we have counter(u) = c and given u ∈ occ ↑ (φ) such that φ(u) =↑ c r , we have counter(u) = c. The set Q of control states is equal to {q 0 } Q × AT(φ) plus some auxiliary control states that are introduced to perform tests. The relation ∆ is defined as follows. First, q 0 , true, 0, q 0 , Y ∈ ∆ whenever ∈ Y and no atom strictly included in Y contains (init). Then, for each transition q, g, a, q ∈ ∆ there is in ∆ the following sequence of transitions q, Y •

• • q aux 1 • • • q aux T g,a -→ q , Y assuming that: 1. occ ↓ (φ) ∩ Y contains T 1 elements, say u 1 , . . . , u T1 ; occ ↑ (φ) ∩ Y contains T 2 elements, say u T1+1 , . . . , u T1+T2 ; {u ∈ Y | u•1 ∈ occ ↑ (φ) and φ(u) is a negation} contains T 3 elements, say u T1+T2+1 , . . . , u T1+T2+T3 with T = T 1 + T 2 + T 3 , 2. Y, Y is a one-step consistent pair, 3. {φ(u) : u ∈ Y } ∩ Q ⊆ {q} and ¬q ∈ {φ(u) : u ∈ Y }, 4. for i ∈ {1, . . . , T 1 } [resp. i ∈ {1, . . . , T 2 }, i ∈ {1, . . . , T 3}
], before reaching the control state q aux i [resp. q aux T1+i , q aux T1+T2+i ], there exists a transition testing equality [resp. equality, inequality] between z k and the counter counter(u i ) [resp. counter(u T1+i ), counter(u T1+T2+i )] with the identity k = reg(u i ) [resp. k = reg(bind(u T1+i )), k = reg(bind(u T1+T2+i ))].

Finally, let u 1 , . . . , u N be the occurrences in occ(φ) such that the outermost temporal connective of φ(u i ) is the until operator U. Then, for

1 ≤ i ≤ N , F i = { q, Y : u i ∈ Y or (u i •2) ∈ Y }.
It remains to show that M |= ω φ iff there exist a concretization C and an infinite run of T S(M , C) such that for 1 ≤ i ≤ N , one control state in F i is repeated infinitely often.

Decidability results

Remark that if the counter machine M is Ibarra reversal-bounded, then the parameterized counter machine M built from M and the flat formula φ is Ibarra reversalbounded. Using Corollary 14 and Theorem 15, we conclude that MC ω (LTL ↓ [•, •]) restricted to Ibarra reversal-bounded counter machines and to flat formulae is decidable. Furthermore this can be extended to the class of reversal-bounded counter machines, using Lemma 16 below. Finally, assume the formula φ is a positively flat formula (see Section 3). For all atoms Y ∈ AT(φ), the set {u ∈ Y | u • 1 ∈ occ ↑ (φ) and φ(u) is a negation} is empty. So, in the construction of M from M and φ, we only use parameterized tests of the form =(z). Hence, if M is a one-counter machine and φ is a positively flat formula, we deduce that M is a restricted parameterized one-counter machine. Using Corollary 14 and Theorem 15, we get the result below.

Theorem 18. MC ω (LTL ↓ [•, •]) restricted to one-counter machines and to positively flat formulae is decidable.

In order to extend Theorem 18 to the full flat fragment, one needs to perform inequality tests in parameterized one-counter machines, which is so far unclear how to perform while preserving decidabibility of the corresponding parameterized reachability problem. This generalization is left as an open problem.

Concluding Remarks

In this paper, we have studied the decidability status of model-checking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable. Our most remarkable technical contributions concern reversal-bounded counter machines and flat formulae. Besides, we have established an original link between reachability problems for parameterized counter machines and model-checking counter machines over the flat fragment of freeze LTL. The table below contains a summary of the main results (D stands for decidability, U for undecidability) in which the columns referred to restriction either on the counter machines or on the formulae. Sometimes, an additional restriction between parentheses is indicated in order to emphasize that the result holds true for a stricter fragment. Bibliographical references in the table indicate that the related result is mainly due to the referred work.

Det.

NDet Here are a few rules of thumb: determinism, flat counter machines and no freeze lead to decidability. However, flat formulae often guarantee decidability (except for VASS) whereas reversal-boundedness can lead to decidability (but the restriction with a single register leads to undecidability). Finally, throwing away the atomic formulae made of control states does not help for decidability. Even though we have established various decidability results, the complexity of the decision problems is far from being known, mainly because we use reductions to Presburger arithmetic. Such characterizations are part of future work.

Lemma 9 .

 9 Let C be a class of deterministic counter machines. If C has the PA-property, then the model-checking problem MC ω (LTL ↓ [•, •]) over counter machines in C is decidable. The proof of Lemma 9 is based on an internalization of the satisfaction relation in Presburger arithmetic. Lemma 10. Deterministic reversal-bounded counter machines and deterministic VASS have the PA-property. Corollary 11. MC ω (LTL ↓ [•, •]) is decidable when restricted to deterministic reversalbounded counter machines and deterministic VASS.

Lemma 16 .

 16 There is an exponential-time reduction from MC ω (LTL ↓ [•, •]) restricted to reversal-bounded counter machines into MC ω (LTL ↓ [•, •]) restricted to Ibarra reversalbounded counter machines. Furthermore this reduction preserves flatness of the formulae. Corollary 17. MC ω (LTL ↓ [•, •]) restricted to reversal-bounded counter machines and to flat formulae is decidable.

Acknowledgments. We would like to thank the anonymous referees for their comments and suggestions on a preliminary version.

A. Sangnier is financed by a postdoctoral fellowship from DGA/ENS Cachan, France. Work also supported by the Agence Nationale de la Recherche, grant ANR-06-SETIN-001.


Jérôme Monnet

PUBLIC LANDSCAPE AS COMMUNICATIVE SPACE: EXPLORING THE THIRD DIMENSION OF PUBLIC SPACE

Keywords: Public Space, Urban Landscape, Architecture, Public Art, Street Art, Orientation, Advertisement, Government Communication

This article proposes an analysis of urban public space as a medium of communication, based not only on the physical interconnection of different places in a city but also on the different communicative uses of the urban landscape: street signs, monumental architecture, shop displays and advertisement, street art, protests or parades, all contribute to the representation of public space as symbol of society.

Introduction: Landscape as the Third Dimension of Public Space

Communicative space is commonly understood in two distinct ways. On the one hand, in communication sciences, it refers to the medium through which messages and information travel: the press, the telecommunications network, advertising, political speeches, etc. In engineering and geography, on the other hand, it refers to the physical spaces that connect other types of space together, such as streets, roads, canals or railways. In the former definition, the concrete spatial dimension is often ignored in favour of an abstract conception of the media or informational sphere. Conversely, in the latter, the informational role played by physical infrastructures beyond simply connecting places together is often underestimated.

This dichotomy between, on the one hand, an abstract sphere in which human beings exchange information, and on the other hand a material space within which places are connected, emerges in conceptions of public space. Philosophers and sociologists like G. Simmel, H. Arendt or J. Habermas, among others, developed major theories on the role of spaces where people can meet to express opinions, accept differences of opinion, debate and reach consensus; in the 20 th century, these theories were linked with the conception of liberal democracy. In parallel, however, an entirely separate vision of public space developed in the technocracies responsible for the planning and construction of the roads, in a context dominated by the functionalist ideology illustrated by Le Corbusier: the roads infrastructure was designed for the sole purpose of connecting areas characterised by separate activities (residence, work, consumption, leisure, etc.).

As a geographer and urban planner, my purpose here is to observe, from a distinct angle, public space as it is actually used by human beings in a wide variety of conditions across the entire planet. My point of view, therefore, is not the idealist position of political philosophy (public space as it should be, open to all forms of expression and discussion in a perfectly democratic society), nor the functionalist standpoint of technocracy (public space as a physical means to move from one place to another). My viewpoint is more consonant with the position of the interactionist micro-sociology illustrated by Lynn [START_REF] Lofland | A World of Strangers[END_REF][START_REF] Lofland | The Public Realm. Exploring the city's quintessential social territory[END_REF] from a pragmatic and constructivist perspective: public space is defined and produced by all the different practices that take place in the presence of strangers. I propose to classify this diversity into seven main categories: 1-Connection, 2-Information, 3-Commerce, 4-Conviviality, 5-Abandonment of things and beings, 6-Regulation and resistance, 7-Symbolisation.

So here it is the 2 nd category of practices that will concern us. Whereas in order to identify the possible routes between places (category No. 1), we usually look at a map of the streets of a city in two dimensions, instead we will focus here on the "third dimension": the landscapes that we see while on the move. That is why I choose to refer to "public landscape", insofar as it is the vertical dimension of public space that informs and communicates with users. In the sections that follow, we will review the different subtypes of uses that make up this broader category.

Directing Behaviours

All of us use public landscape to situate ourselves in time and in space. Public clocks replaced the sundials of the preindustrial era for telling the time; the bells of Christian churches or the Muslim muezzin's call to prayer punctuate the divisions of the day; bells too may mark the beginning and end of the day for workers or schoolchildren; sirens announce the arrival or departure of ships in harbour.

Bell towers, minarets and other monuments that stand out in the landscape also help us to find our way in and around the city. In Rio de Janeiro, for example, it is common for residents to give directions using Sugarloaf Mountain and the statue of Christ the Redeemer as landmarks. Below this regional scale, monumental facades, distinctive architectures, big squares and wide avenues provide valuable directional information. At an even more granular level, the architecture of buildings tells us about their function and the services they offer. At individual street scale, we obtain information from shopfronts, commercial signs, signposts and urban signage of different kinds (names of streets, neighbourhoods or monuments, maps, tourist and historical information, etc.).

Much information that we glean from the landscape has been placed there intentionally by actors who want to guide us, either for reasons of public interest (indicating how to get to a place), or for their own private interest (e.g. to attract customers, a subject we will return to later). As well as this guidance, there is almost always information on the rules of expected or forbidden behaviour for users of different kinds: one-way streets, bus or cycle lanes, traffic calming measures, pedestrian crossing zones, CCTV warnings, etc. (fig. 1).

Monumentality: The Architecture of Glorification

In the previous section, we considered utilitarian uses of information via public space. Now, we examine how monumental architecture and in particular the public facades of buildings have been used to glorify the rulers that ordered their construction.

Everywhere on the planet there are examples of religious architecture placed before the public as an expression of grandeur, superiority, wealth and complexity: pyramids, stairways, towers, walls, gates and galleries, often vast and highly decorated, are part of the universal architectural vocabulary of religious places and buildings.

Some of this vocabulary is reproduced in buildings that represent military power, notably the power of conquerors whose fortresses and citadels are not solely designed to protect the troops against attack, but also to express power and to intimidate subject populations. This is true not only of peoples colonised by foreigners, but also the urban populace to whom the rulers wished to present an image of invincibility. One famous example of symbolic reversal is the "taking of the Bastille" by the revolutionaries on 14 July 1789 in Paris: the invasion of the citadel and the liberation of the prisoners are commemorated as the moment the public recognised the change in political regime.

Figure 2. City Hall in Trieste (Italy), July 2014 (© Jérôme Monnet)

From the 15 th century, the cities of Europe also became the stage of the emergence of a specifically civil monumentality, through the palaces and stately homes of the social elite and the halls or assembly rooms of the merchants or guilds (fig. 2). This monumentality was further reinforced with the industrial revolution, when it glorified the wealth of owners, economic development and technological progress: railway stations in their turn became monuments, and factories took their place in the public landscape with grandiose facades punctuated with ornament, statues or towers. This trend culminated in the architecture of the skyscraper, with the race for height and technical prowess pursued by leaders of the financial or industrial sectors. It may be that the skyscraper has passed its pinnacle, since giants of 21 st -century capitalism, with their focus on the information and communication technologies and services, represented by the famous GAFA (Google, Apple, Facebook, Amazon), prefer to glorify their modernity in greener and more horizontal ways, by establishing their headquarters on high-tech campuses.

Another contributor to this list of monumental uses of public landscape to promote religious, political and/or economic powers, is the urbanism of the "tabula rasa", new cities created either by colonial powers in conquered territories, or as part of a process of internal colonisation apparent in the example of Brasília, or equally in the French, Soviet or Chinese "new towns". In these cases, it is the urban morphology as a whole that expresses the cosmology of the planning state.

Commerce and Services

In the previous section on the architecture of glorification, what matters is the use of public landscape to communicate power, and possibly no other function than the communication of power. This is how commerce differs in its use of public landscape: almost invariably, its communication is linked with a transaction. For a commercial entity, therefore, the function of public landscape is to make the public aware of the availability of goods or services. In this case, we can say that there is a genuine exchange: sellers of goods or providers of services need the landscape to tell the public what they have, whereas the public uses the landscape to locate and identify whatever corresponds to its needs and wants. Public landscape thus becomes an interface between supply and demand that is expressed in different subtypes:

• Shop signs. Visible from a distance, these devices tell potential customers what service or goods can be found in a specific place "open to the public" (often within a building): they enable people to distinguish between a baker and a post office, a service station or a doctor's surgery, a police station or a bar,… When brands are concentrated in certain streets in dense urban areas, they have a major impact on public landscape by adorning facades with a variety of aesthetic forms which combine words and symbols that represent the product sold, the place, or the identity of the owner (e.g. Harbour Hotel or Smith's Pharmacy). • Displays: Here, the aim is to show the merchandise in the place where it is actually sold. Material goods lend themselves most universally to attractive display (fig. 3): markets all over the world are prized by tourists for the visual presentation of food items (fruit and vegetables, fish, joints of meat or other preparations) or manufactured products (particularly craft goods). However, it is also common for stores to position a temporary display in public space to make its goods more visible to passers-by: racks of fruit, newspapers or postcards, ice cream or pancake counters. In certain respects, cafe and restaurant terraces can be seen as a means of display. In general, however, nonmaterial services are less likely to use display to communicate in public space (though one might cite the hairdressing salon that displays the different hairstyles it offers). • Shop windows: although product displays and racks can be found both inside and outside commercial and non-commercial premises, the shop window is a particular device for communication between public and non-public space, since it separates them physically while maintaining a visual connection between them. It thus protects the interior from bad weather while maintaining the visibility of the displays from the outside. While examples of brands and displays dating back millennia can be found in different urban civilisations, the shop window is a device that was created in the context of the industrial revolution in Europe and has spread by means of globalisation, contributing in its own way to the homogenisation of the planet's public landscapes. • Advertising: like the shop window, this has spread through the globalisation of public landscape, with the proliferation of information that I will describe as "remote" because, unlike the systems of communication considered previously, it is not located in the place where the service is provided. In certain cases, this display may indicate a destination and a distance ("service x can be found 5 minutes away" on foot or by car), but advertising increasingly seeks only to familiarise the public with a product without indicating where it can be found, perhaps even communicating nothing about the product, but only a brand image, an abstract value. In recent decades, the use of the urban landscape for advertising has proliferated to an impressive degree. After the spectacular concentration of billboards at iconic locations (Piccadilly Circus in London, Times Square in New York, Shibuya in Tokyo), or tunnels of advertisements lining major traffic arteries (e.g. in Mexico or on the roads into French towns), after the proliferation of lollipop signs in public spaces redeveloped for strolling, shopping, tourism and leisure, there seems to be no limit to the capacity of advertising to invade every kind of space. In the last decade, different European cities (Venice, Madrid, Paris…) have seen advertisements painted on pavements and roads, stuck on public stairways or projected onto facades. In particular, it has become common to see facades, or even entire buildings, completely "wrapped" in an advertisement, on the pretext that a small fraction of the profit would go into restoration work (fig. 4)… • Tracking technologies: apart from physical surfaces, advertising has also set out to conquer the virtual space embodied in portable information-communication devices (smartphones, tablets, connected vehicles, etc.). These days, the advertising screens located in public space can adapt the information they broadcast to the information detected in the devices of passers-by and by mining the socio-economic profiles revealed by personal data. Similarly, stores can send individualised messages to devices informing passers-by of some nearby special or promotional offer. Finally, it will soon be possible to modify the content of shop windows or displays to match the profiles of the people who pass in front of them.

It would thus seem that public art is an important priority for leaders, whether ecclesiastical or civil, or indeed economic in the case of the sponsors of the modern world. The symbolic power attributed to works displayed in public space is also confirmed in times of political change, military conquest or religious overthrow, when the newcomers desecrate pagan representations or revolutionaries tear down the statues of tyrants (kings, dictators, colonisers). Sometimes, a single artistic object crystallises a society's internal antagonisms, as illustrated by the statue of a naked Diana the Huntress adorning a fountain installed on Mexico's most prestigious avenue in 1942 at the request of the federal government, clothed in an undergarment in 1943 following pressure from a conservative Catholic movement, and then once again disrobed by the authorities 25 years later in order to demonstrate the country's modernity at the time of the 1968 Olympic Games.

Public art in urban landscape can therefore express the official order, but can also oppose or subvert it. This alternative use seems to have grown spectacularly from the beginning of the 20 th century. Indeed, while graffiti expressing alternative or critical opinions have existed for millennia, it is only recently that they seem to have acquired any artistic pretensions; under the Ancien Régime in France, historians have shown that politico-artistic opposition mostly took the form of the clandestine circulation of songs and poetic pamphlets. Contemporary public space, on the other hand, has become a flourishing arena for a multiplicity of expression that varies in its oppositional content and artistic form: graffiti, flash mobs, satirical or critical street performances, etc. (fig. 6).

Figure 6. "White wall, red mist of anger", anarchist slogan in Paris (France), May 2017 (© Jérôme Monnet)

In this respect, mural painting is a good example of the contemporary diversification of public art. Following the Mexican revolution of 1910, and supported by the new regime, a significant muralist movement developed to promote leftist progressivism by means of this avant-garde aesthetic. From the 1940s onwards, however, what had initially been revolutionary in both its artistic expression and its political message became an official art that lost its liberating social ambition in Mexico, but maintained its subversive charge in the United States by becoming a preferred mode of expression for the demands of the "Chicano" movement until the 1970s, before undergoing an extraordinary revival in the "Hip-Hop" movement. Since then, graffiti and tagging have spread to walls on every city in the world. The developments of the last decade show a twofold trivialisation of an art form long considered marginal and transgressive by graffiti artists and authorities alike: firstly, the graphic aesthetic of Hip-hop has been adopted by a wide variety of "mainstream" art forms and by advertising, and secondly, the commercial art world has begun to develop a specific and profitable market for what the mass media now call "street art", in which the element of protest has become no more than part of the sales pitch.

The Choreography of Public Movements

Whereas in international parlance "street art" usually refers to the application of graphic techniques to urban surfaces, in France the term arts de la rue (street arts) is used more to refer to what in English are called the "performing arts" (music, theatre, circus, acrobatics, puppets, etc.). These "street performances" which, since the end of the 20 th century, have boomed in parallel with street art, would now seem to be primarily individual initiatives, but are nevertheless part of a long tradition of performance in public space, in which the stated aim is historically not so much artistic as religious (processions), military (parades) or civil (ceremonies), and more recently has taken on an economic character (advertising "flash mobs").

These spectacles, which require a fundamental distance between the spectators who watch and the actors who produce and perform, differ from ritual subversive performances such as carnivals and charivaris, in which the urban public plays a key role. Within the framework of seasonal festivities, carnivals have long provided an opportunity for the expression of social and political opposition, which is also expressed spontaneously, not to say unpredictably, through upsurges of protest against the established order, riots and other forms of insurrection. This anti-establishment use of public space, known since ancient Rome and maintained over the centuries, has recently been theorised in the form of "Temporary Autonomous Zones" that have been promoted by movements like the "Indignados", "Occupy" or "Nuit Debout", following the "Arab Spring" of 2010, in iconic city squares around the planet (Puerta del Sol in Madrid, Tahrir in Cairo, Taksim in Istanbul, Wall Street in New York, Maïdan in Kiev, République in Paris, etc.).

Public expressions of disobedience and resistance are not necessary collective. For an Iranian woman, dressing in a certain way may be a means to protest against a dress code that she considers repressive, whereas the provocations associated with punk or grunge can be used to ridicule the tyranny of appearances. "Speaker's Corner" in Hyde Park in London is famous for allowing anyone to harangue the crowd on any subject whatsoever; in other contexts, it can be dangerous and courageous to sing in public. However, public disobedience is not always about politics, far from it: from one city or country to another, people's tolerance of rules and laws varies greatly, and their behaviour in public space visibly reveals this variability.

Symbolic Uses of Public Space: Iconography

In the cities of the contemporary world, the remarkable diversity in the use of public space for communication and expression easily explains why it has become a symbol of a society as a whole and the freedoms it enjoys (or lacks). In photography, in films or on the television, in postcards or tourist guides, as in advertising, public landscape represents a city in both its topographical and monumental specificities and in its supposedly typical social composition (fig. 7).

Figure 7. Urban skyline as background for a Beauty Salon's mural in Los Angeles (U.S.A.), January 2013 (© Jérôme Monnet)

Under these circumstances, "commonplaces" die hard. The iconography of Paris, of New York or of Rio de Janeiro continues to show a landscape that has remained unchanged for a century. This representational conservatism is problematic when it comes to the symbolisation of the local population: for example, while photographs of New York have incorporated the Blackness of a significant proportion of its inhabitants, representations of public landscaping Paris, Venice, Berlin or other European cities still have a long way to go in this regard…

Conclusions: Monopolies vs. Pluralism

We have seen the extent and diversity of the use of the communicative potential of public landscape, whether to find one's way, as a guide towards a destination, to publicise a service, to glorify or to oppose the possessors of power, etc. Public space thus appears to be an important resource and, as with all resources, certain human actors try to control or monopolise it for themselves, whether for economic profit or political power.

We can see forces that are seeking to monopolise certain dimensions of public landscape. For example, the advertising industry wants to exploit as much space as possible for brand communication, to the detriment of non-commercial uses of the urban landscape. Authorities, whether religious or political, retain a monopoly over the conception of public order and art, and seek to repress other forms of expression. More subtly, architectural conservatism can promote a museum vision of the city on the pretext of heritage protection, but in so doing prevent the emergence of new social and aesthetic forms.

Nonetheless, we find that the communicational complexity of public space allows leeway for alternative, oppositional or competing expressions. We can therefore conclude by recognising that public space plays a fundamental role in the democratic functioning of any society, a role often threatened by populist movements that reduce democracy to an untrammelled transfer of power from the people to the "leaders". Indeed, public landscape is by definition a means of communication where pluralism can be expressed through the coexistence of differences in both messages and in forms of expression.

Just as the advocates of democracy promote pluralism and freedom of expression in the mass media, or the separation of powers between the executive, legislative and judicial institutions, it is up to citizens in the broad sense -i.e. all users of public space, regardless of their status -to defend pluralism in the urban landscape by the diversity of their uses of public space.

Figure 1 .

 1 Figure 1. Street signs in Paris (France), May 2009 (© Jérôme Monnet)

Figure 3 .

 3 Figure 3. Shop fronts in Los Angeles (U.S.A.), January 2013 (© Jérôme Monnet)

Figure 4 .

 4 Figure 4. Building advertising wrap in Venice (Italy), May 2009 (© Jérôme Monnet) 154

Acknowledgements

This paper is based on the lecture delivered at CEECOM 2018: 11th Central and Eastern Communication and Media Conference, Szeged, Hungary, 30 May -1 June 2018. My thanks to the organizers for their invitation, and to LVMT for c vering the cost of the translation from French to English carried out by Mr. John Crisp.


Olivier Commowick

Renaud Hédouin

Charlotte Laurent

Jean-Christophe Ferré

Patient specific tracts-based analysis of diffusion compartment models: application to multiple sclerosis patients with acute optic neuritis

come

Introduction

Multiple sclerosis (MS) is a complex disease [START_REF] Lublin | Defining the clinical course of multiple sclerosis: The 2013 revisions[END_REF] still not well understood. While MRI plays an important role in its diagnosis [START_REF] Thompson | Diagnosis of multiple sclerosis: 2017 revisions of the McDonald criteria[END_REF], there is still a clinical-radiological paradox [START_REF] Healy | Characterizing clinical and MRI dissociation in patients with multiple sclerosis[END_REF][START_REF] Barkhof | The clinico-radiological paradox in multiple sclerosis revisited[END_REF] in which handicap scores evolution is not correlated with MRI observations. This may come from the fact that the explored measures are not specific enough: all lesions are not equivalent depending on their position with respect to major fiber bundles and on the severity of the microstructural damage. To investigate this aspect, many studies have looked at diffusion MRI for its potential to reveal the brain microstructure [START_REF] Filippi | Diffusion tensor magnetic resonance imaging in multiple sclerosis[END_REF]. However, diffusion MRI in MS has still not proven efficient yet for patient-specific follow-up. This comes first from the fact that current methodologies are often targeted at group analysis [START_REF] Lepore | Generalized tensor-based morphometry of HIV/AIDS using multivariate statistics on deformation tensors[END_REF][START_REF] Rovaris | Diffusion MRI in multiple sclerosis[END_REF][START_REF] Whitcher | Statistical group comparison of diffusion tensors via multivariate hypothesis testing[END_REF][START_REF] Raffelt | Investigating white matter fibre density and morphology using fixel-based analysis[END_REF]. Another reason is that although several methods have looked at along tract analysis [START_REF] Smith | Tract-based spatial statistics: Voxelwise analysis of multi-subject diffusion data[END_REF][START_REF] Chamberland | Beyond lesion-load: Tractometry-based metrics for characterizing white matter lesions within fibre pathways[END_REF][START_REF] Chamberland | Tractometry-based anomaly detection for single-subject white matter analysis[END_REF], all methods are most often limited to simple models such as the tensor or to direction-based models that do not incorporate microstructure information. There is thus a need for patient, bundle specific measures of disease burden on directly interpretable parameters of the microstructure.

We propose a new framework for patient, bundle specific analysis of microstructural burden of neurodegenerative diseases. To do so, we propose an atlas-based approach to compute microstructural disease burden on major bundles with advanced diffusion compartment models (DCM) [START_REF] Panagiotaki | Compartment models of the diffusion MR signal in brain white matter: a taxonomy and comparison[END_REF]. We evaluate this approach with a proof-of-concept analysis of optic radiations of MS patients with acute optic neuritis [START_REF] Miller | Walsh and Hoyt's clinical neuroophthalmology[END_REF], showing different microstructural burden patterns depending on the patient.

Materials

Data from 22 control subjects and 6 MS patients with acute optic neuritis were acquired on a Siemens 3T Prisma scanner. For each subject, T1 and T2-weighted images (3D isotropic, 1 mm 3 ) were acquired as well as diffusion images with a CUSP sequence [START_REF] Scherrer | Parametric representation of multiple white matter fascicles from cube and sphere diffusion MRI[END_REF] (6 b 0 , 60 directions with b-values in between 670 and 2000 s.mm -2 , 2x2x2 mm 3 voxels). Data were preprocessed to remove distortion using a reversed phase encoding image [START_REF] Hédouin | Block-matching distortion correction of echo-planar images with opposite phase encoding directions[END_REF] and DCM (three anisotropic tensors plus one free water and one isotropic restricted water compartments [START_REF] Panagiotaki | Compartment models of the diffusion MR signal in brain white matter: a taxonomy and comparison[END_REF]) were estimated [START_REF] Stamm | Comprehensive maximum likelihood estimation of diffusion compartment models towards reliable mapping of brain microstructure[END_REF].

Methods

The overall pipeline of our method is composed of two parts: an offline part to compute a DCM enriched fiber atlas from controls (Fig. 1) performed once for all patients, and an online part performed for each patient (registration and comparison, Fig. 2).

Figure 1: DCM enriched fiber atlas creation pipeline. From DCM images of controls, an atlas is created using tensor registration [START_REF] Suarez | Automated delineation of white matter fiber tracts with a multiple region-of-interest approach[END_REF] and an unbias atlas creation [START_REF] Guimond | Average brain models: A convergence study[END_REF]. At the same time, TractSeg [START_REF] Wasserthal | Tractseg -fast and accurate white matter tract segmentation[END_REF] is used to get bundles endings segmentations on each subject. These endings are then merged onto the atlas using majority voting. They are then used together with tractography [START_REF] Weinstein | Tensorlines: advection-diffusion based propagation through diffusion tensor fields[END_REF] to get the major bundles on the atlas. Finally, the bundles are enriched with microstructural information along tracts extracted from DCM.

The offline part starts by the construction of a control DCM atlas [START_REF] Guimond | Average brain models: A convergence study[END_REF]. Then, fibers are extracted over the whole atlas [START_REF] Weinstein | Tensorlines: advection-diffusion based propagation through diffusion tensor fields[END_REF] and filtered using regions obtained through TractSeg [START_REF] Wasserthal | Tractseg -fast and accurate white matter tract segmentation[END_REF] to get 72 different bundles. These bundles are then enriched with DCM information from each subject of the atlas. To do so, the DCM compartment most collinear to the fiber at a given point is selected and properties from it are extracted: mean diffusivity (MD), fractional anisotropy (FA), parallel and perpendicular diffusivities (d , d ⊥ ); as well as water fractions of isotropic compartments fractions: free (FW) and isotropic restricted water (IRW) fractions.

The online part uses the control atlas as a reference for comparison. The patient DCM image is registered on the atlas [START_REF] Suarez | Automated delineation of white matter fiber tracts with a multiple region-of-interest approach[END_REF]. Along the atlas bundles, information on patient microstructure is extracted from the patient DCM image and a statistical test of abnormality is computed at each point [START_REF] Commowick | Diffusion MRI abnormalities detection with orientation distribution functions: A multiple sclerosis longitudinal study[END_REF]. After correction for multiple comparisons [START_REF] Benjamini | Controlling the false discovery rate: A practical and powerful approach to multiple testing[END_REF], we compute disease burden scores S b,p for each bundle b and microstructure property p illustrating the abnormal fraction of the bundle:

S b,p = 100 M i=1 Ni j=1 b i,j M i=1 N i (1)
with M number of fibers in bundle, N i number of points in i-th fiber of bundle, b i,j = 1 if the point j of fiber i in bundle b is abnormal (i.e. the statistical test performed on that point indicates a significant difference).

Figure 2: Fiber-specific disease burden computation for a patient DCM image. From the controls atlas and the DCM image of the patient, the patient is first registered on the atlas [START_REF] Suarez | Automated delineation of white matter fiber tracts with a multiple region-of-interest approach[END_REF]. Then, the bundles of the atlas are enriched with microstructural information from the patient DCM image. Statistical tests [START_REF] Commowick | Diffusion MRI abnormalities detection with orientation distribution functions: A multiple sclerosis longitudinal study[END_REF] are performed at each fiber point to compare the patient's along fiber microstructure to the controls. After correction for multiple comparisons [START_REF] Benjamini | Controlling the false discovery rate: A practical and powerful approach to multiple testing[END_REF], disease burden scores are computed for each bundle illustrating its level of abnormality for a given microstructure parameter.

Results

Fig. 3 presents results over the optic radiations of two patients suffering from acute optic neuritis related to MS, for two different microstructure parameters. It illustrates well the abnormalities that may be seen in those two patients, closely related to the presence of lesions. However the lesions seem to create different microstructural damage. This can be seen from Tables 1 and2 where disease burden scores are higher for d ⊥ and MD for patient 4, whereas it is higher for FW for patient 6. Moreover, at the time of acute optic neuritis, the higher disease scores for those two patients do not seem to be linked to the side of optic neuritis. No burden score is indeed above 10% on the right optic radiations. 1: Disease burden scores on left optic radiations for several along fiber microstructural properties: d : parallel diffusivity, d ⊥ : perpendicular diffusivity, MD: mean diffusivity, FA: fractional anisotropy, FW: free water fraction, IRW: isotropic restricted water fraction. Bold numbers denote burden scores above 10%. Side denotes which optic nerve suffers from optic neuritis.

Patient ID

Discussion and conclusion

We have proposed a new framework for the patient specific analysis of fiber bundles microstructural damage linked to a disease. We have derived the whole pipeline based on advanced compartmental models of diffusion, enabling the in-depth study of microstructural damage along major fiber tracts. Applied to MS patients suffering from acute optic neuritis, we have highlighted differences located primarily inside lesions but showing different microstructural differences depending on the patient, in line with the high variability of the disease. The code for this framework is available open-source [START_REF]Anima software -RRID:SCR_017072[END_REF]. Further works will study the influence of registration on the results, especially the need or not for advanced diffusion images registration; as well as other disease burden scores based on individual comparisons and their correlation with handicap scores.

Figure 3 :Table 2 :

 32 Figure 3: Results on two MS patients for two different microstructural properties. First line: patient 4 MD abnormalities along tracts. Second line: patient 6 FW abnormalities along tracts. (a,d): Axial view superimposing T2-weighted image and colored tracts, (b,e): zoom on the left optic radiation area, (c,f): 3D view of the T2-weighted image and colored optic radiations. On all images, red is a local significantly different abnormality, while blue is not.

Acknowledgments

This study was partially funded by grants from the VISIO foundation and the ARSEP (aide à la recherche sur la sclérose en plaques) foundation.