S Akshay
email: akshayss@cse.iitb.ac.in

Paul Gastin
email: paul.gastin@lsv.fr

Vincent Jugé
email: vincent.juge@u-pem.fr

Shankara Narayanan

Timed Systems through the Lens of Logic

constraints, or even by allowing (non-) deterministic updates of clocks. Subsequently, there has been a growing body of work [START_REF] Abdulla | Dense-timed pushdown automata[END_REF], [START_REF] Abdulla | Perfect timed communication is hard[END_REF], [START_REF] Akshay | Analyzing timed systems using tree automata[END_REF], [START_REF] Akshay | Towards an efficient tree automata based technique for timed systems[END_REF], [START_REF] Clemente | Decidability of timed communicating automata[END_REF], [START_REF] Clemente | Timed pushdown automata revisited[END_REF], [START_REF] Clemente | Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms[END_REF], [START_REF] Clemente | Timed pushdown automata and branching vector addition systems[END_REF], [START_REF] Krishna | What's decidable about recursive hybrid automata?[END_REF] towards adding auxiliary data structures like stacks [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF], [START_REF] Aiswarya | Verifying communicating multi-pushdown systems via split-width[END_REF], [START_REF] Aiswarya | Reasoning about distributed systems: WYSIWYG (invited talk)[END_REF] or queues [START_REF] Aiswarya | Reasoning about distributed systems: WYSIWYG (invited talk)[END_REF] to such timed automata. In all these, the techniques used to solve the emptiness problem were specific and tailormade to the choice of the data structure, kind of constraints and updates that are allowed.

Our goal is to introduce a novel and uniform approach for reasoning about such timed systems which allow rich timing features along with several types of auxiliary data structures at the same time. This technique captures the behaviors of the underlying model as graphs (see [START_REF] Aiswarya | Reasoning about distributed systems: WYSIWYG (invited talk)[END_REF]) and examines the logical definability of certain properties over these graphs.

We start by abstracting a run of a system, be it timed or not, as a sequence of instructions. When the system has a data structure d such as a stack, these instructions may write to d (denoted w(d)) or read from d (r(d)). The behavior is modeled as a linear graph (the sequence of instructions), with instruction labels and with additional data-structure edges matching writes with corresponding reads, as illustrated in Figure 1. When the system is timed, instructions may also reset clocks (x := 0), check guards (x < 3), etc. These timing instructions are recorded as additional labels in the linear graph without a priori being interpreted as edges, as shown on Figure 2 left. This allows to decouple the behavior of the underlying untimed system from the timing constraints that should be realized for the run to be feasible.

Our first contribution is to show that non-emptiness of a timed system T can be reduced to the satisfiability of a formula Φ T over such labeled linear graphs, which we call T -graphs. A T -graph G τ obtained from a sequence of instructions τ , as depicted in Figure 2 (left), is a witness of non-emptiness of T if it satisfies three properties: 1) The sequence of instructions τ can be generated by T . Since the system T is usually described with a finite automaton where transitions are labeled with instructions, T induces a regular language of instruction sequences which can easily be captured by (Φ 1 ) in our logic.

2) The data-structure edges should comply with the sequence of instructions. Intuitively, a node labeled with w(d) (resp. r(d)) should have an outgoing (resp. incoming) d-edge. If the data structure d is a stack (resp. queue), then d-edges should be well-nested, i.e., satisfy the LIFO (resp. FIFO) policy. It is known that compliance with stack or queue data-structures can be expressed (Φ 2 ) in our logics [START_REF] Bollig | Non-sequential theory of distributed systems[END_REF].

Abstract-In this paper, we analyze timed systems with data structures. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability o f s everal g raph p roperties [START_REF] Courcelle | Regularity equals monadic second-order definability for quasi-trees[END_REF], [START_REF] Blumensath | Monadic second-order definable graph orderings[END_REF] has been a challenging problem, and we show, using a highly nontrivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient a nd u niform p roof t echnique f or the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.

Index Terms-Timed systems, propositional dynamic logic, Logical definability, E fficient al gorithms, graphs

I. INTRODUCTION

The modeling and analysis of complex real-time systems is a challenging and important area, both from theoretical and practical points of view. The challenge often stems from the fact that such models have different sources of infinite behaviors, which makes them highly expressive but difficult to analyze. On one hand, the timing features engender complex constraints between events, which allow (or disallow) infinite sets of timed behaviors (over real numbers) satisfying these constraints. On the other hand, the auxiliary data structures such as multiple stacks allow a rich expressive power often leading to undecidable verification p roblems, e ven i n the absence of time. Thus, each choice of combining these components of real-time and specific d ata s tructures l eads t o rich models whose analysis is complicated and often intractable.

The analysis of timed systems without any additional data structures has often been done using well-accepted models like timed automata [START_REF] Alur | A theory of timed automata[END_REF], where clocks are real-valued variables that are reset and checked at guards. The classical approach to analyze such timed automata is by abstracting the realtimed system using the so-called region abstraction into a finite-state a utomaton p reserving e mptiness. S everal variants and extensions of this basic model have been considered over the years, for instance using event-clocks [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF] ≤ 0

≤ 0 < -2 ≤ 1 < 6 ≤ 5 < -4 < 3 ≤ -2
Fig. 2: Left: labeled linear graph G τ obtained from a sequence of timed instructions τ . For readability, the nodes are numbered and their instruction labels are written below them. Right: the corresponding weighted graph G τ .

3) The real-time constraints induced by the timing instructions should be realizable, i.e., it is possible to timestamp the nodes of G with some real numbers so that all timing constraints are satisfied. The second main contribution of this paper is to show that realizability can be expressed (Φ 3 ) in our logic. We use a light-weight propositional dynamic logic called EQ-ICPDL for the logical definability. Writing formulae for our systems in EQ-ICPDL is rather intuitive and improves readability in several cases compared to the classical MSO. On a technical note, it is known that EQ-ICPDL is a strict fragment of MSO, and gives us a more tractable complexity than MSO (avoiding a non-elementary blowup).

We show that realizability can be expressed in EQ-ICPDL in two steps. First, from the T -graph G τ , we define a weighted graph G τ which retains only the timing constraints induced by the timed instruction sequence τ . For instance, in Figure 2, the T -graph G τ is on the left and the associated weighted graph G τ on the right. In G τ , an edge from node i to node j labeled < 6 means that the difference t(j) -t(i) between the timestamps assigned to i and j should be less than 6. We prove that the weighted graph G τ can be EQ-ICPDL-interpreted in the graph G τ . This holds for all timing features that we consider. Second, we prove that realizability of weighted graphs is expressible in EQ-ICPDL, say with Φ 3 . Since weighted graphs G τ can be EQ-ICPDL-interpreted in T -graphs G τ , we can backward translate Φ 3 into some EQ-ICPDL formula Φ 3 expressing realizability over T -graphs. Finally, non-emptiness of T is equivalent to satisfiability of

Φ T = Φ 1 ∧ Φ 2 ∧ Φ 3 .
Our logical characterization of realizability for weighted graphs is highly non-trivial. It is easier when the underlying system only has closed guards, but we go beyond this and prove that realizability is also definable in EQ-ICPDL in the presence of both open and closed guards. On the other hand, we show that, without the linear order, realizability is not definable in MSO. In fact, we show that this already holds for graphs with a partial order of width (i.e., size of the largest anti-chain) 2, thus proving a tight characterization.

Our third contribution is to show how the two results above can be combined with existing techniques to give an effective algorithm for checking emptiness of several classes of timed systems. First, observe that the above two contributions do not immediately imply that checking emptiness of the system is decidable, as satisfiability of EQ-ICPDL formulae over arbitrary collections of graphs is undecidable. This is expected, since, even in the untimed case, having a single queue or two stacks as data structures leads to undecidability of emptiness. However, we can now consider under-approximations, as classically done for untimed systems. One such underapproximation is to consider collections of T -graphs that have a fixed bound on the tree-width. Such T -graphs can now be interpreted into trees and we can use the fact that checking satisfiability for EQ-ICPDL (with bounded intersection width) over trees is decidable in EXPTIME. This gives us a matching EXPTIME algorithm for checking emptiness of timed systems whose graph behaviors have a bounded tree-width. Using this approach, we retrieve many known results on timed systems with data structures, and also obtain new results. Our approach captures with elan, the intricate flow and exchange of information between data structures and clocks, see Section V. Related work. Our technique is orthogonal to the theory of timed systems via the region construction as well as to other related approaches. In the untimed setting, the closest work to ours is in [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF], [START_REF] Aiswarya | Verifying communicating multi-pushdown systems via split-width[END_REF], where generic approaches for decidability via logic and tree-width have been developed for automata with data structures in the untimed setting. There have been several papers on the decidability of timed systems with a single stack: [START_REF] Bouajjani | On the automatic verification of systems with continuous variables and unbounded discrete data structures[END_REF], [START_REF] Abdulla | Dense-timed pushdown automata[END_REF] deal with specific timing constraints, while [START_REF] Clemente | Timed pushdown automata revisited[END_REF], [START_REF] Clemente | Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms[END_REF] use the language of timed atoms to specify and analyze an orthogonal but powerful extension to timed registers. In [START_REF] Clemente | Timed pushdown automata and branching vector addition systems[END_REF], a NEXPTIME bound is shown in this setting by reduction to one-dimensional branching vector addition systems. However, all these works are restricted to a single stack, while we tackle several data structures including multiple stacks, queues. Many recent papers [START_REF] Clemente | Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms[END_REF], [START_REF] Clemente | Decidability of timed communicating automata[END_REF], [START_REF] Abdulla | Perfect timed communication is hard[END_REF] consider complex constraints between data structures and clocks. In these papers, there are time constraints between data structures d 1 , d 2 , between clocks, and also between a clock c and a data structure d. All of these can be modeled easily in our case, as can be seen in Section V.

