{'fraction_non_alphanumeric': 0.05837191137528338, 'fraction_numerical': 0.007715608390009716, 'mean_word_length': 3.477459802959867, 'pattern_counts': {'":': 0, '<': 126, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 87, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Analyzing Timed Systems Using Tree Automata

Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. Such graphs can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).


Introduction
The advent of timed automata [3] marked the beginning of an era in the verification of real-time systems. Today, timed automata form one of the well accepted real-time modelling formalisms, using real-valued variables called clocks to capture time constraints. The decidability of the emptiness problem for timed automata is achieved using the notion of region abstraction. This gives a sound and finite abstraction of an infinite state system, and has paved the way for state-of-the-art tools like UPPAAL [5], which have successfully been used in the verification of several complex timed systems. In recent times [1,6,13] there has been a lot of interest in the theory of verification of more complex timed systems enriched with features such as concurrency, communication between components and recursion with single or multiple threads. In most of these approaches, decidability has been obtained by cleverly extending the fundamental idea of region or zone abstractions.
In this paper, we give a technique for analyzing timed systems, inspired from a different approach based on graphs and tree automata. This approach has been exploited for analyzing various types of untimed systems, e.g., [17,10]. The basic template of this approach has three steps: (1) capture the behaviors of the system as graphs, (2) show that the class of graphs that are actual behaviors of the system is MSO-definable, and (3) show that this class of graphs has bounded tree-width (or cliquewidth or split-width), or restrict the analysis to such bounded behaviors. Then, non-emptiness of the given system boils down to the satisfiability of an MSO sentence on graphs of bounded tree-width, which is decidable by Courcelle's theorem. Since, graphs of bounded tree-width can be interpreted in binary trees, the problem reduces to non-emptiness of a tree automaton whose existence follows from Courcelle's theorem. But, by providing a direct construction of the tree automaton, it is possible to obtain a good complexity for the decision procedure.
Our technique starts similarly, by replacing timed word behaviors of timed systems with graphs consisting of untimed words with additional time-constraint edges, called words with timing constraints (TCWs). However, the main complication here is that a TCW describes an abstract run of the timed system, where the constraints are recorded but not checked. The TCW corresponds to an actual concrete run iff it is realizable. So, we are interested in the class of graphs which are realizable TCWs. The structural property that a graph must be a TCW is MSO-definable. However, we conjecture that realizability is not MSO definable over words with timing constraints. Given this, we cannot directly appeal to the approach of [17,10]. Instead, we work on decomposition trees and construct a finite tree automaton checking realizability, which is the most involved part of the paper. More precisely, we show that words with timing constraints (TCWs) which are behaviors of certain classes of timed systems (like timed pushdown systems) are graphs of bounded split/tree-width. Hence, these graphs admit binary tree decompositions as depicted in the adjoining figure. Each node of the tree depicts an incomplete behavior/graph of the system, and by combining these behaviors as we go up the tree, we obtain a full or complete behavior (run) of the system. We construct a tree automaton that checks if the generated graph encoded as a tree satisfies the ValCoRe property (1) Validity: The root node depicts a syntactically correct labeled graph (TCW); (2) Correctness of run: The graph is indeed a correct run of the underlying timed system and; (3) Realizability: The root node depicts a realizable graph, i.e., we can find timestamps that realize all timing-constraints. To check realizability, the tree automaton needs to maintain a finite abstraction for each subtree encoding a TCW. Thanks to the bound on split/tree-width, our abstraction keeps a bounded number of positions, called end-points, in the (arbitrarily large) TCW. It subsumes (arbitrarily long) paths of timing constraints in the TCW by new timing constraints between these end-points. The constants in these new constraints are sums of original constants and may grow unboundedly. Hence, a key difficulty is to introduce suitable abstractions which aid in bounding the constants, while at the same time preserving realizability. Using tree decompositions of graph behaviors of bounded split/tree-width and tree automata proved to be a very successful technique for the analysis of untimed infinite state systems [17,11,10,2]. This paper opens up this powerful technique for analysis of timed systems.
To illustrate the technique, we have reproved the decidability of non-emptiness of timed automata and timed pushdown automata (TPDA), by showing that both these models have a split-width (|X| + 2 and 4|X| + 2) that is linear in the number of clocks. This bound directly tells us the amount of information that we need to maintain in the construction of the tree automata. For TPDA we obtain an EXPTIME algorithm, matching the known lower-bound for the emptiness problem of TPDA. For timed automata, since the split-trees are word-like (at each binary node, one subtree is small) we may use word automata instead of tree automata, reducing the complexity from EXPTIME to PSPACE, again matching the lower-bound. Interestingly, if one considers TPDA with no explicit clocks, but the stack is timed, then the split-width is a constant, 2. In this case, we have a polynomial time procedure to decide emptiness, assuming a unary encoding of constants in the system. To further demonstrate the power of our technique, we derive a new decidability result for non-emptiness of timed multi-stack pushdown automata under bounded rounds, by showing that the split-width of this model is again linear in the number of clocks, stacks and rounds. Exploring decidable subclasses of untimed multi-stack pushdown systems is a very active research area [4,12,14,16,15], and our technique can easily extend these to handle time.
It should be noticed that the tree automata for validity and realizability (the most involved construction of this paper) are independent of the timed system under study. Hence, to apply the technique to other systems, one only needs to prove the bound on split-width and to show that their runs can be captured by tree automata. This is a major difference compared to many existing techniques for timed systems which are highly system dependent. Finally, we mention an orthogonal approach to deal with timed systems given in [6], where the authors show the decidability of the non-emptiness problem for a class of timed pushdown automata by reasoning about sets with timed-atoms.

Graphs for behaviors of timed systems
We fix an alphabet Σ and use Σ ε to denote Σ ∪ {ε} where ε is the silent action. We also fix a finite set of closed intervals I which contains the special interval [0, 0]. For a set S, we use ≤ ⊆ S × S to denote a partial or total order on S. For any x, y ∈ S, we write x < y if x ≤ y and x = y, and x y if x < y and there does not exist z ∈ S such that x < z < y.

Abstractions of timed behaviors
Definition 1. A word with timing constraints (TCW) over Σ, I is a structure V = (P, →, λ, , θ) where P is a finite set of positions or points, λ : P → Σ ε labels each position, the reflexive transition closure ≤ = → * is a total order on P and → = is the successor relation, ⊆ < = → + gives the pairs of positions carrying a timing constraint, whose interval is given by θ : → I.
For any position i ∈ P , the indegree (resp. outdegree) of i is the number of positions j such that (j, i) ∈ (resp. (i, j) ∈ ). A TCW is simple (denoted STCW) if each position has at most one timing constraint (incoming or outgoing) attached to it, i.e., for all i ∈ P , indegree(i) + outdegree(i) ≤ 1. A TCW is depicted below (left) with positions 1, 2, . . . , 5 labelled over {a, b}. indegree(4)=1, outdegree(1)=1 and indegree (3)=0. The curved edges decorated with intervals connect the positions related by , while straight edges are the successor relation →. Note that this TCW is simple.
An ε-timed word is a sequence w = (a 1 , t 1 ) . . . (a n , t n ) with a 1 . . . a n ∈ Σ + ε and (t i ) 1≤i≤n is a non-decreasing sequence of real time values. If a i = ε for all 1 ≤ i ≤ n, then w is a timed word. The projection on Σ of an ε-timed word is the timed word obtained by removing ε-labelled positions.
We can (and often will) view a TCW W as a directed weighted graph with edges E = ∪ −1 ∪ → −1 and weights induced by θ as follows: if (i, j) ∈ and θ(i, j) = [I , I r ] then the weight of the forward edge is the upper constraint wt(i, j) = I r and the weight of the back edge is the negative value of the lower constraint wt(j, i) = −I . Further, to ensure that time is non-decreasing we add 0-weight back edges between consecutive positions that are not already constrained, i.e., if (i, j) ∈ \ then wt(j, i) = 0. The directed weighted graph depicted above (right) corresponds to the TCW on its left. A directed path in W is a sequence of positions ρ = p 1 , p 2 , . . . , p n (n > 1) linked with edges: (p i , p i+1 ) ∈ E for all 1 ≤ i < n. It is a cycle or loop if p n = p 1 . Its weight is wt(ρ) = 1≤i<n wt(p i , p i+1 ). Then, we have the following standard result: Proposition 2 ( [7]). A TCW W is realizable iff it has no negative cycles.
Proof. This follows from the well-known method for checking feasibility of systems of difference constraints using constraint graphs. The characterization can be found in any standard textbook on algorithms and constraint solving, for instance, see [7,Chapter 24.4]. (We have additional constraints of the form x i ≥ 0, but this is easy to handle since if (s 1 , . . . , s n ) is a solution vector then (s 1 + d, . . . ; s n + d) is also a solution vector for all constants d.) To check if a TCW is realizable, we only need to check for absence of negative weight cycles, which can be done in polynomial time, for instance, using the Bellman Ford algorithm (see [7] for details).

TPDA and their semantics as simple TCWs
Dense-timed pushdown automata (TPDA), introduced in [1], are an extension of timed automata, and operate on a finite set of real-valued clocks and a stack which holds symbols with their ages. The age of a symbol in the stack represents time elapsed since it was pushed on to the stack. Formally, a TPDA S is a tuple (S, s 0 , Σ, Γ, ∆, X, F ) where S is a finite set of states, s 0 ∈ S is the initial state, Σ, Γ, are respectively a finite set of input, stack symbols, ∆ is a finite set of transitions, X is a finite set of real-valued variables called clocks, F ⊆ S are final states. A transition t ∈ ∆ is a tuple (s, γ, a, op, R, s ) where s, s ∈ S, a ∈ Σ, γ is a finite conjunction of atomic formulae of the kind x ∈ I for x ∈ X and I ∈ I, R ⊆ X are the clocks reset, op is one of the following stack operations: 1. nop does not change the contents of the stack, 2. ↓ c where c ∈ Γ is a push operation that adds c on top of the stack, with age 0. 3. ↑ I c where c ∈ Γ is a stack symbol and I ∈ I is an interval, is a pop operation that removes the top most symbol of the stack provided it is a c with age in the interval I.
Timed automata (TA) can be seen as TPDA using nop operations only. This definition of TPDA is equivalent to the one in [1], but allows checking conjunctive constraints and stack operations together. In [6], it is shown that TPDA of [1] are expressively equivalent to timed automata with an untimed stack. Nevertheless, our technique is oblivious to whether the stack is timed or not, hence we focus on the syntactically more succinct model TPDA with timed stack and get good complexity bounds.
We define the semantics in terms of simple TCWs. An STCW V = (P, →, λ, , θ) is said to be generated or accepted by a TPDA S if there is an accepting abstract run ρ = (s 0 , γ 1 , a 1 , op 1 , R 1 , s 1 ) (s 1 , γ 2 , a 2 , op 2 , R 2 , s 2 ) · · · (s n−1 , γ n , a n , op n , R n , s n ) of S such that, s n ∈ F and the sequence of push-pop operations is well-nested: in each prefix op 1 · · · op k with 1 ≤ k ≤ n, number of pops is at most number of pushes, and in the full sequence op 1 · · · op n , they are equal. We have P = P 0 P 1 · · · P n with P i × P j ⊆ → + for 0 ≤ i < j ≤ n. Each transition gives rise to a sequence of consecutive points P i in the STCW. The transition δ i is simulated by a sequence of "micro-transitions" as depicted below (left) and it represents an STCW shown below (right). Incoming red edges check guards from γ i (wrt different clocks) while outgoing green edges depict resets from R i that will be checked later. Further, the outgoing edge on the central node labeled a i represents a push operation on stack.
The first and last micro-transitions, corresponding to the reset of a new clock ζ and checking of constraint ζ = 0 ensure that all micro-transitions in the sequence occur simultaneously. We have a point in P i for each microtransition (excluding the ε-micro-transitions between δ xj i ). Hence, P i consists of a sequence i → 1 i → · · · → hi i → p i → r 1 i → · · · → r gi i → r i where g i is the number of timing constraints corresponding to clocks reset during transition i and checked afterwards. Similarly, h i is the number of timing constraints checked in γ i . We have λ(p i ) = a i and all other points are labelled ε. The set P 0 encodes the initial resets of clocks that will be checked before being reset. So we let R 0 = X and P 0 is 0 → r 1 0 → . . . → r g0 0 → r 0 . the relation for timing constraints can be partitioned as = s x∈X∪{ζ} x where is a push and op j = ↑ I b is the matching pop (same number of pushes and pops in op i+1 · · · op j−1 ), and we set θ(p i , p j ) = I. for each 0 ≤ i < j ≤ n such that the t-th conjunct of γ j is x ∈ I and x ∈ R i and x / ∈ R k for i < k < j, we have r s i x t j for some 1 ≤ s ≤ g i and θ(r s i , t j ) = I. Therefore, every point t i with 1 ≤ t ≤ h i is the target of a timing constraint. Moreover, every reset point r s i for 1 ≤ s ≤ g i should be the source of a timing constraint: r s i ∈ dom( x ) for some x ∈ R i . Also, for each i, the reset points r 1 i , . . . , r gi i are grouped by clocks (as suggested by the sequence of micro-transitions simulating Finally, for each clock, we request that the timing constraints are well-nested: for all u We denote by STCW(S) the set of simple TCWs generated by S and define the language of S as the set of realizable STCWs, i.e., L(S) = Real(STCW(S)). Indeed, this is equivalent to defining the language as the set of timed words accepted by S, according to a usual operational semantics [1].
The STCW semantics of timed automata (TA) can be obtained from the above discussion by just ignoring the stack components (using nop operations only). To illustrate these ideas, we now provide a simple example of a timed automaton and an STCW that is generated by it.

Bounding the width of graph behaviors of timed systems
In this section, we check if the graphs (STCWs) introduced in the previous section have a bounded tree-width. As a first step towards that, we introduce special tree terms (STTs) from Courcelle [8] and their semantics as labeled graphs. It is known [8] that special tree terms using at most K colors (K-STTs ) define graphs of "special" tree-width at most K − 1. Formally, a (Σ, Γ)-labeled graph is a tuple G = (V, (E γ ) γ∈Γ , λ) where λ : V → Σ is the vertex labeling and E γ ⊆ V 2 is the set of edges for each label γ ∈ Γ. Special tree terms form an algebra to define labeled graphs. The syntax of K-STTs over (Σ, Γ) is given by . . , K} are colors. The semantics of each K-STT is a colored graph τ = (G τ , χ τ ) where G τ is a (Σ, Γ)-labeled graph and χ τ : [K] → V is a partial injective function assigning a vertex of G τ to some colors.
(i, a) consists of a single a-labeled vertex with color i. Add γ i,j adds a γ-labeled edge to the vertices colored i and j (if such vertices exist). Forget i removes color i from the domain of the color map. Rename i,j exchanges the colors i and j. ⊕ is the disjoint union of two graphs if they use different colors and is undefined otherwise.
The special tree-width of a graph G is defined as the least K such that G = G τ for some (K + 1)-STT τ . See [8] for more details and its relation to tree-width. For TCWs, we have successor edges and -edges carrying timing constraints, so we take In this paper, we will actually make use of STTs with the following restricted syntax, which are sufficient and make our proofs simpler: The terms defined by this grammar are called (K, M )-STTs. Here, timing constraints are added directly between leaves in atomic STTs which are then combined using disjoint unions and adding successor edges. For instance, consider the 4-STT given below Its semantics τ is the adjoining STCW where only endpoints labelled a and d are colored, as the other two colors were "forgotten" by τ . Abusing notation, we will also use τ for the graph G τ ignoring the coloring χ t . The term τ is depicted as a tree in Figure 3 in Appendix A.

Split-TCWs and split-game
We find it convenient to prove that a simple TCW has bounded special tree-width by playing a split-game, whose game positions are simple TCWs in which some successor edges have been cut, i.e., are missing. Formally, a split-TCW is a structure V = (P, →, , λ, , θ) where → and are the present and absent successor edges (also called holes), respectively, such that → ∩ = ∅ and (P, → ∪ , λ, , θ) is a TCW. A block or factor of a split-TCW is a maximal connected component of (P, →). We denote by EP(V) ⊆ P the set of left and right endpoints of blocks of V. A left endpoint e is one for which there is no f with f → e. Right endpoints are defined similarly. Points in P \ EP(V) are called internal. The number of blocks is the width of V: width(V) = 1 + | |. TCWs may be identified with split-TCWs of width 1, i.e., with = ∅. A split-TCW is atomic if it consists of a single point (|P | = 1) or a single timing constraint with a hole (P = {p 1 , p 2 }, p 1 p 2 , p 1 p 2 ). The directed weighted graph for a split-TCW is defined on the associated TCW under → ∪ and hence has back edges with wt = 0 across a hole as well. The split-game is a two player turn based game G = (V ∃ V ∀ , E) where Eve's set of game positions V ∃ consists of all connected (wrt. → ∪ ) split-TCWs and Adam's set of game positions V ∀ consists of non-connected split-TCWs. The edges E of G reflect the moves of the players. Eve's moves consist of splitting a factor in two, i.e., removing one successor edge in the graph. Adam's moves amount to choosing a connected component of the split-TCW. Atomic split-TCWs are terminal positions in the game: neither Eve nor Adam can move from an atomic split-TCW. A play on a split-TCW V is a path in G starting from V and leading to an atomic split-TCW. The cost of the play is the maximum width of any split-TCW encountered in the path. Eve's objective is to minimize the cost, while Adam's objective is to maximize it.
Notice that Eve has a strategy to decompose a TCW V into atomic split-TCWs if and only if V is simple, i.e, at most one timing constraint is attached to each point. The cost of a strategy σ for Eve from a split-TCW V is the maximal cost of the plays starting from V and following strategy σ.
The split-width of a simple (split-)TCW V is the minimal cost of Eve's (positional) strategies starting from V. Let STCW K (Σ) (resp. STCW K,M (Σ)) denote the set of simple TCWs with splitwidth bounded by K (resp. and using constants at most M ). The crucial link between special tree-width and split-width is given by the following lemma. Lemma 3. STCWs of split-width at most K have special tree-width at most 2K − 1.
Starting from a STCW having constants ≤ M , and a strategy of Eve of cost ≤ K, we show in Appendix A how to build a (K, M )-STT.

Split-width for timed systems
Viewing these terms as trees, our goal in the next section will be to construct tree automata to recognize sets of (K, M )-STTs, and thus capture the (K split-width) bounded behaviors of a given system. A possible way to show that these capture all behaviors of the given system, is to show that we can find a K such that all the (graph) behaviors of the given system have a K-bounded split-width. We do this now for a TPDA and also mention how to modify the proof for a timed automaton. In Section 7, we also show how it extends to multi-pushdown systems.
Theorem 4. Given a timed system S using a set of clocks X, all words in its STCW language have split-width bounded by K, i.e., STCW(S) ⊆ STCW K , where We prove a slightly more general result, by identifying some properties satisfied by STCWs generated by a TPDA, and showing that all STCWs satisfying these properties have bounded split-width. Let V = (P, →, , λ, , θ) be a split STCW and let = → ∪ . We say that V is well timed w.r.t. a set of clocks Y and a stack s if the relation can be partitioned as = s x∈Y x where (T 1 ) the relation s corresponds to the matching push-pop events, hence it is well-nested: for all i s j and i s j , if i < i < j then i < j < j. (T 2 ) For each x ∈ Y , the relation x corresponds to the timing constraints for clock x and is wellnested: for all i x j and i x j , if i < i are in the same x-reset block (i.e., a maximal consecutive sequence i 1 · · · i n of positions in the domain of x ), and i < i < j, then i < j < j. Each guard should be matched with the closest reset block on its left: for all i x j and i x j , if i < i are not in the same x-reset block then j < i (see Figure 4 in Appendix A).
It is easy to check that STCWs defined by a TPDA with set of clocks X are well-timed for the set of clocks Y = X ∪ {ζ}, i.e., satisfy the properties above (Appendix A, Claim 21). Then, the following lemma completes the proof of Theorem 4 (2).
(2) is when the last event is the target of x for some clock x ∈ Y . In this case, she will detach the last timing constraint i x j where j is the last point of the split-TCW. By (T 2 ) we deduce that i is the first point of the last reset block for clock x. Eve splits three process-edges to detach the matching pair i x j: these three edges are those connected to i and j. Since the matching pair i x j is atomic, to prolong the game Adam should choose the remaining split-TCW V . Notice that we have now a hole instead of position i. We call this a reset-hole for clock x. During the inductive process, we may have at most one such reset hole for each clock x ∈ Y , since the hole only widens in the reset block for each clock. Note that the last event cannot be a push or the source of a timing constraint. So, the remaining Case (3) is a stack edge i s j where the pop event j is the last event of the split-TCW. If there is already a hole before the push event i, or if i is the first event of the split-TCW, then Eve detaches the atomic matching pair i s j by splitting after i and before j and the game continues from the remaining split-TCW. Otherwise, we cannot proceed as before, since this would create a push-hole and the pushes are not arranged in blocks (which results in holes widening, rather than increasing their number). Hence, removing push-pop edges as we removed timing constraints would create an unbounded number of holes. Instead, Eve divides the TCW in two parts, the left one contains the points before i from which she detaches the resets that will be checked in the right part, the right one contains all points between i and j together with the matching resets. This may create at most |Y | reset holes in the left part and requires at most 2|Y | + 1 cuts. The resulting split-TCW is not connected. Indeed, push-pop edges are well-nested (T 1 ) and since j is the last point of the split-TCW, there are no push-pop edges crossing position i: i s j and i < i implies j < i. Hence, only clock constraints may cross position i. See Appendix A (page 21) for details and examples.
Using this strategy, we can show that after a move of Adam, the split-TCW has at most 2|Y | + 1 blocks, and Eve will disconnect it using at most 2|Y |+1 cuts. Therefore Eve wins without introducing more than 4|Y | + 2 blocks. The details are in Appendix A (page 21). Now, if the STCW is from a timed automaton then, s is empty and Eve's strategy only has the first two cases above. Thus, we obtain a bound of |Y | + 3 on split-width, which proves Theorem 4 (1). Figure 2 illustrates our strategy starting from the STCW depicted in Figure 1, generated by the TA shown in that figure.

The tree automata technique illustrated via TPDA and TA
We now describe our proof technique of using tree automata to analyze timed systems. At a high level, given a timed system S using constants less than M (say a timed automaton or a TPDA), we want to construct a tree automaton that accepts (K, M )-STTs whose semantics are STCWs of split-width at most K which are realizable and accepted by S. We break this into three parts.
First, recall that STCWs of bounded split-width are graphs of bounded STTs (Lemma 3). However, not all graphs defined by bounded STTs are STCWs. We construct a tree automaton A K,M valid which accepts only valid (K, M )-STTs, i.e., those representing STCWs of split-width at most K. valid )}. Our next step is to define a tree automaton A K,M real which accepts all valid STTs whose semantics are realizable STCWs. This is the hardest part of the proof due to timing constraints (over dense time).
Proposition 7. We can build a tree automaton  Note that A K,M real may not accept all (K, M )-STTs which denote realizable STCWs, but it will accept all such valid STTs. Once we have this, our third and final step is to build a tree automaton which accepts the valid STTs denoting STCWs accepted by the timed system. Proposition 8. Let S be a TPDA of size |S| (constants encoded in unary) with set of clocks X and using constants less than M . Then, we can build a tree automaton In Section 5, we detail the most complex tree automaton construction, A K,M real for realizability, thus proving Proposition 7. The construction of A K,M valid is somewhat similar (and easier) and its proof, we can also define an MSO formula and use Courcelle's theorem [9], but the direct tree automata construction gives us complexity bounds and helps for A K,M real as explained in Appendix B. Thus, the tree automaton A checking ValCoRe (i.e., validity, correctness and realizability) is . We have L(A) = ∅ iff there exist some realizable STCWs in STCW(S)∩STCW K,M . Since checking emptiness of a finite tree automaton is decidable in PTIME, we obtain that emptiness is decidable for the corresponding timed system restricted to STCWs of split-width at most K. Theorem 9. Checking whether the timed system S accepts a realizable STCW of split-width at most K is decidable.
By Theorem 4, all STCWs in the semantics of a TPDA S have split-width bounded by some fixed K and Theorem 9 gives a complete decision procedure for checking emptiness of TPDA. From these bounds on split-width and the size of the tree automata for validity, realizability and the system given in the above propositions, we obtain EXPTIME decision procedures for checking emptiness of TPDA.
In the above technique, the only system-specific component is the automaton A K,M S for the timed system S. However, Proposition 8 can easily be adapted for timed automata and for several other timed systems, which are discussed in Section 7. Hence, this technique is generic and can be used for several other timed systems.
Moreover, for timed automata, it can be seen, for instance, from the analysis of Cases (1) and (2) of proof of Lemma 5 that one of the connected components (the pair i x j) is always atomic. This is illustrated in the decomposition of the STCW in Figure 2, where Eve, at each step, breaks a split-STCW into two, an atomic and a non-atomic split-STCW (and subsequently Adam always picks the non-atomic STCW to proceed). Therefore the split-tree is "word-like", i.e., for each binary node, one subtree is small, in our case atomic. Therefore, we can encode the subtree in the label of the binary node itself and use word automata instead of tree automata to check for emptiness (in NLOGSPACE instead of PTIME), yielding the complexity stated below.

