R Govind

B. Srivathsan Frédéric Herbreteau

Igor Walukiewicz

Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods

].

A new simulation based abstraction of local-time zones is proposed. The main technical contribution is an efficient algorithm for testing subsumption with respect to this abstraction operator. The abstraction is not finite for all networks. It turns out that, under relatively mild conditions, there is no finite abstraction for local-time zones that works for arbitrary timed networks. To circumvent this problem, we introduce a notion of a bounded-spread network. The spread of a network is a parameter that says how far the local times of individual processes need to diverge. For bounded-spread networks, we show that it is possible to use subsumption and partial-order methods at the same time.

Introduction

The reachability problem for timed automata [START_REF] Alur | A theory of timed automata[END_REF] is to decide if a given automaton has an execution from an initial to a final state. Very frequently a model is given as a network of timed automata working in parallel and synchronizing on common actions. It is tempting to exploit the concurrency information provided by such a representation to speed up reachability testing. For untimed systems, partial-order methods [START_REF] Parosh | Source sets: A foundation for optimal dynamic partial order reduction[END_REF][START_REF] Clarke | State space reduction using partial order techniques[END_REF][START_REF] Flanagan | Dynamic partial-order reduction for model checking software[END_REF][START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF][START_REF] Godefroid | A partial approach to model checking[END_REF][START_REF] Doron | All from one, one for all: on model checking using representatives[END_REF][START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF][START_REF] Valmari | A stubborn attack on state explosion[END_REF] can provide exponential improvements. The presence of time greatly complicates the picture because individual automata may synchronize implicitly via time. In this work we extend the classical zone based approach to the reachability problem so that partial-order reduction methods become applicable.

Let us explain the challenge on a simple example. Figure 1a shows a network of two processes. The first process does a local action 𝑏, the second a local action 𝑐, and then they synchronize on action $. If we ignore the timing constraints, the graph of all executions of this system has a diamond: since 𝑏 and 𝑐 are executed on different processes they are independent, so the sequence 𝑏𝑐 leads to the same state as 𝑐𝑏 as shown in Figure 1b. The timing constraints break this diamond: the sequence 𝑐𝑏 is impossible since doing 𝑐 requires to wait at least 2 time units, and then it is too late for doing 𝑏 that needs to be executed within 1 time unit from the start, as in Figure 1c. This is a major obstacle for applying partial-order methods in the timed automata setting. Before addressing this obstacle let us review how the reachability problem of a single timed automaton is solved. Most efficient solutions to the reachability problem construct an explicit graph, that we call here an abstract zone graph with subsumptions. Zones [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF] are special convex sets of clock valuations with the property that a set of valuations reachable from a zone is once again a zone. The nodes of the graph represent the zones that are reachable by the transitions of the automaton. For some timed automata, there could be infinitely many reachable zones. This is why abstractions [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF], such as Extra 𝐿𝑈 or 𝔞 ≼𝐿𝑈 , are used to "abstract" a finite number of representative sets. Finally, only zones whose abstractions are maximal with respect to inclusion are kept during exploration. This technique is called subsumption [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF], and it is essential for efficiency.

When applying this method to networks of timed automata, the state explosion problem occurs. For untimed systems this problem can be alleviated either by partialorder methods, or by symbolic methods based on BDDs or SAT-solving. For timed systems BDD and SAT based solutions [START_REF] Audemard | Bounded model checking for timed systems[END_REF][START_REF] Badban | Exact incremental analysis of timed automata with an smt-solver[END_REF][START_REF] Behrmann | Efficient timed reachability analysis using clock difference diagrams[END_REF][START_REF] Ehlers | Fully symbolic timed model checking using constraint matrix diagrams[END_REF][START_REF] Jesper | Fully symbolic model checking of timed systems using difference decision diagrams[END_REF][START_REF] Niebert | Verification of timed automata via satisfiability checking[END_REF][START_REF] Wang | Symbolic verification of complex real-time systems with clock-restriction diagram[END_REF] have been tried with mixed results. Here we pursue a partial-order approach to tackle the state explosion problem.

Partial-order methods limit the search space by using the diamonds present in the graph of executions. In our example from Figure 1b, it is enough to explore the sequence 𝑏𝑐$ as thanks to the diamond we are sure that the sequence 𝑐𝑏$ leads to the same state. For more complicated cases, this approach can give exponential gains in time as well in the size of the graph to be explored. In order to apply partial-order (0, 0) 𝑡 1 = 0, 𝑡 2 = 0 (1, 0) 𝑡 1 = 0, 𝑡 2 = 0 (0, 1) 𝑡 1 = 0, 𝑡 2 = 2

(1, 1) 𝑡 1 = 0, 𝑡 2 = 2 methods for timed systems it is essential to recover the diamonds lost due to implicit synchronization caused by time constraints. Otherwise, choosing 𝑐𝑏$ as a representative for 𝑏𝑐$ in Figure 1c would lead to incompleteness. Solutions proposed in the literature consider only diamonds where time does not elapse [START_REF] Bønneland | Stubborn set reduction for timed reachability and safety games[END_REF][START_REF] Bønneland | Start pruning when time gets urgent: Partial order reduction for timed systems[END_REF][START_REF] Kim | Urgent partial order reduction for extended timed automata[END_REF], or try to deduce which diamonds are still bound to stay despite time constraints [START_REF] Dams | Partial-order reduction techniques for real-time model checking[END_REF][START_REF] Hansen | Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions[END_REF]. Here we develop a set of theoretical results permitting a much wider use of partial-order methods in constructing abstract zone graphs with subsumption.

Our starting point is the local-time semantics [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF] for networks of timed automata, that addresses exactly the diamond problem by making time local to each process. The processes are required to synchronize their times when performing common actions. As a result, local-time semantics can be actually used to solve the reachability problem despite allowing more behaviours than the standard global-time semantics. Moreover, actions executing on different processes are independent as there are no implicit synchronizations on time.

Let us revisit our example to see how diamonds are recovered thanks to local-time. Figure 2 illustrates the graph of executions under the local-time semantics. The two processes have their local and independent times represented by clocks 𝑡 1 and 𝑡 2 , respectively. The path 𝑏𝑐$ is still feasible as before, by keeping the local times of process 𝑃 1 and 𝑃 2 synchronized. But now, 𝑐𝑏$ becomes feasible as well. 𝑃 2 may delay by 2 time units and do 𝑐 while 𝑃 1 does not delay at all. Then, 𝑃 1 can do 𝑏, and then delay 2 time units to synchronize its time with 𝑃 2 and enable the common action $. As in the standard (global-time) setting, there is a notion of a local-zone, and one can try to use the local-zone graph for checking reachability. However, this graph may be infinite.

What is lacking to make the local-time approach algorithmically interesting, is an efficient abstraction operator that would guarantee finiteness of abstract local-zone graphs. An abstraction operator has been proposed in [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF], but as we show here, the associated decision problem is Pspace-hard (Proposition 2), so there is little hope that it can be used to give an efficient solution.

To sum up, to be able to use partial-order methods with the help of local-time semantics, we need to find an abstraction operator for local zones that:

1. preserves reachability, 2. leads to a finite abstract local-zone graph, 3. is efficient algorithmically, 4. preserves diamonds of actions from distinct processes.

The first two conditions are required for correctness and termination of an exploration algorithm. The third is essential to be competitive with existing solutions: computing an inclusion between two abstracted zones should be easier than solving the reachability problem in the first place. The fourth condition is needed to apply partial-order methods. The formalization of the fourth condition is actually weaker than requiring diamonds to exist in the abstract local-zone graph with subsumptions. The latter property would be much too strong to demand; c.f. Figure 3.

Our first result is an extension of the well-known 𝔞 ≼𝐿𝑈 abstraction for global-time semantics [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF] to the localtime setting (Theorem 5). We call it 𝔞 ★ ≼𝐿𝑈 . The main technical result is an efficient algorithm for testing inclusion

𝔞 ★ ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) in time O ((|𝑋 | + 𝑛) 2 )
, where |𝑋 | is the number of clocks, and 𝑛 is the number of processes in the network (Theorem 6). This complexity is essentially the same as in the global-time setting, with the factor 𝑛 coming due to extra clocks added by the local-time semantics.

Unfortunately, the 𝔞 ★ ≼𝐿𝑈 abstraction is not finite, that is, it does not satisfy property [START_REF] Parosh | Source sets: A foundation for optimal dynamic partial order reduction[END_REF]. Actually, we observe a strong negative result: there is no simulation based abstraction operator satisfying properties (1), ( 2) and (4) at the same time (Theorem 3). This is a serious obstacle because we do not know how to guarantee (4) for abstractions that are not simulation based. To the best of our knowledge, all abstractions used in timed automata verification algorithms are simulation based. The main hindrance to get finiteness is that the local times of processes can drift from each other by arbitrary amounts, but this quantity cannot be abstracted away.

Given this roadblock, we propose a restricted setting of bounded-spread networks. These are networks where the drift between processes can be controlled: every sequence of actions can be realized while maintaining a bounded drift between processes. For such networks, a suitable adaptation of the 𝔞 ★ ≼𝐿𝑈 abstraction becomes finite, and has all the required four properties (Theorem 7).

The final step is to apply partial-order methods to the finite abstract local-zone graph with subsumptions. This is slightly delicate because the abstract local-zone graph with subsumptions does not have diamonds, precisely due to subsumptions (cf. Figure 3). Yet, we do not want to disallow subsumptions as they are essential to get an effective and an algorithmically efficient solution. We show that every partial-order method that works on graphs without subsumptions, intuitively for untimed systems, can be used for bounded-spread networks (Theorem 2). Abstractly, we see a partial-order method as computing a function src indicating for every state a subset of its outgoing transitions, such that exploring the smaller set of transitions is sufficient to verify reachability. In our example from Figure 1b we may have src(0, 0) = {𝑏} indicating that it is sufficient to explore only the transition 𝑏 from the initial node. Since the 𝔞 ★ ≼𝐿𝑈 abstraction is based on a simulation, we can show that if the src function is correct for the local-zone graph (without subsumptions), it is also correct to use it for the abstract local-zone graph with subsumptions, even though the latter does not have diamonds.

Putting these results together we obtain a methodology allowing to apply existing partial-order methods to timedsystems. The methodology is not general because it applies only to networks of bounded spread, while in general networks could have unbounded spread. Moreover, computing a spread of a given network is at least as difficult as testing reachability. On a positive side, we give examples of some types of networks that are guaranteed to have a bounded spread. We also propose a method to convert an arbitrary network into a bounded-spread network by introducing synchronizations between processes. We conclude with simple examples where our method can bring exponential gains.

Related work.

Local-time semantics has been considered by three groups. Bengtsson et al. in their paper introducing local-time semantics [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF] propose an algorithm for reachability checking. For this they introduce an abstraction called catch-up equivalence. It is rather improbable that an algorithm using this equivalence can be competitive against standard solutions because, as we show here, checking if two valuations are catch-up equivalent is PSPACE-hard. In [START_REF] Minea | Partial order reduction for model checking of timed automata[END_REF] another equivalence is proposed, but it turns out to be not sound [START_REF] Govind | Revisiting local time semantics for networks of timed automata[END_REF]. Paper [START_REF] Govind | Revisiting local time semantics for networks of timed automata[END_REF] introduces sync-subsumption, but this subsumption does not preserve diamonds, hence it is not suitable for partial-order reduction.

An alternative to local-time zones was proposed by Lugiez et. al. [START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF]. In that approach zones maintain a partial-order between clocks. To get finiteness an abstraction similar to sync-subsumption of [START_REF] Govind | Revisiting local time semantics for networks of timed automata[END_REF] is used. Once again, this does not preserve diamonds and hence this approach is not suitable for partial-order reduction on the control states.

Other works have proposed partial-order methods for timed automata, while keeping the standard semantics. For example, limiting partial-order methods only to parts where independent actions occur in zero-time [START_REF] Meyer Bønneland | Stubborn set reduction for two-player reachability games[END_REF][START_REF] Kim | Urgent partial order reduction for extended timed automata[END_REF][START_REF] Jesper | Fully symbolic model checking of timed systems using difference decision diagrams[END_REF]. Some works propose ways to discover which actions remain independent despite time constraints, either statically [START_REF] Dams | Partial-order reduction techniques for real-time model checking[END_REF] or dynamically [START_REF] Hansen | Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions[END_REF]. Two works [START_REF] Bouyer | Timed unfoldings for networks of timed automata[END_REF][START_REF] Cassez | Symbolic unfoldings for networks of timed automata[END_REF] apply unfolding techniques to bounded timed automata which admit a finite representation of their state space without abstraction.

Partial-order methods have been introduced in the 90s [START_REF] Godefroid | A partial approach to model checking[END_REF][START_REF] Doron | All from one, one for all: on model checking using representatives[END_REF][START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF] as a method to speed up verification of transition systems. Later the accent shifted to program verification, and in particular to stateless model-checking [START_REF] Godefroid | Model checking for programming languages using verisoft[END_REF]. The subject has become very active since the work of Abdulla et al. [START_REF] Parosh | Optimal dynamic partial order reduction[END_REF][START_REF] Parosh | Source sets: A foundation for optimal dynamic partial order reduction[END_REF] introducing a notion of optimal partial order reduction (see [START_REF] Chatterjee | Value-centric dynamic partial order reduction[END_REF][START_REF] Kokologiannakis | Truly stateless, optimal dynamic partial order reduction[END_REF][START_REF] Zhang | Dynamic partial order reduction for relaxed memory models[END_REF] and references within). In this paper we take an abstract view of partial-order methods and do not focus on any concrete methods. The most recent works need some adaptation to be applicable in our setting. One reason is that they consider only straight-line processes, i.e., without branching. This is too restrictive in our setting.

Synopsis. In the Preliminaries, we introduce local-time semantics, local-zone graphs and their most important properties. We also present a succinct description of partial-order methods that is sufficient for this work. In Section 3 we introduce a notion of abstraction for local-zone graphs, and study conditions under which an abstraction can be used for reachability. In Section 4 we show how partial-order methods can be used in the presence of abstractions. Unfortunately, under mild assumptions, abstractions of local-zone graphs compatible with partial-order cannot be finite (Section 5). Our solution is to put a restriction on timed networks, but before this we develop in Section 6 an abstraction operator 𝔞 ★ ≼𝐿𝑈 , which is a generalization of the well-known 𝔞 ≼𝐿𝑈 operator. We show that inclusion testing with respect to the new operator 𝔞 ★ ≼𝐿𝑈 can be done efficiently. In Section 7 we introduce bounded-spread networks, give examples of such networks, as well as a general construction transforming a timed network into a bounded-spread network. We show that a modification of 𝔞 ★ ≼𝐿𝑈 is finite on bounded-spread networks. We conclude with some examples where our method gives exponential gains and discuss where they come from.

Preliminaries

In this section we introduce networks of timed automata, local-time semantics, and partial-order reduction. We present the standard global-time semantics as a special case of the local-time semantics. This clearly shows the differences between the two. Our approach allows to transfer any partialorder method from the untimed setting to the timed setting. In this paper, a partial-order method is given as an oracle that tells which transitions need to be explored. The only constraint is that the method keeps at least one execution from each trace equivalence class. At the end of the section, we introduce local-zone graphs, and state their properties.

We use N for the set of natural numbers, R for the set of reals and R ≥0 for the set of non-negative reals. Let 𝑋 be a finite set of variables called clocks. Let 𝜙 (𝑋 ) denote a set of clock constraints generated by the following grammar: 𝜙 := 𝑥 ∼ 𝑐 | 𝜙 ∧𝜙 where 𝑥 ∈ 𝑋 , 𝑐 ∈ N, and ∼ ∈ {<, ≤, =, ≥, >}. The base constraints 𝑥 ∼ 𝑐 will be called atomic constraints.

A network of timed automata is a collection of timed automata communicating with each other via shared actions. We have seen an example of a network in Figure 1a. Each automaton participating in the network is called a process. Formally, a timed network is a 𝑘-tuple of processes N = ⟨𝐴 1 , . . . , 𝐴 𝑘 ⟩. Each process 𝐴 𝑝 = ⟨𝑄 𝑝 , Σ 𝑝 , 𝑋 𝑝 , 𝑞 init 𝑝 ,𝑇 𝑝 ⟩ has a finite set of states 𝑄 𝑝 , a finite alphabet of actions Σ 𝑝 , a finite set of clocks 𝑋 𝑝 . We require that the sets of states, and the sets of clocks are pairwise disjoint: 𝑄 𝑝 1 ∩𝑄 𝑝 2 = ∅, and 𝑋 𝑝 1 ∩𝑋 𝑝 2 = ∅ for 𝑝 1 ≠ 𝑝 2 . The sets of labels need not be disjoint -a label shared by two processes represents an action synchronizing the processes. The remaining components are an initial state 𝑞 init 𝑝 and a set of transitions 𝑇 𝑝 ⊆ (𝑄 𝑝 ×Σ 𝑝 ×𝜙 (𝑋 𝑝 )×2 𝑋 𝑝 ×𝑄 𝑝 ).

A transition (𝑞, 𝑏, 𝑔, 𝑅, 𝑞 ′ ) ∈ 𝑇 𝑝 has a label 𝑏, a guard 𝑔, and a set 𝑅 of clocks to be reset. We write Proc for the set of all processes. We will use some abbreviations: 𝑄 = Π 𝑘 𝑝=1 𝑄 𝑝 , Σ = 𝑘 𝑝=1 Σ 𝑝 and 𝑋 = 𝑘 𝑝=1 𝑋 𝑝 . For a tuple of states 𝑞 ∈ 𝑄, we write 𝑞(𝑝) to be the state of process 𝑝 in the tuple 𝑞. Every action 𝑏 has its domain dom(𝑏) = {𝑝 : 𝑏 ∈ Σ 𝑝 }. The execution of action 𝑏 requires participation of all processes in the domain. We denote by 𝑞 𝑖𝑛𝑖𝑡 the tuple of initial states 𝑞 𝑖𝑛𝑖𝑡 𝑝 for each process 𝑝.

Local-time semantics. We introduce the local-time semantics of timed automata [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF], and then the standard global-time semantics as a particular case. Fix a timed network N .

In the local-time semantics, each process 𝑝 has its local time represented by a clock 𝑡 𝑝 . The processes synchronize their times when doing a common action. The clock 𝑡 𝑝 , called the reference clock of process 𝑝, is never tested in a guard nor reset by the process. We will denote by 𝑋 𝑡