Our work is also related to [START_REF] Akshay | Analyzing timed systems using tree automata[END_REF], [START_REF] Akshay | Towards an efficient tree automata based technique for timed systems[END_REF], where the behaviors of timed systems with stacks are modeled as graphs having data-structure edges as well as time constraint edges. The presence of two types of edges necessitates a fresh proof for the the bound on tree-width for each kind of timing feature. On the contrary, we directly inherit the bound on tree-width established in the untimed setting. The other main difference is that [START_REF] Akshay | Analyzing timed systems using tree automata[END_REF], [START_REF] Akshay | Towards an efficient tree automata based technique for timed systems[END_REF] directly build tree automata instead of going via logic. Using logic instead of directly building a tree automaton allows us to have a simpler higher level approach which is easier to write and less technical.

The logic we use builds on Propositional Dynamic Logic, a classical logic to reason about programs [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. The extension with loop, intersection and converse was explored in [START_REF] Göller | PDL with intersection and converse: satisfiability and infinite-state model checking[END_REF], where complexity bounds were shown for satisfiability and model checking. We inherit these complexity bounds. However, to the best of our knowledge, this is the first time this logic has been used in the analysis of timed systems. Further, even with MSO logic (a strictly more powerful and wellknown logic), the characterization of realizability in MSO over graphs of timed systems was open, as mentioned in [START_REF] Akshay | Analyzing timed systems using tree automata[END_REF]: we settle this problem in this paper.

Complete proofs of all results can be found in [START_REF] Akshay | Timed systems through the lens of logic[END_REF].

II. PRELIMINARIES

Node-and edge-labeled graphs. Let Σ and Γ be two alphabets. Nodes will be labeled with Σ and edges with Γ.

A (Σ, Γ)-labeled graph is a tuple G = (V, E, λ) where V is a finite set of vertices, λ : V → 2 Σ labels vertices with (sets of) letters from Σ and E ⊆ V × Γ × V is the set of labeled edges.

A vertex may have 0, 1 or several labels from Σ. For γ ∈ Γ, we let E γ = {(u, v) : (u, γ, v) ∈ E} be the set of edges labeled γ. G(Σ, Γ) denotes the set of (Σ, Γ)-labeled graphs.

In this paper, graphs model behaviors of sequential systems. Hence, we have a special symbol succ in Γ to define the successor relation E succ of a total order on V . We simply write u ≺• v instead of (u, v) ∈ E succ . We call these graphs linear; we let = ≺• * be the linear order induced by ≺• and we note ≺ = ≺• + the strict order. The other edges E γ , with γ ∈ Γ \ {succ}, are used to model other useful relations in the graph, for instance the matching push-pop relation if we are interested in pushdown systems. Propositional dynamic logic over labeled graphs. We define now the logic that we will use to specify properties of graphs. We use a variant of the propositional dynamic logic [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. This logic is sufficiently expressive for our purposes and enjoys good complexity for the satisfiability problem, rather than the more expressive monadic second order logic (MSO) which has a much higher complexity. The logic ICPDL(Σ, Γ) is defined over Σ (often seen as propositional variables), and Γ (often seen as atomic programs).

Syntax:

We have the following, with p ∈ Σ and γ ∈ Γ: Φ ::= E σ : ¬Φ : Φ ∨ Φ σ ::= : p : σ ∨ σ : ¬σ : π σ : loop(π)

π ::= γ -→ : test{σ} : π + π : π • π : π * : π -1 : π ∩ π
In ICPDL, C stands for converse (π -1 ) and I for intersection (π ∩ π). We also consider LCPDL which is the fragment with loop but without intersection, since it has better complexity, as stated in Theorem 2. We also write CPDL or PDL with the obvious meaning. In the syntax above, Φ are sentences and E is the existential node quantifier. The universal node quantifier A σ is written ¬E ¬σ. Formulae σ are called node or state formulae and have one implicit free first-order variable, while formulae π are called path or program formulae and have two implicit free first-order variables, the endpoints of the path.

Semantics: Given a (Σ, Γ)-labeled graph G = (V, E, λ), we can write the semantics of the formulae. The semantics of a state formula σ is a set σ G ⊆ V , while the semantics of a path formula π is a binary relation π G ⊆ V 2 . Their definitions are mutually inductive. If the graph G is clear from the context, we omit subscripts and simply write σ and π .

The base cases for path formulae are

γ -→ = E γ and test{σ} = {(v, v) : v ∈ σ }.
The operations +, ∩, •, * correspond to rational expression notations, interpreted respectively as union, intersection, concatenation and Kleene star of the respective relations. Finally, the converse is defined by

π -1 = {(u, v) : (v, u) ∈ π }.
The base cases for state formulae are = V and p = {v ∈ V : p ∈ λ(v)}, where p ∈ Σ. Disjunction and negation correspond to union and complement. We let loop(π) consist of the vertices v ∈ E from which there is a loop following path π, i.e., such that (v, v) ∈ π . Similarly, we let π σ consist of the vertices u ∈ E from which it is possible to follow the path π and reach a vertex satisfying σ, i.e., (u, v) ∈ π for some v ∈ σ . We often write π instead of π . A sentence E σ states that there exists a vertex of G satisfying σ, i.e., G |= E σ if σ G = ∅. Disjunction and negation of sentences are as usual.

While ICPDL allows intersection, loop and converse, we also look at EQ-ICPDL where we allow existential quantification over new propositional variables in a similar spirit as in [START_REF] Laroussinie | Quantified CTL: expressiveness and complexity[END_REF]. Thus, formulae of EQ-ICPDL(Σ, Γ) have the form

Ψ = ∃p 1 , . . . , p n Φ where AP = {p 1 , . . . , p n } is disjoint from Σ and Φ ∈ ICPDL(Σ AP, Γ). The semantics is defined by G = (V, E, λ) |= ∃p 1 , . . . , p n Φ if there exists λ : V → 2 AP such that (G, λ ) = (V, E, λ ∪ λ ) |= Φ. For formulae Ψ in ICPDL(Σ, Γ) or EQ-ICPDL(Σ, Γ), we let L(Ψ) = {G ∈ G(Σ, Γ) : G |= Ψ}.
Example 1. We illustrate the semantics of ICPDL(Σ, Γ) using Figure 3. We have a node-and edge-labeled graph, with node labels Σ = {p, q, r, s} and edge labels Γ = {d, e, f, succ}. In path formulae, we simply write → instead of succ --→. The formula E (test{p ∨ q} • →) * r evaluates to true on the given graph: the leftmost node is a witness. Likewise, the formula

-→ • test{r} • f -→ • test{s} • d -→ -1 • c - → p is true, while E test{p} • d -→ r is not.
Satisfiability of propositional dynamic logic. The following definitions and results will be used in Section IV-C. Over arbitrary graphs, the satisfiability problem for PDL is undecidable. On the other hand, when we restrict to graphs of bounded tree-width, then the satisfiability problem becomes decidable with elementary complexity. We explain this now. Tree-width is a well-known measure for graphs [START_REF] Robertson | Graph minors. III. planar treewidth[END_REF]. We say that a labeled graph G = (V, E, λ) has tree-width k if the underlying unlabeled graph has tree-width k. We will not need the formal definition of tree-width in this paper, so it is omitted. We denote by G k (Σ, Γ) the graphs in G(Σ, Γ) having tree-width at most k.

Below is one of the main theorems that we use in this paper. It refers to the intersection width of an EQ-ICPDL formula, which is the maximum of the intersection widths of its path subformulae: the intersection width of path formulae is defined inductively by iw(

γ -→) = iw(test{σ}) = 1, iw(π 1 + π 2 ) = iw(π 1 • π 2 ) = max(iw(π 1 ), iw(π 2 )), iw(π -1 ) = iw(π * ) = iw(π), and iw(π 1 ∩ π 2 ) = iw(π 1 ) + iw(π 2 )
. Hence, a formula in LCPDL has intersection width 1.

Theorem 2 (Satisfiability). Given k ≥ 1 in unary and a formula Ψ in EQ-ICPDL(Σ, Γ) of intersection width bounded by a constant, checking whether

G |= Ψ for some G ∈ G k (Σ, Γ) can be solved in EXPTIME.
This is a consequence of a similar result over trees due to Göller, Lohrey and Lutz [START_REF] Göller | PDL with intersection and converse: satisfiability and infinite-state model checking[END_REF]Theorem 3.8]. Indeed, graphs of tree-width at most k can be represented by binary trees which are called k-terms. Moreover, for each formula

Ψ ∈ ICPDL(Σ, Γ) we can construct an ICPDL formula Ψ k of size O(k 2 |Ψ|) over k-terms such that, for all k-terms τ , we have τ |= Ψ k iff τ |= Ψ,
where τ is the graph denoted by the k-term τ [START_REF] Bollig | Non-sequential theory of distributed systems[END_REF]. Hence, satisfiability of Ψ over G k (Σ, Γ) is reduced to satisfiability of Ψ k over k-terms.

Graph interpretation and backward translation. [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF], [START_REF] Bollig | Non-sequential theory of distributed systems[END_REF]The following definitions and results will be used in Section IV-B. We consider two signatures (Σ, Γ) and (Σ , Γ ). Intuitively, a graph G ∈ G(Σ , Γ ) is interpreted in a graph G ∈ G(Σ, Γ) if we have formulae over the signature (Σ, Γ) which, when evaluated on G, express nodes, labels and edges of G . In this paper, we use CPDL interpretations, which means that the formulae for the interpretation are in CPDL(Σ, Γ). Also, we only need interpretation when the graphs G and G have the same set of nodes. In this simple case, an interpretation I is given by a tuple of state formulae (σ p ) p∈Σ and a tuple of path formulae (π γ ) p∈Γ , all in CPDL(Σ, Γ). Now, we say that a graph

G = (V, E , λ ) ∈ G(Σ , Γ ) is I-interpreted in the graph G = (V, E, λ) ∈ G(Σ, Γ) if, for all u, v ∈ V , all p ∈ Σ and all γ ∈ Γ , we have p ∈ λ (u) iff G, u |= σ p and (u, γ, v) ∈ E iff G, u, v |= π γ .
In this case, we write G = I(G).

Interpretations allow for a backward translation theorem: for each formula Ψ ∈ EQ-ICPDL(Σ , Γ ), we can construct a formula Ψ ∈ EQ-ICPDL(Σ, Γ) such that, for all graphs G ∈ G(Σ, Γ), we have

I(G) |= Ψ iff G |= Ψ.
The formula Ψ is obtained from Ψ by replacing the atomic state formulae p with σ p (for p ∈ Σ ) and the atomic path formulae γ -→ with π γ (for γ ∈ Γ ). Hence, Ψ and Ψ have same intersection width and

|Ψ| ≤ |Ψ | • max{|σ p |, |π γ | : p ∈ Σ , γ ∈ Γ }.

III. LOGICAL DEFINABILITY OF REALIZABILITY

Weighted graphs. We consider linear weighted graphs where node labels are irrelevant, i.e., Σ = ∅, and edges are labeled with constraints of the form < α or ≤ α, where α ∈ Z, i.e., Γ = {succ} ∪ ({<, ≤} × Z). Since node labels are irrelevant, a linear weighted graph is simply denoted G = (V, E). Often we use a maximal constant M ∈ N and let

Γ M = {succ} ∪ ({<, ≤} × {-(M -1), . . . , 0, . . . , M -1}). A graph G ∈ G(∅, Γ M ) is called M weight-bounded.
If we only compare using ≤, i.e., if there are no edges of the form (u, <, α, v), then we say that the graph is closed or a graph with closed constraints. Otherwise, we call it a mixed weighted graph or a graph with mixed constraints.

Realizability. One important property of interest, which is the focus of this paper, is realizability. The property of realizability asks whether the constraints defined by the weights can be satisfied in a manner that is consistent with the order. Definition 3. A weighted graph G is realizable if there exists a time-stamp map ts : V → R such that (i) all constraints are satisfied:

∀(u, , α, v) ∈ E, ts(v) -ts(u) α, and (ii) ts is monotone w.r.t. the linear order: ∀u, v ∈ V , if u v, then ts(u) ≤ ts(v).
If G is realizable via a map ts, then we say that ts is a realization of G. Note that the monotonicity could have been enforced by adding more constraint edges: when u ≺• v we could have added an edge (v, ≤, 0, u). With these extra constraints, realizability corresponds to checking the feasibility of the difference constraints. This is a classical problem on graphs which amounts to checking the absence of a negative cycle (see [START_REF] Cormen | Introduction to Algorithms[END_REF] for more details). There are many algorithms to solve this problem, e.g., the Bellman-Ford shortest path algorithm. Finally, as a quick aside, note that if we have reflexive edges (u, , α, u) ∈ E, checking realizability for these constraints is always vacuously true or false for all y := 0

x := 0 x > 2 3 ≤ y -x < 4 x := 0 1 < x ≤ 3 y -x ≤ 6 < -2 < 4 ≤ -3 ≤ 6 ≤ 3 < -1
Fig. 4: A realizable linear weighted graph obtained from a sequence of instructions of a timed system. x, y are realvalued variables called clocks. x := 0 (y := 0) denotes reset instructions. Changing the last instruction to x -y ≤ 5 gives a non-realizable weighted graph. The non-realizability follows from (i) there is a time elapse more than 5 between the first and third nodes, (ii) the time elapse is at most 5 between the first and fourth nodes, and (iii) time is monotone, hence there is at least zero time elapse between the third and fourth nodes. This gives a negative cycle between the first and fourth nodes.

possible time-stamps, and is easy. A realizable linear weighted graph obtained from a sequence of instructions of a timed system is depicted in Figure 4.

A. The first main result: logical definability of realizability

We are interested in properties of (possibly infinite) collections of such graphs, presented in a finite fashion. In particular, we wish to view graphs as being generated by an automaton, i.e., as behaviors of a system, and we wish to reason about this set of graphs. From this automata-theoretic viewpoint, a natural question to ask is whether the properties that we wish to reason about are definable in a certain logic. We focus on the specific property of realizability in weighted graphs and study its definability in EQ-ICPDL in our first main result below. In the next section, we will explain far-reaching consequences of our logical characterization, and in particular its application for checking emptiness of timed systems. Theorem 4. Realizability is EQ-ICPDL definable on the set of graphs G(∅, Γ M ). The size of the formula is polynomial in M and its intersection width is 2.

We prove the above theorem in two steps: in Subsection III-A1, we consider closed graphs and show that the logical definition is rather easy for them. Then, in Subsection III-A2, we consider graphs with mixed constraints.

Throughout the proof, given a linear weighted graph

G = (V, E) with |V | = n, we let V = {u 1 , . . . , u n } with u 1 ≺• u 2 ≺• • • • ≺• u n .
We start with a simple observation regarding the time-stamps witnessing realizability in weighted graphs. Given an M weight-bounded graph G = (V, E), a mapping ts :

V → R is said to be slowly monotone if 0 ≤ ts(v) - ts(u) ≤ M -1 for all u → v. Lemma 5. A graph G = (V, E) in G(∅, Γ M ) is realizable iff there is a slowly monotone map ts : V → R that realizes G.
Intuitively, if a realization of a graph G is not slowly monotone, then there must exist two consecutive points whose time-stamps are separated by more than M -1. But in this case there can be no forward edge (i.e., upper bound) that crosses this point, and hence the time difference between them can be reduced to any value larger than M -1 without affecting realizability. We detail this proof, via an induction, in [START_REF] Akshay | Timed systems through the lens of logic[END_REF].

Next, we have a crucial definition on general weighted graphs. Given an M weight-bounded linear graph G = (V, E), a time-stamping modulo M is a map tsm :

V → Z M = {0, . . . M -1}. For all u, v ∈ V , we set d tsm (u, v) = tsm(v) -tsm(u) mod M . Further, (u, v) is said to be tsm- big if there exist w 1 , w 2 ∈ V such that u w 1 ≺ w 2 v and d tsm (u, w 1 ) + d tsm (w 1 , w 2 ) ≥ M . Observe that, if v u, then (u, v) cannot be tsm-big. Definition 6. A time-stamping modulo M tsm is said to weakly satisfy G = (V, E) if for all e = (u, , α, v) ∈ E, (a) if u v, then (u, v) is not tsm-big and d tsm (u, v) ≤ α; (b) if v ≺ u then (v, u) is tsm-big or d tsm (v, u) ≥ -α.
Lemma 9 below shows that for linear weighted graphs, existence of such a map is a necessary condition for realizability. But first, we establish some useful facts. Recall that

V = {u 1 , . . . , u n } with u 1 ≺• u 2 ≺• • • • ≺• u n . For i ≤ j, we also define d + tsm (u i , u j ) = min{M, d tsm (u i , u i+1 ) + • • • + d tsm (u j-1 , u j )} and d + tsm (u j , u i ) = -d + tsm (u i , u j ). Notice that we have d + tsm (u i , u i ) = 0. Claim 7. Let G = (V, E) ∈ G(∅, Γ M ) and let ts : V → R be a slowly monotone map (which need not satisfy the constraints of G). Define tsm : V → Z M by tsm(v) = ts(v) mod M for all v ∈ V . Then, for all u, v ∈ V such that u v, we have d + tsm (u, v) = min{ ts(v) -ts(u) , M }. Furthermore, we have d + tsm (u, v) = M if (u, v) is tsm-big, and d + tsm (u, v) = d tsm (u, v) otherwise.
Given that |α| < M for all edges e = (u, , α, v) ∈ E, Claim 7 provides us with the following, alternative characterization of weak satisfiability. A formal proof of the above claim and of the lemma below can be found in [START_REF] Akshay | Timed systems through the lens of logic[END_REF].

Lemma 8. A time-stamping modulo M tsm weakly satisfies the graph G = (V, E) if and only if d + tsm (u, v) ≤ α for all (u, , α, v) ∈ E.
Now, we obtain one direction of the characterization, which works both for closed and open constraints.

Lemma 9. If G ∈ G(∅, Γ M )
is realizable, then there exists a time-stamping modulo M that weakly satisfies G.

Proof. Lemma 5 proves that there exists a slowly monotone time-stamping ts that satisfies the constraints G. We define tsm : V → Z M by tsm(v) = ts(v) mod M , and we show below that tsm weakly satisfies G.

Let (u, , α, v) ∈ E. By Lemma 8, it is enough to show that d + tsm (u, v) ≤ α. According to Claim 7, distinguishing the cases u v and v ≺ u, we show easily that

d + tsm (u, v) ≤ ts(v) -ts(u) or d + tsm (u, v) = -M . In the first case, it follows that d + tsm (u, v) ≤ ts(v) -ts(u) ≤ ts(v)-ts(u) < ts(v) -ts(u) + 1 ≤ α + 1,
and in the second case, we also

have d + tsm (u, v) = -M < α + 1. Hence, in both cases, we have d + tsm (u, v) < α + 1. Observing that d + tsm (u, v) and α are integers proves that d + tsm (u, v) ≤ α.
The converse of the above lemma does not hold with mixed guards and this will be handled in the next subsection. However, for closed guards it yields the following characterization.

1) Characterizing realizability in closed graphs: It remains to encode the characterization of Lemma 10 in EQ-ICPDL to obtain the logical definability of realizability for linear weighted graphs.