Corollary 10.
Emptiness of TPDA and TA are decidable in EXPTIME and PSPACE respectively.

Tree automata for realizable valid (K, M )-STTs
Our goal in this section is to define a finite bottom-up tree automaton A K,M real that runs on (K, M )-STTs and accepts only valid (K, M )-STTs whose semantics are realizable STCWs. Let us first give a high-level picture. A state of the tree automaton will be a split-TCW with at most K blocks and 2K points. At any stage of the run, while processing a subtree τ of the (K, M )-STT, the state, i.e., split-TCW q reached will be a finite abstraction of the split-TCW τ generated by τ , such that q is valid and realizable iff the TCW τ is. At a leaf, the state of an atomic-STT is just a single matching edge with a hole. At each subsequent step going up, the tree automaton simulates the operations of τ : at a ⊕ move, it combines two split-TCW q 1 and q 2 to form a new valid split-TCW q by guessing an ordering between the blocks such that no new negative cycle is introduced (i.e., q continues to be realizable), and at an Add → i,j node, it adds a process edge to fill up the corresponding hole in the split-TCW. At a Forget i node, it removes an internal point, but to maintain realizability, the constraints on internal positions must be propagated to the end-points of the block and this process is continued. Finally, at the root, we obtain a TCW which is a finite abstraction of the semantics τ of a valid (K, M )-STT τ such that τ is a realizable TCW. Then, we show that the tree automaton accepts all such (K, M )-STTs, which concludes the proof of Proposition 7.
There are two key difficulties that we have glossed over in this sketch: first, the propagation of constraints can increase the bounds arbitrarily, along an arbitrarily long (even if finite) run. Fixing this is the hardest part and we carefully define abstractions such that we can bound the constraints by a constant M = O(M ), while preserving realizability. This leads to another subtle issue: while checking that realizability is preserved under our operations (of combining split-TCW and adding process edges), it is no longer sufficient to just check whether this combination is "safe". It may be that currently no negative cycle is formed, but at a later stage, some other operation (⊕) gives rise to a negative cycle, which we do not observe since we capped the value of timing constraints. So, we need to show that all operations are safe no matter what happens in the future. For this we start by defining the notion of preserving realizability "under all contexts" as well as the formal notion of a "shuffle" used at ⊕ nodes.