Δ = {𝛿 𝑝 ∈ R ≥0 } 𝑝 ∈Proc we define 𝑣 Δ - -→ 𝑣 ′ when 𝑣 ′ (𝑡 𝑝 ) = 𝑣 (𝑡 𝑝 ) + 𝛿 𝑝
for all 𝑝 ∈ Proc, and 𝑣 ′ (𝑥) = 𝑣 (𝑥) for all 𝑥 ∈ 𝑋 . This denotes a local delay of Δ from the valuation 𝑣. The notion of a local valuation satisfying a guard is also adapted to this interpretation. For 𝑥 a clock of process 𝑝, i.e. 𝑥 ∈ 𝑋 𝑝 , we define 𝑣 ⊨ 𝑥 ∼ 𝑐 if 𝑣 (𝑡 𝑝 ) -𝑣 (𝑥) ∼ 𝑐 for ∼ ∈ {<, ≤, =, ≥, >}.

Remark: One may wonder why not just keep the value of the clock in 𝑣 (𝑥). This interpretation gives a big problem later when we consider zones of local valuations. It turns out that in this interpretation the set of valuations reachable by a transition from a zone may not be a zone. Quite remarkably the interpretation presented above avoids this problem [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF].

A configuration of the network is a pair (𝑞, 𝑣) where 𝑞 is a tuple of control states of all processes, and 𝑣 is a local valuation. An initial valuation 𝑣 0 associates the same real to each clock: 𝑣 0 (𝑟 -𝑠) = 0 for all 𝑟, 𝑠 ∈ 𝑋 ∪ 𝑋 𝑡 . Let 𝑉 0 denote the set of initial local valuations. The initial configurations are {𝑞 𝑖𝑛𝑖𝑡 } ×𝑉 0 . For an action 𝑏, the network N can execute a transition (𝑞, 𝑣) A local run of N is a sequence of local delay and action transitions from an initial configuration (𝑞 0 , 𝑣 0 ):

𝑏 - -→ (𝑞 ′ , 𝑣 ′ ) if
(𝑞 0 , 𝑣 0 ) Δ 0 - -→ (𝑞 0 , 𝑣 ′ 0 ) 𝑏 1 - -→ (𝑞 1 , 𝑣 1 ) Δ 1 - -→ • • • 𝑏𝑛 - -→ (𝑞 𝑛 , 𝑣 𝑛 ) Δ𝑛 --→ (𝑞 𝑛 , 𝑣 ′ 𝑛 )
We write (𝑞 0 , 𝑣 0 ) 𝑢 (𝑞 𝑛 , 𝑣 ′ 𝑛 ) to say that there is a sequence as above for 𝑢 = 𝑏 1 . . . 𝑏 𝑛 and adequate delays.

Global-time semantics and reachability. The standard semantics of a network, which we refer to as global-time semantics or just global semantics in short, is given by the semantics of the monolithic timed automaton obtained as the "synchronized product" of the individual processes. There is a common time for all processes: their reference clocks are always equal. In other words global semantics uses only synchronized valuations 𝑣 where 𝑣 (𝑡 𝑝 ) = 𝑣 (𝑡 𝑞 ) for all 𝑝, 𝑞 ∈ 𝑃𝑟𝑜𝑐. In consequence, in the global semantics, we only allow global delays 𝑣 Δ --→ 𝑣 ′ which are local delays such that 𝛿 𝑝 = 𝛿 𝑞 for any two processes 𝑝, 𝑞 ∈ 𝑃𝑟𝑜𝑐. We use 𝛿 for global delays to distinguish from local delays Δ. A global run of N is an alternating sequence of global delay and action transitions starting from a synchronized valuation:

(𝑞 0 , 𝑣 0 ) 𝛿 0 - -→ (𝑞 0 , 𝑣 ′ 0 ) 𝑏 1 - -→ (𝑞 1 , 𝑣 1 ) 𝛿 1 - -→ (𝑞 1 , 𝑣 ′ 1 ) 𝑏 2 - -→ • • • 𝑏 𝑛 - -→ (𝑞 𝑛 , 𝑣 𝑛 ) 𝛿 𝑛 - -→ (𝑞 𝑛 , 𝑣 ′ 𝑛 ).
Observe that all the valuations on a global run are synchronized.

The reachability problem asks if a state 𝑞 𝑓 is reachable in the global-time semantics. In other words, does there exist a global run from an initial configuration to a configuration (𝑞 𝑓 , 𝑣) for some synchronized valuation 𝑣. This problem is known to be Pspace-complete [START_REF] Alur | A theory of timed automata[END_REF]. Most algorithms solving the reachability problem use the global semantics [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF][START_REF] Frédéric Herbreteau | Lazy abstractions for timed automata[END_REF][START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF]. The state 𝑞 𝑓 that we check for reachability is called the final state of the network N in the sequel.

Partial-order reduction (POR). We give a general outline of partial-order reductions that is sufficient for this work. The main idea is to use information about concurrency to avoid exploring equivalent interleavings of actions. In Figure 1, we have seen that the order of execution between 𝑏 and 𝑐 is irrelevant: starting from (0, 0) both sequences end in (1, 1). We say that 𝑏 and 𝑐 are independent in a transition system S if this property holds for every state of S. The notion of independence leads to trace equivalence on sequences: two sequences are trace equivalent, denoted 𝑢 ∼ S 𝑣, if one can be obtained from the other by permuting adjacent independent actions. This is an equivalence relation on sequences of actions. Moreover, if 𝑢 leads from an initial to a final state in S then so does 𝑣. A POR method aims at exploring at least one path from every trace-equivalence class, but preferably not much more. For instance in Figure 1 we may only explore the sequence 𝑏𝑐$, and ignore the sequence 𝑐𝑏$. This avoids visiting state (0, 1). In some cases this optimization may lead to exponential reductions in the number of visited states.

We think of a POR method as a way of computing for a given transition system S a source function, src : 𝑄 → P (Σ) assigning to every state of S a set of relevant actions. A path in S is a source path if it is a path in the restriction of S where from every state 𝑞 we eliminate transitions on actions that are not in src(𝑞). A source function should be trace-faithful meaning that for every state 𝑞 and every path 𝑞 𝑢 -→ 𝑞 𝑓 to a final state 𝑞 𝑓 , there must be a trace-equivalent sequence 𝑣 ∼ S 𝑢 such that 𝑞 𝑣 -→ 𝑞 𝑓 is a source path. In the example from Figure 1 we may take src(0, 0) = src(0, 1) = {𝑏}, src(1, 0) = {𝑐} and src(1, 1) = {$}. The goal is to find a trace-faithful source function without exploring the transition system.

A common way to get a src function is to look at the parallelism in a given system. In a network of automata without timing constraints, two actions with disjoint domains are independent in the sense of the previous paragraph. Stubborn sets [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF], ample sets [START_REF] Doron | All from one, one for all: on model checking using representatives[END_REF], persistent sets [START_REF] Godefroid | A partial approach to model checking[END_REF], faithful decompositions [START_REF] Katz | Verification of distributed programs using representative interleaving sequences[END_REF], stamper sets [START_REF] Doron | Relaxed visibility enhances partial order reduction[END_REF], source sets [START_REF] Parosh | Source sets: A foundation for optimal dynamic partial order reduction[END_REF], are different ways of computing a source function in this setting.

Our goal in this work is to develop a theory allowing to use the same approach for networks of timed automata. As seen in Figure 1c, in timed networks, two domain-disjoint actions may not be independent. Global time destroys diamonds, making it difficult to find out which actions are independent. Local-time semantics allows to recover diamonds, cf. Figure 2. Reachability can be solved using local-time, as we see next. Since the initial valuations are all synchronized, the above lemma ensures that a control state 𝑞 is reachable in the localtime semantics iff it is reachable in the global-time semantics. This is particularly true of the final state 𝑞 𝑓 . Given this correspondence, we will henceforth work completely with the local-time semantics. Additionally, the local-time semantics offers the diamond property which is essential for POR.

Lemma 2 (Diamond property). Suppose dom(𝑎) ∩ dom(𝑏) = ∅. If (𝑞, 𝑣) 𝑎𝑏 (𝑞 ′ , 𝑣 ′ ) then (𝑞, 𝑣) 𝑏𝑎 (𝑞 ′ , 𝑣 ′ ).
Local-zone graphs. To make the local-time semantics feasible for use in algorithms, a notion of local-zones, analagous to the zones in the global-time setting [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF], is employed. A local-zone is a set of local valuations given by conjunctions of constraints: 𝑥 -𝑦 ⋖ 𝑐 where 𝑥, 𝑦 ∈ 𝑋 ∪ 𝑋 𝑡 and ⋖ ∈ {<, ≤}. For a set of local valuations 𝑊 , define:

• local-elapse(𝑊

) := {𝑣 + Δ | 𝑣 ∈ 𝑊 , Δ ∈ R 𝑘 ≥0 }, • 𝑊 [𝑅] := {𝑣 [𝑅] | 𝑣 ∈ 𝑊 }, for a set of clocks 𝑅 ⊆ 𝑋 . • 𝑊 ∩ 𝑔 := {𝑣 | 𝑣 ⊨ 𝑔} for a guard 𝑔.
It can be shown that for a local-zone 𝑍 , the sets local-elapse(𝑍 ) (local-time delay), 𝑍 [𝑅] (clock reset) and 𝑍 ∩ 𝑔 (intersection with guard) are local-zones [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Govind | Revisiting local time semantics for networks of timed automata[END_REF].

Local-zones can be implemented using Difference Bound Matrices (DBMs), similar to the case of standard zones. Hence, they can be computed and stored as efficiently as standard zones. Before defining the local zone graph, we lift the local semantics from configurations to sets of configurations.

Definition 1 (Symbolic transition relation). Let𝑊 be a set of local valuations. We write (𝑞,𝑊 )

𝑏 = =⇒ (𝑞 ′ ,𝑊 ′ ) if there exists a tuple of 𝑏-transitions {(𝑞 𝑝 , 𝑏, 𝑔 𝑝 , 𝑅 𝑝 , 𝑞 ′ 𝑝 )} 𝑝 ∈dom(𝑏 ) such that • 𝑞(𝑝) = 𝑞 𝑝 and 𝑞 ′ (𝑝) = 𝑞 ′
𝑝 for all 𝑝 ∈ dom(𝑏), and 𝑞(𝑝) = 𝑞 ′ (𝑝) for all 𝑝 ∉ dom(𝑏);

• 𝑊 ′ = local-elapse(𝑊 2 ) is not empty, where 𝑊 2 is defined as follows:

𝑊 2 = 𝑊 1 [ 𝑝 ∈dom(𝑏 ) 𝑅 𝑝 ] and 𝑊 1 = 𝑊 ∩ ( 𝑝 ∈dom(𝑏 ) 𝑔 𝑝 ∧ {𝑡 𝑝 = 𝑡 𝑞 | 𝑝, 𝑞 ∈ dom(𝑏)})
We write (𝑞,𝑊 )

𝑏 1 ...𝑏 𝑛 = ==== =⇒ (𝑞 𝑛 ,𝑊 𝑛 ) if there is a sequence of symbolic transitions (𝑞,𝑊 ) 𝑏 1 = =⇒ (𝑞 1 ,𝑊 1 ) • • • 𝑏 𝑛 = =⇒ (𝑞 𝑛 ,𝑊 𝑛 ).
The following lemma states the relation between transitions on zones and on valuations. Its proof follows from the definition of symbolic transitions. We say that a local zone The initial zone is time-elapsed. This entails that every zone reachable by = =⇒ transitions is also time-elapsed, due to Definition 1. Using this observation along with the pre-and post-properties of Lemma 3, we get the following theorem.

𝑍 is time-elapsed if 𝑍 = local-elapse(𝑍 ).
Theorem 1. [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Govind | Revisiting local time semantics for networks of timed automata[END_REF] For a given network N , there is a run of N reaching a state 𝑞 iff there is a path in LZG(N ) from the initial node to a node (𝑞, 𝑍 ).

This theorem suggests that the local-zone graph LZG(N ) could potentially be used to analyze reachability. The localzone graph is an untimed transition system and we are interested in applying partial-order methods on it. As desired, domain-disjoint actions are independent in the local zone graph. This is a consequence of Lemmas 2 and 3.

Proposition 1 (Diamond property of LZG(N )). Let dom(𝑎)∩ dom(𝑏) = ∅. If (𝑞, 𝑍 ) 𝑎𝑏 = =⇒ (𝑞 ′ , 𝑍 ′ ) then (𝑞, 𝑍 ) 𝑏𝑎 = =⇒ (𝑞 ′ , 𝑍 ′ ).
Let us remark that the so called enabledness property [START_REF] Clarke | State space reduction using partial order techniques[END_REF] may not hold in a local-zone graph: it is possible to construct a network, a local-zone 𝑍 and two independent actions 𝑎, 𝑏 such that from (𝑞, 𝑍 ) there are both Although the local-zone graph is sound and complete for reachability, and has the diamond property, there are networks for which the local-zone graph is infinite. Hence a finite abstraction of the local-zone graph is required for analysis. This is the subject for the next section.

Abstract local-zone graphs

The goal of this section is to study finite abstractions of localzone graphs that can be used to answer the reachability question. We introduce a general definition of an abstraction and of an abstract local-zone graph. Then we put restrictions on abstractions that make the abstract local-zone graph sound and complete for reachability. We fix a timed network N . This allows us to omit indexing every notion with N . Definition 3. A quasi-abstraction operator 𝔞 : P (LocalVal) → P (LocalVal) is a function from sets of local valuations to sets of local valuations such that 𝔞(𝔞(𝑊 )) = 𝔞(𝑊 ) for all sets of local valuations 𝑊 . If the operator additionally satisfies 𝑊 ⊆ 𝔞(𝑊 ) for all sets 𝑊 , we call it an abstraction operator. A quasi-abstraction operator is finite if its co-domain is finite: there are finitely many sets 𝔞(𝑊 ).

The definition of the abstraction operator is the same as in the global-time semantics [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF], except that now we work with local valuations. We will use the weaker notion which we have called a quasi-abstraction to get finite abstractions in our setting.

A quasi-abstraction operator allows to compute an abstract local-zone graph. An exploration of a local-zone graph is stopped when a node with a bigger abstraction is already in the graph. The smaller node is said to be subsumed by the bigger node. If the quasi-abstraction is finite, then we can have a finite abstract graph.

Definition 4 (LZG 𝔞 (N )). Suppose 𝔞 is a quasi-abstraction operator. An abstract local-zone graph is a subset of nodes and edges of LZG(N ) together with some new edges called subsumption edges. Each node is labeled either covered or uncovered. The graph must satisfy the following conditions:

• The initial node of LZG(N ) belongs to the graph.

• For every uncovered node (𝑞, 𝑍 ), all its successors together with associated transitions (𝑞, 𝑍 )

𝑏 = =⇒ (𝑞 ′ , 𝑍 ′ ) in LZG(N ) should be in the graph.
• For every covered node (𝑞, 𝑍 ) there is an uncovered node (𝑞, 𝑍 ′ ) with 𝔞(𝑍 ) ⊆ 𝔞(𝑍 ′ ); moreover there is an explicit subsumption edge (𝑞, 𝑍 ) ⇝ (𝑞, 𝑍 ′ ). • Every node of the graph must be reachable from the initial node by a path of = ⇒ edges.

We denote by LZG 𝔞 (N ) some abstract zone graph for N One can imagine that we take the first one in some fixed order on graphs.

A point worth noting is that the algorithm stores zones and not abstract sets. Indeed we do not assume that an abstraction of a zone is a zone, and therefore we do not know a priori how to store and manipulate an abstract set directly.

The question now is when it is correct to examine the abstract local-zone graph instead of the network itself: when can we say that a given state is reachable by a run in a network iff it is reachable in its abstract local-zone graph. Since every node of LZG 𝔞 (N ) is reachable by a sequence of = =⇒ transitions, we have:

Lemma 4. Every abstract local-zone graph is sound: if a final state is reachable in LZG 𝔞 (N ) then it is reachable in N .
We now study the converse implication. Definition 5. A quasi-abstraction operator 𝔞 is complete when reachability of a state 𝑞 in N implies its reachability in LZG 𝔞 (N ) .

The challenge is to get complete and finite quasi-abstraction operators for which the test 𝔞(𝑍 ) ⊆ 𝔞(𝑍 ′ ) is efficient. Abstractions for the global semantics are based on simulation relations [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF][START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF]. Our next direction would be to consider abstractions based on simulations for the local semantics.

Δ ′ - -→ (𝑞, 𝑣 ′ 1 ) and (𝑞, 𝑣 1 ) ≼ (𝑞, 𝑣 ′ 1 ), 2. for every transition (𝑞, 𝑣) 𝑏 - -→ (𝑞 1 , 𝑣 1 ) there is a transi- tion (𝑞, 𝑣 ′ ) 𝑏 - -→ (𝑞 1 , 𝑣 ′ 1 ) with (𝑞 1 , 𝑣 1 ) ≼ (𝑞 1 , 𝑣 ′ 1 )
. We say 𝑣 ≼ 𝑣 ′ if (𝑞, 𝑣) ≼ (𝑞, 𝑣 ′ ) for all states 𝑞. When Δ ′ = Δ in the first condition above, the relation is called a strongtimed simulation.

Definition 7. A quasi-abstraction operator 𝔞 is simulation based if there is a simulation ≼ such that 𝔞(𝑊 ) ⊆ {𝑣 : ∃𝑣 ′ ∈ 𝑊 . 𝑣 ≼ 𝑣 ′ }.
In particular, there is the biggest abstraction operator based on a simulation ≼. It is simply the downward closure operator with respect to ≼. Lemma 5. A simulation based abstraction operator is complete.

This lemma (whose proof is in Appendix A) is not true in general for quasi-abstractions. The proof of the lemma crucially uses 𝑍 ⊆ 𝔞(𝑍 ), a property which may not hold in a quasi-abstraction. We propose an additional condition for quasi-abstractions that requires the abstraction 𝔞(𝑍 ) to keep some of the "good" valuations from the local-zone 𝑍 . This property means that 𝔞 should keep all paths leading to a final state. Observe that every abstraction operator keeps runs since 𝑍 ⊆ 𝔞(𝑍 ). The property of keeping runs, along with the operator being simulation based, gives a complete quasi-abstraction. Lemma 6. A simulation based quasi-abstraction operator that keeps runs is complete for reachability.

The aim now is to come up with a concrete quasi-abstraction 𝔞 that satisfies the properties of the above lemma and for which the test 𝔞(𝑍 ) ⊆ 𝔞(𝑍 ′ ) is efficient. We make a short digression into one of the first quasi-abstractions proposed for the local-time semantics.

Catch-up equivalence. A quasi-abstraction operator based on a relation between configurations called catch-up equivalence has been defined in [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF]. However, as we show below, deciding whether two configurations are catch-up equivalent is Pspace-hard.

We start with a definition of the equivalence. A delay The proof is by a reduction from the language emptiness of intersection of finite automata. It is presented in Appendix B. This hardness result makes it very unlikely that catch-up equivalence is suitable in practice.

(𝑞, 𝑣) Δ - -→ (𝑞, 𝑣 ′ ) is a catch-up delay if max({𝑣 ′ (𝑡)} 𝑡 ∈𝑇 ) = (𝑞, 𝑍 ) (𝑞 𝑎 , 𝑍 𝑎 ) (𝑞 𝑏 , 𝑍 𝑏 ) (𝑞 𝑎𝑏 , 𝑍 𝑎𝑏 ) (𝑞 𝑏 , 𝑍 ′ 𝑏 ) (𝑞 𝑎𝑏 , 𝑍 ′ 𝑎𝑏 ) 𝑎 𝑏 𝑏 ⇝ 𝑎 Figure 3. A diamond
To summarize this section, we have seen the properties we need of a quasi-abstraction to get a correct abstract localzone graph (Lemma 6). In Section 6 we will present an efficient simulation based abstraction for local-zone graphs. Before that, we talk about partial-order reduction.

POR on abstract local-zone graphs

We discuss how to use partial-order methods on abstract zone graphs. At this point, we have a local-zone graph of a network LZG(N ) that has diamonds but may be infinite. We suppose that we have some quasi-abstraction 𝔞 giving a finite abstract local-zone graph LZG 𝔞 (N ). We would like to use partial-order methods on LZG 𝔞 (N ), but this graph may not have diamonds as we illustrate in Figure 3. Due to subsumption there are no transitions from (𝑞 𝑏 , 𝑍 𝑏 ). So, LZG(N ) has diamonds but may be infinite, and LZG 𝔞 (N ) is finite but has no diamonds. We show that when 𝔞 satisfies the conditions given by Lemma 6, every partial-order method for LZG(N ) can be used on LZG 𝔞 (N ).

In this section we will assume that we have a source function src for LZG(N ) given by a partial-order method as described in Section 2. In LZG(N ), we have diamonds and so we can use any partial-order method to calculate a source function. Recall that the nodes of LZG(N ) are pairs (𝑞, 𝑍 ). The graph LZG(N ) may be infinite since there are infinitely many local-zones. As we want the source function to be given by some finite description, we assume that it does not depend on the local-zone, and instead depends only on the state 𝑞 and the set of actions enabled from (𝑞, 𝑍 ), denoted as enabled(𝑞, 𝑍 ). Definition 9. A source function for a timed network N is a function src : 𝑄 × P (Σ) → P (Σ). A source function of N is trace-faithful if for every node (𝑞, 𝑍 ) and a path 𝑢 from (𝑞, 𝑍 ) to a final state there is a source path 𝑤 ∼ 𝑢 from (𝑞, 𝑍 ).

The concept of trace-faithful source function is directly inspired by partial-order methods. Indeed, they always compute trace-faithful source functions as they guarantee that every path has at least one equivalent source path.

Remark. Partial-order methods in general require both the diamond and enabledness properties [START_REF] Clarke | State space reduction using partial order techniques[END_REF]. In our case LZG(N ) has diamonds, but not necessarily the enabledness property. The latter property is not needed if, for example, final states are reached by a global synchronization action, or final states are determined by a state of one of the processes. The definition above of the source function hides this problem. When applying some existing partial-order methods, some precaution, or transformation of a system, should be done to ensure that the source function is indeed trace-faithful.

We can now combine abstraction and partial-order reduction. Definition 10. For a timed network N and a source function src : 𝑄 × P (Σ) → P (Σ), the graph LZG src (N ) is obtained from LZG(N ) by keeping only the edges allowed by the src function:

(𝑞, 𝑍 ) 𝑏 = =⇒ (𝑞 ′ , 𝑍 ′ ) such that 𝑏 ∈ src(𝑞, enabled(𝑞, 𝑍 )).
Then, LZG 𝔞,src (N ) is a graph obtained from LZG src (N ) that satisfies the conditions in Definition 4.

We now have a graph LZG 𝔞,src (N ) on which both subsumption and POR have been applied. Used separately, both of them yield transition systems that are sound and complete for reachability. The next theorem, proved in Appendix C says that even the combination is correct. Theorem 2. If src is a trace-faithful source function and 𝔞 is a simulation based quasi-abstraction that keeps runs, then a final state is reachable in LZG(N ) iff it is reachable in LZG 𝔞,src (N ).

No finite abstractions for local-zone graphs

Theorem 2 gives a sufficient condition for a quasi-abstraction to be compatible with POR. There is one ingredient missing to get an algorithm. We need a finite quasi-abstraction. Unfortunately, we show that this is impossible under the assumptions made on the quasi-abstraction in Theorem 2.

In the argument below, we do not really need that the quasiabstraction keeps all runs. It would be enough to keep for every path a run with the same Parikh image. Theorem 3. There is a network N -such that LZG 𝔞 (N -) is infinite for every simulation based quasi-abstraction operator that keeps runs.

Proof. We present a network N -such that LZG 𝔞 (N -) is infinite for every simulation based quasi-abstraction 𝔞 that keeps runs. The same example appears in Lugiez et al. [START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF] in a similar context. The network N -, presented in Figure 4, consists of two processes 𝐴 1 and 𝐴 2 . It is easy to see that any accepting run of the network executes an equal number of 𝑏's and 𝑐's followed by the global synchronizing action $. Consider LZG(N -), the local zone graph of N -. For every 𝑚, 𝑛 ≥ 0, the network has a run on 𝑏 𝑚 𝑐 𝑛 . Let (𝑝 0 , 𝑞 0 , 𝑍 𝑚,𝑛 ) be the node in LZG(N -) reached from the initial node after the sequence 𝑏 𝑚 𝑐 𝑛 : (𝑝 0 , 𝑞 0 , 𝑍 0 )

𝑏 𝑚 𝑐 𝑛 = ==== ⇒ (𝑝 0 , 𝑞 0 , 𝑍 𝑚,𝑛 ). Pick 𝑖 > 𝑗 ≥ 0.
We claim that:

• 𝔞(𝑍 𝑖,𝑗 ) ̸ ⊆ 𝔞(𝑍 𝑘,𝑙 ) for any 𝑘, 𝑙 ≥ 0 with (𝑖 -𝑗) ≠ (𝑘 -𝑙).

Suppose to the contrary that 𝔞(𝑍 𝑖,𝑗 ) ⊆ 𝔞(𝑍 𝑘,𝑙 ) for some 𝑖, 𝑗, 𝑘, 𝑙 with (𝑖-𝑗) ≠ (𝑘-𝑙). Consider an execution (𝑝 0 , 𝑞 0 , 𝑣 0 )

𝑏 𝑖 𝑐 𝑗 (𝑝 0 , 𝑞 0 , 𝑣 𝑖,𝑗 ) 𝑐 𝑖 -𝑗 $ (𝑝 1 , 𝑞 1 , 𝑣) of N -.
We have 𝑣 𝑖,𝑗 ∈ 𝑍 𝑖,𝑗 . Hence by pre-property from Lemma 3, there is a path

(𝑝 0 , 𝑞 0 , 𝑍 𝑖,𝑗 ) 𝑐 𝑖 -𝑗 = == ⇒ (𝑝 1 , 𝑞 1 , 𝑍 ) in LZG(N -)
. Now, as the operator 𝔞 keeps runs, there is 𝑣 ′ 𝑖,𝑗 ∈ 𝔞(𝑍 𝑖,𝑗 ) and a run (𝑝 0 , 𝑞 0 , 𝑣 ′ 𝑖,𝑗 )

𝑐 𝑖 -𝑗 (𝑝 1 , 𝑞 1 , 𝑣 ′ ). By 𝔞(𝑍 𝑖,𝑗 ) ⊆ 𝔞(𝑍 𝑘,𝑙 ) we have 𝑣 ′ 𝑖,𝑗 ∈ 𝔞(𝑍 𝑘,𝑙 ). Since 𝔞 is simulation based there is 𝑣 𝑘,𝑙 ∈ 𝑍 𝑘,𝑙 with configuration (𝑝 0 , 𝑞 0 , 𝑣 𝑘,𝑙 ) simulating (𝑝 0 , 𝑞 0 , 𝑣 ′ 𝑖,𝑗 ). Hence, we have (𝑝 0 , 𝑞 0 , 𝑣 𝑘,𝑙 )

𝑐 𝑖 -𝑗 $ (𝑝 1 , 𝑞 1 , 𝑢) in N -.
From the fact that 𝑣 𝑘,𝑙 ∈ 𝑍 𝑘,𝑙 and the post-property (Lemma 3), there is an execution (𝑝 0 , 𝑞 0 , 𝑣 0 ) 𝑏 𝑘 𝑐 𝑙 (𝑝 0 , 𝑞 0 , 𝑣 𝑘,𝑙 ). Combining the last two executions we obtain: (𝑝 0 , 𝑞 0 , 𝑣 0 )

𝑏 𝑘 𝑐 𝑙 (𝑝 0 , 𝑞 0 , 𝑣 𝑘,𝑙 ) 𝑐 𝑖 -𝑗 $ (𝑝 1 , 𝑞 1 , 𝑢). This is impossible for (𝑖 -𝑗) ≠ (𝑘 -𝑙).
By the diamond property of LZG(N -), any sequence containing 𝑘 occurrences of 𝑏, and 𝑙 occurrences of 𝑐 ends in (𝑝 0 , 𝑞 0 , 𝑍 𝑘,𝑙 ). From 𝔞(𝑍 𝑖,𝑗 ) ̸ ⊆ 𝔞(𝑍 𝑘,𝑙 ), the node (𝑝 0 , 𝑞 0 , 𝑍 𝑖,𝑗 ) (reached by any sequence containing 𝑖 occurrences of 𝑏 and 𝑗 occurrences of 𝑐) cannot be subsumed by any other node. This shows that there are infinitely many nodes in LZG 𝔞 (N ) as there is at least one for every difference (𝑖 -𝑗).

□

In [START_REF] Govind | Revisiting local time semantics for networks of timed automata[END_REF], a simulation based quasi-abstraction is defined which is shown to be finite and complete. This operator however does not keep runs, which is in accordance with the above result. Due to this reason, this operator is not amenable for partial-order reduction.

In the following sections we propose a way out from the apparent deadlock created by Theorems 2 and 3. One direction could be to find an abstraction operator not satisfying the hypothesis of Theorem 3, that is, either not simulation based or not keeping runs. We do not know how to do this while still preserving some form of Theorem 2. Our solution is to put some restrictions on the timed networks we consider. We will first generalize the 𝔞 ≼𝐿𝑈 abstraction [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] for global-time semantics to the local-time semantics. Then we will show sufficient conditions under which it is finite.

𝐿𝑈 -simulation for the local semantics

We will present a concrete strong-timed simulation that generalizes of the 𝐿𝑈 -simulation [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] known in the global semantics to the local semantics. It is parameterized by two functions 𝐿 and 𝑈 that keep for each clock the maximum constant among lower bound constraints 𝑥 ≥ 𝑐, 𝑥 > 𝑐 and upper bound constraints 𝑥 ≤ 𝑐, 𝑥 < 𝑐 respectively. The simulation induces an abstraction operator 𝔞 ★ ≼𝐿𝑈 which is sound, complete and keeps runs for networks with bounds 𝐿 and 𝑈 . The impossibility result from the previous section still applies though. Indeed the operator is not finite. In Section 7, we will present a restriction on timed networks and modify the abstraction operator to a quasi-abstraction operator that will be finite for the restricted class of networks. Definition 11. An 𝐿𝑈 -bounds is a pair of functions 𝐿 : 𝑋 → N ∪ {-∞} and 𝑈 : 𝑋 → N ∪ {-∞}, each of which maps process clocks to a natural number or -∞. An atomic constraint 𝑥 ∼ 𝑐 is an 𝐿𝑈 -constraint if 𝑐 ≤ 𝐿(𝑥) when ∼∈ {≥ , >} (lower bound constraint) and if 𝑐 ≤ 𝑈 (𝑥) when ∼∈ {<, ≤ } (upper bound constraint). A network N is an 𝐿𝑈 -network if every guard in N is a conjunction of 𝐿𝑈 -constraints.

We next lift the 𝐿𝑈 -preorder [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF], written as ≼ 𝐿𝑈 and defined for the global-time semantics to the local-time setting. Here, when we relate 𝑣 and 𝑣 ′ , we require that the difference between reference clocks is the same for both 𝑣 and 𝑣 ′ .

Definition 12 (≼ ★

𝐿𝑈 -preorder). Given 𝐿𝑈 -bounds 𝐿 and 𝑈 . For two local valuations 𝑣, 𝑣 ′ , we say 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ if:

• 𝑣 (𝑡 𝑝 -𝑡 𝑞 ) = 𝑣 ′ (𝑡 𝑝 -𝑡 𝑞 ) for all 𝑝, 𝑞 ∈ Proc • for all 𝑝 ∈ Proc and all 𝑥 ∈ 𝑋 𝑝 -𝑣 (𝑡 𝑝 -𝑥) ≤ 𝑈 𝑥 ⇒ 𝑣 ′ (𝑡 𝑝 -𝑥) ≤ 𝑣 (𝑡 𝑝 -𝑥) -𝑣 (𝑡 𝑝 -𝑥) ≤ 𝐿 𝑥 ⇒ 𝑣 ′ (𝑡 𝑝 -𝑥) ≥ 𝑣 (𝑡 𝑝 -𝑥) -𝑣 (𝑡 𝑝 -𝑥) > 𝐿 𝑥 ⇒ 𝑣 ′ (𝑡 𝑝 -𝑥) > 𝐿 𝑥
Intuitively, the relation 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ ensures the following: (1) whenever 𝑣 + Δ synchronizes 𝑡 𝑝 and 𝑡 𝑞 , 𝑣 ′ + Δ also synchronizes them, (2) whenever 𝑣 + Δ satisfies an 𝐿𝑈 -constraint, 𝑣 ′ + Δ also satisfies the same constraint. This is the basis for ≼ ★ 𝐿𝑈 to induce a simulation over the local semantics. When 𝑣, 𝑣 ′ are synchronized valuations, the ≼ ★ 𝐿𝑈 preorder is identical to the ≼ 𝐿𝑈 preorder of the global-time semantics.

We overload the notation ≼ ★ 𝐿𝑈 to a relation between configurations: we define (𝑞, 𝑣) ≼ • We need an efficient test for 𝔞 ★ ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) because it is used in the definition of LZG 𝔞 ★ ≼𝐿𝑈 (N ). • We need LZG 𝔞 ★ ≼𝐿𝑈 (N ) to be finite. We discuss an efficient inclusion test in Section 6.1. The impossibility result from Theorem 3 tells us that LZG 𝔞 ★ ≼𝐿𝑈 (N ) cannot be always finite. To address this, we introduce the concept of a bounded-spread network in Section 7 and show that a variant of LZG 𝔞 ★ ≼𝐿𝑈 (N ) is finite there.

An algorithm for 𝔞

★ ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) The counterpart of 𝔞 ★
≼𝐿𝑈 in the global-semantics is the abstraction operator 𝔞 ≼𝐿𝑈 [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]. It is well known that the 𝔞 ≼𝐿𝑈 abstraction of a zone need not result in a zone, in fact, it may not even be convex [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF]. The current abstraction operator 𝔞 ★ ≼𝐿𝑈 is a generalization of 𝔞 ≼𝐿𝑈 which is identical to 𝔞 ≼𝐿𝑈 over zones that contain only synchronized valuations. Therefore, 𝔞 ★ ≼𝐿𝑈 is not convex. As in the global setting, the challenge is to decide the inclusion 𝔞 ★ ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) by looking at zones 𝑍 and 𝑍 ′ . We start with some simplification steps. Since 𝔞 ★ ≼𝐿𝑈 is the downward closure operator with respect to ≼ ★ 𝐿𝑈 , we make the first simplication below. Lemma 7. For every pair of zones 𝑍, 𝑍 ′ : 𝔞 ★ ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) iff 𝑍 ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ). The test 𝑍 ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) can be seen as checking whether for every 𝑣 ∈ 𝑍 there exists a 𝑣 ′ ∈ 𝑍 ′ such that 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ .

Define ⟨𝑣⟩ ★ := {𝑣 ′ | 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ }. The next lemma shows that we can reduce inclusion to intersection. Lemma 8. Let 𝑍, 𝑍 ′ be non-empty zones. Then, 𝑍 ̸ ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) iff there exists 𝑣 ∈ 𝑍 satisfying ⟨𝑣⟩ ★ ∩ 𝑍 ′ = ∅.

As mentioned before, when 𝑍, 𝑍 ′ contain only synchronized valuations, we have 𝔞 ★ ≼𝐿𝑈 (𝑍 ) = 𝔞 ≼𝐿𝑈 (𝑍 ), 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) = 𝔞 ≼𝐿𝑈 (𝑍 ′ ) and the test boils down to checking 𝑍 ⊆ 𝔞 ≼𝐿𝑈 (𝑍 ′ ), which is studied in [START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF] for the global semantics. In the local semantics we need to consider valuations that are desynchronized. However, by definition of ≼ ★ 𝐿𝑈 , for 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ , we require 𝑣 (𝑡 𝑝 -𝑡 𝑞 ) = 𝑣 ′ (𝑡 𝑝 -𝑡 𝑞 ). This property allows us to lift the technique used in [START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF] to our setting.

For our analysis, we will make use of a graph representation of local-zones, called distance graphs [START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF][START_REF] Kim Guldstrand Larsen | Compact data structures and state-space reduction for model-checking real-time systems[END_REF]. A distance graph has vertices 𝑋 ∪ 𝑋 𝑡 . For every 𝑥, 𝑦 ∈ 𝑋 ∪ 𝑋 𝑡 there is an edge 𝑥 → 𝑦 with a weight that is either (<, ∞) or of the form (⋖, 𝑐) with 𝑐 ∈ R and ⋖ standing for ≤ or <. The edge 𝑥 (⋖,𝑐 ) ----→ 𝑦 represents the constraint 𝑦 -𝑥 ⋖ 𝑐. For example, the zone 𝑍 1 := 𝑡 1 -𝑥 ≥ 5 ∧ 𝑡 2 -𝑦 ≤ 2 can be represented as a graph with edges: 𝑡 1

( ≤,-5) -----→ 𝑥, 𝑡 2 ( ≤,0) ----→ 𝑦 and 𝑦 ( ≤,2)
----→ 𝑡 2 . To reason about cumulative constraints of a path in this graph representation, an arithmetic over weights is defined.

Order:

for 𝑐 1 , 𝑐 2 ∈ R, we say (⋖ 1 , 𝑐 1 ) < (⋖ 2 , 𝑐 2 ) if 𝑐 1 < 𝑐 2 , or 𝑐 1 = 𝑐 2 , ⋖ 1 is
< and ⋖ 2 is ≤; secondly, we have (⋖, 𝑐) < (<, ∞) for every 𝑐 ∈ R. Addition: for 𝑐 1 , 𝑐 2 ∈ R, we have (⋖ 1 , 𝑐 1 ) + (⋖ 2 , 𝑐 2 ) to be equal to (⋖, 𝑑) where 𝑑 = 𝑐 1 + 𝑐 2 and ⋖ is < if one of ⋖ 1 or ⋖ 2 is <, and ⋖ is ≤ otherwise; secondly, (⋖, 𝑐) + (<, ∞) is defined to be (<, ∞) for every weight (⋖, 𝑐).