Lemma 10. A closed graph G = (V, E) in G(∅, Γ M ) is realizable iff
EQ-LCPDL characterization: We use existential quantification over atomic propositions p 0 , . . . , p M -1 to guess the timestamping modulo M . Intuitively, a node satisfies p i iff its tsm value is i. So we define the formula ∃p 0 , . . . , p M -1 Partition∧ Forward ∧ Backward where the auxiliary formulae are defined in Table I. The formula Partition states that every vertex satisfies exactly one p i (0 ≤ i < M ).

For 0 ≤ i, j < M , let δ M (i, j) = (j -i) mod M . We use a path formula to characterize pairs of vertices that are tsm-big: a pair (u, v) is tsm-big iff we can go from node u to node v following the path formula BigPath.

Since negation is not allowed at the level of path formulae, we provide another formula, SmallPath, to express that a pair (u, v) of vertices is not tsm-big. There are two cases, depending on whether tsm(u) ≤ tsm(v) or not. In both cases, (u, v) |= SmallPath i,j iff u v, (u, v) is not tsm-big, i = tsm(u) and j = tsm(v).

Formulae Forward and Backward respectively state the two conditions in Definition 6. The constraint on -forward edges is stated using the loop operator of LCPDL. By excluding the existence of a loop following the path BigPath

