Pawel Parys

Igor Walukiewicz

Weak Alternating Timed Automata

Alternating timed automata on infinite words are considered. The main result is the characterization of acceptance conditions for which the emptiness problem for the automata is decidable. This result implies new decidability results for fragments of timed temporal logics. It is also shown that, unlike for MITL, the characterisation remains the same even if no punctual constrains are allowed.

. Undecidability proofs relay on the ability to express "infinitely often" properties. Our main result shows that once these kind of properties are forbidden the emptiness problem is decidable.

To say formally what are "infinitely often" properties we look at the theory of infinite sequences. We borrow from that theory the notion of an index of a language. It is known that the index hierarchy is infinite with "infinitely often" properties almost at its bottom. From this point of view, the undecidability result mentioned above left open the possibility that safety properties and "almost always" properties can be decidable. This is indeed what we prove here.

. By translating a logic to automata we can clearly see a combinatorial challenges posed by the formalism. We can also abstract from irrelevant details, such as a choice of operators for a logic. This approach was very beneficial for the development of logical formalisms over sequences.

An automata approach has been missing in timed models for an obvious reason: no standard model of timed automata is closed under boolean operations.

Event-clock automata [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF] may be considered as an exception, but the price to pay is a restriction on the use of clocks. Alternating timed automata seem to be a good model, although the undecidability result over infinite words shows that the situation is more difficult than for sequences. Nevertheless, Ouaknine and Worrell [START_REF] Ouaknine | Safety metric temporal logic is fully decidable[END_REF] have shown decidability of the emptiness problem provided all states are accepting, and some locality restriction on the transition function holds. Using this, they have identified decidable fragment of MTL called Safety MTL.

In this paper we show that our main result allows to get a decidable fragment of TPTL [START_REF] Alur | A really temporal logic[END_REF] with one variable, that we call Constrained TPTL. This fragment contains Safety MTL and allows all eventually formulas. Its syntax has also some similarities with another recently introduced logic: FlatMTL [START_REF] Bouyer | The cost of punctuality[END_REF][START_REF] Bouyer | On expressiveness and complexity in real-time model checking[END_REF]. We give some elements of comparison between the logics later in the paper. In brief, the reason why Constrained TPTL is not strictly more expressive than FlatMTL is that the later includes MITL [START_REF] Alur | The benefits of relaxing punctuality[END_REF]. This is a sub-logic of MTL where punctual constraints are not allowed.

The case of MITL makes it natural to ask what happens to alternating timed automata when we disallow punctual constraints. This is an interesting question also because all known undecidability proofs have used punctual constraints in an essential way. Our second main result (Theorem 32), says that the decidability frontier does not change even if we only allow to test if the value of a clock is bigger than 1. Put it differently, it is not only the lack of punctual constraints, but also very weak syntax of the logic that makes MITL decidable.

Related work

The idea of restricting to one clock automata dates back at least to [START_REF] Hung | On the design of hybrid control systems using automata models[END_REF]. Alternating timed automata where studied in a number of papers [START_REF] Lasota | Alternating timed automata[END_REF][START_REF] Ouaknine | On the decidability and complexity of metric temporal logic over finite words[END_REF][START_REF] Adams | Undecidability of universality for timed automata with minimal resources[END_REF][START_REF] Abdulla | Zone-based universality analysis for single-clock timed automata[END_REF][START_REF] Abdulla | Universality analysis for one-clock timed automata[END_REF]. The most relevant result here is the decidability of emptiness for the case when when all states are accepting and some locality condition holds [START_REF] Ouaknine | Safety metric temporal logic is fully decidable[END_REF]. One of technical contributions of the present paper is to remove the locality restriction, and to add a non-accepting layer of states on the top of the accepting one.

For a long time MITL [START_REF] Alur | The benefits of relaxing punctuality[END_REF] was the most prominent example of a decidable logic for real-time. In [START_REF] Ouaknine | On the decidability and complexity of metric temporal logic over finite words[END_REF] Ouaknine and Worrell remark that MTL over finite words can be translated to alternating timed automata, and hence it is decidable. They also show that over infinite words the logic is undecidable (which is a stronger result than undecidability for the automata model in [START_REF] Lasota | Alternating timed automata[END_REF]). They have proposed a fragment of MTL, called Safety MTL. Decidability of this fragment was shown in [START_REF] Ouaknine | Safety metric temporal logic is fully decidable[END_REF] by reducing to the class of ATA mentioned in the previous paragraph. A fragment of MTL called FlatMTL [START_REF] Bouyer | The cost of punctuality[END_REF][START_REF] Bouyer | On expressiveness and complexity in real-time model checking[END_REF] represents an interesting but technically different direction of development. We will comment more on this in Section 3.

We should also discuss the distinction between continues and pointwise semantics. In the later the additional restriction is that formulas are evaluated only in positions when an action happens. So the meaning of F (x=1) α in the continues semantics is that in one time unit from now formula α holds, while in the pointwise semantics we additionally require that there is an action one time unit from now. Pointwise semantics is less natural if one thinks of encoding properties of monadic predicates over reals. Yet, it seems sufficient for descriptions of behaviors of devices, like timed automata, over time [START_REF] Ouaknine | Some recent results in metric temporal logic[END_REF]. Here we consider the pointwise semantics simply because emptiness of alternating timed automata in continues semantics is undecidable even over finite words. At present it seems that an approach through compositional methods [START_REF] Hirshfeld | Logics for real time: Decidability and complexity[END_REF] is more suitable to deal with continues semantics.

The depth of nesting of positive and negative conditions of type "infinitely often" is reflected in the concept of the index of an automaton. Wagner [START_REF] Wagner | Eine topologische Charakterisierung einiger Klassen regulärer Folgenmengen[END_REF], as early as in 1977, established the strictness of the hierarchy of indices for deterministic automata on infinite words. Weak conditions were first considered by Staiger and Wagner [START_REF] Wagner | Automatentheoretische und automatenfreie charakterisierungen topologischer klassen regularer folgenmengen[END_REF]. There are several results testifying their relevance. For example Mostowski [START_REF] Mostowski | Hierarchies of weak automata and week monadic formulas[END_REF] has shown a direct correspondence between the index of weak conditions and the alternation depth of weak second-order quantifiers. For recent results on weak conditions see [START_REF] Murlak | Weak index versus borel rank[END_REF] and references therein.

Organization of the paper After a section with basic definitions we show our main decidability result (Theorem 2). Section 3 introduces Constrained TPTL, gives a translation of the logic into a decidable class of alternating timed automata, and discusses relations with FlatMTL. The last section presents the accompanying undecidability result (Theorem 32).

Preliminaries

A timed word over a finite alphabet Σ is a sequence w = (a 1 , t 1 )(a 2 , t 2 ) . . . of pairs form Σ × R + . We require that the sequence {t i } i=1,2,... is strictly increasing and unbounded. If t i describes the time when event a i has occurred then these restrictions say that there cannot be two actions at the same instance and that there cannot be infinitely many actions in a finite time (non Zeno).

We will consider alternating timed automata (ATA) with one clock [START_REF] Lasota | Alternating timed automata[END_REF]. Let x be this clock and let Φ denote the set of all comparisons of x with constants, eg. (x < 1 ∧ x ≥ 0).

A one-clock ATA over an alphabet Σ is a tuple

A = Q, Σ, q o , δ, Ω : Q → N
where Q is a finite set of states and Ω determines the parity acceptance condition. The transition function of the automaton δ is a finite partial function

δ : Q × Σ × Φ • → B + (Q × {nop, reset}).
where B + (Q × {nop, reset}) is the set of positive boolean formulas over atomic propositions of the form (q, f ) with q ∈ Q and f ∈ {nop, reset}.

Intuitively, automaton being in a state q, reading a letter a and having a clock valuation satisfying θ can proceed according to the positive boolean formula δ(q, a, θ). It means that if a formula is a disjunction then it chooses one of the disjuncts to follow, if it is a conjunction then it makes two copies of itself each following one conjunct. If a formula is "atomic", i.e., of the form (q, reset) or (q, nop) then the automaton changes the state to q and either sets the value of the clock to 0 or leaves it unchanged, respectively. To simplify the definition of acceptance there is also one more restriction on the transition function:

(Partition) For every q ∈ Q, a ∈ Σ and v ∈ R + , there is at most one θ s.t. δ(q, a, θ) is defined, and v satisfies θ.

The acceptance condition of the automaton determines which infinite sequences of states (runs of the automaton) are accepting. A sequence q 1 , q 2 , . . . satisfies:

• weak parity condition if min{q i : i = 1, 2, . . . } is even,

• strong parity condition if lim inf i=1,2,... Ω(q i ) is even.

Observe that the difference between weak and strong condition is that in the weak case we consider all occurrences of states and in the strong case only those that occur infinitely often. In this paper we will mostly consider automata with weak conditions. Whenever we will be considering strong conditions we will say it explicitly.

For an alternating timed automaton A and a timed word w = (a 1 , t 1 )(a 2 , t 2 ) . . . we define the acceptance game G A,w between two players: Adam and Eve. Intuitively, the objective of Eve is to accept w, while the aim of Adam is the opposite. A play starts at the initial configuration (q 0 , 0). It consists of infinitely many phases. The (k+1)-th phase starts in (q k , v k ), ends in some configuration (q k+1 , v k+1 ) and proceeds as follows. Let v := v + t k+1 -t k . Let θ be a unique (by the partition condition) constraint such that v satisfies θ and b = δ(q k , a k+1 , θ) is defined; if there is no such θ then Eve is blocked. Now the outcome of the phase is determined by the formula b. There are three cases: • b = (q, f ) ∈ Q×{nop, reset}: the phase ends with the result (q k+1 , v k+1 ) := (q, f (v )). A new phase is starting from this configuration.

• b = b 1 ∧b 2 :
The winner is Eve if she is not blocked and the sequence of states appearing in the path satisfies the acceptance condition of the automaton. Formally, a play is a finite sequence of consecutive game positions of the form k, q, v or k, q, b , where k is the phase number, b a boolean formula, q a location and v a valuation. A strategy of Eve is a mapping which assigns to each such sequence ending in Eve's position a next move of Eve. A strategy is winning if Eve wins whenever she applies this strategy.

Definition 1 (Acceptance) An automaton A accepts w iff Eve has a winning strategy in the game G A,w . By L(A) we denote the language of all timed words w accepted by A.

The Mostowski index of an automaton with the, strong or weak, acceptance condition given by Ω is the pair consisting of the minimal and the maximal value of Ω: (min(Ω(Q)), max(Ω(Q))). We may assume without a loss of generality that min(Ω(Q)) ∈ {0, 1}. (Otherwise we can scale down the rank by Ω(q) := Ω(q) + 2.). Automata with strong conditions of index (0, 1) are traditionally called Büchi automata and their acceptance condition is given by a set of accepting states Q + ⊆ Q; in our presentation theses are states with rank 0.

Decidability for one-clock timed automata