Shuffle and Realizability under contexts
be two split-TCWs such that their respective set of positions P 1 and P 2 are disjoint. Further, let ≤ be a total order on P = P 1 ∪P 2 such that 1 ∪ 2 ⊆ < and → 1 ∪→ 2 ⊆ . Such orders are called admissible. Then, we define the split- Indeed, this corresponds to shuffling the blocks V 1 and V 2 with respect to the admissible order ≤ and is called a shuffle, denoted by Let M be a positive integer. An M -context C is a split-TCW such that the maximal constant in the intervals is strictly smaller than the fixed constant M . Given a context C and a split-TCW V, we define an operation C • V if width(C) = width(V) + 1. C • V is the split-TCW obtained by shuffling the blocks of C and V in strict alternation.
Two split-TCWs U and V are equivalent, denoted U ∼ M V , iff they have the same number of blocks and preserve realizability under all M -contexts. That is, there exists k ∈ N such that The idea is to come up with a sound abstraction of finite index, so that a finite tree automaton can be defined which works only on the representatives. The operation preserves the equivalence between split-TCW (Appendix C).
for all admissible orders ≤ on the blocks.

A (possibly infinite) tree automaton for realizability
We now build the tree automaton for realizability in two steps. First, we detail a construction which is correct and sound (i.e., preserves realizability under all contexts), but in which constants can grow unboundedly. Subsequently, we show (i) conditions under which it has finitely many states and (ii) additional abstractions to ensure that it is always finite.
Proposition 12. We can build a tree automaton