• ≤α --→ -1
we make sure that forward edges (u, v) ∈ E ≤α are not tsmbig. Now, to ensure that forward edges (u, , α, v) satisfy d tsm (u, v) ≤ α, we exclude the existence of a path violating this property, i.e., a loop following

test{p i } • ≤α --→ • test{p j } • (→ -1 ) + with δ M (i, j) > α.
2) A characterization with mixed guards: The characterization above is not sufficient when some of the constraints are strict, i.e., E contains edges of the form (u, <, α, v). It turns

Partition = A 0≤i<M [p i ∧ j =i ¬p j ] BigPath = 0≤i,j,k<M δ M (i,j)+δ M (j,k)≥M test{p i } • → + • test{p j } • → + • test{p k } • → * SmallPath i,j = test{p i } • i≤k≤ ≤j test{p k } • → • test{p } * • test{p j } if i ≤ j SmallPath i,j = 0≤ ≤j<i≤k<M SmallPath i,k • → • SmallPath ,j if j < i Forward = ¬E -M <α<M loop(BigPath • ≤α --→ -1 ) ∧ ¬E 0≤i,j<M δ M (i,j)>α loop(test{p i } • ≤α --→ • test{p j } • (→ -1 ) + ) Backward = ¬E -M <α<M 0≤i,j<M δ M (i,j)<-α loop(SmallPath i,j • ≤α --→)
TABLE I: LCPDL for realizability of linear closed graphs out that we need an additional condition to make sure that the fractional parts do not violate the realizability.

Definition 11. Given a graph G = (V, E) and a time-stamping tsm : V → Z M modulo M , we define two binary relations geq Fr and gt Fr on V :

• (u, v) ∈ geq Fr iff one of the following conditions hold:

1) u ≺ v, (u, v) is not tsm-big and d tsm (u, v) = α for some edge (u, , α, v) ∈ E; 2) v ≺ u, (v, u) is not tsm-big and d tsm (v, u) = -α for some edge (u, , α, v) ∈ E; 3) v ≺• u and d tsm (u, v) = 0.
• (u, v) ∈ gt Fr iff one of the following conditions hold:

1) u ≺ v, (u, v) is not tsm-big and d tsm (u, v) = α for some edge (u, <, α, v) ∈ E; 2) v ≺ u, (v, u) is not tsm-big and d tsm (v, u) = -α for some edge (u, <, α, v) ∈ E.

Notice that gt Fr ⊆ geq Fr . The idea is that these relations give the ordering between the fractional parts. Thus, (u, v) ∈ geq Fr (resp. gt Fr ) means that the fractional part of ts(u) must be at least (resp. strictly greater than) the fractional part of ts(v). Once again, since |α| < M for all edges (u, , α, v) ∈ E, Claim 7 provides an alternative characterization of the relations geq Fr and gt Fr .

Lemma 12. Consider graph G = (V, E), tsm : V → Z M modulo M and a pair (u, v) of vertices of G. Then, • (u, v) ∈ geq Fr iff there exists an edge (u, , α, v) ∈ E such that d + tsm (u, v) = α, or if v ≺• u and d + tsm (u, v) = 0; • (u, v) ∈ gt Fr iff there exists an edge (u, <, α, v) ∈ E such that d + tsm (u, v) = α.
Lemma 13. Let G = (V, E) be an M weight-bounded graph with a linear order and mixed constraints. G is realizable iff there exists a time-stamping modulo M tsm such that (i) tsm weakly satisfies G and (ii) there do not exist u, v ∈ V such that (u, v) ∈ gt Fr and (v, u) ∈ geq Fr * , where geq Fr * is the reflexive transitive closure of geq Fr .

Proof. In the forward direction, let G be realizable. Let ts : V → R be a slowly monotone map that realizes G, and let tsm be the time-stamping modulo M defined by tsm : v → ts(v) mod M . Lemma 9 proves that tsm weakly realizes G. We further claim that, if (u, v) ∈ geq Fr , then {ts(u)} ≥ {ts(v)}, and that, if (u, v) ∈ gt Fr , then {ts(u)} > {ts(v)}. The proof is as follows.

• If (u, v) ∈ geq Fr because v ≺• u and d + tsm (u, v) = 0, then ts(v) ≤ ts(u) and 0 = d + tsm (u, v) = min{ ts(v)ts(u) , -M }. Hence, ts(u) = ts(v) , and therefore {ts(v)} ≤ {ts(u)}.

• If (u, v) ∈ geq Fr because there exists an edge (u, , α, v)

∈ E such that d + tsm (u, v) = α, then -M < α = d + tsm (u, v) < M , and Claim 7 proves that α = d + tsm (u, v) = ts(v) -ts(u) . It follows that {ts(v)} = ts(v)-ts(v) ≤ ts(u)+α-ts(v) = ts(u)-ts(u) = {ts(u)}. • If (u, v) ∈ gt Fr , then the same argument proves that α = d + tsm (u, v) = ts(v) -ts(u)
, and it follows that

{ts(v)} = ts(v) -ts(v) < ts(u) + α -ts(v) = ts(u) -ts(u) = {ts(u)}.
In the reverse direction, let tsm : V → Z M be a timestamping modulo M that weakly satisfies G and such that (ii) holds. As a direct consequence of (ii), every path in the graph G geq Fr = (V, geq Fr ) contains at most |V | edges in gt Fr . Indeed, otherwize two such edges would start from the same vertex, so that one edge would belong to a cycle of G geq Fr . Hence, for every vertex v ∈ V , we define the integer ts 1 (v) as the largest number of edges in gt Fr that may be used by a path in G geq Fr starting from v: observe that 0 ≤ ts 1 (v) ≤ |V |.