We are interested in the emptiness problem for one clock ATA. As it was mentioned in the introduction the problem is undecidable for automata with strong Büchi conditions. Here we will show a decidability result for automata with weak acceptance conditions of index (0, 1). A different presentation of these automata is that they are strong Büchi automata where there are no transitions from an accepting state to a non-accepting state. Indeed, once the automaton sees a state of priority 0 then any infinite run is accepting (but there may be runs that get blocked). In the following we will write Q + for accepting states and Q -for the other states. For automata presented in this way the (strong) Büchi acceptance condition says simply: a word is accepted, if there is a strategy for Eve to find an infinite path on which there are only finitely many states from Q -.

Theorem 2 Let A be one-clock Büchi alternating timed automata with no transitions from states in Q + to states in Q -. It is decidable whether the automaton accepts a non Zeno timed word.

In the rest of the section we give the proof of this theorem. To fix the notation we take a one clock ATA:

A = Q, Σ, q o , δ, F ⊆ Q
We will assume that the transition function satisfies the partition condition. For simplicity we also assume that every value of δ is a boolean formula in a disjunctive normal form. Moreover, we will require that every disjunct of every transition of A there is some pair with reset and some pair with nop. It is easy to convert any automaton to an equivalent automaton satisfying these conditions. This form of transitions is required for the structure lemmas of this subsection.

Our first step will be to construct some infinite transition system H(A), so that existence of an accepting run of A is equivalent to existence of some good path in H(A). In the second step we will use some structural properties of this transition system to show decidability of this problem.

An abstract transition system

The goal of this subsection is to define a transition system H(A) such that existence of an accepting computation of A is reduced to existence of some special infinite path in H(A) (Corollary 9). This system will be some abstraction of the transition system of configurations of A. While H(A) will be infinite, it will have some well-order structure and other additional properties that will permit to analyze it.

First consider an auxiliary labeled transition system S(A) whose states are finite sets of configurations, i.e., finite sets of pairs (q, v), where q ∈ Q and v ∈ R + . The initial position in T is P 0 = {(q 0 , 0)} and there are transitions of two types P t → P and P a → P . Transition P t → P is in T iff P can be obtained from P by changing every configuration (q, v) ∈ P to (q, v + t). Transition P a → P is in T iff P can be obtained from P by the following nondeterministic process:

• First, for each (q, v) ∈ P , do the following:

let b = δ(q, a, σ) for the uniquely determined σ satisfied in v , choose one of disjuncts of b, say

(q 1 , r 1 ) ∧ . . . ∧ (q k , r k ) (k > 0), -let Next (q,v) = {(q i , r i (v)) : i = 1 . . . k}.
• Then, let P := (q,v)∈P Next (q,v) .

Definition 3 We will call a sequence P 0 , P 1 , . . . of the states of S(A) accepting if the states of Q -appear only in a finite number of P i .

Lemma 4 A accepts an infinite timed word (a 0 , t 0 )(a 1 , t 1 ) . . . iff there is an accepting sequence in S(A):

P 0 t0 → P 1 a0 → P 2 t1 → P 3 a1 → P 4 . . .

Proof

Recall that acceptance of a word by an automaton is defined as existence of a winning strategy for Eve in the acceptance game. This is a game with Büchi conditions, so if Eve has a winning strategy, then she has a memoryless strategy. This strategy gives a run of the form required by the lemma.

Our next goal is to remove time labels on transitions. Still we do not want just to erase them, as then we will not to be able to say if a word is Zeno or not. We start by introducing regions.

Let d max denote the biggest constant appearing in δ, i.e., the transition function of the automaton. Let set reg of regions be a partition of R + into 2 • (d max + 1) sets as follows: reg := {{0}, (0, 1), {1}, (1, 2), . . . , (d max -1, d max ), {d max }, (d max , +∞)} There are three kinds of regions: bounded intervals (denoted reg I ), one-point regions (denoted reg P ), and one unbounded interval (d max , +∞). We will use the notation I i for the region (i -1, i). In a similar way, I ∞ will stand for (d max , +∞). For v ∈ R + , let reg(v) denote its region; and let fract(v) denote the fractional part of v

Recall that a state P is a finite set of pairs (q, v). If v ∈ I ∞ then the precise value of v does not matter from the point of view of the automaton. For other values it is important to look at their fractional parts. Among all v ∈ I ∞ appearing in P take the one with the biggest fractional part. Then, by making the time pass we can get v to a new region without changing the regions of valuations with smaller, but positive, fractional parts. Intuitively this is a smallest delay what makes a visible change to P . As integer valuation would force us to introduce a case distinction we will set things so that they can be avoided.

In order not to have precise time information on transitions we introduce a new alphabet

Σ = Σ ∪ {(delay, ε)} ∪ ({delay} × Σ),
and three new kinds of transitions. Choose a valuation v among these with reg(v) = I ∞ with a maximal fract(v). A transition on a letter (delay, ε) will make the time pass so that the valuation v goes to the next interval region and other valuations do not change their regions:

P (delay,ε) -→ P if P t1 → P 1 t2
→ P for some P 1 and t 1 , t 2 > 0 such that there is (q, v) ∈ P , with v + t 1 being an integer and v + t 1 + t 2 in the following interval region. Moreover, for all (q , v ) ∈ P if fract(v) = fract(v ) then the value v + t 1 + t 2 is in the same region as v .

Transition on a will do the action and make some time pass without any valuation changing the region. → P for some P 1 , and t 1 > 0 such that for every (q, v) ∈ P , the value v + t 1 is in the same region as v.

Finally, we come to the most complex (delay, a) transition. For reasons explained above, we did not allow transitions (delay, ε) to reach one-point regions. Still it is important to be able to execute actions in those regions. A transition on (delay, a) permits to reach a one-point region, execute the action, and leave the region.

P

(delay,a)

-→ P if P t1 → P 1 a → P 2 t2
→ P for some P 1 , P 2 and t 1 , t 2 > 0 such that there is (q, v) ∈ P , with v+t 1 being an integer and v+t 1 +t 2 in the following interval region. Moreover for all (q , v ) ∈ P if fract(v) = fract(v ) then the value v + t 1 + t 2 is in the same region as v .

The following lemma shows that with a new alphabet we can replace non Zeno condition by a simple infinitary condition. To make the lemma true, we need some additional assumption:

Lemma 5 There is a non Zeno accepting sequence in S(A):

P 0 t0 → P 1 a0 → P 2 t1 → P 3 a1 → P 4 . . .
iff there is an accepting sequence

P 0 σ0 -→ P 1 σ1 -→ P 2 . . .
where σ 0 , σ 1 , • • • ∈ Σ and (delay, •) letters appear infinitely often in the sequence.

The next step in the construction is to abstract from valuations in the states of the transition system. Below we work with finite words of the form Λ * I • Λ ∞ where Λ I = P(Q × reg I ) and Λ ∞ = P(Q) × {∞}). Definition 6 For a state P of T we define a word H(P ) from Λ * I • Λ ∞ as the one obtained by the following procedure:

• replace each (q, v) ∈ P by a triple q, reg(v), fract(v) if v ≤ d max (this yields a finite set of triples)

• sort all these triples w.r.t. fract(v) (this yields a finite sequence of triples)

• group together triples having the same value of fract(v) (this yields a finite sequence of finite sets of triples)

• forget about fract(v), i.e., replace each triple q, reg(v), fract(v) by a pair (q, reg(v)) (this yields a finite sequence of finite sets of pairs, a word in Λ * I ).

• Add at the end the letter ({q : (q, v)

∈ P, v > d max }, I ∞ ) ∈ Λ ∞ .
Finally, we can define H(A). It has Λ * I × Λ ∞ as states, and for every letter α ∈ Σ there is a transition c σ -→ c if there are states P, P of S(A) such that P a -→ P and

H(P ) = c, H(P ) = c . Lemma 7 If H(P 1 ) = H(P 2 ) and P 1 σ -→ P 1 then P 2 σ -→ P 2 with H(P 1 ) = H(P 2 ).
Definition 8 We say that a path in H(A) is good, if it passes through infinitely many transitions labeled by letters (delay, •).

Corollary 9 A accepts an infinite non Zeno timed word iff there is a good path in H(A) starting in the state ({(q 0 , I 1 )}, {∅, I ∞ }) with only finitely many appearances of states from Q -.

Proof

A accepts a non Zeno word iff there is a path in S(A) satisfying the acceptance condition. By Lemma 5 it is equivalent to having a good path in S(A) with transitions from the alphabet Σ satisfying the acceptance conditions. Lemma 7 shows that this is equivalent to having a good path in H(P ).

In the rest of this section we give a more explicit characterization of transitions in H(A).

Lemma 10 Consider a state (λ 1 . . . λ k , λ ∞ ) of H(A). If k = 0 then there is no (delay, •) transition from this state. Otherwise let λ k = {(q, I d+1 ) : d < d max , (q, I d ) ∈ λ k } and λ ∞ = λ ∞ ∪ {(q, I ∞ ) : (q, I dmax ) ∈ λ k }. In H(A)
there is exactly one transition on (delay, •):

(λ 1 . . . λ k , λ ∞ ) (delay, ) -→ (λ k λ 1 . . . λ k-1 , λ ∞ ) if λ k = ∅ (λ 1 . . . λ k , λ ∞ ) (delay, ) -→ (λ 1 . . . λ k-1 , λ ∞ ) otherwise
In order to define transitions of H(A) on an action a, we define an auxiliary notion of a transition from λ ∈ Λ I ∪ Λ ∞ . By the partition condition, for every (q, r) ∈ λ there is at most one constraint θ such that every valuation in r satisfies this constraint and δ(q, a, θ) is defined. We choose a conjunct from δ(q, a, θ):

(q 1 , nop) ∧ • • • ∧ (q l , nop) ∧ (q 1 , reset) ∧ • • • ∧ (q m , reset)
this choice gives two sets: Next(q, r) = {(q 1 , r), . . . , (q l , r)} and Next 0 (q, r) = {(q 1 , I 1 ), . . . , (q m , I 1 )}. We put λ a -→ A (λ , δ ); where λ = (q,r)∈λ N ext(q, r) and δ = (q,r)∈λ N ext 0 (q, r) Lemma 11 In H(A) transitions on an action a have the form:

(λ 1 . . . λ k , λ ∞ ) a -→ (δ λ 1 . . . λ k , λ ∞ ) where λ i a -→ A (λ i , δ i ) and δ = δ i (for i = 1, . . . , k, ∞).
Note that neither δ nor any of λ i may be empty. Observe also that there are as many transitions a -→ from λ as there are choices of different conjuncts for each pair (q, r) in λ.

Finally, we have the most complicated case of (delay, a) action.

Lemma 12

In H(A) the transitions on an action (delay, a) have the form:

(λ 1 . . . λ k , λ ∞ ) (delay,a) -→ (δ λ 1 . . . λ k-1 , λ ∞ )
where the elements on the right are obtained by preforming the following steps:

• First, we change regions in λ k . Every pair (q, I d ) ∈ λ k becomes (q, {d}).

Let us denote the result by λ 1 k .

• For i = 1, . . . , k, ∞ we take λ i , δ i such that:

λ 1 k a -→ A (λ k , δ k ) and λ i a -→ A (λ i , δ i ) for i = k.
• We increase again regions in λ k : from {d} they become I d+1 , or