The addition allows us to define the weight of a path in a distance graph, as the sum of weights of the edges. A distance graph is canonical if for all pairs of vertices 𝑥 ≠ 𝑦, the smallest weight of a path from 𝑥 to 𝑦 is given by the weight of the edge 𝑥 -→ 𝑦. For a zone 𝑍 we denote by 𝑍 𝑥 𝑦 the weight of the 𝑥 → 𝑦 edge in the canonical distance graph representing 𝑍 . We now have all the notation to state our inclusion test. Details of arriving at this test are in Appendix E. Theorem 6. Let 𝑍, 𝑍 ′ be non-empty local zones. We have 𝑍 ⊈ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) iff there exist two variables 𝑥, 𝑦 ∈ 𝑋 ∪ 𝑋 𝑡 s.t. • 𝑍 ′ 𝑦𝑥 < 𝑍 𝑦𝑥 , and • (≤, 𝑈 𝑥 ) + 𝑍 𝑡 𝑝 𝑥 ≥ (≤, 0) if 𝑥 ∈ 𝑋 𝑝 for a process 𝑝, and • (<, -𝐿 𝑦 ) + 𝑍 ′ 𝑦𝑥 < 𝑍 𝑡 𝑞 𝑥 , if 𝑦 ∈ 𝑋 𝑞 for some process 𝑞.

The test runs over pairs of variables 𝑥, 𝑦 and uses weights 𝑍 𝑦𝑥 , 𝑍 ′ 𝑦𝑥 , 𝑍 𝑡 𝑝 𝑥 and 𝑍 𝑡 𝑞 𝑥 to check the conditions given by the theorem. This procedure can be implemented in time O (|𝑋 ∪ 𝑋 𝑡 | 2 ). When we look at local-zones consisting of only synchronized valuations, we can add constraints 𝑡 𝑝 = 𝑡 𝑞 and derive the test 𝑍 ⊆ 𝔞 ≼𝐿𝑈 (𝑍 ′ ) in the global-setting as a special case of the above theorem.

Bounded-spread networks

The impossibility result for local time semantics (Theorem 3) says that no simulation based abstraction can ensure finiteness of an abstract zone graph. Even if we go to quasiabstractions, it is impossible to get a finite abstraction that keeps runs. As we do not know how to obtain abstractions that would go around this problem, we need to look for subclasses of timed networks where abstraction guarantees finiteness. In the example from the proof of Theorem 3, the local times of the two processes can differ by an arbitrary amount, and moreover this difference influences future behavior. We give a sufficient condition to avoid this situation.

We introduce the notion of bounded-spread networks and show how we can adapt the 𝔞 ★ ≼𝐿𝑈 abstraction (Definition 13) to get a finite quasi-abstraction that keeps runs for boundedspread networks. This gives an algorithm for bounded-spread networks that can use both subsumption and POR at the same time. We also discuss some cases when a network is guaranteed to be of bounded spread, as well as present a method of converting any network into an equivalent bounded-spread network by adding some synchronizations. Definition 14. The spread between processes 𝐴 𝑝 , 𝐴 𝑞 in a local valuation 𝑣 is the absolute value of the difference between their reference clocks: |𝑣 (𝑡 𝑝 ) -𝑣 (𝑡 𝑞 )|. Let 𝐷 ≥ 0 be a natural number. We say that a valuation 𝑣 has spread 𝐷 if the spread between every pair of processes in 𝑣 is at most 𝐷. Definition 15. A run in the local time semantics

(𝑞 0 , 𝑣 0 ) Δ 0 - -→ (𝑞 0 , 𝑣 ′ 0 ) 𝑏 1 - -→ (𝑞 1 , 𝑣 1 ) Δ 1 - -→ • • • 𝑏𝑛 - -→ (𝑞 𝑛 , 𝑣 𝑛 ) Δ𝑛 --→ (𝑞 𝑛 , 𝑣 ′ 𝑛 )
is said to be 𝐷-spread if all 𝑣 0 , 𝑣 ′ 0 . . . , 𝑣 𝑛 , 𝑣 ′ 𝑛 have spread 𝐷.

Definition 16. A network N is said to be 𝐷-spread if every local run of N can be converted to a 𝐷-spread run by adjusting the delays: that is, for every run (𝑞 0 , 𝑣 0 )

Δ 0 - -→ (𝑞 0 , 𝑣 ′ 0 ) 𝑏 1 - -→ (𝑞 1 , 𝑣 1 ) Δ 1 - -→ • • • 𝑏𝑛 - -→ (𝑞 𝑛 , 𝑣 𝑛 ) Δ𝑛 --→ (𝑞 𝑛 , 𝑣 ′ 𝑛 ) there ex- ists a 𝐷-spread run (𝑞 0 , v0 ) Δ ′ 0 - -→ (𝑞 0 , v′ 0 ) 𝑏 1 - -→ (𝑞 1 , v1 ) Δ ′ 1 - -→ • • • 𝑏𝑛 - -→ (𝑞 𝑛 , v𝑛 ) Δ ′ 𝑛 --→ (𝑞 𝑛 , v′ 𝑛 ) where v0 = 𝑣 0 .
Example. Consider the network in Figure 1a. We have two processes one with clock 𝑥 and the other with clock 𝑦. There are also two reference clocks 𝑡 1 and 𝑡 2 . Let 𝑣 𝑖,𝑗 stand for a valuation 𝑡 1 = 𝑖, 𝑡 2 = 𝑗, 𝑥 = 𝑦 = 0. In particular, 𝑣 0,0 is an initial valuation. In the local semantics we have a run (0, 0, 𝑣 0,0

) (0,9) ---→ (0, 0, 𝑣 0,9 ) 𝑐 - -→ (0, 1, 𝑣 0,9 ) 𝑏 - -→ (1, 1, 𝑣 0,9 ).
Valuation 𝑣 0,9 has spread 9. Yet the run has a spread 1 because we can adjust the delays: (0, 0, 𝑣 0,0

) (1,2) ---→ (0, 0, 𝑣 1,2 ) 𝑐 - -→ (0, 1, 𝑣 1,2 ) 𝑏 - -→ (1, 1, 𝑣 1,2
). If we did not allow for adjusting delays in the definition of 𝐷-spread, this network would have an unbounded spread. With the adjustment, it is 1-spread.

When is a network bounded-spread

We give some examples where it is easy to check that a network is of bounded spread. For such classes we can apply the verification method presented in this work. In general, checking if the spread of a network is bounded by a given 𝐷 is at least as hard as checking reachability. So an approach consisting of taking an arbitrary network, calculating its spread, and then applying our method, would not work. Observe that every network can be made 0-spread if one makes all the processes synchronize on all actions. However, this removes all parallelism in the network and any possibility of applying POR. We show a less radical method of converting any network to a 𝐷-spread network. The method introduces some new synchronizations, but still leaves some parallelism where partial-order methods can be applied. We start with some sufficient conditions for a network to be bounded spread and later describe the general construction.

Acyclic systems. We claim that acyclic systems are boundedspread where the bound depends on the size of the network description. The local-zone graph of an acyclic network is finite and no abstraction is needed. But, making use of "cross" subsumptions reduces the state-space when there are multiple ways to reach a state. Showing that an acyclic system is bounded-spread allows to use both subsumption and POR. Lemma 9. Suppose 𝑀 is a maximal constant in guards. The spread of a run of length 𝑛 is bounded by 𝑛𝑀 + 1.

Here is an example where we get the maximal spread:

𝑏,𝑥 >𝑀,𝑥:=0 --------→ • • • 𝑏,𝑥 >𝑀,𝑥:=0 --------→ 𝑎,𝑦=0 ----→
Actions 𝑎 and 𝑏 are local actions of two processes. At the beginning the two clocks are at 0. The clock of 𝑏 process gets to some 𝑛𝑀 + 𝜖 ′ for 0 < 𝜖 ′ < 1, while the clock of 𝑎 process is still 0. Lemma 9 gives an upper bound for the spread of any run in an acyclic system (see Appendix F proofs). Frequently communicating systems. More interesting examples of bounded-spread systems are frequently communicating client/server systems. In such systems we have one server process 𝑆, and a number of client processes 𝐶 1 , . . . , 𝐶 𝑛 . The only communication actions are between the server and clients: the domain of an action can be either a singleton or {𝑆, 𝐶 𝑖 } for some 𝑖. Such a network is frequently communicating if there is a bound 𝐷 such that every client communicates with server in every time interval of length 𝐷. It is not difficult to see that in this case the network is 2𝐷-spread.

Another example is a network with barriers that can be modeled as global synchronizations. Assume there are no other communication actions: each action is either local to a process or it is a global synchronization. If we know that there is a synchronizing action on every loop of every process then the system is bounded-spread thanks to Lemma 9. This idea of frequent communication resulting in boundedspread brings us to the next construction. It is possible to convert an arbitrary system to a bounded-spread system, at the price of reducing concurrency. Lemma 9 suggests adding global synchronizations, say on every loop. This would indeed bound the spread as the length of runs between two global configurations would be bounded. This transformation is unfortunately not correct: we miss some behaviors of the original system. Another solution is to synchronize everybody every 𝐷 units of time, which we formalize below. Definition 17. Let N be an arbitrary timed network and 𝐷 ≥ 1 a natural number. Define N 𝐷 to be the timed network obtained from N as follows. Add a fresh clock 𝑧 𝑝 to every process 𝑝, and a new synchronization action 𝑠 whose domain is the set of all processes. To every state of every process we add a self-loop on 𝑠 with a guard 𝑧 𝑝 = 𝐷 and reset of 𝑧 𝑝 . To every other transition add 𝑧 𝑝 < 𝐷 to the existing guard.

The construction ensures that in every 𝐷 units of time every process needs to do the 𝑠 transition. Hence the resulting system is 𝐷-spread bounded. Moreover reachability is preserved as every state that is reachable is reachable by a global run (Lemma 1) and global runs are 0-spread. Hence all global runs of N appear in N 𝐷 , with embedded 𝑠 actions. Proposition 3. For every network N and natural number 𝐷 ≥ 1, the system N 𝐷 is 𝐷-spread. A final state 𝑞 𝑓 is reachable in N iff it is reachable in N 𝐷 .

The methodology that we develop in the subsequent section can be applied to N 𝐷 . While independence between actions of the original network N is preserved in N 𝐷 , there may be more traces due to new synchronization actions. In Section 8, we will see an example where these extra traces get compensated by POR, in fact by an exponential factor.

Abstraction for bounded-spread networks

We come back to the crucial point of obtaining finite abstractions of bounded-spread networks. For a given bound 𝐷 we use 𝔞 ★ ≼𝐿𝑈 abstraction restricted to 𝐷-spread valuations. We show that this guarantees finiteness of the abstract graph.

Examples with exponential gain

Theorems 7 and 2, along with Definitions 10 and 9 give an algorithm for testing reachability in bounded-spread networks: explore the local zone graph restricted to the successors given by the src function, and for each fresh node (𝑞, 𝑍 ) that is discovered, do not explore further if is subsumed, that is 𝔞 𝐷 ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 𝐷 ≼𝐿𝑈 (𝑍 ′ ) for an already visited node (𝑞, 𝑍 ′ ). We now present two examples on which this method gives exponential gain.

The first example shows advantages of local-time semantics together with partial-order methods. Consider a network of 𝑁 timed automata A 𝑖 as depicted below, where 𝑎 𝑖 and 𝑏 𝑖 are local actions, whereas $ is a synchronized action:

𝑞 0 𝑞 1 𝑞 2 𝑞 3 𝑎 𝑖 , (𝑥 𝑖 ≤ 𝑖 ), {𝑥 𝑖 } 𝑏 𝑖 , (𝑥 𝑖 ≥ 2𝑖 ) $
Notice that not all sequences of actions are feasible in global time. For instance, 𝑏 2 requires a delay of 4 time units, hence it cannot happen before 𝑎 3 which only allows a delay of 3 time units. Still, all 3 𝑁 combinations of states 𝑞 0 , 𝑞 1 and 𝑞 2 are reachable, although some of them are deadlocks. POR cannot be applied in algorithms using global-time semantics since the guards remove most diamonds.

In the local-time semantics, all sequences of actions are feasible. The spread is bounded by 2𝑁 . We can apply a very simple partial-order technique: if there is a local action in enabled(𝑞, 𝑍 ) then keep only the action of the smallest process, otherwise only $ action is enabled and keep this action. This source function is complete for reachability of the final state (𝑞 3 , . . . , 𝑞 3 ). There is only one source path and it follows the sequence of actions 𝑎 1 𝑏 1 𝑎 2 𝑏 2 • • • 𝑎 𝑁 𝑏 𝑁 $. Recall that without POR at least 3 𝑁 states are visited.

The second example illustrates the general construction given in Definition 17 converting any network to a boundedspread network (Proposition 3). Recall the example of a network with unbounded spread from Figure 4. We consider an extension of it to 𝑛 processes, N - 𝑛 . We apply to it the construction for bounding the spread to 1, obtaining a network N + 𝑛 = ⟨𝐴 1 , . . . , 𝐴 𝑛 ⟩, where 𝐴 𝑖 are as in the figure below. The actions 𝑠 and $ are global actions and 𝑏 𝑖 is local to 𝐴 𝑖 .

𝑝 𝑖 𝑞 𝑖 𝑏 𝑖 , 𝑧 𝑖 < 1 ∧ 𝑥 𝑖 = 1, {𝑥 𝑖 } 𝑠, 𝑧 𝑖 = 1, {𝑧 𝑖 } $, 𝑧 𝑖 < 1 ∧ 𝑥 𝑖 = 1
Consider a src function that gives for each (𝑝, 𝑍 𝜎 ), the action 𝑠 and the action 𝑏 𝑖 with the least index that is enabled at 𝑍 𝜎 . Denote by LZG (N + ). Without partial-order reduction, there will be a node (𝑝, 𝑍 𝑠𝑢 ) for each 𝑢 that is a sequence of 𝑏 actions without repetitions. This is because 𝑍 𝑠𝑢 1 and 𝑍 𝑠𝑢 2 with 𝑢 1 and 𝑢 2 not being interleavings of each other cannot be covered with respect to each other by the 𝔞 𝐷 ≼𝐿𝑈 quasiabstraction. A detailed analysis, presented in Appendix G, shows that without a partial-order method, an exploration needs to visit exponentially many zones, be it in local or global-time semantics.

Conclusion

We have introduced a framework for applying partial-order methods to the analysis of timed automata. It uses local-time semantics in order to regain commutativity of independent actions. However, the resulting local-time zone graph is usually infinite, and prior finite abstractions were either impractical or incompatible with partial-order methods. We have introduced a new abstraction 𝔞 ★ ≼𝐿𝑈 that is simulation based, and hence compatible with partial-order methods. The abstraction 𝔞 ★ ≼𝐿𝑈 is generally not finite. Even worse, as we have shown here, there does not exist an abstraction that is finite, and simulation based. To circumvent this obstacle, we have introduced bounded-spread timed networks, for which the 𝔞 ★ ≼𝐿𝑈 abstraction can be made finite. This requires the introduction of quasi-abstractions. We have given examples of subclasses of timed networks that are naturally boundedspread, and we have shown that every timed network can be made bounded-spread, at the cost of reducing concurrency. We have illustrated the benefits of our framework on two examples.

Our next steps will be designing concrete partial-order methods that provide exponential gains for a wide class of timed networks. We hope that our framework can be extended to other verification problems, like liveness or solving timed games, as well as to richer timed models, like pushdown timed automata, or weighted timed automata.

A Appendix for Section 3 ▶ Lemma 5. A simulation based abstraction operator is complete.

Proof. Let ≼ be the simulation on which the abstract local zone graph is based on. Let (𝑞 0 , 𝑣 0 )

Δ 0 - -→ (𝑞 0 , 𝑣 ′ 0 ) 𝑏 1 - -→ (𝑞 1 , 𝑣 1 ) • • • 𝑏 𝑛 - -→ (𝑞 𝑛 , 𝑣 𝑛 )
Δ 𝑛 --→ be a local run. For every (𝑞 𝑖 , 𝑣 𝑖 ) we will identify an uncovered node (𝑞 𝑖 , 𝑍 𝑖 ) and a valuation 𝑢 𝑖 ∈ 𝑍 𝑖 such that 𝑣 𝑖 ≼ 𝑢 𝑖 .

Base case is easy since the initial node (𝑞 0 , 𝑍 0 ) contains the initial valuation 𝑣 0 . Assume we have identified (𝑞 𝑖 , 𝑍 𝑖 ) and 𝑢 𝑖 .

By property of simulations, there is a local run (𝑞 𝑖 , 𝑢 𝑖 )

Δ ′ 𝑖 - -→ (𝑞 𝑖 , 𝑢 ′ 𝑖 ) 𝑏 𝑖+1
--→ (𝑞 𝑖+1 , 𝑢 𝑖+1 ) such that 𝑣 ′ 𝑖 ≼ 𝑢 𝑖 and 𝑣 𝑖+1 ≼ 𝑢 𝑖+1 . By pre-property (Lemma 3) there is a symbolic transition (𝑞 𝑖 , 𝑍 𝑖 ) 𝑏 𝑖 -→ (𝑞 𝑖+1 , 𝑍 𝑖+1 ) with 𝑢 𝑖+1 ∈ 𝑍 𝑖+1 . If (𝑞 𝑖+1 , 𝑍 𝑖+1 ) is uncovered, we are done. If not, we have a node (𝑞 𝑖+1 , Ẑ𝑖+1 ) such that 𝔞(𝑍 𝑖+1 ) ⊆ 𝔞( Ẑ𝑖+1 ). Since 𝔞 is an abstraction operator, we have 𝑍 𝑖+1 ⊆ 𝔞(𝑍 𝑖+1 ). Hence there exists a û𝑖+1 ∈ Ẑ𝑖+1 such that 𝑢 𝑖+1 ≼ û𝑖+1 . This node (𝑞 𝑖+1 , Ẑ𝑖+1 ) and valuation û𝑖+1 give the required conclusion. □ ▶ Lemma 6. A simulation based quasi-abstraction operator that keeps runs is complete for reachability.

Proof. We show a more general result in Theorem 2. This lemma follows by taking src in Theorem 2 to be the set of all enabled actions for every (𝑞, 𝑍 ). □

B Catch-up equivalence is PSPACE-complete