By construction, for every pair (u, v) in geq Fr , we have ts 1 (u) ≥ ts 1 (v), and we even have ts 1 (u) > ts 1 (v) if (u, v) ∈ gt Fr . Then, consider the map ts 0 : V → N defined inductively by ts 0 (u 1 ) = 0 and ts 0 (u i+1 ) = ts 0 (u i ) + d tsm (u i , u i+1 ). The proof of Lemma 10 shows that ts 0 is a slowly monotone map and that ts 0 (v) -ts 0 (u) ≤ α for all edges (u, , α, v) ∈ E.

We prove now that the map ts : V → R defined by ts(v) = ts 0 (v) + ts 1 (v)/(|V | + 1) is monotone. For all pairs (u, v),

• if u ≺• v and (v, u) ∈ geq Fr , then ts(v) = ts 0 (v) + ts 1 (v)/(|V | + 1) ≥ ts 1 (u) + ts 1 (u)/(|V | + 1) ≥ ts(u), because ts 0 (v) ≥ ts 0 (u) and ts 1 (v) ≥ ts 1 (u); • if u ≺• v and (v, u) / ∈ geq Fr , then d + tsm (v, u) = 0, and therefore d + tsm (u, v) ≥ 1, which proves that ts(v) ≥ ts 0 (v) = ts 0 (u) + d + tsm (u) ≥ ts 0 (u) + 1 > ts 0 (u) + ts 1 (u)/(|V | + 1) = ts(u).
Then, we prove that ts satisfies the constraints of G. Indeed, for every edge (u, , α, v) ∈ E,

• if d + tsm (u, v) = α, then (u, v) ∈ geq Fr , and therefore ts 1 (v) ≤ ts 1 (u); it follows that ts(v) = ts 0 (v) + ts 1 (v)/(|V | + 1) ≤ ts 0 (u) + α + ts 1 (u)/(|V | + 1) = ts(u) + α; • if d + tsm (u, v) = α and, furthermore, = <, then (u, v) ∈ gt Fr , hence ts 1 (v) < ts 1 (u); it follows that geq Fr = ( ≤α --→ + <α --→) ∩ 0≤i,j<M δ M (i,j)=α SmallPath i,j + 0≤i,j<M δ M (j,i)=-α SmallPath -1 j,i + i<M test{p i } • → -1 • test{p i } gt Fr = <α --→ ∩ 0≤i,j<M δ M (i,j)=α SmallPath i,j + 0≤i,j<M δ M (j,i)=-α SmallPath -1 j,i
ts(v) = ts 0 (v) + ts 1 (v)/(|V | + 1) < ts 0 (u) + α + ts 1 (u)/(|V | + 1) = ts(u) + α; • if d + tsm (u, v) = α, then d + tsm (u, v) ≤ α -1, since tsm weakly satisfies G; it follows that ts(v) = ts 0 (v) + ts 1 (v)/(|V | + 1) < ts 0 (v) + 1 ≤ ts 0 (u) + (α -1) + 1 ≤ ts(u) + α.
Consequently, in all cases, we have ts(v) -ts(u) α, which completes the proof.

EQ-ICPDL characterization: As before, we use existentially quantified propositional variables p 0 , . . . , p M -1 to guess the tsm values. To state weak-realizability, we use the formula WRealizable = Partition ∧ Forward ∧ Backward where the subformulae have been defined in Table I. In addition, we have to check the absence of a cycle among the fractional parts, which contains at least one strict inequality and other, possibly non-strict, inequalities. By Lemma 13, this suffices to ensure realizability. To capture the ordering among the fractional parts, we use two EQ-ICPDL formulae, gt Fr and geq Fr respectively for the strict and non-strict parts, formally defined in Table II. The EQ-ICPDL formula Realizable is then:

∃p 0 , . . . p M -1 WRealizable ∧ ¬E loop(gt Fr • geq Fr * )
The intersection width of gt Fr and geq Fr is 2. Hence, the intersection width of Realizable is also 2. This completes the proof of Theorem 4.

B. Realizability is beyond logical definability in general

Above, we have seen the EQ-ICPDL definability of realizability for linear weighted graphs. In the absence of a linear order, this is no longer true, even if one uses the strictly more expressive MSO logic (an easy example is the property of connectivity which separates EQ-ICPDL from MSO). Theorem 14. The property of realizability is not definable in MSO for weighted graphs without the linear order.

We sketch the proof idea here, and leave the technical details to [START_REF] Akshay | Timed systems through the lens of logic[END_REF]. We consider a family of word structures over {a, b} of the form a * b * and define an MSO transduction that gives rise to a family of weighted graphs. For a word a n b m in the domain, the transduction gives rise to a weighted graph with n + m nodes, with edges from nodes i to i + 1 (with 1 ≤ i ≤ n -1) having weight 1, and edges from node i to i + 1 (with n + 1 ≤ i ≤ n + m -1) having weight -1. Edges of weight 0 go from the node n to the node n + 1, and from the node n+m to the node 1. The constructed weighted graph has width 2, and it is realizable iff n ≥ m. If realizability were MSOdefinable, then using backwards translation theorem [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF], one would obtain a regular language as the pre-image of those realizable graphs. This is not the case with {a n b m : n ≥ m}.

IV. ANALYZING TIMED SYSTEMS WITH DATA STRUCTURES

In this section, we develop a generic technique to analyze timed systems with auxiliary data structures. We start with untimed systems with data structures.

A. Capturing data structure operations as graphs

Let us fix a finite set of data structures DS. Each data structure d ∈ DS can be operated via two instructions, either a write that writes to the data structure, denoted w(d), or a read instruction that reads from the data structure, denoted r(d). The set of instructions from DS is denoted Σ DS = {r(d), w(d) : d ∈ DS} ∪ {nop}, where nop is a special operation that does not access the data-structures. For simplicity and ease of exposition, we restrict each d ∈ DS to be a stack or a queue. However, the approach described here can be adapted to other structures (such as bags) with minor modifications. When d ∈ DS is a stack, r(d) is the pop operation and w(d) is the push operation on stack d. Similarly, if d is a queue, r(d) is the dequeue operation, while w(d) is the enqueue operation on queue d.

A sequence of operations from Σ DS abstracts a run of a system with these data structures. We can then define the system as a generator of (possibly infinitely many) sequences of operations. The mechanism for generating this sequence of operations can be some machine (an automaton), or can be specified by regular expressions. We do not dwell on this detail here, and instead define a system S with data structures as a regular language of sequences of operations over Σ DS . Without loss of generality, we assume that all sequences will start with nop. It is easy to see that standard models such as (multi)pushdown automata, (multi)queue automata, multiset automata and so on generate regular languages of sequences of such operations.

A sequence σ of operations over Σ DS is said to be valid if, for every prefix σ of σ and for every data structure d ∈ DS, the number of reads r(d) in σ is at most the number of writes w(d) in σ , and the number of reads and writes in σ are equal. For a system S, we are only interested in valid sequences generated by S, and we denote this set by L(S). For instance, a valid behavior of a pushdown system cannot read/pop from a stack before writing/pushing to it. Let Γ DS = DS ∪ {succ}. We associate, to any valid sequence σ of operations over Σ DS , a (Σ DS , Γ DS ) linear graph G σ . Definition 15. Let σ = σ 1 . . . σ n be a valid sequence of operations over Σ DS . We define its (Σ DS , Γ DS )-graph as G σ = (V, E, λ), where V = {1, . . . n} and 1) for 1 ≤ i ≤ n, λ(i) = {σ i }, and, for 1≤i<n, i succ --→ i+1, 2) σ i = w(d) (r(d)) iff there is an outgoing (incoming) edge in E labeled d from (to) i. 3) for each stack (queue) d, edges labeled d satisfy the LIFO (FIFO) property.

As an example, let σ be a sequence of operations from DS = {d 1 , d 2 }, where d 1 is a stack and d 2 is a queue. The graph G σ corresponding to σ is depicted in Figure 1, where the node labels are exactly the singleton sets of operations w(d) and r(d), for d ∈ {d 1 , d 2 }. We remark that this graph depends crucially on the interpretation of the data structure, as a stack or a queue. Notice that the edges labeled d 1 respect the stack discipline (well-nesting), while the edges labeled d 2 respect FIFO. For a fixed DS, we assume the interpretation of each data structure to be fixed and simply write G σ .

Given a (Σ, Γ DS )-graph G = (V, E, λ), we define its projection π(G) as the (∅, Γ DS )-graph obtained by removing the node labels: π(G) = (V, E).

Theorem 16 ([11]). Let S be a system with data structures from DS. We can construct an EQ-LCPDL(∅, Γ DS ) formula ψ S such that, for all

(∅, Γ DS )-graphs G, G |= ψ S iff G = π(G σ ) for some σ ∈ L(S).
The classical non-emptiness problem for a system S with data structures can be formulated as whether L(S) = ∅.