I ∞ if d = d max . • We put δ = δ i ∪ {(q, I d ) : (q, {d}) ∈ λ k , d < d max } and λ ∞ = λ ∞ ∪ {(q, I ∞ ) : (q, {d max }) ∈ λ k }.
We write c → c , c

(delay,•) -→ c , c c , c Σ *
c to denote that we may go from a configuration c to c using one transition, one transition reading a letter of the form (delay, •), any number of transitions or any number of transitions reading only letters from Σ, respectively.

Finding a good path in H(A).

By the Corollary 9, our problem reduces to deciding if there is a good path in H(A). The decision procedure works in two steps. In the first step we compute the set G of all configurations from which there exists a good computation. Observe that if a configuration from G has only states from Q + then this configuration is accepting. So, in the second step it remains to consider configurations that have states from both Q -and Q + . This is relatively easy as an accepting run from such a configuration consists of a finite prefix ending in a configuration without states from Q -and a good run from that configuration. Hence, there is a good accepting computation from a configuration iff it is possible to reach from it a configuration from G that has only Q + states. Once we know G, the later problem can be solved using the standard reachability tree technique.

Computing accepting configurations

We start with the second step of our procedure as it is much easier than the first one. We need to decide if from an initial state one can reach a configuration from G having only Q + states. We can assume that we are given G but we need to discuss a little how it is represented. It turns out that there are useful well-quasi-orders on configurations that allow to represent G in a finitary way.

A well-quasi-order is a relation with a property that for every infinite sequence c 1 , c 2 , . . . there exist indexes i < j such that the pair (c i , c j ) is in the relation.

The order we need is a relation over configurations of H(A). We say that (λ

1 . . . λ k , λ ∞ ) (λ 1 . . . λ k , λ ∞ ) if λ ∞ ⊆ λ ∞
and there exists a strictly increasing function f : {1, . . . , k} → {1, . . . , k } such that λ i ⊆ λ f (i) for each i. Observe that here we use the fact that each λ i is a set so we can compare them by inclusion. This relation is somehow similar to the relation of being a subsequence, but we do not require that the corresponding letters are equal, only that the one from the smaller word is included in the one from the greater word. The following lemma follows by a standard application of Highman's lemma.

Lemma 13

The relation is a well-quasi-order.

The following shows an important interplay between relation and transitions of H(A).

Lemma 14 Let c 1 , c 1 , c 2 be configurations of H(A) such that c 1 c 1 . Whenever c 1 c 2 , then there exist c 2 c 2 such that c 1 c 2 and the second computation has the length not greater than the first one. Similarly, when from c 1 there exists a good computation, then from c 1 such a computation exists.

Proof

For the first statement of the lemma we will simulate one transition from -→ c 2 we have two cases depending on the relation between one before last element of the two configurations. To be more precise, suppose that c 1 = (λ 1 . . . λ k , λ ∞ ) and c 1 = (λ 1 . . . λ k , λ ∞ ). If λ k ⊆ λ k then we may do (delay, ) from c 1 and we get c 2 c 2 . Otherwise already c 1 c 2 , we do not do any action and take c 2 = c 1 . Similarly for (delay, a): either we match it with (delay, a) or just with a. An obvious induction gives a proof of the first statement.

For the second statement we need to show that the computation from c 1 obtained by matching steps as described above is good (if the one from c 1 has been good). This is not immediate as we remove some (delay, •) letters in the matching computation.

Fix a good computation from c 1 . Let c 2 be a configuration in a computation starting from c 1 , and let c 2 be the corresponding configuration in the matching computation from c 1 . To arrive at a contradiction assume that there are no delays after c 2 . Let us denote

c 2 = (λ 1 . . . λ k , λ ∞ ) and c 2 = (λ 1 . . . λ k , λ ∞ ).
Because c 2 c 2 , we know that λ k is covered by some λ i , i.e., λ k ⊆ λ i . Let us take the biggest possible i. If some a-action is done from c 2 then it is matched by a-action from c 2 , and for the resulting configurations the inclusion is preserved. This can happen only finitely many times though, as there are infinitely many (delay, •) actions after c 2 . If (delay, •) action is done from c 2 and i = k then it is matched by a (delay, •) action from c 2 , a contradiction with the choice of c i . If i < k then the element λ k is left on its position in c 2 , while in c 2 we remove λ k , hence λ i covering λ k gets closer to the end of the sequence. Repeating this argument, we get that the covering λ i finally becomes the last element and the previous case applies.

Corollary 15

The set G is downward closed, so it can be described by the finite set of minimal elements that do not belong to it.

As we have mentioned before, there is a good accepting computation from a configuration iff it is possible to reach from it a configuration from G that has only Q + states. The following lemma says that this property is decidable.

Lemma 16 Let X be a downward closed set in H(A). It is decidable if from a given configuration one can reach a configuration in X that has only states from Q + .

Proof

We will use a standard reachability tree argument. The reachability tree is a tree in which the initial configuration is in the root, and every configuration has as children all configurations, that may be reached by reading one letter. The algorithm constructs a portion t of the tree according to the following rule: do not add a node c to t in a situation when among its ancestors there is some c c . Each path of t is finite because is a well-quasi-order. Furthermore, since degree of every node is finite, t is a finite tree. Then we check if in t there is a configuration from X without states from Q -.

We only need to prove, that if in the whole reachability tree there is a configuration as above (which means that H(A) may accept), it is also some in t. Let c be such configuration reachable from initial configuration of H(A) by a path π of the shortest length. Assume that c is not in t, i.e. there are two nodes on π, say c 1 and c 2 , such that c 1 is an ancestor of c 2 and c 1 c 2 (i.e. c 2 was not added to t). Then from Lemma 14, there exists c c that may be reached from c 1 and the path from c 1 to c will be no longer than that from c 2 to c. So the path leading to c from the initial configuration is strictly shorter than π. Moreover, as c c and X is downward closed, we immediately deduce that c ∈ X, and c does not contain states from Q -. A contradiction.

Computing G

In this subsection we deal with the main technical problem of the proof that is computing the set G of all configurations from which there exist a good computation. We will actually compute the complement of G. While we will use well-orderings in the proof, standard termination arguments do not work in this case. We need to use in an essential way a very special form of transitions our systems have.

We write X↑ for an upward closure of set X:

X↑= {c : ∃ c ∈X c c}
Observe that by Lemma 14 the complement of G is upward closed. Let set pre ∀ delay (respectively pre ∀ Σ * ) contain all configurations, from which after reading any letter (delay, •) (any number of letters from Σ), we have to reach a configuration from X:

pre ∀ delay (X) = {c : ∀ c (c (delay,•) -→ c ⇒ c ∈ X)} pre ∀ Σ * (X) = {c : ∀ c (c Σ * c ⇒ c ∈ X)}
Now we can use these pre operations to compute a sequence of sets of configurations.

Z -1 = ∅ Z i = pre ∀ Σ * (pre ∀ delay (Z i-1 ↑))
It is important that we may effectively represent and compare all the sets Z i ↑. Because the relation is a well-quasi-order, any upward closed set X ↑ may be represented by finitely many elements c 1 , . . . , c k (called generators) such that X↑= {c 1 , . . . , c k }↑. Moreover, an easy induction shows that Z i-1 ↑⊆ Z i ↑ for every i (because both pre ∀ operations preserve inclusion). Once again, because relation is a well-quasi-order, there has to be i such that

Z i-1 ↑= Z i ↑. Let us write Z ∞ for this Z i .
First, we show that Z ∞ is indeed the complement of G.

Lemma 17 There is a good computation from a configuration c iff c ∈ Z ∞ ↑.

Proof

(⇒) We show by induction that c ∈ Z i for i = -1, 0, 1 . . . . For i = -1 it is obvious. Assume by contrary, that there exists a good computation from c, but c ∈ Z i ↑. Then there exists c c with c ∈ Z i . From Lemma 14 we know that a good infinite computation exists also from c . This computation may first read some letters from Σ, but finally it has to read a letter (delay, •), that results in a configuration c 2 . Definition of Z i tells us that c 2 ∈ Z i-1 ↑. But from c 2 there is also a good infinite computation, a contradiction.

(⇐) Assume, that every computation (finite or infinite) from c reads at most k letters (delay, •). Easy induction on k shows that c ∈ Z k .

To compute Z ∞ it is enough to show how to compute Z i ↑ from Z i-1 ↑. This is the most difficult part of the proof that will occupy the rest of the subsection. Once this is done we will calculate all the sets Z i ↑, starting with Z -1 = ∅ and ending when Z i-1 ↑= Z i ↑.

The main idea in calculating pre ∀ Σ * (pre ∀ delay (X)) is that the length of its generators may be bounded by some function in the length of generators of X. This is expressed by the following lemma.

Lemma 18 Given an upward closed set X we can compute a constant D(X) (which depends also on our fixed automaton A) such that the size of every minimal element of pre ∀ Σ * (pre ∀ delay (X)) is bounded by D(X) Once we know the bound on the size of generators, we can try all potential candidates. The following lemma shows that it is possible.

Lemma 19 For every upper-closed set X, the membership in pre ∀ Σ * (pre ∀ delay (X)) is decidable.

Together Lemmas 18 and 19 allow us to compute the sequence Z 0 , Z 1 , . . . , Z ∞ and hence also G.

To finish the proof of the theorem, it remains to give proofs of the two lemmas. However Lemma 18 is substantially more complicated while Lemma 19 we get as a side effect. We will calculate separately bounds for pre ∀ delay (X) and for pre ∀ Σ * (X). In the sequel we will need to use some special representation for sets of configurations.

Definition 20 A compressed configuration has a form c = (λ 1 . . . λ l , f, λ ∞ ) where λ i ∈ Λ I , λ ∞ ∈ Λ ∞ and f : Λ I → P(Λ I ) (values of f are subsets of Λ I ).
On compressed configurations we introduce an expansion operation parametrized by words from Λ * I .

Definition 21 A compressed configuration c = (λ 1 . . . λ l , f, λ ∞ ) may be expanded in a context of some word λ 0 1 . . . λ 0 k ∈ Λ * I , resulting in the set of configurations (λ 1 . . . λ l λ l+1 . . . λ l+k , λ ∞ ) such that λ l+i ∈ f (λ 0 i ) for 1 ≤ i ≤ k. We will use exp( c, λ 0 1 . . . λ 0 k ) to denote the set of obtained configurations. Similarly, if C is a set of compressed configurations we write Exp( C, λ 0 1 . . . λ 0 k ) for {exp( c, λ 0 1 . . . λ 0 k ) : c ∈ C}.

Observe that the value f (λ) for λ not appearing in λ 0 1 . . . λ 0 k does not matter; moreover if some f (λ 0 i ) = ∅ then the result of expanding is the empty set. We use compressed configurations, because the set of successors of a configuration may be described by a bounded number of compressed configurations. However, due to nondeterminism, there is unbounded number of successors. To see this suppose that there is more than one choice of transition on action a form a letter λ then every occurrence of λ in a configuration may make a choice independently.

Let us see how to calculate pre ∀ delay (X). Some care is needed as this set is not upward closed with respect to relation. This is because (delay, •) action treats the one before last element of a configuration in a special way. So if something is inserted after λ k in (λ 1 . . . λ k , λ ∞ ) then the delay operation uses this inserted element instead of λ k . As a side remark let us mention that using the upward closure of pre ∀ delay (Z i-1 ↑) in the definition of Z i would be incorrect (Lemma 17 would not be true).