A delay (𝑙, 𝑣) Δ --→ (𝑙, 𝑣 ′ ) is a catch-up delay if max({𝑣 ′ (𝑡)} 𝑡 ∈𝑇 ) ≤ max({𝑣 (𝑡)} 𝑡 ∈𝑇 ). So catch-up delays only allow the processes that are behind in time to join the most advanced processes.

Two local-time configurations (𝑞, 𝑣) and (𝑞 ′ , 𝑣 ′ ) are catchup equivalent if (𝑞, 𝑣) and (𝑞 ′ , 𝑣 ′ ) can reach the same synchronized regions (i.e. Alur&Dill's regions) through catch-up delays and discrete transitions.

In the sequel we consider the following decision problem: INPUT: A network of timed automata N and two localtime configurations (𝑞, 𝑣) and (𝑞 ′ , 𝑣 ′ ) of N . QUESTION: are (𝑞, 𝑣) and (𝑞 ′ , 𝑣 ′ ) catch-up equivalent?

To warm-up we consider a simple network:

𝑞 0 0 P 0 𝑞 1 0 𝑞 1 1 𝑐, (𝑥 = 0) P 1
Process 0 has no transitions, and process 1 has one transition guarded with 𝑥 = 0. We claim that the following configurations are not catch-up equivalent:

(𝑞 0 0 , 𝑞 0 1 , [𝑡 0 = 𝑡 1 = 1, 𝑥 = 0]) ≁ (𝑞 0 0 , 𝑞 1 0 , [𝑡 0 = 1, 𝑡 1 = 𝑥 = 0])
Indeed, in the first configuration no catchup transition is possible. In the second process 1 can do transition 𝑐 immediately, and then wait in 𝑞 1 1 reaching (𝑞 0 0 , 𝑞 1 1 , [𝑡 0 = 1, 𝑡 1 = 𝑥 = 1]). On the other hand if there is no 𝑐 transition then the two configurations are equivalent, because the onl thing possible is that process 1 lets the time pass to catch-up with process 0.

We use the same idea to reduce the language emptiness of the intersection of 𝑛 finite automata.

P n

We are given automata A 1 , . . . , A 𝑛 with initial states 𝑞 𝑖 0 and final states 𝑞 𝑖 𝑓 . We guard every transition of every automaton with 𝑥 = 0 (technically we need 𝑥 𝑖 for every process but this just makes notation worse). Moreover on a new letter 𝑏 we add transitions from the initial state of automaton A 𝑖 to every state of A 𝑖 . Finally, from the tuple of finite states (𝑞 1 𝑓 , . . . , 𝑞 𝑛 𝑓 ) we add a transition 𝑐 with the guard 𝑥 = 0, the transition synchronizes process 1, . . . , 𝑛. We claim that if 𝐿(A 1 ) ∩ • • • ∩ 𝐿(A 𝑛 ) ≠ ∅ then the two configurations are not equivalent:

conf 1,1 =(𝑞 0 0 , 𝑞 1 0 , . . . , 𝑞 𝑛 0 , [𝑡 0 = 𝑡 1 = • • • = 𝑡 𝑛 = 1, 𝑥 = 0]) conf 1,0 =(𝑞 0 0 , 𝑞 1 0 , . . . , 𝑞 𝑛 0 , [𝑡 0 = 1, 𝑡 1 = • • • = 𝑡 𝑛 = 𝑥 = 0])
If intersection is empty then transition 𝑐 cannot be taken. The synchronized configurations reachable from conf 1,1 are all combinations of states of A 1 , . . . , A 𝑛 thanks to the added 𝑏 transitions. Similarly, from conf 1,0 , as the processes can just wait in the initial state to conf 1,1 .

If the intersection is non-empty then from 𝑐𝑜𝑛𝑓 1,0 processes can get to 𝑞 1 𝑓 , . . . , 𝑞 𝑛 𝑓 in 0-time, and then do 𝑐 transition reaching (𝑞 0 0 , 𝑞 1 𝑟 , . . . , 𝑞 𝑛 𝑟 ,

[𝑡 0 = 𝑡 1 • • • = 𝑡 𝑛 = 1, 𝑥 = 0]
). This synchronized state is not possible to reach from conf 1,1 .

C Appendix for Section 4

▶ Theorem 2. If src is a trace-faithful source function and 𝔞 is a simulation based quasi-abstraction that keeps runs, then a final state is reachable in LZG(N ) iff it is reachable in LZG 𝔞,src (N ).

Proof. If a final state is reachable in LZG 𝔞,src (N ) then it is reachable by a sequence of = == ⇒ transitions by definition (c.f. Definitions 10,[START_REF] Audemard | Bounded model checking for timed systems[END_REF]. This gives a path in LZG(N ).

Consider left-to-right direction. Since src is trace-faithful, it is sufficient to show that each source path in LZG(N ) that leads to a final state has a representative source path in LZG 𝔞 (N ), potentially with subsumption edges, that goes to a final state. The latter is a path in LZG 𝔞,src (N ) by definition. Suppose 𝑤 0 is a source path in LZG(N ) from (𝑞 0 , 𝑍 0 ) to (𝑞 𝑛 , 𝑍 𝑛 ), with 𝑞 𝑛 an accepting state. Let 𝑛 = |𝑤 0 | be the length of 𝑤 0 . By induction on 𝑖 we show that there are paths 𝑢 𝑖 , 𝑤 𝑖 such that:

• (𝑞 0 , 𝑍 0 ) ----→ 𝑦 represents the constraint 𝑦 -𝑥 ⋖ 𝑐. For a graph 𝐺, we will write [[𝐺]] for the set of valuations satisfying two Item 1 edges with a single Item 1 edge. Moreover, we still have the property that between two consecutive 𝑍 ′ edges on the cycle there is either a single Item 1 edge or a single Item 1 edge followed by an Item 2 edge. This is because transitions entering 𝑥 1 and 𝑥 2 on the cycle must come from 𝑍 ′ . Moreover, transitions from 𝑦 1 and 𝑦 2 must be either from 𝑍 ′ or Item 2 transitions followed by a transition from 𝑍 . After the reduction we can have two consecutive transitions from 𝑍 ′ , but then we can apply Step 1 to shorten the cycle.

𝑢 𝑖 = =⇒ (𝑞 𝑖 , 𝑍 𝑖 ) is a source path in LZG 𝔞,src (N ), • (𝑞 𝑖 , 𝑍 𝑖 ) 𝑤 𝑖 = =⇒ (𝑞 𝑛 , 𝑍 𝑖 𝑛 ) is a source path in LZG(N ), • |𝑤 𝑖 | = 𝑛 -𝑖 The initial
Applying the transformation repeatedly, we are left with a negative cycle having a single Item 1 edge. This edge can be followed by an Item 2 edge. There can only be one 𝑍 ′ edge on the cycle. This means that 𝑁 is either 𝑥 -----------------

( ≤,𝑣 (𝑦-𝑥 ) ) ---------→ 𝑦 𝑍 ′ 𝑦𝑥 ---→ 𝑥 or 𝑥 ( ≤,𝑣 (𝑡 𝑞 -𝑥 ) ) ---------→ 𝑡 𝑞 (<,-𝐿 𝑦 ) ------→ 𝑦 𝑍 ′ 𝑦𝑥 ---→ 𝑥.

Proof of Theorem 6

Left-to-right direction. Suppose 𝑍 ⊈ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ). Then there is a 𝑣 ∈ 𝑍 such that ⟨𝑣⟩ ★ ∩ 𝑍 ′ = ∅ (Lemma 8). From Proposition 4, there exist two clocks 𝑥 ∈ 𝑈 -bounded(𝑣) and if 𝑦 is a process clock, then 𝐿 𝑦 ≠ -∞, and 𝐻 𝑣 𝑥 𝑦 + 𝑍 ′ 𝑦𝑥 < (≤, 0). We will use these conclusions to show the right hand side of the theorem.

We start with the second item, that is, to show that if 𝑥 ∈ 𝑋 𝑝 then (≤, 𝑈 𝑥 ) + 𝑍 𝑡 𝑝 𝑥 ≥ (≤, 0). As 𝑥 ∈ 𝑈 -bounded(𝑣), we have 𝑣 (𝑡 𝑝 -𝑥) ≤ 𝑈 𝑥 . Secondly, since 𝑣 ∈ 𝑍 , replacing the 𝑥 → 𝑡 𝑝 edge of 𝑍 with (≤, 𝑣 (𝑡 𝑝 -𝑥)) will give no negative cycles. Hence, in particular: (≤, 𝑣 (𝑡 𝑝 -𝑥)) + 𝑍 𝑡 𝑝 𝑥 ≥ (≤, 0). Plugging 𝑣 (𝑡 𝑝 -𝑥) ≤ 𝑈 𝑥 into this inequality gives (≤, 𝑈 𝑥 ) + 𝑍 𝑡 𝑝 𝑥 ≥ (≤, 0).

For the first and third items, we make use of a preliminary lemma.

Lemma 12. Let 𝑍 be a non-empty local zone and let 𝑣 ∈ 𝑍 . Let 𝑟, 𝑠 ∈ 𝑋 ∪ 𝑇 be arbitrary clocks, and let (⋖, 𝑑) be a weight with 𝑑 ∈ Z. If (≤, 𝑣 (𝑟 -𝑠)) + (⋖, 𝑑) < (≤, 0) then (⋖, 𝑑) < 𝑍 𝑟𝑠 .

Proof. Since 𝑣 ∈ 𝑍 , 𝑣 satifies all constraints of 𝑍 . Consider the weight 𝑍 𝑟𝑠 , which is the weight of the 𝑟 → 𝑠 edge in the canonical distance graph of 𝑍 . This weight gives an upper bound for 𝑣 (𝑠 -𝑟 ).

Suppose 𝑍 𝑟𝑠 = (≤, 𝑐) (with a weak inequality in the weight). Then 𝑣 (𝑠 -𝑟 ) ≤ 𝑐, which implies -𝑐 ≤ 𝑣 (𝑟 -𝑠). Since (≤, 𝑣 (𝑟 -𝑠)) + (⋖, 𝑑) < (≤, 0), we also have (≤, -𝑐) + (⋖, 𝑑) < (≤, 0). From this inequality, we can infer that either 𝑑 -𝑐 < 0, or 𝑑 = 𝑐 and ⋖ =<. Either way, we get (⋖, 𝑑) < (≤, 𝑐).

Suppose 𝑍 𝑟𝑠 = (<, 𝑐) (with a strict inequality in the weight). Then 𝑣 (𝑠 -𝑟 ) < 𝑐, which implies -𝑐 < 𝑣 (𝑟 -𝑠). Let 𝑣 (𝑟 -𝑠) = -𝑐 + 𝜀 for some 𝜀 > 0. We then have (≤, -𝑐 + 𝜀) + (⋖, 𝑑) < (≤ , 0). By the previous argument, we have (⋖, 𝑑) < (≤, 𝑐 -𝜀). Since 𝑑 is an integer, this implies (⋖, 𝑑) < (<, 𝑐).

In both cases, we can infer (⋖, 𝑑) < 𝑍 𝑟𝑠 . □ Thanks to Lemma 12, it is sufficient to show (≤, 𝑣 (𝑦 -𝑥)) + 𝑍 ′ 𝑦𝑥 < (≤, 0)

to conclude the first item, and (≤, 𝑣 (𝑡 𝑞 -𝑥)) + (<, -𝐿 𝑦 ) + 𝑍 ′ 𝑦𝑥 < (≤, 0)

to conclude the third item. We consider the case when 𝑦 ∈ 𝐿 -bounded(𝑣). In this case 𝐻 𝑣 𝑥 𝑦 is (≤, 𝑣 (𝑦 -𝑥)). The assumption 𝐻 𝑣 𝑥 𝑦 +𝑍 ′ 𝑦𝑥 < (≤, 0) gives immediately (3). For equation ( 4) we use the fact that 𝑦 is L-bounded, giving us 𝑣 (𝑦 -𝑡 𝑞 ) ≥ -𝐿 𝑦 . Substituting this inequality into 𝑣 (𝑦 -𝑥) = 𝑣 (𝑦 -𝑡 𝑞 ) +𝑣 (𝑡 𝑞 -𝑥) we obtain 𝑣 (𝑦 -𝑥) ≥ -𝐿 𝑦 +𝑣 (𝑡 𝑞 -𝑥). Then the hypothesis 𝐻 𝑣 𝑥 𝑦 +𝑍 ′ 𝑦𝑥 < (≤, 0) gives the desired (<, -𝐿 𝑦 ) + (≤, 𝑣 (𝑡 𝑞 -𝑥)) + 𝑍 ′ 𝑦𝑥 < (≤, 0). When 𝑦 ∉ 𝐿 -bounded(𝑣), we have 𝐻 𝑣 𝑥 𝑦 = (≤, 𝑣 (𝑡 𝑞 -𝑥)) + (<, -𝐿 𝑦 ). Therefore, (≤, 𝑣 (𝑡 𝑞 -𝑥)) + (<, -𝐿 𝑦 ) + 𝑍 ′ 𝑦𝑥 < (≤ , 0). Hence (4) is true. Moreover, 𝑣 (𝑡 𝑞 -𝑦) > 𝐿 𝑦 as 𝑦 ∉ 𝐿 -bounded(𝑣). Now, 𝑣 (𝑦 -𝑥) = 𝑣 (𝑦 -𝑡 𝑞 ) + 𝑣 (𝑡 𝑞 -𝑥) which is strictly lesser than -𝐿 𝑦 + 𝑣 (𝑡 𝑞 -𝑥). In terms of weights, (≤, 𝑣 (𝑦 -𝑥)) ≤ (<, -𝐿 𝑦 ) + (≤, 𝑣 (𝑡 𝑞 -𝑥)). This implies that (≤, 𝑣 (𝑦 -𝑥)) + 𝑍 ′ 𝑦𝑥 < (≤, 0) is also true, proving (3). Right to left direction. We will show that if the right hand side is true, there is a valuation 𝑣 ∈ 𝑍 satisfying the left hand side of Proposition 4 with clocks 𝑥 and 𝑦. The third item of the right hand side already shows that 𝐿 𝑦 ≠ -∞ when 𝑦 is a process clock. We now need to get a valuation 𝑣 ∈ 𝑍 such that 𝑥 ∈ 𝑈 -bounded(𝑣) and 𝐻 𝑣 𝑥 𝑦 + 𝑍 ′ 𝑦𝑥 < (≤, 0). Let 𝐺 𝑍 be the canonical distance graph of 𝑍 .

Step 1. Consider the graph 𝐺 1 obtained from 𝐺 𝑍 by replacing weight of edge 𝑥 → 𝑡 𝑝 with min((≤, 𝑈 𝑥 ), 𝑍 𝑥𝑡 𝑝 ) where 𝑝 is the process of clock 𝑥, 𝑥 ∈ 𝑋 𝑝 . Adding this edge causes no negative cycles, since (≤, 𝑈 𝑥 ) + 𝑍 𝑡 𝑝 𝑥 ≥ (≤, 0). Therefore [[𝐺 1 ]] ≠ ∅ and contains the set of all valuations 𝑣 ∈ 𝑍 such that 𝑥 ∈ 𝑈 -bounded(𝑣). Let 𝐺 * 1 be the canonical graph derived from 𝐺 1 . The shortest path from any variable 𝑠 to 𝑥 in 𝐺 1 does not involve the edge 𝑥 → 𝑡 𝑝 since any path from 𝑠 to 𝑥 containing edge 𝑥 → 𝑡 𝑝 will have a cycle, and we have seen that cycles in 𝐺 This gives an abstract zone graph (without partial-order reduction) where sequences with three 𝑠 actions are covered by a sequence with two 𝑠 actions, and a sequence 𝑠𝑢 where 𝑢 contains all actions 𝑏 𝑖 is covered by 𝑍 0 . There is an uncovered node for every 𝑍 𝑠𝑢 where 𝑢 has at most 𝑛 -1 𝑏 𝑖 actions. Hence, without partial-order reduction, the abstract local zone graph has at least 2 𝑛-1 nodes.

We

2 ( 1 , 1 ) 2 ( 2 , 2 )Figure 1 .

 2112221 Figure 1. A network of two processes. Timing constraints break the diamond formed by two independent actions.

( 2 , 2 )Figure 2 .

 222 Figure 2. Diamonds are recovered in local-time semantics. In the rightmost path the local times of the two process differ.

  Reachability and diamonds in local-time. Observe that every global run is a local-time run. Conversely, for every local-time run there is a trace equivalent global run. Lemma 1. [23] Let 𝑣, 𝑣 ′ be synchronized local valuations, and let (𝑞, 𝑣) 𝑢 (𝑞 ′ , 𝑣 ′ ) be a local run. Then there exists a global run (𝑞, 𝑣) 𝑤 (𝑞 ′ , 𝑣 ′ ) such that 𝑢 ∼ 𝑤.

Lemma 3 (

 3 Pre and post properties). For every network of timed automata and every action 𝑏: pre-property: If (𝑞, 𝑣) 𝑏 (𝑞 ′ , 𝑣 ′ ) and 𝑣 ∈ 𝑍 for some time-elapsed local-zone 𝑍 then (𝑞, 𝑍 ) 𝑏 = =⇒ (𝑞 ′ , 𝑍 ′ ) and 𝑣 ′ ∈ 𝑍 ′ for some local-zone 𝑍 ′ . post-property: If (𝑞, 𝑍 ) 𝑏 = =⇒ (𝑞 ′ , 𝑍 ′ ) and 𝑣 ′ ∈ 𝑍 ′ for localzones 𝑍, 𝑍 ′ , then (𝑞, 𝑣) 𝑏 (𝑞 ′ , 𝑣 ′ ) for some 𝑣 ∈ 𝑍 . Definition 2 (Local-zone graph LZG(N )). The local-zone graph LZG(N ) of a network N is a transition system whose nodes are of the form (𝑞, 𝑍 ) where 𝑞 is a state of the network, and 𝑍 is a local-zone. The initial node is (𝑞 0 , 𝑍 0 ) with 𝑍 0 = local-elapse(𝑉 0 ) where 𝑉 0 is the set of initial valuations and 𝑞 0 = 𝑞 𝑖𝑛𝑖𝑡 . The transitions are given by the symbolic transition relation (𝑞, 𝑍 ) 𝑏 = =⇒ (𝑞 ′ , 𝑍 ′ ).

  𝑏𝑎= =⇒ are feasible from (𝑞, 𝑍 )[START_REF] Minea | Partial order reduction for model checking of timed automata[END_REF]. Enabledness is however true at the level of configurations.

Definition 6 .

 6 A (time-abstract) simulation relation ≼ on the local semantics is a reflexive and transitive relation (𝑞, 𝑣) ≼ (𝑞, 𝑣 ′ ) between configurations having the same discrete state that satisfies two conditions: 1. for every local delay transition (𝑞, 𝑣) Δ --→ (𝑞, 𝑣 1 ), there exists a local delay Δ ′ such that (𝑞, 𝑣 ′ )

Definition 8 .

 8 A quasi-abstraction 𝔞 keeps runs if for every node (𝑞, 𝑍 ) in LZG(N ) that is reachable from the initial node, and every path (𝑞, 𝑍 ) 𝑢 = =⇒ (𝑞 𝑓 , 𝑍 𝑓 ) to the final state 𝑞 𝑓 there is a valuation 𝑣 ∈ 𝔞(𝑍 ) and a run (𝑞, 𝑣) 𝑢 (𝑞 𝑓 , 𝑣 𝑓 ).

2 Figure 4 .

 24 Figure 4. A network of two processes without a finite abstract zone graph that contains all runs.

Corollary 1 .

 1 An acyclic timed network N = ⟨𝐴 1 , . . . , 𝐴 𝑘 ⟩ is ( 𝑖=𝑘 𝑖=1 |𝑇 𝑖 |) × 𝑀 + 1-spread bounded where |𝑇 𝑖 | is the number of transitions in 𝐴 𝑖 , and 𝑀 is the maximum constant in N .

  the set {𝑡 𝑝 | 𝑝 ∈ Proc} of reference clocks. The other clock variables will store the local-time when the clock was last reset. Thus the value of 𝑡 𝑝 cannot be smaller than values of clocks of process 𝑝. More formally, a local valuation assigns a value, a real number, to each clock in 𝑋 ∪ 𝑋 𝑡 : LocalVal as 𝑋 and Proc will be clear from the context. Operations of clock reset for local valuations as well as local time elapse are defined accordingly, based on the interpretation given above. For a set of clocks 𝑅, let 𝑣 [𝑅] denote the local valuation obtained by resetting 𝑅 in 𝑣. That is: 𝑣 [𝑅] (𝑥) = 𝑣 (𝑡 𝑝 ) if 𝑥 ∈ 𝑅 ∩ 𝑋 𝑝 for some 𝑝 ∈ 𝑃𝑟𝑜𝑐, and 𝑣 [𝑅] (𝑥) = 𝑣 (𝑥) otherwise. For a tuple of non-negative reals

	𝑣 : (𝑋 ∪ 𝑋 𝑡 ) → R	provided 𝑣 (𝑡 𝑝 ) ≥ 𝑣 (𝑥) for 𝑥 ∈ 𝑋 𝑝
	With this intuition, the difference 𝑣 (𝑡 𝑝 ) -𝑣 (𝑥) gives the time
	since the last reset of clock 𝑥. This is what is considered as
	the value of 𝑥 in the standard semantics. In the local-time
	semantics we allow negative values for 𝑣 (𝑡 𝑝 ), 𝑣 (𝑥) since we
	will always work with the difference 𝑣 (𝑡 𝑝 ) -𝑣 (𝑥) and allow-
	ing for negative values offers some simplicity later while
	handling zones of local valuations. We use LocalVal(𝑋, Proc)
	for the set of local valuations, but mostly we will just write

  there is a tuple of 𝑏-transitions {(𝑞 𝑝 , 𝑏, 𝑔 𝑝 , 𝑅 𝑝 , 𝑞 ′ 𝑝 )} 𝑝 ∈dom(𝑏 ) such that: • states of involved processes change: 𝑞 𝑝 = 𝑞(𝑝), 𝑞 ′ 𝑝 = 𝑞 ′ (𝑝), if 𝑝 ∈ dom(𝑏), and 𝑞(𝑝) = 𝑞 ′ (𝑝) if 𝑝 ∉ dom(𝑏); • local times are synchronized: 𝑣 (𝑡 𝑝 1 ) = 𝑣 (𝑡 𝑝 2 ), for every 𝑝 1 , 𝑝 2 ∈ dom(𝑏); • guards are satisfied: 𝑣 ⊨ 𝑔 𝑝 , for every 𝑝 ∈ dom(𝑏); • resets are performed: 𝑣 ′ = 𝑣 [ 𝑝 ∈dom(𝑏 ) 𝑅 𝑝 ];

  that is destroyed by a subsumption. max({𝑣 (𝑡)} 𝑡 ∈𝑇 ). So catch-up delays only allow the processes that are behind in time to join the most advanced processes. Two local-time configurations (𝑞, 𝑣) and (𝑞 ′ , 𝑣 ′ ) are catch-up equivalent if the two can reach the same synchronized regions (i.e. Alur & Dill's regions[START_REF] Alur | A theory of timed automata[END_REF]) through catch-up delays and discrete transitions.

Proposition 2. The problem of deciding if two given configurations (𝑞, 𝑣), (𝑞 ′ , 𝑣 ′ ) of a given timed network are catch-up equivalent is Pspace-hard.

  𝑞 ′ with guard 𝑥 1 > 𝑐 ∧ 𝑥 2 ≤ 𝑑 and a reset {𝑥 1 }. Action 𝑏 is shared between processes 1 and 2. Suppose (𝑞, 𝑣) , 𝑣 1 ). Then 𝑣 (𝑡 1 ) = 𝑣 (𝑡 2 ), and 𝑣 satisfies the guard. Let 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ . We will see that (𝑞, 𝑣 ′ ) 𝑡 1 ) = 𝑣 ′ (𝑡 2 ) by the first item in the ≼ ★ 𝐿𝑈 definition. Next, we have 𝑣 (𝑡 1 -𝑥 1 ) > 𝑐 and 𝑣 (𝑡2 -𝑥 2 ) ≤ 𝑑. If 𝑣 (𝑡 1 -𝑥 1 ) ≤ 𝐿(𝑥 1 ), then 𝑣 ′ (𝑡 1 -𝑥 1 ) ≥ 𝑣 (𝑡 1 -𝑥 1 )by the second sub-item in the second condition; else 𝑣 ′ (𝑡 1 -𝑥 1 ) > 𝐿(𝑥 1 ) by third sub-item. Since 𝐿(𝑥 1 ) ≥ 𝑐, we get 𝑣 ′ (𝑡 1 -𝑥 1 ) > 𝑐 in both cases. Similarly, we can argue that 𝑣 ′ (𝑡 2 -𝑥 2 ) ≤ 𝑑 using the first sub-item with 𝑈 (𝑥 2 ). Moreover, after resetting 𝑥 1 , all conditions of ≼ ★ 𝐿𝑈 are still satisfied in the resulting valuations 𝑣 1 and 𝑣 ′ 1 . Theorem 4. Let N be an 𝐿𝑈 -network. The relation ≼ ★ 𝐿𝑈 is a strong-timed simulation on the local semantics of N . Definition 13. The abstraction operator 𝔞 ★ ≼𝐿𝑈 is defined as 𝔞 ★ ≼𝐿𝑈 (𝑊 ) := {𝑣 | 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ for some 𝑣 ′ ∈ 𝑊 } for every set of local valuations 𝑊 . This is the downward closure of 𝑊 with respect to the ≼ ★ 𝐿𝑈 relation. Theorem 5. For every LU-network N , the abstraction operator 𝔞 ★ ≼𝐿𝑈 is sound and complete. It also keeps runs. Unfortunately, despite this theorem we still miss two pieces to analyze timed networks with local semantics:

	𝑏 -→ (𝑞 1 𝑏 -→ (𝑞 1 , 𝑣 ′ 1 ) and 𝑣 1 ≼ ★ 𝐿𝑈 𝑣 ′ 1 . Firstly, we have
	𝑣 ′ (

★ 𝐿𝑈 (𝑞, 𝑣 ′ ) whenever 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ . The next theorem (proved in Appendix D) states that ≼ ★ 𝐿𝑈 relation is a strong-timed simulation on N . We illustrate the theorem on an example. Consider a transition 𝑞 𝑏 -→

  Definition 18. For a set of valuations𝑊 define spread 𝐷 (𝑊 ) to be {𝑣 ∈ 𝑊 | 𝑣 has spread 𝐷 }. The quasi-abstraction operator 𝔞 𝐷 ≼𝐿𝑈 is defined as 𝔞 𝐷 ≼𝐿𝑈 (𝑊 ) := 𝔞 ★ ≼𝐿𝑈 (spread 𝐷 (𝑊 )) for every set of valuations 𝑊 . Theorem 7. Quasi-abstraction 𝔞 𝐷 ≼𝐿𝑈 is sound, complete, finite, and keeps runs for 𝐷-spread networks. The inclusion 𝔞 𝐷 ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 𝐷 ≼𝐿𝑈 (𝑍 ′ ) can be checked in time O (|𝑋 ∪ 𝑋 𝑡 | 2 ) for time-elapsed local-zones 𝑍, 𝑍 ′ . Proof. Soundness follows from Lemma 4. We now show that 𝔞 𝐷 ≼𝐿𝑈 keeps runs. Consider a 𝐷-spread network N and a node (𝑞, 𝑍 ) reachable from the initial node in LZG(N ): there exists a path (𝑞 0 , 𝑍 0 ) 𝑞 𝑓 , 𝑍 𝑓 ) be a path to a final state. By post-property there is a local run (𝑞 0 , 𝑣 0 ) 𝑓 , 𝑣 𝑓 ) with 𝑣 0 ∈ 𝑍 0 , 𝑣 ∈ 𝑍 and 𝑣 𝑓 ∈ 𝑍 𝑓 . Since N is 𝐷-spread we can assume 𝑣 ∈ spread 𝐷 (𝑍 ), and hence by Definition 18 we have 𝑣 ∈ 𝔞 𝐷 ≼𝐿𝑈 (𝑍 ). This proves that 𝔞 𝐷 ≼𝐿𝑈 keeps runs, as per Definition 8. Lemma 6 then entails that 𝔞 𝐷 ≼𝐿𝑈 is complete. By using the inclusion test from Theorem 6, we show that an order between zones defined as 𝑍 ≼ 𝑍 ′ if 𝔞 𝐷 ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 𝐷 ≼𝐿𝑈 (𝑍 ′ ) is a well-quasi order (Lemma 14 in Appendix F.1). This proves finiteness of 𝔞 𝐷 ≼𝐿𝑈 . Complexity of the inclusion test is discussed in Lemma 13 of Appendix F. Since the local-zone graph has only time-elapsed zones, it is sufficient to consider such zones for the inclusion test. □

	𝑢 ′
	𝑢 ′
	(𝑞, 𝑣)