Corollary 17. For system S, ψ S is satisfiable iff L(S) = ∅. This corollary, along with Theorem 2, and using known bounds on tree-width, provides a "uniform" proof for the decidability of checking non-emptiness for a variety of untimed systems including (multi)pushdown and (multi)queue systems with bounded contexts, scope, or phases in a sequential setting. In many cases, the complexity obtained matches the best known bounds. We extend this approach uniformly to timed systems, using the realizability proof of Section III.

B. Combining timing and data structures

While combining time constraints and data structures, we cannot directly rely on the formula for realizability from Section III in the approach outlined above. The vocabulary of graphs obtained from systems having time constraints and data structures might differ from the (weighted) (∅, Γ M )-graphs of Section III and the (unweighted) (Σ, Γ DS )-graphs above, where Σ = ∅ or Σ = Σ DS . The crucial observation is that, for a large class of timing constraints and data structures that we are interested in, it turns out that the former weighted graphs can be interpreted in the latter unweighted graphs, paving the way to extend the approach for systems having both time constraints and data structures. We now detail this intuition.

1) Timing instructions: In a timed system with data structures, the sequence of instructions generated by the system includes (i) checking time constraints on clocks (encoded as operations on clocks), (ii) checking time constraints on data structures, and (iii) mixing operations on clocks and data structures. Recall that we already have a fixed set of data structures DS consisting of stacks and queues. To be concrete, we also fix a representative set of timing features.

We fix a finite set Clocks of real-valued "clock" variables and a maximal constant M ∈ N. We also fix notations ∈ {≤, <, =, >, ≥}, β ∈ [0, M ) ∩ N and use letters x, y, x 1 , . . . for clock variables. Atomic timing instructions are as follows:

1) for x ∈ Clocks, x:=0 represents clock resets, while x β represent guards or clock constraints; 2) for d ∈ DS, d β represents an age constraint checking the "age" of the message read; 3) for d ∈ DS and x, y ∈ Clocks, (x -y) β, (d -x) β and (x-d) β represent diagonal constraints. The latter two capture mixing clock variables and data structures. Thus, we define a set of instructions Σ DS Clocks which contains Σ DS with the atomic timing instructions described above. Without loss of generality, we only consider sequences of instruction sets (also called sequences of instructions for simplicity) from Σ DS Clocks starting with the set {nop}∪{x:= 0 : x ∈ Clocks}, i.e., which resets all clocks at start-up. A sequence τ of such instructions is shown in Figure 2. We associate to every such sequence τ a sequence of untimed instructions σ τ , obtained by ignoring the atomic timing instructions. Now we say τ is valid if σ τ is valid. Then, for every valid τ , we can immediately associate a (Σ DS Clocks , Γ DS )labeled linear graph G τ by considering G στ and enriching its node labels with the timing instructions.

We define a timed system with data structures T as a regular language of sequences of instructions over Σ DS Clocks . It is easy to see that classical models, such as timed automata, (multistack) timed pushdown automata or timed automata with gap order constraints, can be modeled in this formalism. The set of valid sequences generated by T is denoted L(T ). Now, a valid sequence of instructions τ = τ 1 . . . τ n over Σ DS Clocks is said to be timed feasible or just feasible if there exists a time-stamping ts : {1, . . . , n} → R ≥0 such that all timing constraints engendered by the timing instructions are satisfied. That is, for ∈ {≤, <, =, >, ≥} and β ∈ N: (C 1 ) For every guard of the form x β at position i, if the last reset instruction of the clock x in τ before i was at position j, then ts(i) -ts(j) β. (C 2 ) For every age constraint of the form d β at position i,

we have an edge j d -→ i in G τ (which implies w(d) ∈ λ(j) and r(d) ∈ λ(i)), and ts(i) -ts(j) β. (C 3 ) For every diagonal constraint of the form x -y β at position i, if j and k are the last resets of clocks x and y respectively, then ts(k) -ts(j) β. (C 4 ) We can similarly define diagonal constraints between clocks and data structures. Thus, the non-emptiness problem for the timed system T is to check whether there exists a feasible τ ∈ L(T ).

2) From timing instructions to weighted graphs: We reduce checking non-emptiness of T to checking satisfiability of an EQ-ICPDL formula over (Σ DS Clocks , Γ DS )-graphs. Towards this, we first define the weighted graph G τ corresponding to a valid sequence of instructions τ of T in a natural manner. We extend from Section III, where all timing instructions were simply clock constraints and resets of clocks i.e., corresponding to (C 1 ) and (C 3 ) above. In Figure 2, the check of x = 0 on node 2 gives two bidirectional weighted edges in the weighted graph G τ depicted on the right, between the last reset point of x and node 2. Similarly, instruction y ≤ 1 at node 4 gives rise to the forward edge labeled ≤ 1 between last reset of y and node 4.

For diagonal constraints (C 3 ), the edge obtained is between the last reset points. E.g, y -x < 6 at node 9 yields the weighted edge from node 3 to node 6 (last resets of clocks y and x).

This construction easily lifts to (C 2 ) and (C 4 ) as well. For (C 2 ), we just observe that each age constraint engenders edges between the source write and target read of that data structure edge. E.g., in Figure 2, the age constraint 4 < d ≤ 5 at node 8 yields two weighted edges between the source of the data structure edge, i.e., node 4 and target, node 8. The upper bound is captured by the forward edge while the lower bound by the backward edge. Similarly the constraint 2 < d -y at node 5 yields the backward edge from node 3 (the last reset of clock y) to node 2 (the source of the data structure edge reaching node 5) labeled < -2 (as it is a lower bound constraint).

The main property about the weighted graph is that it captures feasibility of a sequence of instructions as realizability.

Lemma 18. A valid sequence of instructions τ over Σ DS Clocks is feasible iff G τ is realizable.

3) Interpreting weighted graphs in unweighted graphs: From the above discussion, given a timed system T , for each valid τ of T , we have a weighted graph G τ . A significant contribution of this paper, of possible independent interest, is the following proposition which relates these weighted graphs with unweighted (Σ DS Clocks , Γ DS )-graphs obtained from τ . Proposition 19 allows us to logically interpret weighted graphs into unweighted ones and, therefore, to decouple the data structure and process edges from the timing constraints.

Proposition 19. Let τ be a valid sequence of instructions over Σ DS Clocks . Then the weighted graph G τ can be CPDL-interpreted in the (Σ DS Clocks , Γ DS )-graph G τ . Proof. Given a valid sequence of instructions τ over Σ DS Clocks , let M be the maximal constant appearing in these instructions. We saw in the previous subsection that the weighted graph G τ = (V, E) has successor edges, and weighted edges arising from constraints of type (C 1 -C 4 ). First, we observe that successor edges in G τ are already present as successor edges in G τ . For weighted edges, let ∈ {<, ≤}, and c ∈ [0, M ) ∩ N. We assume that equality constraints such as x = c have been replaced by the conjunction of x ≤ c and c ≤ x. For a clock x ∈ Clocks, we define the path formula

Reset x = → -1 • (test{¬(x := 0)} • → -1 ) * • test{(x := 0)}
which moves backwards along successor edges up to the last reset of clock x. Then, towards the interpretation of forward edges weighted with c, we define the path formula Π c as

x∈Clocks Reset -1 x • test{x c} (C 1 ) + d∈DS d -→ •test{d c} (C 2 ) + x,y∈Clocks Reset -1 x • test{x -y c} • Reset y (C 3 ) + x∈Clocks d∈DS Reset -1 x • test{x -d c}• d -→ -1 (C 4 ) + d -→ •test{d -x c} • Reset x
Then, for all u, v ∈ V and c > 0 (we will discuss the case c = 0 below), we have

(u, , c, v) ∈ E iff (G τ , u, v) |= Π c .
The four types of upper constraints defined in (C 1 -C 4 ) are described by the respective path formulae (C 1 -C 4 ) in Π c . As an example, if we refer to the i th node of G τ (and G τ ) as u i in Figure 2, we have the edge

(u 3 , , 6, u 6 ) in G τ because (G τ , u 3 , u 6 ) |= Reset -1 y • test{y -x 6} • Reset x . Similarly, the edge (u 6 , <, 3, u 7 ) is present in G τ since (G τ , u 6 , u 7 ) |= Reset -1 x • test{x -d < 3}• d -→ -1 . Notice that in Reset x , we
walk backward to the first node labeled x := 0, while, in C 2 and C 4 , for checking the age of a data structure, it is sufficient to check the existence of a data structure backward edge from the point where the age is checked.

Similarly, towards the interpretation of backward edges weighted with -c, we define the path formula Π -c as

x∈Clocks test{c x} • Reset x (C 1 ) + d∈DS test{c d}• d -→ -1 (C 2 ) + x,y∈Clocks Reset -1 y • test{c x -y} • Reset x (C 3 ) + x∈Clocks d∈DS Reset -1 x • test{c d -x}• d -→ -1 (C 4 ) + d -→ •test{c x -d} • Reset x
Then, for all u, v ∈ V and c > 0, we have

(u, , -c, v) ∈ E iff (G τ , u, v) |= Π -c
. Again, the four types of lower constraints defined in (C 1 -C 4 ) are described by the respective path formulae (C 1 -C 4 ) in Π -c . Now, when c = 0, an edge weighted 0 may arise from an upper constraint such has x 0 or a lower constraint such as 0 x. Therefore, for all u, v ∈ V , we have (u, , 0, v)