To remedy this problem we use a refined relation r . Given two configura-

tions c = (λ 1 . . . λ k , λ ∞ ) and c = (λ 1 . . . λ k , λ ∞ ) we set c r c iff k > 0, c c and λ k ⊆ λ k
Note that the set pre ∀ delay (X) is upward closed with respect to relation r , when X is upward closed with respect to . This is because if

c 1 r c 1 and c 1 (delay,•) -→ c 2 then also c 1 (delay,•) -→ c 2 with some c 2 c 2 . Hence, if c 1 ∈ pre ∀ delay (X) then c 1 ∈ pre ∀ delay (X).
The following lemma tells us that successors of a configuration may be described using compressed configurations and that there are not too many of them:

Lemma 22 For every configuration c 0 = (λ 1 . . . λ k , λ ∞ ), k > 0 there exists a finite set of compressed configurations C(λ k , λ ∞ ) (depending only on λ k and λ ∞ ) such that:

• if c 0 (delay,•) -→ c then c ∈ Exp( C(λ k , λ ∞ ), λ 1 . . . λ k-1 ); • if c ∈ Exp( C(λ k , λ ∞ ), λ 1 . . . λ k-1 ) then c 0 (delay,•)
-→ c for some c c.

Proof

The transition on (delay, ) is deterministic. If c 0 (delay, )

-→ c then we either have c = (λ k λ 1 . . . λ k-1 , λ ∞ ) or c = (λ 1 . . . λ k-1 , λ ∞ ) depending on λ k . In the first case we add c = (λ k , sgl, λ ∞ ) into C(λ k , λ ∞ ), in the second case c = ( , sgl, λ ∞ ), where sgl(λ) = {λ}. In both cases exp( c, λ 1 . . . λ k-1 ) = {c }. Now consider transitions reading (delay, a). A result of this transition is not unique and depends on the choice of a transition for each element of the configuration. We fix a set T of transitions λ a -→ A (λ , δ ); intuitively these are allowed transitions from λ 1 , . . . , λ k-1 . We also fix transitions λ

1 k a -→ A (λ k , δ k ) and λ ∞ a -→ A (λ ∞ , δ ∞ ) (where λ 1
k is λ k with increased regions as in Lemma 12). This choice of transitions gives us a compressed configuration c = (δ, f, λ ∞ ) where

δ = δ k ∪ δ ∞ ∪ {(q, I d+1 ) : (q, {d}) ∈ λ k } ∪ {δ : (λ a -→ A (λ , δ )) ∈ T , λ ∈ Λ I } f (λ) = {λ : (λ a -→ A (λ , δ )) ∈ T } λ ∞ =λ ∞ ∪ {(q, I ∞ ) : (q, {d max }) ∈ λ k } We add c into C(λ k , λ ∞ ).
We now show that the constructed C(λ k , λ ∞ ) has the required properties. Consider a successor c of c 0 that is reached using the transitions we have fixed.

In particular, we require that each transition from T is used at least once. Take c as calculated above. Directly from the definition we get c ∈ exp( c, λ 1 . . . λ k-1 ). As the choice of transitions was arbitrary this gives the first statement of the lemma.

Now consider c = (δλ 1 . . . λ k-1 , λ ∞ ) ∈ exp( c, λ 1 . . . λ k-1 ) where c = (δ, f, λ ∞ ) is obtained by a choice of some T and some transitions from λ 1 k and λ ∞ . For every i let us choose some transition λ i a -→ A (λ i , δ i ) from T (there is at least one such transition in T because

λ i ∈ f (λ i )). Take c = (δ λ 1 . . . λ k-1 , λ ∞ ) where δ = δ k ∪ δ ∞ ∪ {(q, I d+1 ) : (q, {d}) ∈ λ k } ∪ 1≤i≤k-1 δ i
Then δ ⊆ δ so c c. It is easy to check that there is a transition c 0 (delay,a)

-→ c .

We need to find all minimal elements of pre ∀ delay (Z i-1 ↑). The following lemma will allow us to get a bound on their size.

Lemma 23 For a given C and a set X upward closed with respect to relation r there exists a constant B(X, C) (and we may compute it) such that if for some λ 0 1 . . . λ 0 k :

Exp( C, λ 0 1 . . . λ 0 k ) ⊆ X then there exist 1 ≤ i 1 < • • • < i m ≤ k, m < B(X, C) with Exp( C, λ 0 i1 . . . λ 0 im ) ⊆ X Proof
First suppose that C is a singleton { c}; where c = (λ 1 . . . λ l , f, λ ∞ ). We describe a construction of a finite automaton A X b c accepting the language L X b c = {λ 1 . . . λ k : exp( c, λ 1 . . . λ k ) ⊆ X} Recall that X is an upward closed set with respect to r relation. This implies that L X b c is upward closed with respect to the standard subsequence relation . It is easy to check that for every letter λ ∈ Λ I , if L ⊆ Λ * I is -upward closed then the quotient L/λ is also -upward closed. Moreover L ⊆ L/λ, as if w ∈ L then aw ∈ L that implies w ∈ L/λ. Because is a well-quasi-order, this last property implies that the set of all possible quotients of L X b c , i.e. the languages L X b c /w for w ∈ Λ * I , is finite. These quotients are the states of A X b c we were looking for. Indeed A X b c is the minimal deterministic automaton for L X b c . Take B(X, { c}) to be the size of the automaton. Form the pumping lemma it follows that if the word λ 0 1 . . . λ 0 k is accepted by A X b C then there is a subsequence of length ≤ B(X, { c}) accepted by A X b C . Now consider a general situation. For every c ∈ C from above we have some subsequence λ 0 i1 . . . λ 0 im of length m ≤ B(X, { c}), such that exp( c, λ 0 i1 . . . λ 0 im ) ⊆ X. We take all the elements from all these subsequences, getting a subsequence of length ≤ B(X, C) := b c∈ b C B(X, { c}) such that all the inclusions hold. The above two lemmas give us a bound on the size of minimal elements in pre ∀ delay (Z i-1 ↑).

Lemma 24 There is an algorithm that given X↑ computes a constant M delay (X↑ ) such that, the size of every minimal element of pre ∀ delay (X ↑) is bounded by M delay (X↑).

Proof

There are only finitely many different C(λ k , λ ∞ ) as constructed in Lemma 22. Let M delay be the maximal possible value of B(X↑, C(λ k , λ ∞ )).

Suppose c 0 = (λ 0 1 . . . λ 0 k , λ 0 ∞ ) is a minimal element of pre ∀ delay (X↑). Take the set C(λ 0 k , λ 0 ∞ ) as given by Lemma 22. We have that Exp( C(λ 0 k , λ 0 ∞ ), λ 0 1 . . . λ 0 k-1 ) ⊆ X ↑ by the second statement of this lemma. From Lemma 23 we get a subsequence λ 1 . . . λ l of λ 0 1 . . . λ 0 k-1 whose length is bounded by B(X↑, C(λ 0 k , λ 0 ∞ )) ≤ M delay and such that Exp( C(λ 0 k , λ 0 ∞ ), λ 1 . . . λ l ) ⊆ X↑. By the first statement of Lemma 22 we get that (λ 1 . . . λ l λ 0 k , λ 0 ∞ ) ∈ pre ∀ delay (X↑). By the minimality of c 0 , we have that c 0 = (λ 1 . . . λ l λ 0 k , λ 0 ∞ ), so its length is bounded by M delay + 2. Now we describe how to calculate pre ∀ Σ * (Y )↑ for any set Y upward closed with respect to r relation. The first lemma says, that we may represent successors using compressed configurations.

Lemma 25 For every compressed configuration c 0 there is a set of compressed configurations C( c 0 ) (and we may compute it) such that for every λ 0 1 . . . λ 0 k :

• if c 0 ∈ exp( c 0 , λ 0 1 . . . λ 0 k ) and c 0 a -→ c for some letter a ∈ Σ then c ∈ Exp( C( c 0 ), λ 0 1 . . . λ 0 k );

• if c ∈ Exp( C( c 0 ), λ 0 1 . . . λ 0 k ) then c 0 a -→ c for some c r c, a ∈ Σ and c 0 ∈ exp( c 0 , λ 0 1 . . . λ 0 k ).

Proof

Let c 0 = (λ 1 . . . λ l , f, λ ∞ ). Fix a letter a ∈ Σ. We fix a set T of transitions λ a -→ A (λ , δ ); intuitively these are allowed transitions from λ ∈ f (λ 0 i ). We also fix transitions λ i a -→ A (λ i , δ i ) for i = 1, . . . , l, ∞. This choice of transitions gives us a compressed configuration c = (δλ 1 . . . λ l , f , λ ∞ ) where

δ = i=1...,l,∞ δ i ∪ {δ : (λ a -→ A (λ , δ )) ∈ T , λ ∈ Λ I } f (λ 0 ) ={λ : (λ a -→ A (λ , δ )) ∈ T , λ ∈ f (λ 0 )} We add c into C( c 0 ).
For the first statement of the lemma, take c 0 ∈ exp( c 0 , λ 0 1 . . . λ 0 k ) and consider any successor c of c 0 that is reached using the transitions we have fixed. In particular we require that each transition from T is used at least once. Take c as calculated above. Then directly from the definition we get c ∈ exp( c, λ 0 1 . . . λ 0 k ). As the choice of transitions was arbitrary this gives the first statement of the lemma. Now consider some c ∈ C( c 0 ). It is of the form (δλ 1 . . . λ l , f , λ ∞ ). According to the above, it was constructed from c 0 using some transitions λ i a -→ A (λ i , δ i ) for i = 1, . . . , l, ∞ and some set of transitions T . Take c ∈ exp( c, λ 0 1 . . . λ 0 k ). We have that c is of the form (δ λ 1 . . . λ l , λ l+1 . . . λ l+k , λ ∞ ) where λ 1 , . . . λ l are as in c and for i = 1, . . . , k we can choose from T transitions λ l+i a -→ A (λ l+i , δ l+i ) such that λ l+i ∈ f (λ 0 i ). Take c 0 = (λ 1 . . . λ l , λ l+1 , . . . , λ l+k , λ ∞ ), i.e., a configuration whose components are predecessors of transitions we have selected. We have c 0 ∈ exp( c 0 , λ 0 1 . . . λ 0 k ) by the definition of expansion. Let c = (δ λ 1 . . . λ l+k , λ ∞ ) with δ = i=1,...,l+k,∞ δ i . Observe that δ may be a proper subset of δ if not all transitions from T has been used. Then c r c and there is a transition c 0 a -→ c .

The following lemma says that we may list a big enough portion of all configurations reachable from some c 0 (similarly like in step two of the decision procedure) and moreover that size of this portion is bounded by a constant.

Lemma 26 For every λ ∞ ∈ Λ ∞ we can construct a set C Σ * (λ ∞ ) such that for every λ 1 . . . λ k ∈ Λ * I : • If (λ 1 . . . λ k , λ ∞ ) Σ * c for some c then there is c r c such that c ∈ Exp( C Σ * (λ ∞ ), λ 1 . . . λ k ). • If c ∈ Exp( C Σ * (λ ∞ ), λ 1 . . . λ k ) then there is c r c with (λ 1 . . . λ k , λ ∞ ) Σ * c .