= =⇒ (𝑞, 𝑍 ). Let (𝑞, 𝑍 ) 𝑢 = =⇒ (𝑢 (𝑞

  1,𝑠𝑟𝑐 𝑛 ) are those accessible by paths 𝑠𝑏 1 . . . 𝑏 𝑖 for 0 ≤ 𝑖 < 𝑛 and by 𝑠𝑏 1 . . . 𝑏 𝑖 𝑠𝑏 1 . . . 𝑏 𝑗 where 0 ≤ 𝑖 < 𝑛 and 0 ≤ 𝑗 < 𝑖. The covered nodes are the ones accessible by paths 𝑠𝑏 1 . . . 𝑏 𝑛 and by 𝑠𝑏 1 . . . 𝑏 𝑖 𝑠𝑏 1 . . . 𝑏 𝑗 𝑠 where 0 ≤ 𝑖 < 𝑛, 0 ≤ 𝑗 ≤ 𝑖. This gives an O (𝑛 2 ) bound on the number of nodes present in LZG 1,𝑠𝑟𝑐

	𝐿𝑈	(N + 𝑛 ) the abstract local-zone graph
	over the 𝔞 𝐷 ≼𝐿𝑈 operator with 𝐷 = 1. The uncovered nodes in LZG 1,𝑠𝑟𝑐 𝐿𝑈 (N +
	𝐿𝑈

  step is trivial. The induction step is easy if (𝑞 𝑖 , 𝑍 𝑖 ) is uncovered in LZG 𝔞,src (N ). In this case, let 𝑏 be the first letter of 𝑤 𝑖 : 𝑤 𝑖 = 𝑏𝑤 𝑖+1 . We have (𝑞 𝑖 , 𝑍 𝑖 ) 𝑞 𝑖+1 , 𝑍 𝑖+1 ) and 𝑏 ∈ src(𝑞 𝑖 , enabled(𝑍 𝑖 )). Hence taking 𝑢 𝑖+1 = 𝑢 𝑖 𝑏 and 𝑤 𝑖+1 we obtain the induction step.It remains to check what happens when(𝑞 𝑖 , 𝑍 𝑖 ) is covered in LZG 𝔞,src (N ). Say (𝑞 𝑖 , 𝑍 𝑖 ) is subsumed by (𝑞 𝑖 , 𝑍 ′ 𝑖 ), meaning 𝔞(𝑍 𝑖 ) ⊆ 𝔞(𝑍 ′ 𝑖 ). Since (𝑞 𝑖 , 𝑍 𝑖 ) 𝑤 𝑖 = =⇒ (𝑞 𝑛 , 𝑍𝑖 𝑛 ) and 𝔞 keeps runs, there exists a valuation 𝑣 𝑖 ∈ 𝔞(𝑍 𝑖 ) and an execution (𝑞 𝑖 , 𝑣 𝑖 ) 𝑞 𝑛 , 𝑣 𝑛 ). From 𝔞(𝑍 𝑖 ) ⊆ 𝔞(𝑍 ′ 𝑖 ), we have 𝑣 𝑖 ∈ 𝔞(𝑍 ′ 𝑖 ). Secondly, as 𝔞 is simulation based, there exists 𝑣 ′ 𝑖 ∈ 𝑍 ′ 𝑖 such that 𝑣 𝑖 ≼ 𝑣 ′ 𝑖 , where ≼ is the simulation on which 𝔞 is based on. Hence we also have an execution (𝑞 𝑖 , 𝑣 ′ 𝑖 ) Since 𝑤 𝑖 is a path reaching a final state, and src function is trace faithful, there is a source path (𝑞 𝑖 , 𝑍 ′ 𝑖) ) with 𝑤 𝑖 ∼ 𝑤 ′ 𝑖 . In particular, |𝑤 𝑖 | = |𝑤 ′ 𝑖 |.Let 𝑏 be the first letter of 𝑤 ′ 𝑖 , i.e., 𝑤 ′ 𝑖 = 𝑏𝑤 𝑖+1 . We claim that 𝑢 𝑖+1 = 𝑢 𝑖 𝑏 and 𝑤 𝑖+1 satisfy the induction conditions. The path 𝑢 𝑖 𝑏 contains a subsumption edge. This first means that all processes in dom(𝑏) are synchronized in 𝑣, that is, 𝑣 (𝑡 𝑝 -𝑡 𝑞 ) = 0 for all 𝑡 𝑝 , 𝑡 𝑞 ∈ dom(𝑏). From the first item of Definition 12, we have 𝑣 ′ (𝑡 𝑝 -𝑡 𝑞 ) = 0 as well, for 𝑝, 𝑞 ∈ dom(𝑏). Hence the processes in dom(𝑏) are synchronized in 𝑣 ′ too. Next, from the definition of the local step (𝑞, 𝑣) 𝑞 1 , 𝑣 1 ), there is a tuple of 𝑏-transitions {(𝑞 𝑝 , 𝑔 𝑝 , 𝑅 𝑝 , 𝑞 ′ 𝑝 )} 𝑝 ∈dom(𝑏 ) such that 𝑣 |= 𝑔 𝑝 for all 𝑝 ∈ dom(𝑝). Since 𝑏 is enabled at 𝑣, valuation 𝑣 satisfies all the constraints occurring in all the guards 𝑔 𝑝 . We will now show that 𝑣 ′ satisfies all these constraints by invoking the second item of Definition 12.Since N is an 𝐿𝑈 -network, for every 𝑥 ⋖ 𝑐 (resp. 𝑦 ⋗ 𝑑) occurring in the tuple, we have 𝑐 ≤ 𝑈 (𝑥) (resp. 𝑑 ≤ 𝐿(𝑦)). Consider a constraint 𝑥 ⋖ 𝑐 from some 𝑔 𝑝 . As 𝑣 (𝑡 𝑝 -𝑥) ⋖ 𝑐, we have 𝑣 (𝑡 𝑝 -𝑥) ≤ 𝑈 𝑥 . Hence 𝑣 ′ (𝑡 𝑝 -𝑥) ≤ 𝑣 (𝑡 𝑝 -𝑥) from the first sub-item. This implies 𝑣 ′ (𝑡 𝑝 -𝑥) ⋖ 𝑐. Consider a constraint 𝑦 ⋗ 𝑑. As 𝑣 |= 𝑦 ⋗ 𝑑, we have 𝑣 (𝑡 𝑝 -𝑦) ⋗ 𝑑. If 𝑣 (𝑡 𝑝 -𝑦) ≤ 𝐿 𝑦 , then 𝑣 ′ (𝑡 𝑝 -𝑦) ≥ 𝑣 (𝑡 𝑝 -𝑦) from the second sub-item. This implies 𝑣 ′ |= 𝑦 ⋗ 𝑑. Otherwise, from the third sub-item, 𝑣 ′ (𝑡 𝑝 -𝑦) > 𝐿 𝑦 ≥ 𝑑, which again implies that𝑣 ′ |= 𝑦 ⋗ 𝑑.Therefore there is a transition (𝑞, 𝑣 ′ ) It remains to show that𝑣 1 ≼ ★ 𝐿𝑈 𝑣 ′ 1 . Since the transition 𝑏 is instantaneous, 𝑣 1 (𝑡 𝑝 -𝑡 𝑞 ) = 𝑣 (𝑡 𝑝 -𝑡 𝑞 ) and 𝑣 ′ 1 (𝑡 𝑝 -𝑡 𝑞 ) = 𝑣 ′ (𝑡 𝑝 -𝑡 𝑞 ) for all 𝑝, 𝑞. As 𝑣 (𝑡 𝑝 -𝑡 𝑞 ) = 𝑣 ′ (𝑡 𝑝 -𝑡 𝑞 ) we get 𝑣 1 (𝑡 𝑝 -𝑡 𝑞 ) = 𝑣 ′ 1 (𝑡 𝑝 -𝑡 𝑞 ) for all 𝑝, 𝑞 ∈ Proc.This gives the first item in the ≼ ★ 𝐿𝑈 definition. Secondly, notice that 𝑣 1 = [𝑅]𝑣 and 𝑣 ′ 1 = [𝑅]𝑣 ′ . Therefore, for all clocks 𝑥 ∉ 𝑅, the second item is already satisfied for valuations 𝑣 1 and 𝑣 ′ 1 . For all 𝑥 ∈ 𝑅, we have 𝑣 1 (𝑡 𝑝 -𝑥) = 𝑣 ′ 1 (𝑡 𝑝 -𝑥) = 0, when 𝑥 ∈ 𝑋 𝑝 . Hence the second item is true for such clocks as well. □ ▶ Theorem 5. For every LU-network N , the abstraction operator 𝔞 ★ ≼𝐿𝑈 is sound and complete. It also keeps runs. Proof. Soundness and completeness follow from Lemmas 4, 5. Since 𝑍 ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ), the abstraction also keeps runs. Proof. The left-to-right direction is immediate since 𝑍 ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ). For the right-to-left direction, suppose 𝑍 ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ). Pick 𝑣 ∈ 𝔞 ★ ≼𝐿𝑈 (𝑍 ). There exists 𝑣 1 ∈ 𝑍 such that 𝑣 ≼ ★ 𝐿𝑈 𝑣 1 . From 𝑍 ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ), we have 𝑣 1 ∈ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ), and hence there is 𝑣 ′ 1 ∈ 𝑍 ′ such that 𝑣 1 ≼ ★ 𝐿𝑈 𝑣 ′ 1 . This also implies that 𝑣 ≼ ★

	𝑤 𝑖 --→ (𝑤 𝑖 --→ (𝑞 𝑛 , 𝑣 ′ 𝑛 ). By pre-property of zones (𝑞 𝑖 , 𝑍 ′ 𝑖 ) 𝑤 ′ 𝑖 = = ⇒ (𝑞 𝑛 , 𝑍 ′ 𝑛 ) in LZG(N Proof. It is easy to see that ≼ ★ 𝐿𝑈 is reflexive and transitive. Moreover, notice that if 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ then (𝑣 + Δ) ≼ ★ 𝐿𝑈 (𝑣 ′ +Δ) for	and hence 𝑣 ∈ 𝔞 ★ ≼𝐿𝑈 (𝑍 ). E.1 Representing local zones	𝑏 --→ (𝑏 --→ (𝑞 1 , 𝑣 ′ 1 ). 𝐿𝑈 𝑣 ′ 1 , □
	every local delay Δ. Hence ≼ ★ 𝐿𝑈 is a reflexive and transitive	Local zones can be represented using Difference Bound Ma-
	relation that satisfies condition (1) required for a simulation	trices (DBMs). For our analysis, we will make use of a graph
	as in Definition 6.	representation of local zones, called distance graphs. A dis-
	We now show condition (2). Let 𝑣 ≼ ★ 𝐿𝑈 𝑣 ′ and suppose	tance graph has vertices 𝑋 ∪𝑋
	(𝑞, 𝑣)

𝑏 = =⇒ (𝑤 𝑖 = = ⇒ (𝑞 𝑛 , 𝑍 ′ 𝑛 ) in LZG(N ). □ D Appendix for Section 6 ▶ Theorem 4. Let N be an 𝐿𝑈 -network. The relation ≼ ★ 𝐿𝑈 is a strong-timed simulation on the local semantics of N . 𝑏 --→ (𝑞 1 , 𝑣 1 ). □ E Appendix for Section 6.1 ▶ Lemma 7. For every pair of zones 𝑍, 𝑍 ′ : 𝔞 ★ ≼𝐿𝑈 (𝑍 ) ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) iff 𝑍 ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ). 𝑡 . For every 𝑥, 𝑦 ∈ 𝑋 ∪𝑋 𝑡 there is an edge 𝑥 → 𝑦 with a weight is either (<, ∞) or of the form (⋖, 𝑐) with 𝑐 ∈ R and ⋖ standing for ≤ or <. The edge 𝑥 (⋖,𝑐 )

  In the latter case, we can replace 𝑥 → 𝑡 𝑞 → 𝑦 with the 𝐻 𝑣 edge 𝑥 → 𝑦 and get a negative cycle 𝑥 ( ≤,𝑣 (𝑡 𝑞 -𝑥 ) )+(<,-𝐿 𝑦 )

  → 𝑦 Let 𝑍, 𝑍 ′ be non-empty local zones. We have 𝑍 ⊈ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ ) iff there exist two variables 𝑥, 𝑦 ∈ 𝑋 ∪ 𝑇 such that • 𝑍 ′ 𝑦𝑥 < 𝑍 𝑦𝑥 , and • if 𝑥 ∈ 𝑋 𝑝 for some process 𝑝, then (≤, 𝑈 𝑥 ) + 𝑍 𝑡 𝑝 𝑥 ≥ (≤ , 0), and • if 𝑦 ∈ 𝑋 𝑞 for some process 𝑞, then (<, -𝐿 𝑦 ) + 𝑍 ′ 𝑦𝑥 < 𝑍 𝑡 𝑞 𝑥 .

	𝑍 ′ 𝑦𝑥 ---→ 𝑥. This finally
	gives us a negative cycle in the required form.	□
	▶ Theorem 6.

  1 have non-negative weight. Therefore, weight of 𝑠 → 𝑥 in 𝐺 * 1 is 𝑍 𝑠𝑥 . Step 2. Suppose 𝑍 𝑦𝑥 = (⋖ 𝑦𝑥 , 𝑐 𝑦𝑥 ) and 𝑍 𝑡 𝑞 𝑥 = (⋖ 𝑡 𝑞 𝑥 , 𝑐 𝑡 𝑞 𝑥 ), where 𝑞 is the process clock of 𝑦. Define 𝜂 𝑦𝑥 = 𝑐 𝑦𝑥 if ⋖ 𝑦𝑥 equals ≤, otherwise 𝜂 𝑦𝑥 = 𝑐 𝑦𝑥 -0.5. Since 𝑍 ′ 𝑦𝑥 < 𝑍 𝑦𝑥 and 𝑍 ′ gives 𝔞 0 ≼𝐿𝑈 (𝑍 𝑠𝑢 1 𝑠𝑢 2 𝑠 ) ⊆ 𝔞 0 ≼𝐿𝑈 (𝑍 𝑠𝑢 2 𝑠 ) and 𝔞 0 ≼𝐿𝑈 (𝑍 𝑠𝑏 1 𝑏 2 ...𝑏 𝑛 ) ⊆ 𝔞 0 ≼𝐿𝑈 (𝑍 0 ). Now consider 𝑣 𝑠𝑢 where 𝑢 ≠ 𝑏 1 𝑏 2 . . . 𝑏 𝑛 . Valuation 𝑣 𝑠𝑢 can neither be simulated by 𝑣 𝑠𝑢 ′ nor any of its time successors, when 𝑢 ′ ≠ 𝑢. Similarly, valuation 𝑣 𝑠𝑢 cannot be simulated by valuations of the form 𝑣 𝑠𝑢 1 𝑠 or its time successors. Therefore, 𝑍 𝑠𝑢 cannot be subsumed by any node of the form 𝑍 𝑠𝑢 ′ or 𝑍 𝑠𝑢 1 𝑠 . An analogous reasoning gives that 𝑍 𝑠𝑢 1 𝑠𝑢 2 cannot be subsumed by zones 𝑍 𝑠𝑢 , 𝑍 𝑠𝑢𝑠 , 𝑍 𝑠𝑢 ′ 1 𝑠𝑢 , 𝑍 𝑠𝑢 1 𝑠𝑢 ′ 2 where 𝑢 1 ≠ 𝑢 ′ 1 and 𝑢 2 ≠ 𝑢 ′ 2 .

  now look at what happens with partial-order reduction. Here is a trace-faithful source function: at (𝑝, 𝑍 𝜎 ) the source function gives 𝑠, the 𝑏 𝑖 with the least index that is enabled at 𝑍 𝜎 and the $ action if it is enabled. Observe that enabled(𝑍 𝑠𝑢 ) = {𝑠} ∪ {𝑏 𝑖 | 𝑖 ∉ 𝑢} ∪ {$ | if 𝑢 is empty} and enabled(𝑍 𝑠𝑢 1 𝑠𝑢 2 ) = {𝑠} ∪ {𝑏 𝑖 | 𝑖 ∈ 𝑢 1 , 𝑖 ∉ 𝑢 2 }. Therefore, at 𝑍 𝑠𝑢 the source function picks the smallest 𝑏 𝑖 that is not present in 𝑢, and at𝑍 𝑠𝑢 1 𝑠𝑢 2 it picks the smallest 𝑏 𝑖 that is present in 𝑢 1 , but not yet in 𝑢 2 .The zone graph for four processes, LZG 0,𝑠𝑟𝑐 𝐿𝑈 (N + 4 ) is depicted in Figure5. In the general case, the uncovered nodes in LZG 0,𝑠𝑟𝑐 𝑛 ) are 𝑠𝑏 1 . . . 𝑏 𝑖 for 0 ≤ 𝑖 < 𝑛 and 𝑠𝑏 1 . . . 𝑏 𝑖 𝑠𝑏 1 . . . 𝑏 𝑗 where 0 ≤ 𝑖 < 𝑛 and 0 ≤ 𝑗 < 𝑖. The covered nodes are 𝑠𝑏 1 . . . 𝑏 𝑛 (since 𝑣 𝑠𝑏 1 ...𝑏 𝑛 ≼ ★ 𝐿𝑈 𝑣 0 ) and 𝑠𝑏 1 . . . 𝑏 𝑖 𝑠𝑏 1 . . . 𝑏 𝑗 𝑠 where 0 ≤ 𝑖 < 𝑛, 0 ≤ 𝑗 ≤ 𝑖. This gives an O (𝑛 2 ) bound on the number of nodes present in LZG 0,𝑠𝑟𝑐 Figure 5. Illustration of the abstract local zone graph LZG 0,𝑠𝑟𝑐 𝐿𝑈 (N + 4 ). The label of the node reached after a sequence 𝜎 represents the value of 𝑥 1 , 𝑥 2 , 𝑥 3 , 𝑥 4 in the valuation 𝑣 𝜎 . Covered nodes are shown in blue. Nodes 𝑠𝑢 1 𝑠𝑢 2 𝑠 are covered by 𝑠𝑢 2 𝑠 and node 𝑠𝑏 1 𝑏 2 𝑏 3 𝑏 4 is covered by the initial node. Subsumption edges have not been shown explicitly.

		𝑠
	𝑠	𝑠	$
		𝑏 1
	𝑠	𝑠
	𝑏 1	𝑏 2
	𝑠		𝑠	𝑠
		𝑏 3	𝑏 1
	𝑠	𝑠		𝑠
	𝑏 1	𝑏 4	𝑏 2
				𝑠
	𝑠
	𝑏 2
	𝑠
	𝑏 3
	𝑠
	LZG 0,𝑠𝑟𝑐 𝐿𝑈 ( N + 4 )