∈ E iff (G τ , u, v) |= Π 0 + Π -0 .
The size of Π α is O(|Clocks| 2 + |DS| + |Clocks||DS|).

Thus we have described how each edge of the weighted graph G τ can be interpreted in the (Σ DS Clocks , Γ DS )-graph G τ by an CPDL-formula, of size O(|Clocks| 2 +|DS|+|Clocks||DS|), which completes the proof of this proposition. Thus, any formula over weighted graphs can be translated into an "equivalent" formula over (Σ DS Clocks , Γ DS )-graphs: Corollary 20. Given a formula ψ ∈ EQ-ICPDL(∅, Γ M ), we can construct ψ ∈ EQ-ICPDL(Σ DS Clocks , Γ DS ) such that, for all valid sequences of instructions τ over Σ DS Clocks , we have

G τ |= ψ iff G τ |= ψ . The size of ψ is O((|Clocks| 2 + |DS| + |Clocks||DS|)|ψ|)
and its intersection width is same as ψ.

4) Reducing emptiness of T to satisfiability of EQ-ICPDL: From Theorem 4, we know that there exists a formula capturing realizability on weighted graphs, with signature (∅, Γ M ). Combining with Corollary 20 gives us the second main theorem of the paper regarding logical characterization of emptiness checking in timed systems with data structures.

Theorem 21 (Logical characterization of a timed system). Given a timed system with data structures T , we can construct a formula Ψ T ∈ EQ-ICPDL(∅, Γ DS ) such that for all (∅, Γ DS ) linear graphs G, we have G |= Ψ T iff G = π(G τ ) for some feasible τ ∈ L(T ). The size of Ψ T is polynomial in the size of T and its intersection width is 2.

Proof sketch. By Theorem 4, we can construct a formula Realizable in EQ-ICPDL(∅, Γ M ) that captures realizability over weighted graphs G(∅, Γ M ). By Corollary 20, we obtain a formula ψ real ∈ EQ-ICPDL(∅, Γ DS ) such that, for all τ ∈ L(T ), G τ |= ψ real iff G τ |= Realizable. In fact, ψ real is simply obtained from Realizable by replacing every reference to a weighted edge in the formula by its logical interpretation in G τ . Now, by definition of EQ-ICPDL, we have ψ real = ∃p 1 . . . p r ψ for some ψ ∈ ICPDL({p 1 , . . . p r }, Γ DS ).

Next, recall that a timed system T is a regular language of sequences of timed instructions. We consider the automaton that describes this regular collection, denoted by A = (Q, i, F, ∆) with Q the set of states, i the initial state and F the final states and ∆ the transition function. Then, the accepted sequences of instructions can be captured in EQ-LCPDL, by guessing the states visited along an accepting run, and by checking that consecutive states have a transition between them and start from initial and end at final state.

Set Σ = Σ DS Clocks ∪ Q = {q 1 , . . . , q n }. There exists a formula ξ = ∃q 1 . . . q n ξ , with ξ ∈ LCPDL(Σ, Γ DS ), such that, for all (∅, Γ DS )-graphs G, we have G |= ξ iff G = π(G τ ) for some sequence τ ∈ L(T ). Combining this with the formula above, and define ψ T = ∃p 1 . . . p r , q 1 , . . . q n (ξ ∧ ψ ). Then we have for any (∅, Γ DS )-graph G, G |= ψ T iff G = π(G τ ) for some τ ∈ L(T ) and τ is feasible, which completes the proof.

C. Application: deciding emptiness

While we have reduced checking emptiness of timed systems to checking satisfiability of a formula in EQ-ICPDL, this does not immediately give decidability results. This is obvious since systems with multiple data structures (such as stacks or even single queue) are all Turing powerful, even without any timing features. To obtain decidability, one often considers under-approximations, for which we essentially restrict the class of graphs that are considered as behaviors. As mentioned in the preliminaries, graphs of bounded tree-width form a large family of graphs where we regain decidability thanks to Theorem 2. Recall that G k denotes graphs of tree-width at most k. Combining Theorems 2 and 21, we have the following corollary about decidability in timed systems.

Corollary 22 (Underapproximations.). Let k ∈ N. Let S be a timed system with data structures that uses clocks from Clocks and has maximum constant M ∈ N. We can check whether there exists a feasible τ ∈ L(S) such that G τ ∈ G k (∅, Γ DS ) in time 2 poly(k,M,|Clocks|,|DS|) × |S| poly(k,|DS|) . Thus, if the set {G τ : τ ∈ L(S)} has a bounded treewidth, we obtain the same complexity bounds for checking emptiness of S. As concrete applications, the following models of timed systems all fall in this category of having bounded tree-width, hence we obtain decidability (and efficient algo- rithms) for checking emptiness: timed automata [START_REF] Alur | A theory of timed automata[END_REF], densetimed pushdown automata with a single stack [START_REF] Abdulla | Dense-timed pushdown automata[END_REF], multi-stack dense-timed pushdown automata with bounded rounds [START_REF] Akshay | Analyzing timed systems using tree automata[END_REF].

In fact, the complexity obtained for dense-timed pushdown automata with a single stack is even optimal. In addition, by this technique, we also have the following (new, to the best of our knowledge) results on the decidability of the emptiness problem for multi-stack dense-timed pushdown automata with (i) bounded contexts (the tree-width of graphs in the case of p-bounded context systems is ≤ p + 1 [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF]), (ii) bounded phase (the tree-width of graphs in the case of p-bounded phase systems is ≤ 2 p+1 [22]), and (iii) bounded scope (the tree-width of graphs in the case of p-bounded scope is ≤ 2(p + 2) [START_REF] Cyriac | MSO decidability of multipushdown systems via split-width[END_REF]). Further, if one considers timed automata with b-bounded channels (a b-bounded channel is one where the number of unread messages is bounded by b ∈ N at any point of time), then the (∅, Γ DS )-graphs have a tree-width ≤ b + 2 [START_REF] Bollig | Non-sequential theory of distributed systems[END_REF]. We expect that many other data structures and various novel combinations (e.g., any combination of the above with multiple stacks and queues) can be handled using our technique, and leave these as routine exercises.

V. EXTENSIONS

A. Extending time features -a generic template

We develop a two-step template to add new timing features to our approach above. Step 1 consists in expressing the edges engendered by the new feature in the weighted graph and Step 2 consists in writing a formula in LCPDL to capture this new edge relation. If we can accomplish these steps, then our theorems lift to the setting with these new timing features.

This highlights the robustness of our approach, since we are able to easily and uniformly handle these extra features. That apart, this template is interesting even for timing features which can be simulated by ordinary clocks. A classical instance of this are diagonal guards in timed automata, which do not add expressiveness. Indeed, eliminating diagonal guards incurs an exponential blow-up in the worst-case [START_REF] Bouyer | On conciseness of extensions of timed automata[END_REF]. This is avoided in our approach by directly expressing their edges in the weighted graph as in Equation C 4 .

1) Event clocks: Let us illustrate this template in action via another example of a well-studied model, namely, event predicting clocks [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF], [START_REF] Geeraerts | On regions and zones for event-clock automata[END_REF], which can be simulated by ordinary (non-deterministic) timed automata. We fix a set AP of atomic propositions (events) arising from the system. An event-predicting timing instruction next a α, for a ∈ AP, ∈ {≤, <, >, ≥} and α ∈ [0, M ) ∩ N, entails a constraint between the current point (call it u) and the point at which node label a occurs next (call it v). Consistently with the notations on timing constraints C 1 -C 4 , in section IV-B1, we call this constraint C 5 . Now, Step 1 is that this can be expressed in the weighted graph as an edge between these two vertices u and v. For Step 2, it is easy to write the PDL formula that allows to interpret these edges of the weighted graph as edges in the Γ DS -graph. Specifically, we just have to add to the path formula Π α in proof of Proposition 19 the following term:

a∈AP test{(next a α)}• → •(test{¬a}• →) * • test{a} (C 5 )
We proceed similarly for the path formula Π -α . It is not difficult to see that we can define similar formulae to capture event recording clocks as well.

2) Clock renaming via tracking: While event clocks are relatively straightforward, for some other timing features, it is not easy to figure out, from the timing instruction, what edges in the weighted graph must be added. This happens for instance in clock renaming: if we assign to x the value of clock y and then check it later with x ≤ α, the edge to be added is from the last reset of y to the point of checking the constraint. This is the case even if y has been reset in between after the assignment. Figure 5 illustrates this.

We consider a generic class of (deterministic) clock renaming in timed systems. These are a special case of clock updates, again a classical notion in timed automata [START_REF] Bouyer | Updatable timed automata[END_REF], [START_REF] Bouyer | On conciseness of extensions of timed automata[END_REF], but have not been studied much for timed systems with single or multiple data structures such as stacks and queues. We divide the features we consider into 4 classes: (i) the usual reset of a clock x to 0 (x := 0), (ii) assigning to clock x the value of clock x (x := x ), (iii) assigning to clock x the value associated to data structure d ∈ DS, while reading from d (x := d), (iv) writing to d ∈ DS the value of clock x (d := x).