Proof

Take the compressed configuration c 0 = ( , sgl, λ ∞ ). We define a set C of compressed configurations as a closure of { c 0 } on the operation defined in Lemma 25. This set may be infinite but we do not worry about it for the moment. We show first that it satisfies the requirements of the lemma. Take some λ 1 . . . λ k ∈ Λ * I and c such that (λ

1 . . . λ k , λ ∞ ) Σ * c.
We need to show that we can find an extended configuration c ∈ C such that c ∈ exp( c, λ 1 . . . λ k ). The proof is by easy induction on the number of transitions. For the base step we have (λ 1 . . . λ k , λ ∞ ) ∈ exp( c 0 , λ 1 . . . λ k ), and the induction step is given by the first statement of Lemma 25. Now, suppose that c ∈ C and c ∈ exp( c, λ 1 . . . λ k ). An induction using the second statement of Lemma 25 shows that there is c r c such that (λ

1 . . . λ k , λ ∞ ) Σ * c .
In order to reduce C to a finite set we once again use well-quasi-orders. We define a relation on compressed configurations:

(λ 1 . . . λ l , f , λ ∞ ) (λ 1 . . . λ l , f, λ ∞ ) ⇐⇒ (λ 1 . . . λ l , λ ∞ ) r (λ 1 . . . λ l , λ ∞ ) and f = f
This relation is a well-quasi-order. We take C Σ * (λ ∞ ) to be the set of minimal elements in this quasi-order. It is clear that

Exp( C Σ * (λ ∞ ), λ 1 . . . λ k ) ⊆ Exp( C, λ 1 . . . λ k ) for

Proof

There are only finitely many different C(λ ∞ ) constructed in the above lemma.

Let M Σ * be the maximal possible value of

B(Y, C(λ ∞ )). Suppose c 0 = (λ 0 1 . . . λ 0 k , λ 0 ∞ ) is a minimal element of pre ∀ Σ * (Y ).

Proof

Given a configuration c we need to decide if c ∈ pre ∀ Σ * (Y ). We apply successively a -→ transitions to c constructing a part of the reachability tree. We stop the development in a node if it has an ancestor smaller with respect to r -relation.

As r is a well-quasi-order, and the branching at each node is finite, we get a finite tree t.

It remains to argue that this construction is correct. If in the above process we find a configuration that is not in Y then clearly c is not in pre ∀ Σ * (Y ). For the other direction, assume conversely that there is c / ∈ Y with c c . This is impossible by the choice of c .

Proof (of Lemma 18) Take an upward closed set X. By Lemma 24 we can compute a constant M delay that bounds the size of minimal elements in Y = pre ∀ delay (X). Using Lemma 28 we can find the minimal elements of Y by enumerating all configurations of size bounded by M delay . Observe that Y is r upward closed.

Once we have computed Y , Lemma 27 gives us a constant

M Σ * (Y ) bounding the size of minimal elements in pre ∀ Σ * (Y ) = pre ∀ Σ * (pre ∀ delay (X)).

Proof (of Lemma 19)

We first compute the set Y = pre ∀ delay (X) as described above. We can then use Lemma 29 to test for the membership in pre ∀ Σ * (Y ) = pre ∀ Σ * (pre ∀ delay (X)).

Constrained TPTL

In this section we discuss a fragment of TPTL (timed propositional temporal logic) that can be translated to automata from our decidable class. We compare this fragment with other known logics for real time. We will be rather brief in presentations of different formalisms, and refer the reader to recent surveys [START_REF] Bouyer | Model-checking timed temporal logics[END_REF][START_REF] Ouaknine | Some recent results in metric temporal logic[END_REF]. TPTL [START_REF] Alur | A really temporal logic[END_REF] is a timed extension of linear time temporal logic that allows to explicitly set and compare clock variables. We will consider the logic with only one clock variable that we denote TPTL 1 . The syntax of the logic is:

p | α ∧ β | α ∨ β | αUβ | α U β | x ∼ c | x.α
where: p ranges over action letters, x is the unique clock variable, and x ∼ c is a comparison of x with a constant. We do not have negation in the syntax, but from the semantics it will be clear that the negation is definable.

The logic is evaluated over timed sequences w = (a 1 , t 1 )(a 2 , t 2 ) . . . We define the satisfiability relation, w, i, v α saying that a formula α is true at a position i of a timed word w with a valuation v of the unique clock variable:

w, i, v p if a i = p w, i, v x ∼ c if t i -v ∼ c w, i, v x.α if w, i, t i α w, i, v αUβ if ∃ j>i (w, j, v α and ∀ k∈(i,j) w, k, v β) w, i, v α Uβ if ∀ j>i (w, j, v β or ∃ k∈(i,j) w, k, v α)
As usual, until operators permit us to introduce sometimes and always operators:

F α ≡ ttUα Aα ≡ ff Uα
For the following it will be interesting to note that the two until operators are inter-definable once we have always and sometimes operators:

α Uβ ≡ Aβ ∨ βUα αUβ ≡ Eβ ∧ β Uα
Observe that TPTL 1 subsumes metric temporal logic (MTL). For example: αU (i,j) β of MTL is equivalent to x.(αU((x > i) ∧ (x < j) ∧ β)). We will not present MTL here, but rather refer the reader to [START_REF] Bouyer | On the expressiveness of tptl and mtl[END_REF] where it is also shown that the following TPTL 1 formula is not expressible in MTL:

x.(F (b ∧ F (c ∧ x ≤ 2))). (1)
The satisfiability problem over infinite timed sequences is undecidable for MTL [START_REF] Ouaknine | On the decidability of metric temporal logic[END_REF], hence also for TPTL 1 . Using our decidability result for alternating timed automata, we can nevertheless find a decidable fragment, that we call Constrained TPTL. The definition of this fragment will use an auxiliary notion of positive TPTL 1 formulas. These formulas can be translated into automata where all states are accepting. The set of positive formulas is given by the following grammar:

p | x.ϕ | x ∼ c | ϕ ∨ ψ | ϕ ∧ ψ | ϕ Uψ | F ((x < c) ∧ ψ) | F ((x ≤ c) ∧ ψ)
The set of formulas of Constrained TPTL is:

p | x.ϕ | x ∼ c | α ∨ β | α ∧ β |αUβ | ϕ ϕ positive.
Observe that the formula (1) belongs to the positive fragment if we add redundant (x ≤ 2) after b.

Theorem 30 It is decidable if there is a non Zeno timed word that is a model of a given Constrained TPTL formula. The complexity of the problem cannot be bounded by a primitive recursive function.

Proof

It is enough to give a translation from formulas to automata in the class from Theorem 2. The translation is on the syntax of the formula.

We start for the automaton for the positive formulas. The states of an automaton for a formula will be all subformulas of the formula. A state associated to a formula α will be denoted by [α]. The intended semantics is that a timed word w is accepted from [α] iff w, 1, 0 α.

The transition relation of the automaton is given in the following table.

[p]

p -→ [x ∼ c] * -→ x∼c [α ∨ β] ε -→ [α] ∨ [β] [α ∧ β] ε -→ [α] ∧ [β] [x.α] ε -→ x:=0 [α] [α Uβ] * -→ [α] ∨ ([β] ∧ [α Uβ]) [F β] * -→ [β] ∨ [F β]
The transitions follow directly the semantics of formulas; state is a special state from which every timed word is accepted. As our automaton is alternating, on the right hand side of the transition we can write a boolean expression on successor states. We should also explain labels * and ε over transitions. Transition * -→ is just a shortcut for transitions on all letters of the alphabet. Transitions ε -→ and ε -→

x:=0 can be seen as eager ε-transitions of the automaton: they are executed as soon as they are enabled. The other way is to consider them as rewrite rules where the real transition of the automaton is obtained at the end of the rewriting, i.e., reaching a transition on a letter. In this interpretation we should not forget to accumulate resets. For example, the above rules give

[x.(αUβ)] * -→ x:=0 [α] ∨ ([β] ∧ [αUβ])
as a "real" transition of the automaton.

All the states are accepting. Notice that in the case of positive formulas we will have a state [F β] only when β is of the form (x < c) ∧ β , or possibly with non strict inequality. As we consider only non Zeno words, this assures that the language accepted from this state is correct even if the state is accepting. One way to look at them is as eager For other formulas of Constrained TPTL we first assume that for every positive formula we have already an automaton constructed by the above procedure. We then use the clauses above and the clause for the U operator:

[αUβ] -→ [β] ∨ ([α] ∧ [αUβ])
to construct the part of the automaton corresponding the remaining formulas. The accepting states are all those corresponding to positive formulas. All the other states are rejecting.

For the complexity bound announced in the statement of the theorem, it is enough to check that the proof of the same complexity bound for alternating timed automata over finite words can be translated into Constrained TPTL.

Relation with other logics

Safety MTL [START_REF] Ouaknine | Safety metric temporal logic is fully decidable[END_REF] can be seen as an MTL fragment of positive TPTL. Indeed, both formalisms can be translated to automata with only accepting states, but the automata obtained from MTL formulas have also the locality property (cf. [START_REF] Ouaknine | Safety metric temporal logic is fully decidable[END_REF]). The satisfiability problem for both logics is non-elementary.

Using equivalences mentioned above FlatMTL [START_REF] Bouyer | The cost of punctuality[END_REF] with pointwise non Zeno semantics can be defined as a set of formulas of the grammar:

p | α ∨ β | α ∧ β | αU J β | ϕU I β| χ J bounded and χ ∈ M IT L.
The original definition admits more constructs, but they are redundant in the semantics we consider. Both FlatMTL and Constrained TPTL use two sets of formulas. The MTL part of the later logic would look like

p | α ∨ β | α ∧ β | αU I β | ϕ ϕ positive
From this presentation it can be seen that there are at least two important differences: Constrained TPTL does not have restrictions on the left hand side of until and it uses positive fragment instead of MITL. We comment on these two aspects below. Allowing unrestricted until makes the logic more expressive but also more difficult algorithmically. For example, to get the non primitive recursive bound it is enough to use the formulas generated by the later grammar without the clause for positive formulas. This should be contrasted with Expspace-completeness result for FlatMTL.

The use of positive fragment instead of MITL is also important. The two formalisms have very different expressive powers. The crucial technical property of MITL is that a formula of the form αU I β can change its value at most three times in every unit interval. This is used in the proof of decidability of FlatMTL, as the MITL part can be described in a "finitary" way. The crucial property of the positive fragment is that it can express only safety properties (and all such properties). We can remark that by reusing the construction of [START_REF] Ouaknine | On the decidability of metric temporal logic[END_REF] we get undecidability of the positive fragment extended with a formula expressing that some action appears infinitely often. Theorem 32 implies that this is true even if we do not use punctual constraints in the positive fragment. In conclusion, we cannot add MITL to the positive fragment without loosing decidability.

Undecidability without testing for equality

Ouaknine and Worell [START_REF] Ouaknine | On the decidability of metric temporal logic[END_REF] have proved undecidability of MTL over infinite words in the case of pointed semantics. Their construction immediately implies that the decidability result from the last section is optimal if classes of accepting conditions are concerned.