𝐿𝑈

(N + 𝐿𝑈 (N + 𝑛 ).

all the constraints given by 𝐺. To reason about cumulative constraints of a path in this graph representation, we define an arithmetic over weights:

Order. for 𝑐 1 , 𝑐 2 ∈ R, we say (⋖ 1 , 𝑐 1 ) < (⋖ 2 , 𝑐 2 ) if 𝑐 1 < 𝑐 2 , or 𝑐 1 = 𝑐 2 , ⋖ 1 is < and ⋖ 2 is ≤; secondly, we have (⋖, 𝑐) < (<, ∞) for every 𝑐 ∈ R, Addition. for 𝑐 1 , 𝑐 2 ∈ R, we have (⋖ 1 , 𝑐 1 ) + (⋖ 2 , 𝑐 2 ) to be equal to (⋖, 𝑑) where 𝑑 = 𝑐 1 + 𝑐 2 and ⋖ is < if one of ⋖ 1 or ⋖ 2 is <, and ⋖ is ≤ otherwise; secondly, (⋖, 𝑐) + (<, ∞) is defined to be (<, ∞) for every weight (⋖, 𝑐).

The addition allows us to define the weight of a path in a distance graph, as the sum of weights of the edges. A distance graph is canonical if for all pairs of vertices 𝑥 ≠ 𝑦, the smallest weight of a path from 𝑥 to 𝑦 is given by the weight of the edge 𝑥 -→ 𝑦. Given two distance graphs 𝐺 1 , 𝐺 2 we define min(𝐺 1 , 𝐺 2 ) to be the graph obtained by replacing the weight of every edge by the minimum of the corresponding weights from 𝐺 1 and 𝐺 2 . Finally, we will often reason about cycles in a distance graph. A cycle in a distance graph is positive if the sum of the weights of its edges is greater than or equal to (≤, 0). Otherwise, it is negative. It is well-known that [[𝐺]] is non-empty iff there are no negative cycles in 𝐺.

We end this section with an observation about the local zones present in the local zone graph. This says that each local zone in the local zone graph can be described by difference constraints that use only integers. Lemma 10. Let N be a network. For every node (𝑞, 𝑍 ) in LZG(N ), the canonical distance graph of 𝑍 has weight either (<, ∞) or (⋖, 𝑐) with 𝑐 ∈ Z, in each of its edges.

Proof. This is true of the initial zone. We show that this property is preserved during successor computation.

Suppose 𝐺 1 , 𝐺 2 are distance graphs with only integral weights. Then their intersection min(𝐺 1 , 𝐺 2 ) will have only integral weights since the canonicalization procedure only adds weights. This observation is sufficient to show the required property since each operation in the successor computation either involves removing edges or doing the intersection as above. □

E.2 Steps to the final test

For convenience of presentation, we define two sets of clocks for a given local valuation 𝑣:

Notice that the reference clocks 𝑇 are present in both 𝐿 -bounded(𝑣) and 𝑈 -bounded(𝑣).

Define

For the second item of Definition 12 take some process 𝑝 and a clock 𝑥 ∈ 𝑋 𝑝 . We have three conditions to check.

For the first condition, suppose 𝑣 (𝑡 𝑝 -𝑥) ≤ 𝑈 𝑥 . The edge 𝑥 → 𝑡 𝑝 gives the constraint (≤, 𝑣 (𝑡 𝑝 -𝑥)) in 𝐻 𝑣 since 𝑥 is 𝑈 -bounded in 𝑣, and 𝑡 𝑝 is 𝐿-bounded in 𝑣. As 𝑣 ′ satisfies this constraint, we get the desired 𝑣 ′ (𝑡 𝑝 -𝑥) ≤ 𝑣 (𝑡 𝑝 -𝑥).

For the second condition, suppose 𝑣 (𝑡 𝑝 -𝑥) ≤ 𝐿 𝑥 . The edge 𝑡 𝑝 → 𝑥 has weight 𝑣 (𝑥 -𝑡 𝑝 ). Thus 𝑣 ′ satisfies 𝑣 ′ (𝑥 -𝑡 𝑝 ) ≤ 𝑣 (𝑥 -𝑡 𝑝 ) equivalent to the required 𝑣 ′ (𝑡 𝑝 -𝑥) ≥ 𝑣 (𝑡 𝑝 -𝑥).

The third condition assumes 𝑣 (𝑡 𝑝 -𝑥) > 𝐿 𝑥 . We have two cases. The first one is when 𝐿 𝑥 ≠ -∞. In this case the weight of the edge 𝑡 𝑝 → 𝑥 is (≤, 𝑣 (𝑡 𝑝 -𝑡 𝑝 )) + (<, -𝐿 𝑥 ). So 𝑣 ′ (𝑥 -𝑡 𝑝 ) satisfies (<, -𝐿 𝑥 ), giving 𝑣 ′ (𝑡 𝑝 -𝑥) > 𝐿 𝑥 . The second case is when 𝐿 𝑥 = -∞. The constraint on the edge 𝑡 𝑝 → 𝑥 is 0, giving the constraint 𝑣 ′ (𝑡 𝑝 -𝑥) ≥ 0. This constraint always holds as 𝑣 ′ is a local valuation.

Proving ⟨𝑣⟩ ★ ⊆ [[𝐻 𝑣 ]]: Pick 𝑣 ′ ∈ ⟨𝑣⟩ ★ . We will show that 𝑣 ′ satisfies every edge constraint 𝑥 → 𝑦 in 𝐻 𝑣 . Let us start with the case when 𝑥 is a process clock in 𝑋 𝑝 and 𝑦 is a process clock in 𝑋 𝑞 . Then, rewrite 𝑣 ′ (𝑦 -𝑥) as:

We restrict to the situation when 𝑥 ∈ 𝑈 -bounded(𝑣), because if not, the constraint 𝑥 → 𝑦 in 𝐻 𝑣 is (<, ∞). We now make some conclusions from the definition of ≼ ★ 𝐿𝑈 preorder. Since 𝑥 ∈ 𝑈 -bounded(𝑣), we have 𝑣 ′ (𝑡 𝑝 -𝑥) ≤ 𝑣 (𝑡 𝑝 -𝑥). Further, we have 𝑣 ′ (𝑡 𝑞 -𝑡 𝑝 ) = 𝑣 (𝑡 𝑞 -𝑡 𝑝 ). Therefore:

When 𝑦 ∈ 𝐿 -bounded(𝑣), we have 𝑣 ′ (𝑡 𝑞 -𝑦) ≥ 𝑣 (𝑡 𝑞 -𝑦) from Definition 12. Hence 𝑣 ′ (𝑦 -𝑡 𝑞 ) ≤ 𝑣 (𝑦 -𝑡 𝑞 ). Plugging this to [START_REF] Parosh | Source sets: A foundation for optimal dynamic partial order reduction[END_REF] gives gives 𝑣 ′ (𝑦 -𝑥) ≤ 𝑣 (𝑦 -𝑥). Hence the 𝑥 → 𝑦 constraint of 𝐻 𝑣 is satisfied. When 𝑦 ∉ 𝐿 -bounded(𝑣) and 𝐿 𝑦 ≠ -∞, we have 𝑣 ′ (𝑡 𝑞 -𝑦) > 𝐿 𝑦 , which gives 𝑣 ′ (𝑦 -𝑡 𝑞 ) < -𝐿 𝑦 . Plugging this to [START_REF] Parosh | Source sets: A foundation for optimal dynamic partial order reduction[END_REF] gives 𝑣 ′ (𝑦 -𝑥) < -𝐿 𝑦 + 𝑣 (𝑡 𝑞 -𝑥). Hence 𝑣 ′ satisfies the constraint when the edge weight comes from the second item. When 𝐿 𝑦 = -∞, we still have a trivial constraint that 𝑣 ′ (𝑡 𝑞 -𝑦) ≥ 0 as 𝑣 ′ is a local valuation. This can be rewritten as 𝑣 ′ (𝑦 -𝑡 𝑞 ) ≤ 0. Plugging this in [START_REF] Parosh | Source sets: A foundation for optimal dynamic partial order reduction[END_REF] gives 𝑣 ′ (𝑦 -𝑥) ≤ 𝑣 (𝑡 𝑞 -𝑥), therefore satisfying the 𝑥 → 𝑦 edge constraint when the weight comes from the third item.

When 𝑥 is a reference clock, the third term of (1) is 0. When 𝑦 is a reference clock, the first term of (1) is 0. The rest of the argument follows similarly.

Proving that 𝐻 𝑣 is in canonical form. To show that 𝐻 𝑣 is canonical, we will show that the weight of 𝑥 → 𝑦 is smaller than or equal to weight of the path 𝑥 → 𝑠 → 𝑦 for every variable 𝑠. When 𝑥 ∉ 𝑈 -bounded(𝑣), edge 𝑥 → 𝑠 has weight (<, ∞) and the claim is trivially true. Similarly, if 𝑠 ∉ 𝑈 -bounded(𝑣), the claim is true as 𝑠 → 𝑦 has weight (<, ∞). Let us therefore assume 𝑥, 𝑠 ∈ 𝑈 -bounded(𝑣).

Suppose to the contrary that the sum of constraints on 𝑥 → 𝑠 → 𝑦 is strictly smaller than the constraint on 𝑥 → 𝑦. Let 𝑤 𝑥→𝑠 stand for the constraint on the edge 𝑥 → 𝑠.

Once again this simplifies to 𝑤 𝑥→𝑠 < (≤, 𝑣 (𝑠 -𝑥)). The same happens when 𝐿 𝑦 = -∞.

It remains to show that

, then there is a negative cycle in 𝐻 min . This gives the right-to-left direction of the proposition. We will now show the left-toright direction.

Suppose ⟨𝑣⟩ ★ ∩ 𝑍 ′ is empty. Then 𝐻 min has a negative cycle 𝑁 . Note that some of the edges of 𝐻 min come from 𝐻 𝑣 and the others come from 𝐻 𝑍 ′ . We will now reduce 𝑁 to the form given in the right-hand-side of the proposition.

Step 1. Since 𝐻 𝑣 and 𝐻 𝑍 ′ are canonical, we can replace consecutive edges 𝑥 → 𝑦 → 𝑢 coming from the same graph with the edge 𝑥 → 𝑢 from that graph. Hence we can assume that the edges in 𝑁 alternate between edges from 𝐻 𝑣 and 𝐻 𝑍 ′ .

Step 2. We transform 𝑁 so that every edge coming from 𝐻 𝑣 has a weight given by either Item 1 or 2 of Definition 19. Clearly Item 4 does not apply as the sum of weights in 𝑁 is a finite negative value, and hence we cannot have edges with (<, ∞) weight in 𝑁 . Suppose there is an edge 𝑥 → 𝑦 falling under Item 3. This edge can be replaced with the sequence 𝑥 → 𝑡 𝑞 → 𝑦 from 𝐻 𝑣 with weight (≤, 𝑣 (𝑡 𝑞 -𝑥)) to edge 𝑥 → 𝑡 𝑞 (due to Item 1) and weight (≤, 0) to edge 𝑡 𝑞 → 𝑦 (due to Item 3). The weight of the edge 𝑡 𝑞 → 𝑦 in 𝐻 𝑍 ′ is lesser than or equal to (≤, 0): this is because in local valuations the value of the corresponding reference clock is always greater than or equal to the value of a process clock, hence 𝑡 𝑞 ≥ 𝑦 in all valuations of 𝑍 ′ , reflecting that 𝑦 -𝑡 𝑞 ≤ 0. Therefore replacing the edge 𝑡 𝑞 → 𝑦 in 𝑁 with the corresponding edge from 𝐻 𝑍 ′ gives another negative cycle with weight at most that of 𝑁 . This way we remove all edges coming from Item 3. Eventually, we apply once again Step 1 to collapse consecutive edges from 𝑍 ′ , so we have a cycle 𝑁 with edges alternating between those of 𝐻 𝑣 and 𝐻 𝑍 ′ .

Step 3. Consider an edge 𝑥 → 𝑦 in 𝑁 coming from 𝐻 𝑣 and having weight due to Item 2, that is, 𝑥 ∈ 𝑈 -bounded(𝑣) , 𝑦 ∉ 𝐿 -bounded(𝑣) and 𝐿 𝑦 ≠ -∞. The weight of the edge is (≤, 𝑣 (𝑡 𝑞 -𝑥)) + (<, -𝐿 𝑦 ), where 𝑡 𝑞 is the reference clock of 𝑦.

Replace this edge with two edges 𝑥

------→ 𝑦, both from 𝐻 𝑣 . This keeps the same value of the negative cycle. Perform this change for every edge coming from Item 2. We now have a negative cycle 𝑁 where blocks of edges alternate between 𝐻 𝑣 and 𝐻 𝑍 ′ : each 𝐻 𝑣 block either has a single edge 𝑥 → 𝑦 with weight (≤, 𝑣 (𝑦 -𝑥)) from Item 1, or two edges 𝑥 → 𝑡 𝑞 → 𝑦 with 𝑥 → 𝑡 𝑞 having weight (≤, 𝑣 (𝑡 𝑞 -𝑥)) from Item 1, and 𝑡 𝑞 → 𝑦 having weight (<, -𝐿 𝑦 ) from Item 2.

Step 4. Suppose 𝑁 has two 𝐻 𝑣 edges 𝑥 1 → 𝑦 1 and 𝑥 2 → 𝑦 2 with weights 𝑢 1 := (≤, 𝑣 (𝑦 1 -𝑥 1 )) and 𝑢 2 := (≤, 𝑣 (𝑦 2 -𝑥 2 )) due to Item 1. Therefore, 𝑥 1 , 𝑥 2 ∈ 𝑈 -bounded(𝑣) and 𝑦 1 , 𝑦 2 ∈ 𝐿 -bounded(𝑣). Let 𝑤 1 be the weight of the path in 𝑁 from 𝑦 1 to 𝑥 2 and 𝑤 2 the weight from 𝑦 2 to 𝑥 1 . The cycle 𝑁 can be broken into four parts as depicted below:

From Definition 19, the weights of edges 𝑥 1 → 𝑦 2 and 𝑥 2 → 𝑦 1 come due to Item 1. Let the weight of the edge

Expanding this inequality, we get:

) on both sides gives 𝑤 1 + (≤, 𝑣 (𝑦 1 -𝑥 2 )) < (≤, 0). As mentioned in the beginning of this paragraph, we know that the weight of the edge