Note that renamings (iii) and (iv), combined with the age and diagonal constraints on data structures, give us a very rich and expressive class of timed systems. This allows us to consider timed systems where we can write to some d 1 ∈ DS the value of a clock x 1 , then read from d 1 this value (which changes with passage of time) into a clock x 2 , write this value of x 2 to some d 2 ∈ DS, and retrieve the value (after some time elapse) into a clock x 4 . This value in x 4 can then be checked with the value read from some d 4 ∈ DS, or with a clock x 5 , or with a constant α. In such a sequence, the clock x 1 has come a long way at this time of checking, and we need to track it, to ensure that the time elapse we are looking at happens from the last reset of x 1 before it was written to d 1 . See Figure 5, where the value of clock x 1 flows through d 1 , x 2 , d 2 and finally x 4 , from where it is checked. Likewise, the value of clock x 2 flows through clocks x 4 , x 3 , and is checked at x 3 . Now, x 2 is reset after it flows into x 4 ; however, when checking x 3 , we use the reset of x 2 before x 2 flowed inside x 4 .

Inferring such constraints requires us to follow and track the clock reset back to the original event. Rather than writing a formula in CPDL, we find it easier to describe an automaton which "walks" in the graph and performs this tracking. This enables us to express the weighted edges engendered by the constraints using the accepting paths of the automaton. This essentially handles the Step 1 we mentioned earlier. To handle Step 2, which is the logical definability, we write CPDL formulae whose paths π use this automaton. This allows us to interpret the weighted edges.

Formally, we construct an automaton A with set of states Q = {q x : x ∈ Clocks}. A run of A starting from some state q x will track the name of the clock whose value originates from x. Without loss of generality, we assume that each transition of the timed system T contains exactly one update for each clock, which could be of the form x := 0 (reset), x := x (deterministic clock update, we use x := x if the clock is unchanged), x := d (x is updated with the value read from d ∈ DS), or d := x. There are two types of transitions:

• (clock update): if there is an update x := x then we have a transition q x test{x :=x}•→ ---------→ q x , • (DS update): if there is an update x := d for some d ∈ DS, then for all clocks x, we have a transition q x test{d:=x}• d -→•test{x :=d} ----------------→ q x . This corresponds to writing the value of clock x to some d ∈ DS, and, at the time of reading from d ∈ DS, assign this value to a clock x . Consider a run ρ = q x0 π1 -→ q x1 π2 -→ q x2 • • • πn --→ q xn in A. Let τ ∈ L(T ) be a valid sequence of instructions from the timed system T . Let G τ be the associated (Σ DS Clocks , Γ DS )-graph and let u, v be vertices in G τ . Then, G τ , u, v |= label(ρ) = π 1 • π 2 • • • π n iff the value of clock x n at v originates from clock x 0 at u. We write G τ , u, v |= A x,x if there is a run ρ of A from q x to q x such that G τ , u, v |= label(ρ). Now, we can revisit and generalize the timing constraints above in (C 1 -C 4 ) using A instead of the paths tracking the last reset of a clock. For instance, the subformulae (C 1 -C 3 ) of Π α in the proof of Proposition 19 should be replaced with This completes Steps 1 and 2 of our template. Hence, timed systems with data structures whose timing features include updates can be analyzed by our approach, with a complexity blow-up that is polynomial in the size of the input. Even for timed automata without data structures, the presence of clock renamings makes the model exponentially more succinct [START_REF] Bouyer | On conciseness of extensions of timed automata[END_REF]. Converting timed automata with clock renamings to ordinary timed automata (using the reduction from [START_REF] Bouyer | Updatable timed automata[END_REF]) and then applying our technique would incur an additional exponential blowup that we avoid by using our template above.

B. Extending to other problems: Model checking

Here, we would like to check whether a system satisfies a specification. As usual, we assume a finite set AP of atomic propositions which are used to link the system and the specification, and thus we will write specifications in the logic LCPDL(AP, Γ DS ). For instance, if req, grant ∈ AP, the formula A (req =⇒ → + grant) says that every request should eventually be granted. As another example, the formula A ((a∧ →• d -→ ) =⇒ →• d -→•→ a) says that, if some property a ∈ AP holds before a message is sent over data structure d, then a still holds after the message is received.

Specifications are evaluated over (AP, Γ DS )-graphs. Such graphs are generated by runs of the timed system. Again, we consider valid sequences τ = τ 1 • • • τ n of instructions over AP ∪ Σ DS Clocks . An instruction τ i ⊆ AP ∪ Σ DS Clocks defines the atomic propositions τ i ∩ AP which hold on the i th event, together with the set of operations τ i ∩Σ DS Clocks which are executed at the i th event. Let G τ = (V, E, λ) be the (AP∪Σ DS Clocks , Γ DS )graph associated with τ . When Σ ⊆ Σ, we note π Σ the projection on Σ : if G = (V, E, λ) is a (Σ, Γ)-graph, then π Σ (G) = (V, E, λ ), where λ (u) = λ(u) ∩ Σ for all u ∈ V .

Let T be a timed system with data structures DS and let Φ ∈ LCPDL(AP, Γ DS ) be a specification. Recall that, in Theorem 21, we define the formula Ψ T = ∃p 1 , . . . , p n Ψ T . Consider Ψ = ∃p 1 , . . . , p n (Ψ T ∧ ¬Φ). Let G = (V, E) be an (∅, Γ DS )-graph. By Theorem 21, if G |= Ψ then G τ |= Ψ and there exists a feasible τ ∈ L(T ) such that G = π ∅ (G τ ). Then G τ |= ¬Φ, and since the specification uses AP only, we deduce that π AP (G τ ) |= ¬Φ. Thus, as a corollary of Theorem 21, we can construct a formula Ψ ∈ EQ-ICPDL(∅, Γ DS ) which is satisfiable over (∅, Γ DS )-linear graphs iff there is a run of the system which violates the specification Φ.

Corollary 23. Let T be a timed system with data structures DS and let Φ ∈ LCPDL(AP, Γ DS ) be a specification. For all (∅, Γ DS )-linear graphs G, we can construct a formula Ψ such that G |= Ψ iff there exists a feasible τ ∈ L(T ) such that G = π ∅ (G τ ) and π AP (G τ ) |= Φ. The size of Ψ is polynomial in the size of T and Φ, and its intersection width is 2.

VI. CONCLUSION

We studied timed systems via their behaviors depicted as graphs and reasoned about them via logic EQ-ICPDL. This gave rise to a problem of independent and basic interest: logical definability of realizability of weighted graphs. We showed that realizability is definable in EQ-ICPDL over sequential graphs but not definable, even in MSO, over non-sequential graphs. We developed a new logic based technique to analyze and model-check timed systems having a complex interplay of time and data structures. Potential future work would be to generalize this approach to handle larger classes of timed systems. In light of the negative result for non-sequential systems, an intriguing question is to come up with classes of concurrent systems that can be analyzed.

1 d 1 d 1 d 2 d 2 Fig. 1 :

 11121 Fig. 1: Labeled linear graph G σ of a sequence of instructions σ = nop w(d 1 ) w(d 2 ) w(d 2 ) r(d 1 ) w(d 1 ) r(d 2 ) w(d 1 ) r(d 2 ) r(d 1 ) nop r(d 1 ) from a system having two data structures (a stack d 1 and a queue d 2 ).

x 4 := x 2 4 d 2 := x 2 x 2 := 0 x 3 := x 4 5 x 4 := d 2 x 3 3 < 4 Fig. 5 :

 44223543345 Fig. 5: Intricate flow of information in complex updates.

x,x

  ∈Clocks test{(x := 0)} • A x,x • test{x α} (C 1 ) + x,x ∈Clocks d∈DS test{(x := 0)} • A x,x • test{d := x } • d -→ • test{d α} (C 2 ) + x,x ,y,y ∈Clocks test{(x := 0)} • A x,x • test{x -y α} • (A y,y ) -1 • test{(y := 0)} (C 3 )

  there exists a time-stamping modulo M that weakly satisfies G.Proof. One direction is Lemma 9. Conversely, suppose that tsm : V → Z M is a time-stamping modulo M that weakly satisfies G. Then, the map ts : V → N defined inductively by ts(u 1 ) = 0 and ts(u i+1 ) = ts(u i ) + d tsm (u i , u i+1 ) is a slowly monotone map.Let (u, , α, v) ∈ E. By Claim 7, distinguishing the cases u v and v ≺ u, we show easily that d + tsm (u, v) ≥ ts(v)ts(u) or d + tsm (u, v) = M . Since tsm weakly satisfies G (i.e., d + tsm (u, v) ≤ α) and M > α, the second case is impossible. It follows that ts(v) -ts(u) = ts(v) -ts(u) ≤ d + tsm (u, v) ≤ α, which shows that ts satisfies the constraints of G.

TABLE II :

 II ICPDL formulae for capturing strict guards