Theorem 31 (Ouaknine, Worell) It is undecidable whether a given one-clock nondeterministic timed automaton A accepts every infinite word, even when there are no transitions in A from states in Q -to states in Q + .

The construction in op. cit. relies on equality constraints. Indeed, if we do not allow equality constraints in MTL then we get a fragment called MITL, and the satisfiability problem for MITL over infinite words is decidable [START_REF] Alur | The benefits of relaxing punctuality[END_REF].

In this section we would like to show that a similar phenomenon is very particular to MTL and does not occur in the context of automata. We show that the undecidability result holds even when it is only allowed to test if the clock is bigger than 1.

Theorem 32 It is undecidable whether a given one-clock alternating timed automata A accepts an infinite word, even when there are no transitions in A from states in Q -to states in Q + and when A does not test for equality.

To prove Theorem 32 we code a problem of deciding whether there is a successful run of a counter machine with insertion errors: Definition 33 A k-counter machine with insertion errors M g has configurations (q, c 1 , . . . , c k ) consisting of a control state q ∈ Q and values of the counters c i ∈ N. There are three kinds of transitions: (q : c i := c i + 1; goto q ) or (q : if c i = 0 then goto q ) or (q : if c i > 0 then c i := c i -1; goto q ). The set of transitions δ of M g gives rise to a relation between configurations, describing a single step of M g . The machine has insertion errors, which means that before and after every step it may increase any of its counters by any value. We will denote this by (q, c 1 , . . . , c k ) -→ (q , c 1 , . . . , c k ), to say that we may reach configuration (q , c 1 , . . . , c k ) from (q, c 1 , . . . , c k ) using some transition from δ and possibly increasing some counters before and after the transition. The initial configuration of the machine M g is (q 0 , 0, . . . , 0). Together with the machine there is given some subset of states Q acc ⊆ Q. We say, that a run of M g satisfies the Büchi condition, if in infinitely many its configurations there appears state from Q acc .

Theorem 34 (Ouaknine,Worell [23]) It is undecidable whether a given 5counter machine with insertion errors M g has a run satisfying the Büchi condition.

For completeness, we give a short proof of Theorem 34 by reduction to boundedness of a lossy 4-counter machine. The principle of lossy k-counter machine is similar to that with insertion errors, but for the fact that before or after every step it may decrease any of its counters by any value (instead of increasing). We say that a run of such a machine is bounded, iff there is a common bound for values of all counters in all configurations throughout the run.

Theorem 35 (Mayr [19]) It is undecidable whether every run of a given lossy 4-counter machine M l is bounded.

Proof

First note, that a counter machine with insertion errors is exactly the same as lossy counter machine working backward. Let M l be a given lossy 4-counter machine. We construct a 5-counter machine M g that can simulate in a backward fashion a computation of M l on the first four counters. This machine will be able to go from a configuration (q, c 1 , c 2 , c 3 , c 4 , c 5 ) to a configuration (q 0 , 0, 0, 0, 0, c 5 ) iff M l can go form (q 0 , 0, 0, 0, 0), that is the initial configuration, to (q, c 1 , c 2 , c 3 , c 4 ). Additionally to the states of M l , the machine would have some auxiliary states, one of them would be an accepting state q acc . The machine will start in the state q acc , and this state will be reachable only from a configuration (q 0 , 0, 0, 0, 0, c 5 ). In the state q acc , the machine would increase c 5 by 1 and then (in a nondeterministic way) increase counters c 1 , c 2 , c 3 , c 4 , so that c 1 + c 2 + c 3 + c 4 ≥ c 5 . To do that it may the move value of c 5 simultaneously into c 1 and c 2 , then move value from c 2 back to c 5 and finally while decreasing c 1 increase c 2 , c 3 , c 4 . After that it chooses a state of M l and starts computing backward (using only the first four counters). When configuration (q 0 , 0, 0, 0, 0, c 5 ) is reached we make the machine to go to (q acc , 0, 0, 0, 0, c 5 ).

Assume that M l has an unbounded computation. We will show that M g has a run visiting q acc infinitely often. Suppose that some initial fragment of this run is already constructed and we are in a configuration (q acc , 0, 0, 0, 0, c 5 ) for some value of c 5 . As M l has an unbounded computation, it can reach a configuration (q, c 1 , c 2 , c 3 , c 4 ) with the sum of the counters bigger than c 5 +1. We increase c 5 by 1, distribute c 5 into other counters to get the values c 1 , c 2 , c 3 , c 4 , we choose the state q and then execute the computation of M l backwards, starting from (q, c 1 , c 2 , c 3 , c 4 ). When reaching (q 0 , 0, 0, 0, 0, c 5 + 1) we go to (q acc , 0, 0, 0, 0, c 5 + 1) and repeat this process. This gives the required infinite computation.

For the opposite direction, assume that there is a successful computation of M g . Every appearance of q acc is followed by some initialization, and by a backward computation of M l , starting in a configuration of size bigger than the value of c 5 and ending in (q 0 , 0, 0, 0, 0). However, every time this happens the value of c 5 increases by at least one. So we get computations of M l ending in bigger and bigger configurations. By König's lemma, there exists also an unbounded computation of M l . Now we return to the proof of Theorem 32. For given 5-counter machine with insertion errors M g we will construct an alternating one-clock timed automaton A that accepts some infinite word iff M g has a successful run. The input alphabet of A will consist of the instructions of M g and some auxiliary letters whose use will be explained later: Σ = δ ∪ {shc, sh$, new, init}.

As states of A we take:

Q + = Q M ∪ {1, 2, 3, 4, 5, $, q ∞ , q init } and Q -= {q -}.
States Q M ∪ {1, 2, 3, 4, 5} will be used to represent configurations of M g : the current state and the values of the five counters. States q ∞ and q -will encode the condition on successful runs. State $ is important for technical reasons. State q init is the initial state that will not be reachable from other states.

In our description below we will consider a characterisation of acceptance given by Lemma 4. In this presentation a run of A is a sequence

P 1 a1,t1 → P 2 a2,t2 → P 3 . . . ,
where each P i ⊆ P(Q A × R + ) is a set of pairs (q, v) consisting of a state of A and a valuation of the clock. Compared with Lemma 4 we have joined together a transition letting the time pass with an action transition and write just a,t → transitions. We will use only two regions:

I 1 = [0, 1] and I ∞ = (1, ∞).
Definition 36 A configuration θ of A is well-formed if:

• For every (q, v) ∈ θ: if q ∈ {1, . . . , 5, $} then v ∈ I 1 , and v ∈ I ∞ otherwise.

• For every v ∈ I 1 there is at most one σ ∈ Σ with (σ, v) ∈ θ.

• In θ there is exactly one pair with a state from Q M , exactly one pair with the state q ∞ , and no pairs with q init ;

• Suppose (q, v) is in θ where q ∈ {1, . . . , 5}. Then this pair is immediately preceded by some ($, v ) (there is no pair (q , v ) in θ with v < v < v).

Intuitively, a well formed configuration is divided into two parts: the set of pairs with the clock value in I 1 and those in I ∞ . The first part can be seen as representing a word over {1, . . . , 5, $} that is obtained by using the standard order on clock values. From the conditions above it follows that this word is of the form $ + q i1 $ + q i2 . . . $ + q in $ + ; where q i k ∈ {1, . . . , 5}. Such a word represents values of the counters when the value of the counter c i is equal to the number of i in the word. The clock values of pairs in I ∞ will not matter, so this part can be seen as a multiset of states. There will be always one state from Q M representing the state of the simulated machine. State q ∞ plus some number of states q -will be there to encode a condition on a successful run.

Automaton A will pass also through configurations that are not well-formed, but in its accepting run it will have to repeatedly return to well-formed configurations.

Now we describe transitions of the automaton. In order to have an intuition for reading the rules below it is important to observe that if the automaton reads a letter σ then all states in its current configuration have to make a transition according to some rule labeled σ. In consequence, if there is a state in the configuration that does not have a rule for σ then the automaton cannot read σ.

The automaton starts in the state q init and waits at least one time unit to start its two copies: one is a state q 0 and another is q ∞ (where q 0 is the initial state of M g ):

q init , I ∞ init -→ q 0 ∧ q ∞
This means that the configuration becomes {(q 0 , v), (q ∞ , v )} with v, v ∈ I ∞ .

States $ for time ≤ 1 are preserved by any transition:

$, I 1 σ -→ $ ∀σ ∈ Σ
Similarly states 1, . . . , 5, with the exception that a transition checking for zero should not be possible if appropriate counter is non-zero:

i, I 1 σ -→ i ∀i = 1, . . . , 5 ∀σ = (q : if c i = 0 then goto q )
When the clock value for a pair with $ or i becomes greater than 1, it may be reset:

$, I ∞ sh$ -→ ($, reset) i, I ∞ shc -→ $ ∧ (i, reset) ∀i = 1, . . . , 5 q, I ∞ σ -→ q q ∈ Q M ∪ {q ∞ , q -}, σ = sh$ or σ = shc
Note that the transition on $ reads a different letter than that on i. In consequence, if in a configuration there are pairs with both $ and i having clock values in I ∞ then neither sh$ nor shc are possible. As we will have no more transitions from ($, I ∞ ) this means that the automaton will be blocked in such a configuration. Now we consider moves on transitions of the machine M g . For σ = (q : if c i = 0 then goto q ) we just do q, I ∞ σ -→ q Note that, thanks to earlier restriction, the transition is possible only when there are no i states in the configuration. For σ = (q : if c i > 0 then c i := c i -1; goto q ) we do:

q, I ∞ σ -→q i, I ∞ σ -→
For σ = (q : c i := c i + 1; goto q ) we do:

q, I ∞ σ -→ q ∧ $ ∧ (i, reset)
As the machine should allow insertion errors, we add a transition: q, I ∞ new -→ q ∧ $ ∧ (i, reset) Finally, we have special states q ∞ and q -, that are used to ensure that states from Q acc appear infinitely often. The state q ∞ produces repeatedly new q - states:

q ∞ , I ∞ σ -→ q ∞ ∧ q - ∀σ ∈ Σ

The state q -is the only one, which is in Q -, so in the accepting run every q - state has to disappear after some time. The states q -disappear, when there there is a transition ending in state from Q acc :

q -, I ∞ σ -→ ∀σ = (. . . goto q ), q ∈ Q acc q -, I ∞ σ -→ q -for all other σ Lemma 37 There exists a run of M g satisfying the Büchi condition iff A accepts some infinite word.

Proof

Assume that M g has a run satisfying the Büchi condition. From the initial state, A may go to a well-formed configuration corresponding to the initial configuration of M g . Then every step of M g may be simulated by A: When M g increases some of its counters, we may do the same using transitions on letters new and then sh$. When M g does a transition σ = (q : if c i = 0 then goto q ) we may do the same in A reading letter σ. When M g does σ = (q : c i := c i + 1; goto q ), we do the same reading letter σ and then sh$. It is easy to check, that after each step the resulting configuration remains well formed.