Proof. The construction builds on the construction of
, < is a total order on P , → ⊆ is the successor relation between points in the same block, q has at most K blocks; and wt : P 2 → Z = Z ∪ {+∞} gives the timing constraints. The first component is finite but weights can grow unboundedly. We assume wt(k, k) = 0 for all k ∈ P and if i < j then wt(j, i) ≤ 0 ≤ wt(i, j). We identify (q, wt) with a split-TCW (ignoring , Σ, as these are irrelevant for realizability).
We first give the invariant that will be maintained by the automaton. Let τ be a inf reads τ and reaches state (q, wt) with q = (P, <, →), it induces a total order on blocks of τ and turns it into a split-TCW ( τ , The key invariant is that A K,M inf always computes a sound abstraction of the given STT. We now formalize the definition of the tree automaton. In both cases, it is easy to check that (q, wt) is a sound abstraction of τ .
is obtained by exchanging colors i and j in (q, wt), which clearly preserves soundness.
, when q is obtained from q = (P, <, →) by adding a successor edge between (i, j) ∈ \ →. Then, if τ = Add → i,j τ and (q, wt) is a sound abstraction of τ , it follows that (q , wt ) is a sound abstraction of τ (adding an edge only reduces the number of contexts to be considered to show equivalence of realizability under contexts.) are sound abstractions of τ 1 , τ 2 then (q, wt) is a sound abstraction of τ . The total ordering < of q indicates how blocks of q 1 and q 2 are shuffled. Hence (q, wt) = (q 1 , wt 1 ) ≤ (q 2 , wt 2 ). Now, the induced ordering on the blocks of τ corresponds to the same shuffle of blocks, i.e., ( τ , . Now, applying the congruence Lemma 11, we obtain that (q, wt) is a sound abstraction of τ .
If the second condition above is not satisfied then the tree automaton A K,M inf has no transitions from (q, wt) reading Forget i . With this we can prove that if τ = Forget i τ and (q, wt) is a sound abstraction of τ , then (q , wt ) is a sound abstraction of τ (Claim 28 in Appendix C).
Accepting condition: Finally, we define a state (q, wt) to be accepting if q consists of a single block with no internal points, left endpoint i and right endpoint j (possibly i = j), and the pair (q, wt) is realizable, i.e., wt(i, j) + wt(j, i) ≥ 0.
Observe that the constants in wt increase only at forget transitions, where a back edge j > k with j > i > k grows in absolute value with the update wt (j, k) = min(wt(j, k), wt(j, i) + wt(i, k)). A forward edge j < k may get a big value only if wt(j, k) = ∞, else it can only decrease due to the min operation. A first question is if there are classes where they will not grow unboundedly. A simple solution is to consider time-bounded classes where all behaviors must occur within some global time bound T : if some back edge grows > T in absolute value after a forget move we reject the STT; while if the same happens with a forward edge, then replace it with ∞. Thus, we obtain, Corollary 13. If the system is time-bounded by some constant T , then there exists a finite tree However, in general, when we do not assume a global time bound the constants in the states of A K,M inf may grow unboundedly. We next show how to modify the above construction so that the constants are always bounded. This generalizes the above corollary with a better complexity.

Bounding the constants
The finite tree automaton A K,M real will work on a finite subset of the states of Now, to bound back edges we define a transformation β which reduces the weight of a back edge when it goes above a certain constant, while preserving realizability under all contexts. In fact, we define it on back edges across a block. Let (q, wt) be a state of A K,M inf with q = (P, <, →). A pair of points (j, i) ∈ P 2 is said to be a block back edge (denoted BBE) if i < j are the end points of a block in q, i.e., i → + j and this →-path cannot be extended (on the left or on the right). A big block back edge (BBBE) is block back edge e such that M + wt(e) ≤ 0. For any two positions i < j, we define BBE(i, j) to be the set of block back edges between i and j. That is, We also define B(i, j) to be the set of big block back edges between i and j: The idea is to change the weight of big BBE to −M by adding an offset to all the other edges (backward and forward) crossing this block. Note that this does not increase the absolute value of any constant. Further, after the backward abstraction, the absolute value of weights of block back edges is bounded by M , i.e., for all BBE i j, we have wt (j, i) ≥ −M . Indeed, either the edge was big and we get wt (j, i) = −M or it was not big and wt (j, While block back edges are now bounded (and back edges across holes can also be bounded by −M ), this does not suffice to bound all back edges. To obtain such a bound on all back edges, we need to relate large back edges to edges contained within them.
With this, we have our second and crucial invariant, that we maintain inductively in the tree automaton, (I2): A K,M real always satisfies BEP. Preserving this invariant requires a slight transformation of the shuffle operation (at a ⊕ node). Namely, after every shuffle we must strengthen the constraints of the back edges. Formally, we define a map σ,  Finally, forward abstraction γ removes all forward edges (i.e., changes their weight to ∞) that are too large to be useful for creating negative cycles. Let W = (q, wt) be a state of Note, wt(e) ≤ 0 as it is a (block) back edge. Then, we define γ(q, wt) = (q, wt ) where, for any i < j, wt (j, i) = wt(j, i) and wt (i, j) = ∞ if (i, j) is big and unchanged otherwise. While the definition of this abstraction is simple, it turns out that showing that it is sound (i.e., it preserves realizability under all contexts) is rather tricky. With details in Appendix C.2 (page 32) we have, inf by applying the abstractions at ⊕ nodes and at Forget i nodes.
More precisely, ) if q has no internal points and (q , wt ) = (q , wt ) otherwise. The reason for assuming that q has no internal points before applying the abstractions is that it is a precondition for Lemmas 14

Dense time multi-stack pushdown systems
As another application of our technique, we now consider the model of dense-timed multi-stack pushdown automata (dtMPDA), which have several stacks. The reachability problem for untimed multi-stack pushdown automata (MPDA) is already undecidable, but several restrictions have been studied on (untimed) MPDA, like bounded rounds [14], bounded phase, bounded scope and so on to regain decidability.
In this section, we consider dtMPDA with the restriction of "bounded rounds". To the best of our knowledge, this timed model has not been investigated until now. Our goal is to illustrate how our technique can easily be applied here with a minimal overhead (in difficulty and complexity).
Formally, a dtMPDA is a tuple S = (S, Σ, Γ, X, s 0 , F, ∆) similar to a TPDA defined in Section 2.2. The only difference is the stack operation op which now specifies which stack is being operated on. That is, 1. nop does not change the contents of any stack (same as before), 2. ↓ i c where c ∈ Γ is a push operation that adds c on top of stack i, with age 0. 3. ↑ i c∈I where c ∈ Γ and I ∈ I is a pop operation that removes the top most symbol of stack i provided it is a c with age in the interval I.
A sequence σ = op 1 · · · op m of operations is a round if it can be decomposed in σ = σ 1 · · · σ n where each factor σ i is a possibly empty sequence of operations of the form nop, ↓ i c , ↑ c∈I . Let us fixed an integer bound k on the number of rounds. The semantics of the dtMPDA in terms of STCWs is exactly the same as for TPDA, except that the sequence of stack operations along any run is restricted to (at most) k rounds. Thus, any run of dtMPDA can be broken into a finite number of contexts, such that in each context only a single stack is used. As before, the sequence of push-pop operations of any stack must be well-nested. We denote by STCW(S, k) the set of simple TCWs generated by runs of S using at most k rounds. We let L(S, k) be the corresponding language of realizable STCWs in STCW(S, k).
We now lift the definition of well-timed STCWs to k-round well-timed STCWs and show that such STCWs have bounded split-width and thus all simple TCWs in STCW(S, k) have bounded split-width (note that the realizable STCWs are a subset of this and hence will also have a bounded split-width). An STCW V = (P, →, λ, , θ) is k-round well timed with respect to a set of clocks Y and stacks 1 ≤ s ≤ n if it uses at most k-rounds and the relation for timing constraints can be partitioned as = 1≤s≤n s x∈Y x where for each 1 ≤ s ≤ n, the relation s corresponds to the matching push-pop events of stack s as in (T 1 ), and for each x ∈ Y , the relation x corresponds to the timing constraints for clock x and is well-nested as in (T 2 ).
Proof sketch. Again, we play the split-game between Adam and Eve. Eve should have a strategy to disconnect the word without introducing more than (4nk + 4)(|Y | + 1) blocks. The strategy of Eve is as follows: Given the k-round word w, Eve first breaks this into two words. The first word only has stack 1 edges, and the second word has stack edges corresponding to stacks 2, . . . , n. The first word can now be dealt with as we did in the case of TPDA. Eve then breaks the second word into two words, the first of which has only stack 2 edges, while the second word has edges of stacks 3,4 . . . , n, and so on. Finally, we obtain n split-STCW's, each having edges corresponding to only one stack. Once this is achieved, these words can be processed as was done in the case of TPDA. The only thing to calculate is the number of cuts required in isolating each word, whose details are in Appendix E.
Having established a bound on the split-width for dtMPDA restricted to k rounds, we now discuss the construction of a tree automaton that checks ValCoRe when the underlying system is a dtMPDA. As a first step, we keep track of the current round (context) number in the finite control. This makes sure that the tree automaton only accepts runs using at most k-rounds. The validity and realizability checks (Val and Re parts) are as discussed in Appendices B and C. The only change pertains to the automaton that checks correctness of the underlying run, namely, A K,M S , as we need to handle n stacks (and k rounds) instead of the single stack. As shown in Appendix E, this results in the blow up of the number of locations of A K,M S by n · k. Thus the size of the tree automaton A K,M S that checks correctness when the underlying system is a k-round dtMPDA is (nk|S| Combining this with Lemma 18, we can apply our technique (i.e., exactly the same reasoning as) explained in Section 4 to obtain our decidability result.
Theorem 19. Checking emptiness for k-round dtMPDA is decidable in EXPTIME.

Discussion and Future work
The main contribution of this paper is the technique for analyzing timed systems via tree automata. As a result, we have made a few simplifying assumptions to best illustrate this method. However, our technique can easily be adapted to remove these. We give two examples of this: For simplicity, we only considered closed intervals in this paper, but our technique can be easily adapted to work for all kinds of intervals, i.e., open, half-open etc. Of course this requires us to consider a few more cases, but it is not hard to see that our complexity bounds do not change. Diagonal constraints of the form x − y ∈ I can be handled easily by adding matching edges. For a constraint x − y ∈ [1, 5], we add an edge between the last reset of x and last reset of y with [1,5] interval. Thus, we can check the diagonal constraint at the time of last reset. Unlike in the classical removal of diagonal guards, this does not induce any blowup in the number of states of the system.

Future work
We can also extend our results to other restrictions for dtMPDA such as bounded scope and phase. Further, our techniques can be applied to the more general model [13] of recursive hybrid automata, where we can already see some (new) decidability results.
As future work, an interesting question is to use our technique to go beyond reachability and show results on model checking for timed systems. While model-checking against untimed specifications is easy to obtain with our approach, the challenge is to extend it to timed specifications. We also see a strong potential to investigate the emptiness problem for classes of alternating timed automata and hybrid automata.
In this appendix, we give details of proofs as well as a few more illustrative examples and explanations. In order to make the appendix easier to read and somewhat self-contained, we have chosen to repeat some of the material given in the main paper. The appendix is organized section-wise.

A Details for Section 3
Special tree terms We start by giving the formal semantics of specital tree terms in more detail together with an example. To help reading this appendix, we also recall some definitions from Section 3.
The formal syntax of K-STTs over (Σ, Γ) is given by where λ : V → Σ is the vertex labeling and E γ ⊆ V 2 is the set of edges for each label γ ∈ Γ. Special tree terms form an algebra to define labeled graphs.
Each K-STT represents a colored graph τ = (G τ , χ τ ) where G τ is a (Σ, Γ)-labeled graph and χ τ : [K] → V is a partial injective function assigning a vertex of G τ to some colors.
Finally, ⊕ constructs the disjoint union of the two graphs provided they use different colors. This operation is undefined otherwise.
The special tree-width of a graph G is the least K such that G = G τ for some (K + 1)-STT τ .
For TCWs, we have successor edges and -edges carrying timing constraints, so we take Γ = The term τ is depicted as a binary tree on the left of Figure 3 and its semantics τ is the following simple TCW where only the endpoints labelled a and d are colored.

Figure 3
An STT and a simple TCW with its split-tree Split-game and split-tree Split-TCWs and the split-game were defined in Section 3. A strategy for Eve from a split-TCW V can be described with a split-tree T which is a binary tree labeled with split-TCWs satisfying: 1. The root is labeled by V = labroot(T ).

3.
Eve's move: Each unary node is labeled with some connected (wrt. → ∪ ) split-TCW V and its child is labeled with some V obtained by splitting a factor of V in two, i.e., by removing one successor edge. Thus, width(V ) = 1 + width(V). 4. Adam's move: Each binary node is labeled with some non connected split-TCW V = V 1 V 2 where V 1 and V 2 are the labels of its children. Note that width(V) = width(V 1 ) + width(V 2 ).
The width of a split-tree T , denoted width(T ), is the maximum width of the split-TCWs labeling the nodes of T . In other words, the cost of the strategy encoded by T is width(T ). A K-split-tree is a split-tree of width at most K. An example of a split-tree is given in Figure 3 (right). Observe that the width of the split-tree is 4. Hence the split-width of the simple TCW labeling the root is at most four.
Let V = (P, →, , λ, , θ) be a split-TCW. Recall that we denote by EP(V) the subset of events that are endpoints of blocks of V. A left endpoint is an event e ∈ V such that there are no f with f → e. We define similarly right endpoints. Note that an event may be both a left and right endpoint. The number of endpoints is at most twice the number of factors: |EP(V)| ≤ 2 · width(V).
Lemma 20. A (split) simple TCW of split-width at most K has special tree-width at most 2K − 1.
Proof. We associate with every split-tree T of width at most K a 2K-STT T such that T = (V, χ) where V = labroot(T ) is the label of the root of T and the range of χ is the set of endpoints of V: Im(χ) = EP(V). Notice that dom(χ) ⊆ [2K] since T is a 2K-STT. The construction is by induction on T .
Assume that labroot(T ) is atomic. Then it is either an internal event labeled a ∈ Σ, and we let T = (1, a). Or, it is a pair of events e f with a timing constraint θ(e, f ) = [c, d] and we let T = Add c,d 1,2 ((1, λ(e)) ⊕ (2, λ(f ))). If the root of T is a binary node and the left and right subtrees are T 1 and T 2 then labroot(T ) = labroot(T 1 ) labroot(T 2 ). By induction, for i = 1, 2 the STT T i is already defined and we have T i = (labroot(T i ), χ i ). We first rename colors that are active in both STTs. To this end, we choose an injective map f : Assuming that dom(f ) = {i 1 , . . . , i m }, we define Finally, assume that the root of T is a unary node with subtree T . Then, labroot(T ) is obtained from labroot(T ) by splitting one factor, i.e., removing one word edge, say e → f . We deduce that e and f are endpoints of labroot(T ), respectively right and left endpoints. By induction, the STT T is already defined. We have T = (labroot(T ), χ ) and e, f ∈ Im(χ ). So let i, j be such that χ (i) = e and χ (j) = f . We add the process edge with τ = Add → i,j T . Then we forget color i if e is no more an endpoint, and we forget j if f is no more an endpoint: Bound on split-width for TPDA. We complete this section by providing a detailed proof of Theorem 4. We provide more intuition and pictures to elucidate the ideas presented succinctly in Section 3. We show that for a TPDA S, all words in STCW(S) have bounded split-width. As mentioned, we identify some properties satisfied by all simple TCWs generated by a TPDA, and then we show that all simple TCWs satisfying these properties have bounded split-width. Let V = (P, →, , λ, , θ) be a simple-TCW. We say that V is well timed with respect to a set of clocks Y and a stack s if the relation can be partitioned as = This lemma is proved by playing the split-width game between Adam and Eve. Eve should have a strategy to disconnect the word without introducing more than 4|Y | + 2 blocks. The strategy of Eve uses three operations processesing the word from right to left.
Removing an internal point. If the last/right-most event on the word (say event j) is not the target of a relation, then she will split the →-edge before the last point, i.e., the edge between point j and its predecessor.
Removing a clock constraint Assume that we have a timing constraint i x j where j is the last point of the split-TCW. Then, by (T 2 ) we deduce that i is the first point of the the last reset block for clock x. Eve splits three word-edges to detach the matching pair i x j: these three edges are those connected to i and j. Since the matching pair i x j is atomic, Adam should continue the game from the remaining split-TCW V . Notice that we have now a hole instead of position i. We call this a reset-hole for clock x. For instance, starting from the split-TCW of Figure 4, and removing the last timing constraint of clock x, we get the split-TCW on top of Figure 5. Notice the reset hole at the beginning of the x reset block.
During the inductive process, we may have at most one such reset hole for each clock x ∈ Y . Note that the first time we remove the last point which is a timing constraint for clock x, we create a hole in the last reset block of x which contains a sequence of reset points for x, by removing two edges. This hole is created by removing the leftmost point in the reset block. As we keep removing points from the right which are timing constraints for x, this hole widens in the reset block, by removing each time, just one edge in the reset block. Continuing the example, if we detach the last internal point and then the timing constraint of clock y we get the split-TCW in the middle of Figure 5. Now, we have one reset hole for clock x and one reset hole for clock y.
We continue by removing from the right, one internal point, one timing constraint for clock x, one timing constraint for clock y, and another internal point, we get the split-TCW at the bottom of Figure 5. Notice that we still have a single reset hole for each clock x and y. Note that if i is not the first point of the split-TCW and there is no hole before i, we cannot proceed as we did in the case of clock constraints, since this would create a push-hole and the pushes are not arranged in blocks as the resets. Hence, removing push-pop edges as we removed timing constraints would create an unbounded number of holes. Instead, we split the TCW just before the matching push event i. Since push-pop edges are well-nested (T 1 ) and since j is the last point of the split-TCW, there are no push-pop edges crossing position i: i s j and i < i implies j < i. Hence, only clock constraints may cross position i.
Consider some clock x having timing constraints crossing position i. All these timing constraints come from the last reset block B x of clock x which is before position i. Moreover, these resets form the left part of the reset block B x . We detach this left part with two splits, one before the reset block B x and one after the last reset of block B x whose timing constraint crosses position i. We proceed similarly for each clock of Y . Recall that we also split the TCW just before the push event i. As a result, the TCW is not connected anymore. Notice that we have used at most 2|Y | + 1 new splits to disconnect the TCW. For instance, from the bottom split-TCW of Figure 5, applying the procedure above, we obtain the split-TCW on top of Figure 6 which has two connected components. Notice that to detach the left part of the reset block of clock x we only used one split since there was already a reset hole at the beginning of this block. The two connected components are depicted separately at the bottom of Figure 6. Figure 6 is representative of the split-TCW which may occur during the split-game using the strategy of Eve described above. These split-TCW satisfy the following invariant.

Invariant. The split-TCW at the bottom right of
(I 1 ) The split-TCW starts with reset blocks, at most one for each clock in Y . For instance, the split-TCW of Figure 7 starts with two reset blocks, one for clock x and one for clock y (see the two hanging reset blocks on the left, one of x and one of y). (I 2 ) After these reset blocks, the split-TCW may have reset holes, at most one for each clock in Y .
For instance, the split-TCW of Figure 7 has two reset holes, one for clock z and one for clock y. A reset hole for clock x is followed by the last reset block of clock x, if any. Hence, for all timing constraints i x j such that j is on the right of the hole, the reset event i is in the reset block that starts just after the hole.
Lemma 23. A split-TCW satisfying (I 1 -I 2 ) has at most 2|Y | + 1 blocks. It is disconnected by Eve's strategy using at most 2|Y | + 1 new splits, and the resulting connected components satisfy (I 1 -I 2 ). Therefore, its split-width is at most 4|Y | + 2.  Proof. Let us check that starting from a split-TCW satisfying (I 1 -I 2 ), we can apply Eve's strategy and the resulting connected components also satisfy (I 1 -I 2 ). This is trivial when the last point is internal in which case Eve makes one split before this last point.
In the second case, the last event checks a timing constraint for some clock x: we have i x j and j is the last event. If there is already a reset hole for clock x in the split-TCW, then by (I 2 ) and (T 2 ), the reset event i must be just after the reset hole for clock x. So with at most two new splits Eve detaches the atomic edge i x j and the resulting split-TCW satisfies the invariants. If there is no reset hole for clock x then we consider the last reset block B x for clock x. By (T 2 ), i must be the first event of this block. Either B x is one of the first reset blocks of the split-TCW (I 1 ) and Eve detaches with at most two splits the atomic edge i x j. Or Eve detaches this atomic edge with at most three splits, creating a reset hole for clock x in the resulting split-TCW. In both cases, the resulting split-TCW satisfies the invariants.
The third case is when the last event is a pop event: i s j and j is the last event. Then there are two subcases: either, there is a hole before event i then Eve detaches with two splits the atomic edge i x j and the resulting split-TCW satisfies the invariants. Or we cut the split-TCW before position i. Notice that no push-pop edges cross i: if i s j and i < i then j < i. As above, for each clock x having timing constraints crossing position i, we consider the last reset block B x for clock x which is before position i. The resets of the timing constraints for clock x crossing position i form a left factor of the reset block B x . We detach this left factor with at most two splits. We proceed similarly for each clock of Y . The resulting split-TCW is not connected anymore and we have used at most 2|Y | + 1 more splits. For instance, if we split the TCW of Figure 7 just before the last push following the procedure described above, we get the split-TCW on top of Figure 8. This split-TCW is not connected and its left and right connected components are drawn below.
To see that the invariants are maintained by the connected components, let us inspect the splitting of block B x . First, B x could be one of the beginning reset blocks (I 1 ). This is the case for clock x in Figures 7 and 8. In which case Eve use only one split to divide B x in B 1 x and B 2 x . The left factor B 1 x corresponds to the edges crossing position i and will form one of the reset block (I 1 ) of the right connected component. On the other hand, the suffix B 2 x stays a reset block of the left connected component. Second, B x could follow a reset hole for clock x. This is the case for clock z in Figures 7  and 8. In which case again Eve only needs one split to detach the left factor B 1 x which becomes a reset block (I 1 ) of the right component. The reset hole before B x stays in the left component. Finally, assume that B x is neither a beginning reset block (I 1 ), nor follows a reset hole for clock x. This is the case for clock y in Figures 7 and 8. Then Eve detaches the left factor B 1 x which becomes a reset block (I 1 ) of the right component and creates a reset hole in the left component.

B Tree automata for Validity
Not all graphs defined by (K, M )-STTs are TCWs of split-width at most K. Indeed, if τ is such an STT, the edge relation → may have cycles or may be branching, which is not possible in a TCW. Also, the timing constraints given by need not comply with the → relation: for instance, we may have a timing constraint e f with f → + e. Moreover, some subterm may define graphs having more than K blocks. So we use A K,M valid to check for validity. Proposition 24. We can build a tree automaton x,y ⊆ → + . Also, a pair of points may have at most one timing constraint, hence the matching relations should be disjoint: x,y ∩ x ,y = ∅ if (x, y) = (x , y ). If these conditions are satisfied, with = x,y x,y and θ(i, j) = (x, y) for (i, j) ∈ x,y we see that τ is a TCW. Further, we should check that this TCW is simple. Since being a simple TCW is a graph property which is MSO definable and since a graph τ has an MSO-interpretation in the tree τ , we deduce that there is a tree automaton that accepts all (K, M )-STTs τ such that τ is a simple TCW (cf. [9]).
But this is not exactly what we want/need. So we provide in the proof below a direct construction of another tree automaton. There are several reasons for directly constructing the tree automaton A K,M valid . First, this allows to have a clear upper-bound on the size of A K,M valid (though maybe not impossible, this would be technical via MSO). Second, simplicity of the TCW and the bound on split-width can be enforced with no additional cost. Third and most importantly, A K,M valid does not accept all (K, M )-STTs denoting TCWs. Instead, it accepts the STTs T arising from split-trees T . We will take advantage of the special form of these STTs when constructing the tree automaton A K,M real checking the realizability of simple-TCWs. Proof. A state of A K,M valid will be an abstraction of the graph defined by the STT read so far. The finite abstraction will keep only the colored points of the graph. The abstraction is enriched with a guessed total order < on the colored points. This guessed total order will be compatible both with the -edges corresponding to the timing constraints defined at atomic STTs and with the →-edges added later. When adding a new →-edge, we will check that it is compatible with the guessed total order <. This will ensure that the graph defined by the STT is in fact a split-TCW.
Formally, states of A K,M valid are tuples of the form q = (P, <, →) where P ⊆ [2K] is the set of points, < is a total order on P , → ⊆ is the successor relation between points that are in the same block, and q has at most K blocks, i.e., (P, →) has at most K connected components.
The automaton A K,M valid is non-deterministic since at ⊕-nodes it has to guess how the blocks will eventually be ordered in the TCW denoted by the full STT. To help understanding the construction, we first define properties that will be maintained by the automaton.
Let τ be a (K, M )-STT with τ = (V, →, λ, , θ, χ). Let q = (P, <, →) be a state of A K,M valid . Notice some overloading of notations for → but since we assume that P and V are disjoint this is not a problem. We say that q is an abstraction of τ if it satisfies the following properties (A 1 ) dom(χ) = P and EP( τ ) ⊆ χ(P ) i.e., the points of q are in bijection with the colored points of τ and the endpoints of τ are colored, ) is a split-STCW, i.e., →∪ is the direct successor relation of a total order (→∪ ) + on V which is compatible with the timing constraints ⊆ (→ ∪ ) + .
Claim 25. The blocks (resp. left/right endpoints) of q are in 1-to-1 correspondance with blocks (resp. left/right endpoints) of τ .
Proof. Let i ∈ P be a right endpoint, i.e., i has no outgoing →-edge. Assume that χ(i) is not a right endpoint of τ . Since (V, →) is acyclic by (A 3 ), following from χ(i) a →-path, we must reach a →-maximal point f ∈ V , i.e., a right endpoint. Since endpoints are colored, we find j ∈ P such that f = χ(j). Now, we have χ(i) → + χ(j) and we deduce that i → + j, a contradiction. Conversely, a right endpoint e of (V, →) is colored hence we find i ∈ P with χ(i) = e. Now, if i is not a right endpoint then i → j for some j ∈ P . We deduce that χ(i) → + χ(j), a contradiction. Therefore, χ is a bijection between right endpoints of q and right endpoints of τ . Similarly, χ is a bijection between left endpoints of q and left endpoints of τ . Now, we deduce that (i, j) is a block in q (i.e., i is a left endpoint, i → * j and j is a right endpoint) iff (χ(i), χ(j)) is a block of τ .
If τ = Forget i τ and q is an abstraction of τ then we can check that q is an abstraction of τ . In particular, condition (A 3 ) follows from \ → = \ →. Note that if the first condition above is not satisfied then the tree automaton A K,M valid has no transitions from q reading Forget i . Add → i,j : We define transitions q = (P, <, →) when the following hold q has no internal points, i.e., there are no k , k, k ∈ P with k → k → k (internal points should be abstracted away with Forget k before adding a successor edge), (i, j) ∈ \ →: successor edges are only added between <-consecutive points, P = P , < = < and → = → ∪ {(i, j)}.
If τ = Add → i,j τ and q is an abstraction of τ then q is an abstraction of τ . Indeed, conditions (A 1 -A 2 ) for q are easy to check. Condition (A 3 ) follows from the fact that the relation → ∪χ( \→ ) in τ equals the relation → ∪ χ( \ →) in τ since the pair (χ(i), χ(j)) is added to → and removed from χ( \ → ). Again, if the first two conditions above are not satisfied then the tree automaton A K,M valid has no transitions from q reading Add → i,j . ⊕: We define transitions q 1 , q 2 ⊕ − → q when the following hold (with q 1 = (P 1 , < 1 , → 1 ) and q 2 = (P 2 , < 2 , → 2 )) there are no internal points in q 1 and q 2 (internal points should be forgotten first), P 1 ∩ P 2 = ∅: the ⊕ operation on STTs requires that the "active" colors of the two arguments are disjoint, q = (P, <, →) where P = P 1 ∪ P 2 , → = → 1 ∪ → 2 , the total order < is obtained by guessing how the blocks of q 1 and q 2 are shuffled: it could be any total order satisfying both → ⊆ and < 1 ∪ < 2 ⊆ <.
If τ = τ 1 ⊕ τ 2 and q 1 , q 2 are abstractions of τ 1 , τ 2 then q is an abstraction of τ . Again, conditions (A 1 -A 2 ) for q are easy to check. Now the relation \ → on q defines how the blocks of q 1 and q 2 are shuffled in q. Similarly, the relation = χ( \ →) defines how the blocks of τ 1 and τ 2 are shuffled in τ . Notice that if (i, j) ∈ \ → then i is a right endpoint and j is a left endpoint. Hence, the relation connects right enpoints of τ to left endpoints of τ , following the order dictated by q. We deduce that (A 3 ) holds for q. Again if the first two conditions above are not satisfied then the tree automaton A K,M valid has no transitions from q 1 , q 2 reading ⊕. ) is a split-STCW. But since q is accepting, we have = ∅. Hence τ is a simple TCW. Moreover, for every subterm τ of τ , the number of blocks in τ is the number of blocks in the state q that labels τ in this accepting run. By definition, the number of blocks of q is at most K. Therefore, τ describes a split-decomposition of τ of width at most K.
(V 2 ) Let T be a (K, M )-STTs arising from a split-tree T of width at most K and using constants less than M . Following the inductive construction of T from T given in the proof of Lemma 20, it is easy to see that

C Section 5: Tree automaton for realizability
Shuffle operation Let V 1 = (P 1 , → 1 , 1 , λ 1 , 1 , θ 1 ) and V 2 = (P 2 , → 2 , 2 , λ 2 , 2 , θ 2 ) be two split-TCWs such that their respective set of positions P 1 and P 2 are disjoint. Further, let ≤ be a total order on P = P 1 ∪ P 2 such that 1 ∪ 2 ⊆ < and → 1 ∪ → 2 ⊆ . Such orders are called admissible. Then, we define the split-TCW V = (P, →, , λ, , θ) by P = P 1 P 2 , λ = λ 1 ∪ λ 2 , → = → 1 ∪ → 2 , = \ →, = 1 ∪ 2 , and θ = θ 1 ∪ θ 2 . Indeed, this corresponds to shuffling the blocks V 1 and V 2 with respect to the admissible order ≤ and is called a shuffle, denoted by V = V 1 ≤ V 2 . This total order can be unambiguously specified by a word over the alphabet { , r} as follows. If width(V 1 ) = k and width(V 2 ) = m, then the shuffle of V 1 , V 2 is specified by a word That is, there exists k ∈ N such that width(U ) = width(V ) = k and for all M -contexts C ∈ TCW with width(C) = k + 1, C • U is realizable iff C • V is realizable. It is easy to see that ∼ M is an equivalence relation. A function f : STCW → STCW is said to be sound if it preserves realizability under all Mcontexts, i.e., for all W ∈ STCW we have W ∼ M f (W ). The idea is to come up with a sound abstraction of finite index, so that a finite tree automaton can be defined which works only on the representatives. The operation preserves the equivalence between split-TCW as shown below.
Lemma 27 (Congruence lemma). Let U 1 , U 2 , U 1 and U 2 be split-TCWs such that U 1 ∼ M U 1 and U 2 ∼ M U 2 . Then, for all x ∈ { , r} n with n = width(U 1 )+width(U 2 ), we have Proof. Let width(U 1 ) = K 1 , width(U 2 ) = K 2 and let C ∈ TCW be a context of width K 1 +K 2 +1. K1+K2 . Then it can be seen from Figure 9 that there exist contexts C 1 ∈ TCW of width K 2 + 1 and C 2 ∈ TCW of width

C.1 The (possibly infinite) tree automaton for realizability
We now build a tree automaton for realizability, which can possibly have infinitely many states. Subsequently, we show (i) some conditions under which it has finitely many states and (ii) additional abstractions ensuring that it is always finite.
Proposition 12. We can build a tree automaton valid is finite the first component is finite. But as we will see below the weights in the states can grow unboundedly in general. We assume that wt(k, k) = 0 for all k ∈ P . Also, if i < j are points then wt(j, i) ≤ 0 ≤ wt(i, j).
Below, we identify such a pair (q, wt) with a split-TCW, ignoring the relation since the weight function is totally defined on P 2 , and ignoring the Σ-labelings of nodes since they are irrelevant for the realizability of TCWs.
To help understand the construction, we first give the invariant that will be maintained by the automaton. Let τ be a (K, M )-STT with τ = (V, →, λ, , θ, χ). Assume that there is a (bottomup) run of A K,M inf reading τ and reaching state (q, wt) with q = (P, <, →). Then, projecting this run on the first component, we obtain a run of A K,M valid reading τ and reaching state q. From (A 3 ) of A K,M valid , the state q induces a total order on the blocks of τ and turns τ into a split-STCW ( τ , ). We say that the abstraction (q, wt) of τ computed by A K,M inf is sound if it preserves realizability under contexts: The key invariant is that A K,M inf always computes a sound abstraction of the given STT.
We now formalize the definition of the tree automaton.
Atomic STTs: When reading the atomic STT τ = (1, a) with a ∈ Σ, the tree automaton In both cases, it is easy to check that (q, wt) is a sound abstraction of τ . by  exchanging i and j in (q, wt). Exchanging colors preserves soundness: if τ = Rename i,j τ and (q, wt) is a sound abstraction of τ then (q , wt ) is a sound abstraction of τ . j τ and (q, wt) is a sound abstraction of τ , it immediately follows that (q , wt ) is a sound abstraction of τ . This is because adding of an edge only reduces the number of contexts to be considered to show equivalence of realizability under contexts. ⊕: We define transitions (q 1 , wt 1 ), (q 2 , wt 2 ) ⊕ − → (q, wt) when the following hold the weights are inherited and completed as follows: for all i, j ∈ P = P 1 P 2 , Now, if τ = τ 1 ⊕ τ 2 and (q 1 , wt 1 ), (q 2 , wt 2 ) are sound abstractions of τ 1 , τ 2 then (q, wt) is a sound abstraction of τ . Indeed, by definition of ⊕-transitions in A K,M valid , the total ordering < of q indicates how blocks of q 1 and q 2 are shuffled. Hence (q, wt) = (q 1 , wt 1 ) x (q 2 , wt 2 ) for some x ∈ { , r} * . Now, the induced ordering on the blocks of τ corresponds to the same shuffle of blocks, i.e., ( τ , . Now, applying the congruence Lemma 27, we obtain that (q, wt) is a sound abstraction of τ .
valid (in particular, i is not an endpoint), i is not part of a negative cycle of length 2: for all j = i we have wt(j, i) + wt(i, j) ≥ 0, for all j, k ∈ P = P \ {i}, we define wt (j, k) = min(wt(j, k), wt(j, i) + wt(i, k)), i.e., wt is obtained by eliminating i.
Notice that if the second condition above is not satisfied then the tree automaton A K,M inf has no transitions from (q, wt) reading Forget i . With this we have Claim 28. If τ = Forget i τ and W = (q, wt) is a sound abstraction of τ , then W = (q , wt ) is a sound abstraction of τ .
Proof. We will first show that W ∼ M W . Notice that since i is not an endpoint, W and W have the same number of blocks. Let C ∈ TCW be an M -context with width(C) = 1 + width(W ) = 1 + width(W ). We show that C • W is realizable iff C • W is realizable. Suppose C • W has a negative cycle Q. Wlog we may assume that Q is simple.

1.
If this cycle Q does not pass through i, then the same cycle Q is present in C • W , and by definition of wt , the weight of Q in C • W is at most the weight of Q in C • W . 2. Let the cycle Q pass through i. Since i is not part of a negative cycle of length 2, there are points j = i = k such that j, i, k is a part of the cycle. Removing i, we obtain a cycle Q containing j, k in C • W . By definition, wt (j, k) ≤ wt(j, i) + wt(i, k), and hence wt (Q ) ≤ wt(Q).
In both cases, we obtain a negative cycle Q in C • W . Conversely, assume that there is a negative cycle Q in C • W . We obtain a cycle Q in C • W by inserting i between each pair of consecutive points j, k in Q such that wt (j, k) < wt(j, k).
Notice that in this case wt (j, k) = wt(j, i) + wt(i, k), and otherwise wt (j, k) = wt(j, k). Therefore, wt(Q) = wt (Q ) and we have a negative cycle in C • W as well. This completes the proof that W ∼ M W . Now, we know by hypothesis that W ∼ M ( τ , ). Further, we also have ( τ , ) since τ differs from τ only in the coloring; the remaining part is the same and in particular = . Hence the paths (and cycles) are exactly the same. Thus, combining these, we obtain W ∼ M ( τ , ), which completes the proof of the claim.
Accepting condition: Finally, we define a state (q, wt) to be accepting if q is an accepting state of A K,M valid , hence it consists of a single block with left endpoint i and right endpoint j (possibly i = j), the pair (q, wt) is realizable, i.e., wt(i, j) + wt(j, i) ≥ 0.
This completes the construction of A K,M inf , whose correctness follows from the claim below and thus, completes the proof of Proposition 12.
has an accepting run reading τ reaching state (q, wt) at the root. Then τ is accepted by A K,M valid . Moreover, (q, wt) is a sound abstraction of τ , which implies ( τ , ) ∼ M (q, wt). Now, since q has a single block, so does τ and the hole relation is empty. Therefore, τ ∼ M (q, wt). Since the latter is realizable by definition of accepting states, we deduce that τ is realizable.
Conversely is the fact that i should not be part of a negative cycle of length 2 when reading Forget i . Assume that there is a subterm Forget i τ of τ and that in the state (q , wt ) associated with τ , point i is part of a negative cycle of length 2. Then (q , wt ) is not realizable and since it is a sound abstraction of τ it follows that ( τ , ) is not realizable either. But τ is a subgraph of τ . This would imply that τ is not realizable, a contradiction. Finally, let (q, wt) be the state reached at root of τ in this run of A K,M inf . Since we started from an accepting run of A K,M valid , state q is accepting in A K,M valid . Moreover, since τ is realizable and (q, wt) is a sound abstraction of τ , we also have (q, wt) realizable. Therefore, (q, wt) is accepting in Observe that the number of states of A K,M inf may grow unboundedly, since the constants in wt can grow in the automaton (due to taking sum during forget transitions). A backward edge j > k with j > i > k may grow in absolute value with the update wt (j, k) = min(wt(j, k), wt(j, i) + wt(i, k)). On the other hand, a forward edge j < k may get a big value due to the formula above only if wt(j, k) = ∞. After having a finite value, the weight of a forward edge may only decrease due to the min operation.
A first question we ask is if there are classes where this does not happen. A simple solution is to consider time-bounded classes where all behaviors must occur within some global time bound T . The idea here is to check if some backward edge grows above T in absolute value after a forget move, in which case we reject it; while if the same happens with a forward edge, then replace it with ∞.
Corollary 30. If the system is time-bounded by some constant T , then there exists a finite tree automaton A K,M real of size at most T O(k 2 ) · 2 O(k 2 lg k) for checking realizability.
However, in general, when we do not assume a global time bound, the constants in the states of A K,M inf may grow unboundedly. We next show how to modify the above construction so that we can make sure that the constants are always bounded and hence obtain a finite tree automaton for realizability. Thus, this generalizes the above corollary with a better complexity.

C.2 Bounding the constants
We now prove Proposition 7, by constructing a finite tree automaton A K,M real to check realizability. The set of states of A K,M real will be a finite subset of the states of A K,M inf . More precisely, a state (q, wt) of A K,M inf with q = (P, <, →) is a state of A K,M real if for all i, j ∈ P we have wt(i, j) = +∞ or |wt(i, j)| ≤ 8KM , where K and M are constants defined earlier.
As mentioned earlier, the weights on back and forward edges may grow (due to taking sums) after each forget transition. We will define three transformations σ, β, γ which change the weights of a state without affecting its realizability under contexts 1 . Each transformation maps a state (q, wt) of For instance, the simplest of these transformations is the map σ defined by σ(q, wt) = (q, wt ) where for all i < j, wt (i, j) = wt(i, j) and wt (j, i) = min{wt(j , i ) | i ≤ i ≤ j ≤ j}. In other words, the transformation σ strengthens the constraints of backward edges. It is then easy to check that σ preserves realizability under contexts: Proof. Let W = (q, wt) and W = σ(W ) = (q, wt ). Observe that since we apply only min operations, the weights of edges given by wt in σ(W ) can only be lower than the weights of edges given by wt in W . Let C be a context. If Q is a negative cycle in C • W , then the same cycle taken in σ(W ) will have either the same or a lower total weight and hence be negative. In the other direction, suppose C • σ(W ) has a negative weight cycle Q: i 1 i 2 . . . i r = i 1 . Consider the weight of the same cycle in W . The weights of the forward edges are the same. For each backedge e = (i j , i j+1 ), by definition of σ, there exists a backedge e contained in (or possibly equal to) e such that wt (e) = wt(e). That is, e = (k, ) such that i j+1 ≤ < k ≤ i j . Then we can replace in Q, each such backedge e by the backward path segment i j k i j+1 , whose weight is lesser than or equal to wt (e) = wt(e ). Thus, we have a negative cycle in C • W .
The backward abstraction β Next, to bound back edges we define a transformation β which reduces the weight of a back edge when it goes above a certain constant in absolute value, while preserving realizability under all contexts. In fact, we define it on back edges across a block. Let (q, wt) be a state of A K,M inf with q = (P, <, →). A pair of points (j, i) ∈ P 2 is said to be a block back edge (denoted BBE) if i < j are the end points of a block in q, i.e., i → + j and this →-path cannot be extended (on the left or on the right). A big block back edge (BBBE) is a block back edge e such that M + wt(e) ≤ 0. For any two positions i < j, we define BBE(i, j) to be the set of block back edges between i and j. That is, BBE(i, j) = {( , k) | ( , k) is a BBE and i ≤ k < ≤ j}. We also define B(i, j) to be the set of big block back edges between i and j: B(i, j) = {e ∈ BBE(i, j) | e is big}. We now define β(q, wt) = (q, wt ) where, for any i < j, The idea is to change the weight of big BBE to −M by adding an offset to all the other edges (backward and forward) crossing this block. Note that this does not increase the absolute value of any constant. Further, after the backward abstraction, the absolute value of weights of block back edges is bounded by M , i.e., for all BBE i j, we have wt (j, i) ≥ −M . Indeed, either the edge was big and we get wt (j, i) = −M or it was not big and wt (j, i) = wt(j, i) > −M . Notice also that a BBE is big in (q, wt) iff it is big in β(q, wt). The crucial property is that we leave the weights of all cycles unchanged (under all contexts). Let Q be a path in C • W . Assume Q uses a backedge n m in C going over a BBBE e = i j in W . Then we replace in Q the edge n m by the path m j, i n. We then have We deduce that C • W has a negative cycle Q iff C • W has a negative cycle Q using no edges in C crossing over a BBBE of W , forward or backward.
Similarly, we can show that C • β(W ) has a negative cycle Q iff C • β(W ) has a negative cycle Q using no edges in C crossing over a BBBE of β(W ). Recall that a BBE is big in W iff it is big in β(W ).
Therefore, in order to prove that C • W is realizable iff C • β(W ), it suffices to consider cycles Q using no edges in C crossing over a BBBE of W . Now, for such a cycle, we can show that the weight wt(Q) in C • W equals the weight wt (Q) in C • β(W ). Indeed, for each BBBE e = i j in W , the number of forward edges k in Q going accross e (i.e., k ≤ i < j ≤ ) equals the number of backward edges k going across e (i.e., k ≤ i < j ≤ ). This uses the fact that all points of W are endpoints. Moreover, by the hypothesis on Q, none of these edges are from C. We deduce that wt(Q) = wt (Q).
While block back edges are now bounded (and back edges across holes can also be bounded by −M ), this does not suffice to bound all back edges. To obtain such a bound on all back edges, we need to relate large back edges to edges contained within them. For this, we need to define another property, that we will inductively maintain as an invariant in the tree automaton.
Definition 33 (Backward-edge property (BEP)). A split-TCW W is said to satisfy the backward- With this, we have our second and crucial invariant.
real always satisfies BEP. Note that, by definition, any M -context C satisfies BEP. Preserving this invariant requires a slight transformation of the shuffle operation (at a ⊕ node), which we will discuss later in this appendix. However, assuming that Invariant (I2) holds, we now show that all back edges are bounded. Proof. Assume that W = β(W ) = (q, wt ) satisfies BEP. Let i j be some backward edge in W , i.e., i < j. Then there exist some n ≥ 0 points i = j n+1 j n j n−1 . . . j 1 j 0 = j. Notice that in W also, all points are endpoints. Hence, for all 0 ≤ k ≤ n we have either j k+1 j k or j k+1 → j k and in the latter case, (j k+1 , j k ) is a block.
We show by induction on m−k that for 0 ≤ k < m ≤ n+1 we have wt (j k , j m ) ≥ −(m−k)M . In particular, we deduce that wt (j, i) ≥ −(n + 1)M .
If m = k + 1 then either j k+1 j k is a hole and applying BEP we get wt (j k , j k+1 ) > wt (j k , j k ) − M + wt (j k+1 , j k+1 ) = −M , or j k+1 → j k is a block and by definition of β we get wt (j k , j k+1 ) ≥ −M . Now, assume that m > k + 1. Since we only have endpoints, there must be a hole j +1 j for some k ≤ < m. Then applying BEP we get wt (j k , j m ) > wt (j k , j ) − M + wt (j +1 , j m ).
Applying the above property to k = 0 and m = n + 1, we deduce that wt (j, i) ≥ −(n + 1)M . Now the number of points in P is at most 2K, therefore, n + 1 ≤ 2K − 1, which concludes the proof of the lemma.
Forward abstraction γ. Finally, we turn to forward edges. We apply a forward abstraction γ that removes all forward edges (i.e., changes their weight to ∞) that are too large to be useful for creating negative cycles. Let W = (q, wt) be a state of A K,M inf with q = (P, <, →). A forward edge (i, j) ∈ P 2 with i < j is called big if wt(i, j) + e∈BBE(i,j) wt(e) ≥ (3K − 1)M . Note that as e is a (block) back edge, its weight is negative. Then we define γ(q, wt) = (q, wt ) where, for any i < j, wt (j, i) = wt(j, i) and While the definition of this abstraction is simple, it turns out that showing that it is sound (i.e., it preserves realizability under all contexts) is rather tricky, even with the additional BEP assumption (which will be maintained inductively on the tree automaton).
Proof. Let W = (q, wt) be a state of A K,M inf with q = (P, <, →). Assume that W satisfies BEP. Let C be an M -context. Note that C • W and C • γ(W ) have the same paths and the same cycles. Moreover, if Q is such a cycle, its weight wt (Q) in C • γ(W ) is at most its weight wt(Q) in C • W . Therefore, if there is a negative cycle in C • γ(W ) then the same cycle is negative in C • W .
Conversely, we have to prove now that if there is a negative cycle in C • W then there is also a negative cycle in C • γ(W ). So we assume that C • W has a negative cycle. Let Q be a shortest (in terms of path length) negative cycle in C • W . We will show that Q must be also a negative cycle in C • γ(W ), i.e., wt (Q) < 0.
If Q does not pass through any big forward edge then wt (Q) = wt(Q) and we are done.
Else, suppose Q passed through i j, a big edge in W . Then, we can always break Q into ijQ 1 j j Q 2 i i Q 3 i as depicted in Figure 11, where j j is the last time Q crosses j backward and i i is the first time that Q crosses i backward (both these must happen since the cycle has to return from j to i). As a result, we have that Q 2 lies completely within i and j, i.e., for all ∈ Q 2 , i ≤ ≤ j. Now, let the points within i to j be i j n j n−1 . . . j 1 j 0 = j for some n ≥ 0. Applying BEP on backedge j j with respect to point j 0 = j, we obtain wt(j , j ) ≥ wt(j , j 0 ) − M + wt(j 0 , j ). Similarly we apply BEP on i i with respect to i. Denoting by R 0 the path j 0 j Q 2 i i, we maintain the invariant that R 0 lies to the left of j 0 (and right of i). We have: In the above we have wt(Q 1 ) + wt(j , j 0 ) ≥ 0, else we have a shorter negative cycle jQ 1 j j. Similarly wt(i, i ) + wt(Q 3 ) ≥ 0. Now, the sketch of the proof is as follows: We consider the points between i and j and process them inductively, from the right. We start from j = j 0 and for each point, we use BEP to move left while maintaining the invariant that the resulting path cannot go right (this is true when we begin since as we observed above R 0 indeed stays within [i, j]). Finally, since the number of points in R 0 can at most be 2K we terminate and are left with a lower bound on wt(R 0 ). This in conjuction with the equation above gives the theorem. Let us start with j 1 j 0 . We have two cases: Assume that R 0 passes through j 1 (see Figure 12). Then R 0 = j 0 j Q j 1 R 1 i where Q is the part of R 0 going from j to j 1 and R 1 is the part of R 0 going from j 1 to i. Thus R 1 satisfies the invariant property that it stays between i and j 1 . Applying BEP on backedge j j wrt the point j 1 we have: Again, we have wt(j 1 , j ) + wt(Q ) ≥ 0 by minimality of the negative cycle Q. Assume R 0 does not pass through j 1 . Then it cannot pass through anything on the right of j 1 , i.e., in this case j 0 . Thus, R 0 (after the first backedge j j 0 ) stays on the left of j 1 , i.e., we write R 0 = j 0 j Q for some Q which stays to left of j 1 . We then define R 1 = j 1 j Q , which satisfies the invariant property that it lies in [j 1 , i]. Applying BEP on backedge j j 1 wrt the point j 1 we have: Inductively, we can apply the same argument for j 2 , . . . , j n and obtain segments R 2 , . . . R n (notice that R n must consist of the single backedge i j n since i j n ) such that finally, we have: If any j i+1 j i is a hole, we apply BEP on the backedge to obtain wt( valid , there are at most K blocks in W , hence at most K − 1 holes. Moreover, there are at most 2K points and n ≤ 2K − 2. We deduce that, This gives: which is a contradiction. The last inequality follows by the definition of a big edge. Thus, no big edge can be part of the shortest negative weight cycle. This shows that the existence of negative cycles is preserved by the forward abstraction.

Construction of A K,M real
The finite tree automaton A K,M real is derived from A K,M inf by applying the abstraction σ (strengthening) at ⊕ nodes and β (backward) and γ (forward) at Forget i nodes. More precisely, (q 1 , wt 1 ), (q 2 , wt 2 ) β(q , wt )) if q has no internal points and (q , wt ) = (q , wt ) otherwise. The reason for assuming that q has no internal points before applying the abstractions is that it is a precondition for Lemmas 14 and 16. The reason for performing the σ abstraction on ⊕ if m and n are not from the same q i , then wt ( , i) = wt(n, m) = 0 > −M ≥ wt ( , k) − M + wt (j, i). So we assume below that m and n are both from the same state, say q 1 . if m n does not cross j, k. Wlog, let us say that it remains entirely to right of k, i.e., k ≤ m < n. Then, wt ( , i) = wt(m, n) ≥ wt ( , k) > wt ( , k) − M + wt (j, i) since last two terms add a negative quantity. if m n crosses j, k, i.e., m ≤ j ≤ k ≤ n. Let k be the least point in q 1 which is above k: we have k ≤ k ≤ n. Similarly, let j be the greatest point in q 1 below j: m ≤ j ≤ j. We must have j = k or j k . In this case, applying BEP on edge (m, n) of (q 1 , wt 1 ), we get wt Forget c : Let (q, wt) . We assume that (q, wt) satisfies BEP. We show that (q , wt ) also satisfies BEP. So let i ≤ j ≤ k ≤ be points in q such that j k or j = k. Notice that also in q we have j k or j = k since a forget transition only removes an internal point. We have wt( , i) > wt( , k) − M + wt(j, i). There are two cases.
Case 2: wt ( , i) < wt( , i). In this case, by definition of the transition, we must have wt ( , i) = wt( , c) + wt(c, i). First, note that c ∈ {i, j, k, }, since these points are in P but by definition c ∈ P . Now we have two cases, either k < c or c < j. Indeed, since j k or j = k, we cannot have j < c < k. Wlog let k < c (the other case is symmetric and follows by similar arguments).
β: Let (q, wt) be a state satisfying BEP and let β(q, wt) = (q, wt ) be its backward abstraction. We will show that (q, wt ) also satisfies BEP. Let i ≤ j ≤ k ≤ be such that j k or j = k. Notice that the BBBE between i and are either between i and j or between k and : B(i, ) = B(i, j) B(k, ). Hence, we have γ trivially preserves BEP as it does not change the weights of backedges.

D Tree automata for timed systems
The goal of this section is to build a tree automaton which accepts the STTs denoting TCWs accepted by a TPDA. We recall the formal statement given in Section 4.
Proposition 8. Let S be a TPDA of size |S| (constants encoded in unary) with set of clocks X and using constants less than M . Then, we can build a tree automaton A K,M S of size |S| O(K 2 ) · 2 O(K 2 (|X|+1)) such that Again, we could prove the existence of a tree automaton by arguing that the existence of a run of S on a simple TCW is MSO definable and appealing to Courcelle's theorem [9]. But, as for the automaton A K,M valid in Appendix B we choose to directly construct the tree automaton A K,M S , allowing in particular to analyse its size which is stated above.
Let us explain first how the automaton would work for an untimed system with no stack. At a leaf of the STT of the form (i, a) the tree automaton guesses a transition δ from S which could be executed reading action a. It keeps the transition in its state, paired with color i. After reading a subterm τ , the tree automaton stores in its state a map ∆ which assigns with each active (free) color k of τ the transition ∆(k) guessed at the corresponding leaf. The map ∆ can be easily updated at nodes labelled ⊕ or Forget i or Rename i,j . When, reading a node labelled Add → i,j , the tree automaton checks that the target state of the transition ∆(i) equals the source state of the transition ∆(j). This ensures that the transitions guessed at leaves form a run when taken in the total order induced by the word denoted by the final term. At the root, we check that at most two colors remain free: i and j for the leftmost (resp. rightmost) endpoint of the word. Then, the tree automaton accepts if the source state of ∆(i) is initial in S and the target state of ∆(j) is final in S.
The situation is a bit more complicated for timed systems. First, we are interested in the simple TCW semantics in which each event is blown-up in several micro-events. Following this idea, each transition (s, γ, a, op, R, s ) of the timed system S is blown-up in micro-transitions as explained in Section 2.2, assuming that γ = γ 1 ∧ · · · ∧ γ n has n conjuncts of the form x ∈ I, and that R = {x 1 , x 2 , . . . , x m }: Notice the reset part at the end which allows an arbitrary number (possibly zero) resets of clock x 1 (depending on how many timing constraints for clock x 1 will originate from this reset), followed by an arbitrary number (possibly zero) resets of clock x 2 , etc. The second difficulty is to make sure that, when a guard of the form x ∈ I is checked in some transition, then the source point of the timing constraint in the simple TCW indeed corresponds to the latest transition resetting clock x. To check this property, the tree automaton A K,M S stores, for each color k of the left endpoint of a block, the set C(k) of clocks reset by some transition whose middle point (the one corresponding to a, op micro-transition) occurs in the block. for each pair (i, j) of colors of left endpoints of distinct blocks, set D(i, j) of clocks that are reset in block i and checked in j.
Finally, the last property to be checked is that the push-pop edges are well-nested. To this end, the tree automaton A K,M S stores the set E of pairs (i, j) of left endpoints of distinct blocks such that there is at least one push-pop edge from block i to block j.
Either the target state of ∆(i) equals the source state of ∆(j), or there is an ε-path of microtransitions − → between the target state of ∆(i) and the source state of ∆(j): indeed, adding → between i and j means that these points are consecutive in the final TCW, hence it should be possible to concatenate the micro-transition taken at i and j. ⊕ We define (q 1 , ∆ 1 , C 1 , D 1 , E 1 ), (q 2 , ∆ 2 , C 2 , D 2 , E 2 ) ⊕ − → (q, ∆, C, D, E) to be a transition if q 1 , q 2 ⊕ − → q is a transition of A K,M valid . The other components of are inherited: ∆ = ∆ 1 ∪ ∆ 2 , C = C 1 ∪ C 2 , D = D 1 ∪ D 2 and E = E 1 ∪ E 2 . For all i < k < j left endpoints in q = (P, <, →), we have C(k) ∩ D(i, j) = ∅. This is the crucial condition which ensures that a timing constraint always refers to the last transition resetting the clock being checked. If some clock x ∈ D(i, j) is reset in block i and checked in block j, it is not possible to insert a block k between blocks i and j if clock x is reset by a transition in block k. For all (i, j) ∈ E and (k, ) ∈ E, if i < k < j then < j. This ensures that the push-pop edges are well-nested.
Accepting condition A state (q, ∆, C, D, E) is accepting if q is an accepting state of A K,M valid , hence it consists of a single block with left endpoint i and right endpoing j (possibly i = j), the source state of ∆(i) is an initial state of S, and the target state of ∆(j) is a final state of S, or there is an ε-path of micro-transitions from the target state of ∆(j) to some final state of S. If the underlying system is a timed automata, it is sufficient to store the maps C, D in the state, since there are no stack operations.

E Dense-Time Multi-stack Pushdown Automata
In this section, we consider the model of dense-timed multistack push down automata (dtMPDA). The reachability problem for untimed MPDA is already undecidable. Several restrictions have been studied on MPDA like bounded phase, bounded context, bounded scope and so on to regain decidability. We look at dtMPDA restricted to a bounded number of rounds.
A dtMPDA is a tuple S = (S, Σ, Γ, X, s 0 , F, ∆) where S is a finite set of states, Σ is a finite alphabet, Γ is the stack alphabet, s 0 is the initial state, X is a finite set of clocks, F ⊆ S is a finite set of final states, and ∆ is a finite set of transitions of the form (s, γ, a, op, R, s ) where s, s ∈ S, a ∈ Σ, γ is a finite conjunction of atomic formulae of the kind x ∈ I for x ∈ X and I ∈ I, R ⊆ X is the set of clocks reset, and op is a stack operation of one of the following kinds: 1. nop does not change the contents of any stack, 2. ↓ i c where c ∈ Γ is a push operation that adds c on top of stack i, with age 0. 3. ↑ i c∈I where c ∈ Γ and I ∈ I is a pop operation that removes the top most symbol of stack i provided it is a c with age in the interval I.
A sequence σ = op 1 · · · op m of operations is a round if it can be decomposed in σ = σ 1 · · · σ n where each factor σ i is a possibly empty sequence of operations of the form nop, ↓ i c , ↑ i c∈I .

E.1 Simple TC-word semantics for dtMPDA
We define the semantics for dtMPDA in terms of simple TCWs. Let n denote the number of stacks. A simple TCW V = (P, →, λ, , θ) is said to be generated or accepted by a dtMPDA S if there is an accepting abstract run ρ = (s 0 , γ 1 , a 1 , op 1 , R 1 , s 1 ) (s 1 , γ 2 , a 2 , op 2 , R 2 , s 2 ) · · · (s m−1 , γ m , a m , op m , R m , s m ) of S such that s m ∈ F is a final state and the sequence of push-pop operations of any stack 1 ≤ y ≤ n is well-nested. In each prefix op 1 · · · op o with 1 ≤ o ≤ m, the number of pops of stack y is at most the number of pushes on stack y, and in the full sequence op 1 · · · op m the number of pops equals the number of pushes. the sequence op 1 · · · op m of stack operations has (at most) k-rounds. We have P = P 0 P 1 · · · P m with P i × P j ⊆ → + for 0 ≤ i < j ≤ n. Each transition δ i = (s i−1 , γ i , a i , op i , R i , s i ) gives rise to a sequence of consecutive points P i in the simple TCW. op i is an operation on some stack y. Intuitively, the transition δ i is simulated by a sequence of micro-transitions where γ i = γ 1 i ∧ · · · ∧ γ hi i and R i = {x 1 , . . . , x m }. The first and last micro-transtions, corresponding to the reset of a new clock ζ and checking the constraint ζ = 0 make sure that all micro-transtions in the sequence occur simultaneously. We have a point in P i for each micro-transition (excluding the ε-micro-transitions between the δ xj i ). Hence, P i consists in a sequence i → 1 i → · · · → hi i → p i → r 1 i → . . . → r gi i → r i where g i is the number of timing constraints corresponding to clocks reset during transition i and checked afterwards. Similarly, h i is the the number of timing constraints checked in γ i . We have λ(p i ) = a i and all other points are labelled ε. The set P 0 encodes the initial resets of clocks that will be checked before being reset. So we let R 0 = X and P 0 consists of a sequence the relation for timing constraints can be partitionned as = 1≤y≤n y x∈X∪{ζ} x where ζ = {( i , r i ) | 0 ≤ i ≤ m} and we set θ( i , r i ) = [0, 0] for all 0 ≤ i ≤ n. We have p i y p j if op i =↓ y b is a push and op y j =↑ y b∈I is the matching pop for stack y (same number of pushes and pops of stack y in op i+1 · · · op j−1 ), and we set θ(p i , p j ) = I. for each 0 ≤ i < j ≤ n such that the t-th conjunct of γ j is x ∈ I and x ∈ R i and x / ∈ R k for i < k < j, we have r s i x t j for some 1 ≤ s ≤ g i and θ(r s i , t j ) = I. Therefore, every point t i with 1 ≤ t ≤ h i is the target of a timing constraint. Moreover, every reset point r s i for 1 ≤ s ≤ g i should be the source of a timing constraint: r s i ∈ dom( x ) for some x ∈ R i . Also, for each i, the reset points r 1 i · · · r gi i are grouped by clocks (as suggested by the sequence of micro-transitions simulating δ i ): if 1 ≤ s < u < t ≤ g i and r s i , r t i ∈ dom( x ) for some x ∈ R i then r u i ∈ dom( x ). Finally, for each clock, we request that the timing constraints are well-nested: for all u x v and u x v , with u, u ∈ P i , if u < u then u < v < v.
We denote by STCW(S) the set of simple TCWs generated by S. The language of L(S) is the set of realizable simple TCWs in STCW(S). Given a bound k on the number of rounds, we denote by STCW(S, k) the set of simple TCWs generated by runs of S using at most k rounds. We let L(S, k) be the corresponding language.
Given a dtMPDA S, we show that all simple TCWs in STCW(S, k) have bounded split-width. Actually, we will prove a slightly more general result. We first identify some properties satisfied by all simple TCWs generated by a dtMPDA, then we show that all simple TCWs satisfying these properties have bounded split-width.
Let V = (P, →, λ, , θ) be a simple TCW. Recall that < = → + is the transitive closure of the successor relation. We say that V is k-round well timed with respect to a set of clocks Y and stacks 1 ≤ s ≤ n if the relation for timing constraints can be partitionned as = 1≤s≤n s x∈Y x where (T 1 ) for each 1 ≤ s ≤ n, the relation s corresponds to the matching push-pop events of stack s, hence it is well-nested: for all i s j and i s j , if i < i < j then i < j < j, see Figure 4. Moreover, V consists of at most k rounds, i.e., we have P = P 1 · · · P k with P i × P j ⊆ < for all 1 ≤ i < j ≤ k. And each P is a round, i.e., P = P 1 · · · P n with P s × P t ⊆ < for 1 ≤ s < t ≤ n and push pop events of P s are all on stack s (for all i t j with t = s we have i, j / ∈ P s ). (T 2 ) An x-reset block is a maximal consecutive sequence i 1 · · · i n of positions in the domain of the relation x . For each x ∈ Y , the relation x corresponds to the timing constraints for clock x and is well-nested: for all i x j and i x j , if i < i are in the same x-reset block, then i < i < j < j. Each guard should be matched with the closest reset block on its left: for all i x j and i x j , if i < i are not in the same x-reset block then j < i .
It is easy to check that the simple TCWs in STCW(S, k) where S is a dtMPDA using set of clocks X are well-timed for clocks in Y = X ∪ {ζ}, i.e., satisfy the properties above. The first condition (T 1 ) is satisfied by STCW(S, k) by definition. Consider (T 2 ). Let i x j and i x j for some clock x ∈ X. If i, i are points in the same x-reset block for some x ∈ X, then by construction of STCW(S), if i < i then i < j < j which gives well nesting. Similarly, if i < i are points in different x-reset blocks, then by definition of STCW(S), we have j < i . It is clear that the new clock ζ also satisfies (T 2 ).
Again, we play the split-game between Adam and Eve. Eve should have a strategy to disconnect the word without introducing more than (4nk + 4)(|Y | + 1) blocks. The strategy of Eve is as follows: Given the k-round word w, Eve first breaks this into two words. The first word only has stack 1 edges, and the second word has stack edges corresponding to stacks 2, . . . , n. The first word can now be dealt with as we did in the case of TPDA. Eve then breaks the second word into two words, the first of which has only stack 2 edges, while the second word has edges of stacks 3,4 . . . , n, and so on. Finally, we obtain n split-STCW's, each having edges corresponding to only one stack. Once this is achieved, these words can be processed as was done in the case of TPDA. The only thing to calculate is the number of cuts required in isolating each word.
Obtaining a word containing only stack i edges Since we are dealing with k-round TCWs, we know that the stack operations follow a nice order : stacks 1, . . . , n are operated in order k times. More precisely, by (T 1 ), the set P of points of the simple TCW V can be partitionned in P = P 1 ∪ P 1 ∪ · · · ∪ P k ∪ P k such that P 1 < P 1 < · · · < P k < P k and P 1 ∪ · · · ∪ P k contains all and only stack operations from stack 1. Eve's strategy is to separate all these sets, i.e., cut just after P 1 , P 1 , . . . , P k . This results in 2k − 1 cuts. This will not disconnect the word if there are edges with clock timing constraints across blocks, i.e., from P i or P i to some other block on the right.
Consider the case when we have timing constraints on some clock x which is reset in some block P i and checked in some block P j with i ≤ j. All these timing constraints come from the last reset block R x of clock x which lies in P i . With two cuts, we detach the consecutive sequence of resets in R x which are checked in P j . So with at most 2|Y | cuts, we detach all the resets that come from blocks P i with i ≤ j and are checked in block P j . Similarly, with at most 2|Y | cuts, we detach all the resets that come from blocks P i with i < j and are checked in block P j .
The split-TCW is now disconnected, and we obtain 2 words, one containing only stack 1 edges, and the other containing only stack 2, . . . , n edges. Each word has at most k|Y | holes after the