with the last edge 𝑥 2 → 𝑦 1 from 𝐻 𝑣 . In both the cases, we replace has integer weights, we also have 𝑍 ′ 𝑦𝑥 < (≤, 𝜂 𝑦𝑥 ). Similarly, define 𝜂 𝑡 𝑝 𝑥 . From the third item of the rhs, we have (<, -𝐿 𝑦 )+ 𝑍 ′ 𝑦𝑥 < (≤, 𝜂 𝑡 𝑞 𝑥 ).

Let 𝐺 2 be the distance graph obtained from 𝐺 * 1 by replacing 𝑥 → 𝑦 with (≤, -𝜂 𝑦𝑥 ) and 𝑥 → 𝑡 𝑞 with (≤, -𝜂 𝑡 𝑞 𝑥 ). This gives the set of valuations simultaneously satisfying 𝑣 (𝑦 -𝑥) ≤ -𝜂 𝑦𝑥 and 𝑣 (𝑡 𝑞 -𝑥) ≤ -𝜂 𝑡 𝑞 𝑥 . If indeed [[𝐺 2 ]] is non-empty and there is such a valuation 𝑣, then we are done: we will have (≤, 𝑣 (𝑦 -𝑥)) + 𝑍 ′ 𝑦𝑥 < (≤, 0) and (≤, 𝑣 (𝑡 𝑞 -𝑥)) + (<, -𝐿 𝑦 ) + 𝑍 ′ 𝑦𝑥 < (≤, 0). Notice that the value of 𝐻 𝑣 𝑥 𝑦 comes from either case 1 or 2 of Definition 19. Hence we get 𝐻 𝑣 𝑥 𝑦 +𝑍 ′ 𝑦𝑥 < (≤, 0). It remains to show that 𝐺 2 has no negative cycles. The only two edges that are modified from 𝐺 * 1 are 𝑥 → 𝑦 and 𝑥 → 𝑡 𝑞 . If there is a negative cycle, it should contain at least one of these two edges. If it contains both then the cycle can be broken down into two, with one of them being negative and containing exactly one of the above two edges. Therefore, we can assume without loss of generality that the negative cycle contains exactly one edge 𝑥 → 𝑠 where 𝑠 is either 𝑦 or 𝑡 𝑞 . As 𝐺 * 1 is canonical, and the edges of 𝐺 2 other than these two come from 𝐺 * 1 , we can conclude that the shortest path from 𝑠 → 𝑥 is the weight of 𝑠 → 𝑥 in 𝐺 * 1 , which we have seen in the end of Step 1 to be 𝑍 𝑠𝑥 . Therefore, the possible negative cycle is of the form 𝑥 → 𝑠 → 𝑥 with weight (≤, -𝜂 𝑠𝑥 ) + 𝑍 𝑠𝑥 . By construction of 𝜂 𝑠𝑥 this cycle cannot be negative for both the cases, when 𝑠 = 𝑦 and 𝑠 = 𝑡 𝑞 .

F Appendix for Section 7

▶ Lemma 9. Suppose 𝑀 is a maximal constant in guards. The spread of a run of length 𝑛 is bounded by 𝑛𝑀 + 1.

Proof. Consider a timed automaton and let 𝑀 be its maximal constant. We claim that the minimal time for executing 𝑛 actions in the automaton is at most 𝑛𝑀 + 1 in the global semantics. Indeed, in the global-time semantics there is no point of waiting more than 𝑀 time units in a state, since after waiting 𝑀 time units the valuation is already in the biggest region and valuations within a region simulate each other (see [START_REF] Alur | A theory of timed automata[END_REF] for the definition and properties of regions). This intuition is less evident in local-time semantics but we can transfer this observation from the global-time to local-time.

Consider a local run on a sequence 𝑏 1 . . . 𝑏 𝑛 . By Lemma 1 there is a global run on a sequence 𝑐 1 . . . 𝑐 𝑛 such that 𝑏 1 . . . 𝑏 𝑛 is trace equivalent to 𝑐 1 . . . 𝑐 𝑛 . This means that there is a bijection 𝑓 : [𝑛] → [𝑛] with 𝑏 𝑖 = 𝑐 𝑓 (𝑖 ) and respecting order of actions on each process: if 𝑏 𝑖 and 𝑏 𝑗 are two actions of process 𝑝, and 𝑖 < 𝑗 then 𝑓 (𝑖) < 𝑓 ( 𝑗).

The global run has the form:

We can assume that the cumulated time of this run is at most 𝑛𝑀 + 1; this is because if some 𝛿 𝑖 is strictly bigger than 𝑀 then we can shorten it to 𝑀 + 𝜖 for a 0 < 𝜖 < 1 𝑛 as anyway the resulting valuation is the maximal region. Let 𝜃 𝑖 be the cumulated time before the 𝑖-th action:

such that for every 𝑖 and process 𝑝 ∈ dom(𝑏 𝑖 ) we have

. This means that we execute action 𝑏 𝑖 exactly the time when the corresponding action 𝑐 𝑓 (𝑖 ) was executed in the global run. This constraint determines Δ 𝑖 , hence determines the run completely. It can be checked that it is indeed a run: all Δ's are positive, and all guards are satisfied. By definition we have 𝑣 𝑖 (𝑡 𝑝 ) -𝑣 0 (𝑡 𝑝 ) ≤ 𝑛𝑀 + 1 for all reference clocks and for all 𝑖. Since all reference clocks are equal in 𝑣 0 , we get that the spread is at most

gives the number of transitions in process 𝐴 𝑖 , and 𝑀 is the maximum constant used in N .

Proof. No transition repeats in an acyclic system. Hence the length of a run is bounded by ( 𝑖=𝑘 𝑖=1 |𝑇 𝑖 |). Lemma 9 gives the bound ( 𝑖=𝑘 𝑖=1 |𝑇 𝑖 |) × 𝑀 + 1 for each run, and hence the system is spread bounded with this constant. □ ▶ Proposition 3. For every network N and natural number 𝐷 ≥ 1, the system

Proof. Consider a local run in N 𝐷 . Valuations reached after the 𝑠 action are synchronized. Between any two such valuations, the run can elapse at most 𝐷 time units in each process.

As the initial valuation is synchronized, the prefix of the run upto the first 𝑠 action can also elapse at most 𝐷 time units. Similarly, after the last 𝑠 action, the run cannot elapse more then 𝐷 time units in each process. This shows that the run is 𝐷-spread. Pick a global run in N . At every delay of 𝐷 time units, insert the action 𝑠. This gives a run in N 𝐷 . By Lemma 1, every state 𝑞 reachable in the local semantics is reachable in the global semantics. As N 𝐷 contains a representative for every global run, we get that N 𝐷 is complete for reachability. □ Lemma 13. Let 𝑍, 𝑍 ′ be time-elapsed zones. The test

). Proof. The test involves two steps: (1) computing 𝑍 1 := spread 𝐷 (𝑍 ) and 𝑍 ′ 1 := spread 𝐷 (𝑍 ′ ) and then (2) checking 𝔞 ★ ≼𝐿𝑈 (𝑍 1 ) ⊆ 𝔞 ★ ≼𝐿𝑈 (𝑍 ′ 1 ). The second step can be done in time O (|𝑋 ∪ 𝑋 𝑡 | 2 ) thanks to Theorem 6. We show that spread 𝐷 (𝑍 ) can also be computed in the same complexity.

Let 𝐺 𝑍 be the canonical distance graphs of 𝑍 . Let (⋖ 𝑥 𝑦 , 𝑐 𝑥 𝑦 ) be the weight of 𝑥 → 𝑦 in 𝐺 𝑍 . Since 𝑍 is time-elapsed, there are no constraints that give an upper bound on the reference clocks, that is, there are no constraints of the form 𝑡 𝑝 -𝑥 ⋖ 𝑐. This implies that every edge of the form 𝑥 → 𝑡 𝑝 with 𝑥 ∈ 𝑋 ∪ 𝑋 𝑡 and 𝑡 𝑝 ∈ 𝑋 𝑡 has weight (<, ∞). Same is the case with 𝐺 𝑍 ′ as 𝑍 ′ is time-elapsed.

Computing spread 𝐷 (𝑍 ) involves taking 𝐺 𝑍 , adding edges

----→ 𝑡 𝑞 between every pair of reference clocks 𝑡 𝑝 , 𝑡 𝑞 and canonicalizing the resulting graph. Call this resulting graph 𝐺. Since 𝐺 𝑍 had no incoming edges to reference clocks, the only incoming edges to 𝑡 𝑝 in 𝐺 are from other reference clocks. In particular, there are no edges in 𝐺 of the form 𝑥 → 𝑡 𝑝 where 𝑥 ∈ 𝑋 . Therefore, the only shortest paths that can change are of the form 𝑡 𝑝 → 𝑦, where 𝑦 is a process clock. The shortest path from 𝑡 𝑝 to 𝑦 is given by the minimum of (⋖ 𝑡 𝑝 𝑦 , 𝑐

G Appendix for Section 8

We describe the second example from section 8 in more detail here.

Since N + is obtained by applying the construction of Definition 17 to an 𝑛-process extension of N -, we have N + 𝑛 to be 1-spread by Proposition 3. We show that network N + 𝑛 is in fact 0-spread. We will subsequently work with the graph LZG 𝐷,𝑠𝑟𝑐 𝐿𝑈 (N + 𝑛 ) by taking 𝐷 = 0 instead of 𝐷 = 1 as this makes the discussion simpler. The same results hold when we consider 𝐷 = 1 too. Consider an arbitrary local run of N + 𝑛 . Since 𝑠 is a global synchronization the valuations reached after doing 𝑠 are synchronized, hence 0-spread. The final action $ is also a global synchronization which results in a 0-spread valuation. Between two 𝑠 actions, we can only have some 𝑏-sequence happening in 0 time. Hence each intermediate valuation is 0-spread, making the run 0-spread.

Next, we look at some of the valuations reached. From the above paragraph, every valuation obtained after an action transition in a run has 𝑧 𝑖 = 0 for all 𝑖: action 𝑠 resets 𝑧 𝑖 , and between two 𝑠 there is no time elapse. The 𝑧 𝑖 clocks will not play a role in deciding subsumption and hence we will ignore 𝑧 𝑖 clocks for our analysis. For a sequence of actions 𝜎 not containing $, we let (𝑝, 𝑣 𝜎 ) be the configuration reached after executing 𝜎 from the initial configuration (𝑝, 𝑣 0 ). Let 𝑢, 𝑢 1 , 𝑢 2 be 𝑏-sequences. We say 𝑖 ∈ 𝑢 if 𝑢 contains 𝑏 𝑖 . Our sequences of interest are 𝑠𝑢𝑠, 𝑠𝑢, 𝑠𝑢 1 𝑠𝑢 2 𝑠 and 𝑠𝑢 1 𝑠𝑢 2 . We tabulate the values of the valuations reached after such sequences. For simplicity, we will write 𝑣 (𝑥 𝑖 ) for 𝑣 (𝑡 𝑖 -𝑥 𝑖 ), where 𝑡 𝑖 is the reference clock of 𝐴 𝑖 . All valuations below are synchronized.

The zone 𝑍 𝜎 reached after each sequence 𝜎 as above is given by local-elapse(𝑣 𝜎 ). The 0-spread valuations in 𝑍 𝜎 are those obtained by elapsing the same local delay on each process from valuation 𝑣 𝜎 . By property of simulations, 𝑣 𝜎 ≼ ★ 𝐿𝑈 𝑣 𝜎 ′ implies 𝑣 𝜎 + Δ ≼ ★ 𝐿𝑈 𝑣 𝜎 ′ + Δ. Therefore, 𝑣 𝜎 ≼ ★ 𝐿𝑈 𝑣 𝜎 ′ implies 𝔞 0 ≼𝐿𝑈 (𝑍 𝜎 ) ⊆ 𝔞 0 ≼𝐿𝑈 (𝑍 𝜎 ′ ) (in fact, 𝑣 𝜎 ≼ ★ 𝐿𝑈 𝑣 𝜎 ′ implies 𝔞 𝐷 ≼𝐿𝑈 (𝑍 𝜎 ) ⊆ 𝔞 𝐷 ≼𝐿𝑈 (𝑍 𝜎 ′ ) for all 𝐷 ≥ 0 and hence the analysis that follows will hold for 𝐷 = 1 too). Notice that we have 𝐿 = 𝑈 = 1 for every 𝑥 𝑖 . Definition 12 then gives 𝑣 𝜎 ≼ ★ 𝐿𝑈 𝑣 𝜎 ′ iff either 𝑣 𝜎 (𝑥 𝑖 ) = 𝑣 𝜎 ′ (𝑥 𝑖 ) or both 𝑣 𝜎 (𝑥 𝑖 ), 𝑣 𝜎 ′ (𝑥 𝑖 ) > 1.

Based on the valuations above, we have: 𝑣 𝑠𝑢 1 𝑠𝑢 2 𝑠 ≼ ★ 𝐿𝑈 𝑣 𝑠𝑢 2 𝑠 . Secondly we have 𝑣 𝑠𝑏 1 𝑏 2 ...𝑏 𝑛 ≼ ★ 𝐿𝑈 𝑣 0 where 𝑣 0 is an initial valuation that is synchronized and has 𝑣 0 (𝑥 𝑖 ) = 0 for all 𝑖. This