The most difficult transition is σ = (q : if c i > 0 then c i := c i -1; goto q ). Suppose that the automaton is in a well-formed configuration θ. Let us look at the biggest valuation v ≤ 1 appearing in θ. By the conditions of well-formedness there is exactly one state q ∈ Q + such that (q, v) ∈ θ. This state can be one of 1, . . . , 5, $. The automaton lets the time pass so that v becomes greater than 1, but all other valuations from I 1 stay in I 1 . If q = i then the automaton does σ. Otherwise, it does sh$ or shc followed by sh$ that has an effect of putting $ or $ followed by q at the beginning of the configuration. After this we obtain a well formed configuration where the one but the maximal valuation before became the maximal one. These operations are repeated until q = i. We are sure that this process ends, as there is a state i in θ.

To ensure that the obtained word is nonZeno, we have to wait some time after every transition of M g , doing shc and sh$ if necessary. Observe that every state q -would disappear when in the computation of M g there is a transition ending in a state from Q acc . As this computation satisfies the Büchi condition,, this will happen infinitely often.

For the other direction consider some accepting run of A on some word. In the first step, A has to reach a well-formed configuration corresponding to the initial configuration of M g . Let us see what may happen from any well-formed configuration. Suppose that time passes and timer for some states 1, . . . , 5, $ becomes greater than 1. If it happens simultaneously for state $ and some state i, then from the obtained configuration there will be no more transitions. If it happens only for state $, then the only possible transition is the one reading sh$ after which we go back to a well-formed configuration corresponding to the same configuration of M g . If it happens just for some state i, then the automaton can read either shc or some (q : if c i > 0 then c i := c i -1; goto q ). If it reads shc, then after that it has to read sh$, and we also are back in a well-formed configuration corresponding to the same configuration of M g . If it reads σ = (q : if c i > 0 then c i := c i -1; goto q ), then we immediately get a well-formed configuration.

Transition reading shc or sh$ when no state of 1, . . . , 5, $ has timer above 1 do not change the configuration. Transition reading new, has to be followed by transition sh$ and we get a well-formed configuration with one of the counters increased. Transition reading σ = (q : if c i = 0 then goto q ) is possible only when counter c i is zero. After transition reading σ = (q : c i := c i + 1; goto q ) there has to be a transition reading sh$ and we get a well-formed configuration that corresponds to a correct configuration of M g . Transition reading σ = (q : if c i > 0 then c i := c i -1; goto q ) gives us always a wellformed configuration. The obtained configuration correctly represents the result but for the fact that the counter i may not be decremented. This is not a problem as we are simulating a machine with insertion errors, so we can suppose that the incrementation error has occurred immediately after execution of this instruction.

The above argumentation gives some (finite or infinite) computation of M g . As A accepts, every q -disappears after some time. This is only possible when reading a letter of the form (. . . goto q ) with q an accepting state of M g . As q -needs to disappear infinitely often, we have an infinite computation of M g satisfying the Büchi condition.

  Adam chooses one of subformulas b 1 , b 2 and the play continues with b replaced by the chosen subformula; • b = b 1 ∨ b 2 : dually, Eve chooses one of subformulas;

2 a-→ c 2 . When c 1 (

 221 c 1 by at most one transition from c 1 . If c 1 a -→ c 2 then directly from Lemma 11 it follows that there is c 2 c 2 such that c delay,ε)

  arbitrary λ 1 . . . λ k . So, by the above observations the second property of the lemma holds. For the first property observe that whenever c c and c ∈ exp( c, λ 1 . . . λ k ) then there is c ∈ exp( c , λ 1 . . . λ k ) with c r c. Lemma 27 There is an algorithm that given Y upper closed with respect to r relation computes a constant M Σ * (Y ) such that, the size of every minimal element of pre ∀ Σ * (Y ) is bounded by M Σ * (Y ).

1 and c 1 (

 11 Take the set C(λ 0 ∞ ) as given by Lemma 26. We have that Exp( C Σ * (λ 0 ∞ ), λ 0 1 . . . λ 0 k ) ⊆ Y by the second statement of this lemma. From Lemma 23 we get a subsequenceλ 1 . . . λ l of λ 0 1 . . . λ 0 k whose length is bounded by B(X, C(λ 0 ∞ )) ≤ M Σ * and such that Exp( C Σ * (λ 0 ∞ ), λ 1 . . . λ l ) ⊆ Y . By the first statement of Lemma 26 we get that (λ 1 . . . λ l , λ 0 ∞ ) ∈ pre ∀ Σ * (Y ). By the minimality of c 0 , we have that c 0 = (λ 1 . . . λ l , λ 0 ∞ ), so its length is bounded by M Σ * + 1. The last step before proving Lemmas 18 and 19 consists of two simple observations.Lemma 28 For every set X upward closed with respect to relation, the membership in Y = pre ∀ delay (X) is decidable. Moreover Y is a r -upward closed set. Proof The first part of the lemma is obvious, it suffices to test all possible transitions that are explicitly characterized in Lemmas 10 and 12. The second part follows from the property that we have already noticed before (page 15): if c 1 r c delay,•) -→ c 2 then also c 1 (delay,•) -→ c 2 with some c 2 c 2 .Lemma 29 For every set Y upward closed with respect of r relation, the membership in pre ∀ Σ * (Y ) is decidable.

1 a-→ c 2 then also c 1 a-→ c 2

 112 that the length of a derivation c Σ * c is the smallest possible. We show that c ∈ t. Recall that Lemma 11 characterizes transitions on letters. Directly form this characterization we obtain that if c 1 r c 1 and c with some c 2 r c 2 . Using this fact, we get that if c is not in t then there is d c such that the derivation cΣ * d is shorter than c Σ *


des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

1

The Scots' Response to the American Revolution: A North British Vision of Empire, Constitution, and Representation

By Florence Petroff, University of Paris 8

As Linda Colley argued persuasively in Britons: Forging the Nation, 1707-1837 (1992), Britishness was invented in the eighteenth century and has since been superimposed on preexisting identities without either replacing or merging with them. Yet eighteenth-century Scottish elites eagerly engaged in Anglicization while preserving many aspects of their distinctiveness. The contours of the resulting "North British" identity have been defined by Colin Kidd ("North Britishness and the Nature of Eighteenth-Century British Patriotisms," Historical Journal 39.2, 1996). Being British was commonly understood throughout the British Empire as enjoying the "English liberties" enshrined in the constitution and protected by the Hanoverian dynasty. Bernard Bailyn, Jack Greene, Pauline Maier, Eliga Gould, and a number of other historians have pointed out that the Thirteen Colonies initially resisted attempts at centralization by Britain in the name of these liberties. Being British also meant taking part in a shared transatlantic culture, as Ned Landsman has shown in From Colonials to Provincials: American Thought and Culture, 1680-1760(1997), as well as Brendan McConville in The King's Three Faces: The Rise and Fall of Royal America, 1688-1776 (2012).

My work explores the notions of Britishness that the Scots and the colonists forged in the context of the imperial crisis, from the enactment of the Stamp Act in 1765 to the Treaty of Paris in 1783. It contends that two distinct, even competing, conceptions of Britishness were shaped by the Scots and the Americans through processes of identification with England and differentiation with one another. The American Revolution was undoubtedly the catalyst for the emergence of an American identity. Yet before rejecting Britishness, the American Patriots first built up a hybrid identity combining Britishness with Americanness; until the mid-1770s they claimed that they could remain part of the empire while benefiting from the large amount of autonomy that their colonial assemblies had acquired since the late seventeenth century. They asserted their Britishness through differentiation with the French, as all Britons then did, as well as with the Scots. In 1967 Bernard Bailyn briefly mentioned in The Ideological Origins of the American Revolution that a version of the conspiracy theory that pervaded the colonies involved former Prime Minister Lord Bute, a Scot accused of secretly manipulating George III and the government against America (pp. 147-48). The question of what Scotland embodied for American revolutionaries has not drawn much attention since then, possibly because Scotland was hardly ever mentioned in American revolutionary literature. It was, however, discussed in the colonial press. Newspapers throughout the Thirteen Colonies, particularly in Virginia, disseminated an image of Scotland as inherently Jacobite and supportive of tyranny and Roman Catholicism. They reveal a different political culture from that of the pamphlets and display a discourse based on disinformation, fantasy, and fear that originated in the English Scottophobic Grub Street rhetoric of John Wilkes and Charles Churchill. The belief in a "Scottish plot" against America waged by Bute, Scottish ministers, and the Scottish nation was in turn appropriated by Americans such as Rev. Ezra Stiles, whose diary entry for 23 July 1777 states: "Let us boldly say, for History will say it, that the whole of this War is so far chargeable to the Scotch Councils, & to the Scotch as a Nation (for they have nationally come into it) as that had it not been for them, this Quarrel had never happened. Or at least they have gloried in the Honor of exciting & conduct[ing] these Measures avowedly by their Earl of Bute behind the Curtain." Scotland was not just considered an enemy to the American Patriots' cause. It was also the antithesis of the Britishness that the Americans identified with through binary oppositions such as Hanover/Stuart, liberty/tyranny, and Protestantism/Catholicism.

Conversely, the Scots considered themselves the opposite of the American rebels and predominantly opposed the American Revolution. The perceptions of the American Revolution in Scottish public opinion were explored by Dalphy Fagerstrom in 1954 ("Scottish Opinion and the American Revolution," William and Mary Quarterly, 11.2) and D. B. Swinfen in 1977 ("The American Revolution in the Scottish Press," in Scotland, Europe, and the American Revolution, ed. Owen Dudley Edwards and George Shepperson). My approach is based on a more extensive study of the Scottish pamphlet literature in order to investigate the various reasons why the Scots stood against the Americans. At least sixty-six works on America were published either by a Scot or anonymously in Scotland between 1768 and 1784, with a peak of forty-two between 1776 and 1779. Thirty-six authors produced one, two, sometimes three pamphlets, sermons, or books discussing the conflict with the colonies. A number of them took part in the Scottish Enlightenment, including prominent figures such as Adam Smith and Adam Ferguson and less familiar ones such as William Barron. About half these authors published on a variety of other topics, including religion, history, husbandry, poetry, economic improvement, and literature. They were educated professionals who worked as teachers, lawyers, or clergymen. With the exception of a few officers of the Crown and the loyalists George Chalmers and John McAlpine, none had ever been to America. Some, like George Johnstone, Alexander Wedderburn, and Lord Mansfield, were pursuing careers as politicians, judges, or civil servants in London. Ministers in the Church of Scotland account for almost half these authors, dominated by Moderate Party clergymen such as Alexander Carlyle, George Campbell, Adam Ferguson, Alexander Gerard, and Thomas Somerville. A majority of these Scottish authors argued that the Americans were wrong in declaring themselves independent. They believed them to be manipulated by a faction of ungrateful American politicians apt to endanger the empire and the wellbeing of all its inhabitants for the sake of their personal ambitions. Some expected Britain to bring the rebels back to their senses by force, others believed that the colonists could be convinced by sound reasoning. The Johnstone brothers, who both sat in Parliament in the 1770s, first appeared as "friends of America" when they advocated the right of the colonists to tax themselves and condemned the Coercive Acts of 1774. George, known as Governor Johnstone, reversed his opinion after the creation of the United States and its alliance with Britain's rival, France. In some of the most thoughtful and articulate pamphlets on the topic, his brother Sir William Pulteney recounted the growing tensions between Britain and its colonies and proposed a peace negotiation in 1779 based on the granting of fiscal and legislative autonomy to the colonies, assuming independence could still be reversed. John Erskine and William Thom in the Popular Party disapproved of the war but did not support the Declaration of Independence. All told, only two Scots openly endorsed American resistance to Britain's policy throughout the Revolution. George Dempster, politician and agricultural improver, expressed his staunch belief that the American Patriots were in the right, even after they seceded from the empire. James Murray, a Presbyterian minister at Newcastle upon Tyne, kept defending the American Patriots in sermons and in An Impartial History of the Present War in America (1778).

The Scots did not actually engage in a direct debate with the American pamphleteers, whom they hardly ever quoted or mentioned. Rather, they tried to refute Richard Price's Observations on the Nature of Civil Liberty (1776) and other British pamphlets. Thus, they addressed the American controversy as Britons speaking to other Britons, in an attempt to convince them that the American rebellion was unconstitutional and that the empire had to be preserved. The American controversy provided Scottish elites with an opportunity to display their British patriotism. They professed their commitment to the constitution and the principle of parliamentary sovereignty as well as their Hanoverian loyalty. The Americans were accused of being far worse rebels than the Scottish Jacobites in 1745 because they threatened not only the dynasty but also the constitution and "English liberties." The natural rights that the Declaration of Independence cited were considered "an inalienable right to talk nonsense," according to the comments inserted in the text of the Declaration in the Scots Magazine of August 1776. The colonists' grievances and claims were seen as a ploy that could not disguise the real motive of Congress: a quest for power. The American republic that pretended to ensure the liberties of its citizens challenged the belief in the perfection of the British constitution which, most Scots believed, remained the only real source of liberty. The Scottish approach to the issue of the American Revolution combined a commitment to Britishness with a desire to promote the interests of the Scottish nation. Sir John Dalrymple and Alexander Carlyle called for the right to establish a Scots militia and to expand recruitment of Highlanders in the army. Robert Alves, Charles Nisbet, and John Stevenson glorified the part played by the Scots, especially the Highlanders, in the patriotic war against the rebels. British patriotism mixed with Scottish patriotism, as in Stevenson's description of the Highlanders in his Letters in Answer to Dr. Price's Two Pamphlets on Civil Liberty (1778): "they fought, they bled, and they conquered as Britons" (p. 149).

As Emma Macleod has shown in British Visions of America, 1775America, -1820America, (2013)), American independence met with dismay and disbelief in Britain. Consequently, most of the Scots who published their reaction to the American Revolution from 1776 onward discussed matters that had been settled before 1776 in the eyes of the American Patriots. To the American claim for "no taxation without representation," the Scots answered that not only could the colonists be rightfully taxed by Parliament but also that they were not entitled to reject its authority since they were represented virtually. The empire was described as a community in which each part had to contribute to the defense of the whole through taxation in order to maintain its dominance. Scottish pamphleteers articulated the vision of a centralized empire, united by a unique fiscal system and transatlantic commerce. Adam Smith even suggested in The Wealth of Nations (1776) that the colonists should be given the right to elect their own representatives in Parliament, an idea that did not generate much enthusiasm in Great Britain, much less in America. Even though they were not in favor of an imperial Parliament, those who discussed the imperial crisis generally assumed that the empire should somehow be reorganized on the model of the Union.

The concept of representation exemplifies the discrepancy between Scottish and American visions of empire and constitution. The colonists believed they were not represented in the Westminster Parliament because their understanding of representation was based on their political experience within the colonies. Their assemblies were regarded by the American Whigs as the only bodies that represented them. These political bodies had grown into the main institutions in colonial America by enlarging their prerogatives at the expense of governors and councils. Not only were they geographically close, whereas the Westminster Parliament was more than three thousand miles away, but they defended the interests of their constituents. Bernard Bailyn has argued that the American concept of representation drew on the English medieval notion of representation seen as a form of attorneyship, in which the electors delegated power to the elected. The representatives in the colonial assemblies were accountable to their voters, whose interests they defended, sometimes even receiving instructions from them (Ideological Origins of the American Revolution, p. 164). It was a general rule that candidates had to live in the county, parish, or precinct where they were running for an election. In Virginia, they had at least to possess land in the county as it was the case for George Washington in 1758 when he was elected to the Virginia House of Burgesses in Frederick County even though he lived in the neighboring county of Fairfax (see Richard R. Beeman, The Varieties of Political Experience in Eighteenth-Century America, 2004, p. 39). An average of 75 percent of the white adult male population having access to vote, the colonial assemblies had a direct connection with a large part of the community, even though many voters did not care to exert their right. Representation was also conceived on the local scale in eighteenth-century America because the colonists identified first and foremost with their colony. From the failure of Benjamin Franklin's Albany Plan in 1754, the building of a collective American identity and the unification of all colonies was a long, arduous process. It is the conflict with Britain that actually stimulated the creation of the Stamp Act Congress in New York in 1765 and the Continental Congress from 1774. In the American vision of empire, sovereignty was shared, and each colony acted as a state within a confederation under the sole authority of the Crown. There was the historical precedent of Scotland and England between 1603 and 1707, Benjamin Franklin argued in 1768 in a letter to his son William and in the press (The Papers of Benjamin Franklin, vol. 15, ed. William B. Willcox, 1972, pp. 74-78;A Briton, "Arguments Pro and Con: I," London Chronicle, 18-20 October 1768;Boston Evening-Post, 11 April 1774, p. 1). Why should America be ruled by the Westminster Parliament, asked John Adams, when Scotland was not at the time of the union of the crowns: "So the Scots held their lands of him who was then king of England, his heirs and successors, and were bound to allegiance to him, his heirs and successors, but it did not follow from thence that the Scots were subject to the English parliament" (Novanglus, "XII. To the Inhabitants of the Colony of Massachusetts-Bay, 17 April 1775," Novanglus, and Massachusettensis, or, Political Essays: Published in the Years 1774and 1775, on the Principal Points of Controversy, between Great Britain and Her Colonies, 1819, pp. 133-39).

Contrary to the Americans, most eighteenth-century Scots regarded the incorporating union as an improvement compared to the time when they had their own Parliament. They conceptualized a notion of representation on the scale of Britain which was not based on the electoral process. In Britain the voting population was much more limited than in America, even more so in Scotland where there were fewer than three thousand electors for a population of one million people. The unequal distribution of the franchise between men and between burghs and counties was not considered an issue, for it was understood that MPs were not accountable to their electors since, once elected, they became "representatives of the state at large; not only their own constituents, but every individual member of the community" (Free Thoughts on the American Contest, 1776, p. 22). They defended the interests of the whole nation when voting on laws and taxes that everyone was subjected to, including themselves. Representatives were in any case increasingly less connected to the constituency that elected them in eighteenth-century Britain since many did not live there; some 60 Scots even sat for an English or a Welsh constituency between 1760 and 1790, 130 between 1790 and 1820. The Scots thus felt as much under the protection of Parliament against oppression and unfair taxation as any part of England or Wales, even though they elected only 45 MPs out of 558 in the House of Commons. They were committed to centralization, believing the empire needed a single head to keep all its parts together, and their attitude toward authority was the opposite of American distrust of central power (see Jack P. Greene, Peripheries and Center: Constitutional Development in the Extended Polities of the British Empire and the United States, 1678States, -1788States, , 1986; Ned C. Landsman, "British Union and American Revolution: Imperial Authority and the Multinational State," in The American Revolution Reborn, ed. Patrick Spero and Michael Zuckerman, 2016; Paul Tonks, "Rethinking the Eighteenth Century Province and Periphery: A Historiographical Reflection on Scotland, Scottish Thought, and the Government of the British Atlantic Empire," Korean Journal of British Studies, no. 22, Dec. 2009).

Scottish elites believed their interests were better protected in the Westminster Parliament, which provided a stronger counterweight to the Crown's prerogative than they had enjoyed in their pre-Union unicameral Parliament or in local institutions such as town councils. They adopted the notion that virtual representation included the colonists, as George Grenville's government maintained. James Macpherson, who was pensioned by the government, argued in The Rights of Great Britain Asserted against the Claims of America: Being an Answer To the Declaration of the General Congress (1776) that, like the Americans, most British subjects did not vote, and he concluded: "the truth is, Representation never accompanied Taxation in any State" (p. 4). In his Letters in Answer to Dr. Price's Two Pamphlets on Civil Liberty, John Stevenson added that the members of the House of Commons "represent actually and virtually, not only all the inhabitants of this island, but also every individual throughout the colonies" (p. 24). Liberty was not seen as contingent upon the franchise by most Scottish pamphleteers, who contended that Britons were free because they had a Parliament that checked the Crown's power, no matter how it was elected. Eighteenth-Century Britain (1977) that a movement for electoral reform swept through England from the 1770s, partly under the influence of American revolutionary ideas (pp. 217-18). Since they considered the British system of representation as nearly perfect, the Scots who wrote about the American controversy did not support that movement, with the exception of James Burgh, a member of the radical society of London. Burgh's 1500-page work Political Disquisitions (1774-75) called for reform that would correct the many flaws and inequalities in the electoral system and reduce the influence of the aristocracy, for example by putting an end to government intrusion in elections and establishing a more equitable electoral franchise at all levels of society. He believed that most people who paid indirect taxes on malt, soap, and other necessities were not represented in Parliament since they could not vote. These radical views were hardly supported in Scotland. The burgh reform movement had connections with the Society for Constitutional Information and Chistopher Wyvill's Yorkshire Association, but it followed a different path. Its appeal for an enlargement of the ruling elite in Scottish burghs stemmed not from a hope to reform the constitution but from a wish to modernize local institutions, which were seen as archaic compared to those in England.

Harry T. Dickinson observed in Liberty and Property: Political Ideology in

The Scottish reception of the American Revolution was generally unsympathetic, as the Americans correctly perceived, but it was not rooted in Jacobitism, as the Americans believed. On the contrary, the Scots rejected Whig American thought because it questioned the British conception of liberty and empire that they endorsed. The American notions of natural rights, direct representation, and shared sovereignty within the empire induced the Scots to assert their commitment to the principle of parliamentary sovereignty over the empire, the belief in the perfection of the constitution, and loyalty to the Hanoverian dynasty, which were the fundamentals of the emerging British identity. The imperial crisis arguably weakened the empire but was also a catalyst for Britishness, which was built not merely in opposition to a French "Other" but also in opposition to an American one.

This article is based on Florence Petroff's doctoral thesis, "Le Miroir atlantique. L'Ecosse et l'Amérique dans la crise impériale: regards croisés et identités hybrides au sein du monde britannique (1765-1783)"/"Scotland and America in the Imperial Crisis: Mutual Perceptions and Hybrid Identities within the Anglo-American World (1765-1783)," for which she was awarded a PhD in history from the University of Paris 8 in 2020. She is planning to publish her thesis in French and a few articles in English. Florence's research interests focus on cultural studies, especially the circulation of political thought, opinions, and representations within the British Atlantic world. She would welcome any comments or be happy to engage in a discussion of those topics (florence.petroff@gmail.com).