# Symbolic domains and reachability for nets with trajectories

Loïc Hélouët, Prerak Contractor

► To cite this version:

Loïc Hélouët, Prerak Contractor. Symbolic domains and reachability for nets with trajectories. PETRI NETS 2024 - 45th International Conference on Theory and Application of Petri Nets and Concurrency, University of Geneva, Jun 2024, Genève, Switzerland. pp.244-265, 10.1007/978-3-031-61433-0_12 hal-04711503

HAL Id: hal-04711503

https://inria.hal.science/hal-04711503v1

Submitted on 27 Sep 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Symbolic domains and reachability for nets with trajectories

Loïc Hélouët<fnref n="1" /> and Prerak Contractor<fnref n="2" />

**Abstract.** This paper considers verification of timed models handling additional quantities progressing linearly such as distance of moving objects to a target. We introduce a variant of Petri nets called *trajectory nets* where some places are standard control places containing tokens, and other places contain a trajectory of an object. We give a semantics for this model, and propose an abstraction of sets of equivalent trajectories into symbolic domains. These domains cannot be represented by Difference Bound Matrices, but one can compute in polynomial time a symbolic representation of successor configurations. Furthermore domains are closed under this successor relation, and the set of domains of a trajectory net is finite. A consequence is that, when the control part of a trajectory net is bounded, reachability, coverability and verification of safety properties involving distances are PSPACE-Complete.

# 1 Introduction

Some properties of cyber-physical systems such as transport networks call for the verification of quantitative properties addressing time, but also continuous values such as distances. A typical example is safety of metro networks, where one wants to guarantee safety headways, or bound the number of trains in tunnels to guarantee safe evacuation of passengers in case of power failure. Models such as timed automata [3] or time Petri nets [20] only address time, and cannot be used to handle such problems. Models that can address both time and continuous values such as distances rapidly have the expressive power of hybrid automata [2], for which most problems become undecidable.

This paper introduces *trajectory nets*, a model tailored for the analysis of safety properties of systems involving both time and distances such as metro networks. Trajectory nets are a variant of time Petri nets, where some places are dedicated to control, and other places depict object movements with simplified representations called *trajectories*. Configurations assign an integral number of token to control places, and a trajectory, representing the remaining time and distance to the end of a trip to a subset of trajectory places. Dealing with trajectories allows to define properties that address both distances and time. Verification of a safety property of the form "At each instant, less than *K* trains are in a tunnel" amounts to a reachability question for sets of configurations depicting forbidden positions of objects.

<footnote n="1">¹ Univ. Rennes, IRISA, CNRS & INRIA, Rennes, France, loic.helouet@inria.fr</footnote>

<footnote n="2">² IIT Bombay, Mumbai, India, preerakcontractor@gmail.com</footnote>
As a first contribution of this paper, we define trajectory nets and give their semantics in terms of configurations, discrete events (end of progress of a trajec- tory, creation of a new one) and timed moves. As in many continuous models, the set of possible configurations is infinite. This comes on one hand from the unboundedness of the discrete contents of control places, and on the other hand from the continuous representation of trajectories. We show that in their full generality, trajectory nets can simulate a two-counters machine, and are hence Turing Powerful. As a consequence, safety properties relying on coverability or reachability of a configuration are undecidable.

As a second contribution of the paper, we show that the continuous part of configurations can be represented symbolically by sets of linear inequalities called *domains*. Abstracting time with regions and zones in timed automata [3] or domains in variants of Petri nets [5,18,14] is a standard approach. However, for trajectory nets, domains have to abstract away two types of continuous values : time and distance. They define sets of solutions that cannot be represented with the usual zones, and cannot be encoded by Difference Bound Matrices. Nevertheless, we show that we can compute in polynomial time a successor relation on domains, that domains are closed under this relation, and that the set of reachable domains of a given trajectory net is finite. A consequence is that, for trajectory nets with bounded control places, one can compute a sound and complete symbolic abstraction of the timed behaviour called a *state class graph*, and use it to verify properties of the original model. We then show that checking coverability, reachability and safety properties involving distances are PSPACE-Complete problems for bounded trajectory nets. For space reasons, some proofs are only sketched, but can be found in a long version of this work [15].

## 2 Preliminaries

In the rest of the paper, we will denote respectively by $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{N}$ the sets of reals, rationals, and non-negative integers. We will denote by $\mathbb{R}^{\ge 0}$, $\mathbb{Q}^{\ge 0}$ the sets of positive reals and rationals, and by $\mathcal{I}_{\mathbb{Q}}$ the set of intervals of the form $[a, b]$ or $[a, \infty)$ where $a, b \in \mathbb{Q}$. Let $X = \{x_1, \dots, x_n\}$ be a set of variables. A *linear constraint* over $X$ with rational coefficients (or simply constraint for short) is an expression of the form $a_1 \cdot x_1 + a_2 \cdot x_2 + \dots + a_n \cdot x_n \leq b$, where $b$ is a rational value and $a_i$s are rational coefficients (which can have value 0). A constraint is *two-dimensional* if it has at most two variables with non-zero coefficients.

A *valuation* for a set of variables $X$ is a map $\mu : X \to \mathbb{R}$. We will say that a valuation $\mu$ *satisfies* a linear constraint $C(X) ::= \sum a_i \cdot x_i \leq b$ iff replacing every $x_i$ by its valuation $\mu(x_i)$ in $C(X)$ yields a tautology.

A *system* of linear constraints over a set of variables $X$ is a set of linear constraints. It is two-dimensional iff all its constraints are two-dimensional, i.e. all its linear inequalities are of the form $a_i \cdot x_i \leq b_i$, or $a_i \cdot x_i - b_j \cdot x_j \leq c_{i,j}$. A valuation satisfies a system $S$ iff it satisfies all linear constraints in $S$ (i.e. systems are conjunctions of constraints over $X$). A valuation that satisfies $S$ is called a *solution* for $S$. We will denote by $\llbracket S \rrbracket$ the set of solutions for $S$ and say that $S$ is *satisfiable* iff $\llbracket S \rrbracket \neq \emptyset$. Slightly abusing our definition, we will sometimes
adopt a compact notation and write $a \le expr \le b$ instead of a conjunction of
constraints of the form $-expr \le -a$ and $expr \le b$.

A two-dimensional system $S$ involving only inequalities of the form $a_i \le x_i, x_i \le b_i$, or $x_i - x_j \le c_{i,j}$ is called a *zone*. It can be encoded by a Difference Bound Matrix (DBM for short) [10], that is a matrix $DB_S$ indexed by $x_\perp, x_1, \dots, x_n$, where variable $x_\perp$ is a dummy variable representing value 0. In a DBM $DB_S$, a cell $DB_S[x_i, x_j]$ holding value $b_{i,j}$ encodes inequality $x_i - x_j \le b_{i,j}$ and a constraint of the form $x_i \le b_i$ is represented by an entry $DB_S[x_i, x_\perp] = b_i$. Alternatively, zones and DBMs can be represented with *constraint graphs*, i.e. weighted graphs whose vertices are variables $x_\perp, x_1, \dots, x_n$, and whose edges $(x_i, w_{i,j}, x_j)$ are weighted by $w_{i,j} = DB[x_i, x_j]$. DBMs and their graph representations allow for efficient polynomial algorithms to check satisfiability, compute canonical forms, intersections... (see [6] for a survey). For instance, checking non-emptiness of $[S]$ amounts to verifying that the constraint graph for $S$ does not contain negative cycles.

## 3 Trajectory nets

This section describes a new model called *trajectory nets* that can represent movements of objects in a one-dimensional space. This model can describe conveyors, metro networks,... and refers to positions of objects. We show in section 6 how to address safety properties that depend on simultaneous positions of objects. As explained in introduction, such properties are useful for metro operators to guarantee that passengers can be safely evacuated in a short amount of time in case of power failure. This means setting a limit on the number of trains that are positioned on a dangerous zone (tunnel, bridge...) at any instant, and verifying that this limit is never exceeded. Granting such properties means that one is able to refer to positions of trains.

Petri nets are a rather straightforward choice to model transport networks. Stations and track segments between stations can be represented with places, arrivals and departures of vehicles with transitions, and the structure of the network itself is depicted by the flow relation of the net. Addressing trips and dwells durations can be done via a time(d) extension of Petri nets. For instance, one can use time Petri nets [20], that assign a static interval $[\alpha_t^s, \beta_t^s]$ to every transition to represent possible durations of dwells in stations and of trips from one station to the next one. A standard semantics of Time Petri nets is to keep track at each instant of the time remaining before firing of each enabled transition. However, time(d) variants of Petri nets cannot handle real valued variables beyond timing information related to transitions or tokens, and are hence not expressive enough to address properties referring to positions of vehicles.

Consider, for instance, the pictures in Figure 1. These diagrams are standard representations of metro trajectories called *space-time diagrams*. They represent trips with functions mapping time elapsed with the remaining distance to the next station. The two diagrams on the left represent movements of two trains *train*₁, *train*₂ traveling respectively on a track from a station $S_1$ to a station $S_2$, and from a station $S_5$ to a station $S_6$. The track segments represented on these
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** Space time diagrams: trains positions are needed to address safety issues</figcaption></figure>

diagrams contain dangerous zones, symbolized by red areas. The remaining trip duration for *train*₁ and *train*₂ is 100 in both diagrams, but one can easily notice that *train*₁ moves faster than *train*₂. From this situation, both trains cannot be simultaneously in their danger zone in the future, because *train*₂ already exited this area. So, knowing durations of trips does not suffice to distinguish two trajectories or detect dangers. Now consider the two space-time diagrams on the right of Figure 1. The two trains represented will enter and leave their danger zone. However, as *train*₃ is fast, it will leave its danger zone before *train*₄ enters it. These two examples illustrate the fact that addressing safety of moving objects requires to consider more information than a remaining trip duration for each object. A model such as Time Petri nets [20] is hence not precise enough. A solution is to work with hybrid models, that can handle variables representing evolution of objects positions. It is however well known that most problems are undecidable for hybrid automata [4]. In the rest of this section, we introduce a new model that can address time and distance, without reaching the expressive power of hybrid automata. This model contains transitions that represent objects arrivals or departures, standard places holding tokens, and a new type of place containing space-time diagrams representing forecast trajectories of objects.

**Definition 1.** A Trajectory net is a tuple $\mathcal{N} = (P, T, F, I, H)$ where $P = P_T \uplus P_C$ is a set of places. We distinguish a set $P_T$ of trajectory places, and a set $P_C$ of control places. $T = \{\sigma_1, \dots, \sigma_{|T|}\}$ is a set of transitions, $F \subseteq P \times T \cup T \times P$ is a flow relation. The function $I: P_T \to \mathcal{I}_{\mathcal{Q}}$ associates a rational interval $[\alpha_p^s, \beta_p^s]$ to every trajectory place $p \in P_T$, and the function $H: P_T \to \mathcal{Q}$ associates a rational distance to every trajectory place.

The rational value $H(p) \in \mathbb{Q}^{\ge 0}$ is called the *initial distance* of *p*, and is the length of the physical space represented by *p*. The rational interval $I(p) = [\alpha_p^s, \beta_p^s]$ defines the range of possible durations of trips in that physical space. Trajectory places in $P_T$ are holders for trajectories, and control places are standard places containing tokens, used to allow or forbid firing of transitions. The flow relation
of a trajectory net follows the usual terminology of Petri nets. A pair $(p, \sigma) \in F$ from a place $p \in P_C$ to a transition $\sigma$ means that $\sigma$ needs a token in place $p$ to fire. Similarly a pair $(p, \sigma) \in F$ with $p \in P_T$ means that $\sigma$ can fire only if place $p$ contains a trajectory with remaining trip duration (resp. remaining distance to destination) equal to 0. On the other hand, a pair $(\sigma, p) \in F$ indicates that firing of transition $\sigma$ will produce a fresh token (or a fresh trajectory) in place $p$. We denote by $\bullet(\sigma) = \{p \in P \mid (p, \sigma) \in F\}$ the *preset* of $\sigma$, i.e. the set of places from which $\sigma$ consumes a token or a trajectory when firing, and by $(\sigma)^{\bullet} = \{p \in P \mid (\sigma, p) \in F\}$ the *postset* of $\sigma$, i.e., the set of places where tokens or trajectories are added when firing $\sigma$. In the rest of the paper, to simplify semantics, we consider trajectory nets where $|\bullet(\sigma) \cap P_T| \le 1$ and $|(\sigma)^{\bullet} \cap P_T| \le 1$. Slightly abusing notations, we will hence write $p = \bullet(\sigma) \cap P_T$ instead of $\{p\} = \bullet(\sigma) \cap P_T$, and similarly for $(\sigma)^{\bullet} \cap P_T$.

Figure 2 shows the basic elements of trajectory net: two trajectory places $p_1, p_2$ represented by large circles, two control places $p_3, p_4$, represented by small circles, a transition $\sigma$ represented by a rectangle. The flow relation is represented as usually in Petri nets with arrows connecting places and transitions. On this example, we have $\bullet(\sigma) = \{p_1, p_3\}$ and $(\sigma)^{\bullet} = \{p_2, p_4\}$. Place $p_3$ contains a token, and place $p_1$ a trajectory.

<figure><img src="image_3.png" /><figcaption>**Fig. 2.** Basic elements of a trajectory net: places, transitions, trajectories.</figcaption></figure>

**Definition 2.** Let $p \in P_T$ be a trajectory place, and $I(p) = [\alpha_p^s, \beta_p^s]$ be the interval depicting the possible duration of a movement in place $p$. A trajectory in $p$ is a pair of real numbers $tr_p = (T_p, t_p)$, where $T_p \in [\alpha_p^s, \beta_p^s]$ denotes the initial duration of a movement in the physical space represented by place $p$ and $t_p \le T_p$ is the current remaining trip time in that place. A trajectory $tr_p$ is progressing if $t_p > 0$ and is blocked otherwise.

As the initial distance $H(p)$ is fixed for every trajectory place $p \in P_T$, choosing non deterministically an initial duration $T_p$ of a trajectory in interval $[\alpha^s, \beta^s]$ amounts to choosing a speed for an object. A consequence is that $T_p$ and $t_p$ provide information on the speed $v_p$ and remaining distance $d_p$ of an object following trajectory $(T_p, t_p)$. We have $v_p = \frac{H(p)}{T_p}$, and $d_p = t_p \cdot \frac{H(p)}{T_p}$. Given a trajectory place $p \in P_T$, we denote by $\mathcal{T}r(p)$ the set of all trajectories that may appear in $p$, that is the set of all pairs $\mathcal{T}r(p) = \{(T_p, t_p) \mid T_p \in [\alpha_p^s, \beta_p^s] \wedge 0 \le t_p < T_p\}$. We
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** A Trajectory $(T_p, t_p)$ in a place $p$ with $H(p) = 800m$ and $I(p) = [60, 85]$. We have $T_p = 76$ and $t_p = 34$. The blue cone represents all initial trajectories in $p$ for possible initial values for $T_p \in I(p)$. The red area represents a danger zone (e.g. a tunnel) between distance 400 to 600, that needs to be considered for safety.</figcaption></figure>

assume that represented objects have a constant speed $v = H(p)/T_p$ during their trip, which allows us to represent their trajectories as segments. The semantics of a trajectory net is defined in terms of configurations, that assign an integral number of tokens to control places in $P_C$, and a trajectory to a subset of places in $P_T$. We explicitly differentiate blocked and progressing trajectories.

More formally, a configuration is a triple $C = (M, B, \mathcal{T})$, where $M: P_C \to \mathbb{N}$ is a marking of control places, $B \subseteq P_T$ is a subset of trajectory places containing blocked trajectories, and $\mathcal{T}: P_T \to \bigcup_{p \in P_T} \mathcal{T}r(p)$ associates a progressing trajectory to a subset of places in $P_T$. For consistency, we require that $\mathcal{T}(p) \in \mathcal{T}r(p)$. Given a marking, we will write $M \ge \bullet(\sigma)$ iff $M(p) \ge 1$ for every $p \in \bullet(\sigma) \cap P_C$. We will denote by $M - \bullet(\sigma)$ the marking $M'$ such that $M'(p) = M(p)$ for every place $p \notin \bullet(\sigma) \cap P_C$ and $M'(p) = M(p) - 1$ for every place $p \in \bullet(\sigma) \cap P_C$. We will denote by $M + (\sigma) \bullet$ the marking $M'$ such that $M'(p) = M(p)$ for every place $p \notin (\sigma) \bullet \cap P_C$ and $M'(p) = M(p) + 1$ for every place $p \in (\sigma) \bullet \cap P_C$.

We represent a configuration $C = (M, B, \mathcal{T})$, with the following graphical convention: we draw $M(p)$ tokens (black dots) in each control place $p \in P_C$, and for a trajectory place $p \in P_T$ we represent trajectory $\mathcal{T}(p) = (T_p, t_p)$ by a dashed segment with coordinates $[(0, H(p)); (T_p, 0)]$ representing the initial trajectory of an object, and a thick segment with coordinates $[(d_p, 0); (0, t_p)]$ representing the remaining displacement. Figure 3, shows a possible trajectory in a place $p \in P_T$ with $H(p) = 800m$, and $I(p) = [60, 85]$. The trajectory represented is $(T_p, t_p)$ with $T_p = 76s$ and $t_p = 34s$. The object moving in the physical space represented by $p$ initially started a trip of duration $76s$ and of length $800m$, represented by the dashed segment in Figure. The speed of this object is $v_p = 800/76 = 10.52m/s$. As the remaining trip duration is $t_p = 34s$, one can easily compute the remaining distance to go for this object, namely $d_p = 357m$. The remaining trip is represented by the thick segment in the diagram. Similarly, in Figure 2, let $H(p_1) = 500m$, and $I(p_1) = [40, 50]$. Place $p_1$ contains a trajectory $(T_{p_1}, t_{p_1})$ with $T_{p_1} = 46s$ and $t_{p_1} = 25s$. The remaining distance to go for this object is $d_{p_1} = 271,73m$, and its speed is $v_{p_1} = 10.87m/s$.
The semantics of a trajectory net is defined in terms of timed and discrete
moves from a configuration to the next one. The system starts in an initial
configuration $C_0 = (M_0, B_0, \mathcal{T}_0)$ such that $B_0 = \emptyset$, and for every $p$ such that
$\mathcal{T}_0$ is defined, $\mathcal{T}_0(p) = (T_p^0, t_p^0)$ with $T_p^0 = t_p^0 \in [\alpha_p^s, \beta_p^s]$. The main idea of the
semantics is that a transition $\sigma$ can fire if the control places in the preset $\bullet(\sigma)$
allow firing of $\sigma$ and the objects in the trajectory places of $\bullet(\sigma)$ have reached
their final destination. In other terms, all trajectories in the preset of a fired
transition must be blocked.

Upon firing of a transition $\sigma$, control tokens in $\bullet(\sigma) \cap P_C$ are consumed, blocked trajectories in $\bullet(\sigma) \cap P_T$ are deleted, and new trajectories in $(\sigma)^{\bullet} \cap P_T$ and new tokens in control places of $(\sigma)^{\bullet} \cap P_C$ are created. We adopt an exclusive semantics w.r.t. trajectory places, i.e. a transition $\sigma$ can fire only if the trajectory places in $(\sigma)^{\bullet}$ are empty. When modeling metro networks, this semantics is appropriate to represent a fixed block policy, where tracks are divided into exclusive blocks that can contain at most one train at any instant<fnref n="3" />. Upon firing, for each place $p \in (\sigma)^{\bullet} \cap P_T$ new trajectories are sampled: their initial duration $T_p$ is a value chosen non deterministically in $[\alpha_p^s, \beta_p^s]$ and we set $\mathcal{T}(p) = (T_p, T_p)$. On the other hand, elapsing time allows for the progress of existing trajectories. However, we consider an urgent semantics, that allows elapsing $\delta > 0$ time units in a configuration $C$ only if no discrete firing can occur in $C$.

**Discrete moves:** Discrete moves are either the blocking of a trajectory or the firing of a transition. Blocking a trajectory $tr_p = (T_p, t_p)$ in place $p$ is possible only if $t_p = 0$, and consists in deleting $tr_p$, and adding $p$ to the list of places containing a blocked trajectory. Formally, it is defined by the following operational semantics rule:

$$
\begin{array}{l}
p \in P_T \\
\mathcal{T}(p) = (x, 0) \text{ for some } x \in [\alpha_p^s, \beta_p^s] \\
\mathcal{T}'(p_i) = \begin{cases} \mathcal{T}'(p_i) & \text{if } p_i \neq p \\ \text{is undefined otherwise} \end{cases} \\
B' = B \cup \{p\} \\
C = (M, B, \mathcal{T}) \xrightarrow{\text{block } p} C' = (M, B', \mathcal{T}')
\end{array}
$$

We will say that a transition $\sigma$ is *firable* in a configuration $C = (M, B, \mathcal{T})$
iff $M \ge \bullet(\sigma)$, the trajectory in $\bullet(\sigma) \cap P_T$ is blocked, and the place depicting
the physical space needed to perform action $\sigma$ is free, that is, $\forall p \in (\sigma)^{\bullet} \cap P_T$,
$p \notin B$ and $\mathcal{T}(p)$ is undefined. The effect of a firing $\sigma$ is the consumption of all
tokens in $\bullet(\sigma) \cap P_C$, the production of a new token in each place of $(\sigma)^{\bullet} \cap P_C$,
the deletion of the blocked trajectory in $\bullet(\sigma) \cap B$, and the creation of a new
trajectory $\mathcal{T}(p') = (T_{p'}, T_{p'})$ in place $p' = (\sigma)^{\bullet} \cap P_T$ with $T_{p'} \in [\alpha_{p'}^s, \beta_{p'}^s]$. We
will write $M[\sigma]M'$ when $M'$ is the marking obtained after firing of $\sigma$ from $M$,
i.e. when $M' = M - \bullet(\sigma) + (\sigma)^{\bullet}$. Then, the firing of a transition $\sigma$ is formally
defined by the following operational semantics rule:

<footnote n="3">³ Though this fixed block semantics may seem very constrained, many metro networks
in the world are operated this way.</footnote>
$$M \geq \bullet(\sigma) \wedge M[\sigma]M'$$

$$\forall p \in (\sigma)^{\bullet} \cap P_T, p \notin B \wedge \mathcal{T}(p) \text{ is undefined}$$

$$\bullet(\sigma) \cap P_T \subseteq B \wedge B' = B \setminus \bullet(\sigma)$$

$$\mathcal{T}'(p) = \begin{cases} (T_p, T_p), & \text{with } T_p \in [\alpha_p^s, \beta_p^s] \text{ if } p = (\sigma)^{\bullet} \cap P_T \\ \mathcal{T}(p) & \text{otherwise} \end{cases}$$

$$C = (M, B, \mathcal{T}) \xrightarrow{\sigma} C' = (M', B', \mathcal{T}')$$

When a new trajectory is added in a trajectory place, we necessarily have $d_p = H(p)$. As $H(p)$ is constant, choosing $T_p$ is equivalent to choosing a speed $v_p$ for a vehicle, and memorizing this initial choice and $t_p$ allows to compute $d_p$ after several timed moves.

**Timed moves:** The effect of time elapsing is to reduce the remaining trip time of progressing transitions. Elapsing $\delta$ time units is allowed if this duration does not exceed remaining trip time of any progressing trajectory. As in Time Petri nets [20], we adopt an *urgent semantics*, that is we forbid time progress if a discrete event can occur. Time progress of $\delta$ is hence forbidden if some transition is firable less than $\delta$ time units after the current date, or if a trajectory gets blocked. For a given description of trajectories $\mathcal{T}$, we denote by $\mathcal{T}+\delta$ the function that associates the pair $(\mathcal{T}+\delta)(p) = (T_p, t_p - \delta)$ with place $p$ if $\mathcal{T}(p) = (T_p, t_p)$.

$$0 < \delta \leq \min\{t_p \mid \exists T_p, (T_p, t_p) \in \mathcal{T}(P_T)\} \\ \forall \sigma \in T, \sigma \text{ is not firable} \\ C = (M, B, \mathcal{T}) \xrightarrow{\delta} C' = (M, B, \mathcal{T} + \delta)$$

Obviously, our semantics enjoys time additivity, i.e. if $C_1 \xrightarrow{\delta_1} C_2$ and $C_2 \xrightarrow{\delta_2} C_3$, then $C_1 \xrightarrow{\delta_1+\delta_2} C_3$. Notice also that timed and discrete moves are exclusive. It is hence natural to describe runs of a trajectory net as an alternation of timed and discrete moves. A *run* of a trajectory net from a configuration $C_0 = (M_0, B_0, \mathcal{T}_0)$ is a sequence $\rho = (M_0, B_0, \mathcal{T}_0) \xrightarrow{\delta_0} (M_0, B_0, \mathcal{T}_0 + \delta_0) \xrightarrow{e_1} (M_1, B_1, \mathcal{T}_1) \cdots$ of timed and discrete moves, where each move $(M_i, B_i, \mathcal{T}_i) \xrightarrow{\delta_i} (M_i, B_i, \mathcal{T}_i + \delta_i)$ is a legal timed move, and $(M_i, B_i, \mathcal{T}_i) \xrightarrow{e_i} (M_{i+1}, B_{i+1}, \mathcal{T}_{i+1})$ is a legal discrete move, that is a blocking of a trajectory, $(M_i, B_i, \mathcal{T}_i) \xrightarrow{\text{block} p} (M_{i+1}, B_{i+1}, \mathcal{T}_{i+1})$ or a firing of a transition $(M_i, B_i, \mathcal{T}_i) \xrightarrow{\sigma_i} (M_{i+1}, B_{i+1}, \mathcal{T}_{i+1})$.

We will write $(M, B, \mathcal{T}) \xrightarrow{*} (M', B', \mathcal{T}')$ if there exists a sequence of discrete and timed moves leading from $(M, B, \mathcal{T})$ to $(M', B', \mathcal{T}')$. Without loss of generality, we assume that a net starts in an initial configuration $C_0 = (M_0, B_0, \mathcal{T}_0)$ without blocked trajectories, i.e. such that $B_0 = \emptyset$. We also assume that the trajectories of all trains are at their beginning, i.e. for every $p \in P_T$ where $\mathcal{T}_0(p)$ is defined, we have $\mathcal{T}_0(p) = (T_p^0, T_p^0)$ for some $T_p^0 \in [\alpha_p^s, \beta_p^s]$, and that all trains still have some remaining time before being blocked, i.e. $T_p^0 > 0$. We will denote by $\text{Reach}(C_0)$ the set of reachable configurations, i.e. $\text{Reach}(C_0) = \{(M, B, \mathcal{T}) \mid C_0 \xrightarrow{*} (M, B, \mathcal{T})\}$. We will say that a trajectory net is *bounded* iff, there exists an integer $K$ such that for every configuration $(M, B, \mathcal{T})$ in $\text{Reach}(C_0)$, and for every place $p \in P_C$, $M(p) \leq K$.
<figure><img src="image_5.png" /><figcaption>Fig. 4. A trajectory net and its untimed abstraction into a Petri net.</figcaption></figure>

We will address reachability problems, i.e. study whether a particular configuration $(M, B, \mathcal{T})$ is reachable. Now, asking whether a configuration $(M, B, \mathcal{T})$ is reachable refers to the exact position of objects, and is a too precise question. To cope with this problem, we transform contents of trajectory places into markings as follows: given a configuration $C = (M, B, \mathcal{T})$ we define a complete marking $M_C$ that associates an integral number of tokens to each place in $P$, such that $M_C(p) = M(p)$ if $p \in P_C$, and $M_C(p) = 1$ if $p \in P_T$ and $\mathcal{T}(p)$ is defined or if $p \in B$. We then differentiate three decision problems:

- exact reachability: for a given configuration $C$, does $C \in \text{Reach}(C_0)$?

- boolean reachability: for a given configuration $C$, is there a configuration $C' \in \text{Reach}(C_0)$ such that $M_C = M_{C'}$?

- coverability: for a given configuration $C$, is there a configuration $C' \in \text{Reach}(C_0)$ such that $M_C \le M_{C'}$?

Coverability can be used to check that at a given instant, two trains cannot occupy rail sections that require mutual exclusion. Note however that coverability is not fine enough to define safety properties involving distances. For instance, one cannot use coverability to check existence of configurations where two objects are simultaneously in a critical area (a red zone similar to those in the diagrams of Figure 1). As explained at the beginning of this Section, this is a standard property to ensure in metro networks to guarantee passengers safety. In Section 6, we will show that we can address such properties involving distances.

Reachability is decidable for timed automata, using a abstraction of clock values and building a region automaton [3]. Reachability and coverability are undecidable in general for time Petri nets [16]. Coverability is decidable for timed-arc Petri nets [1,13], but reachability remains undecidable [23]. For a weak interpretation of TPNs semantics, [22] shows that the set of reachable markings of a TPN $\mathcal{N}$ coincides whith the set of reachable markings of an untimed version of $\mathcal{N}$. It is well known that coverability [21] and reachability [19] are decidable for Petri nets, and hence also for TPNs with a weak semantics.

Inspiring from [22], we can easily transform a trajectory net $\mathcal{N} = (P = P_C \cup P_T, T, F, I, H)$ and its initial configuration $C_0 = (M_0, B_0, \mathcal{T}_0)$ into a standard untimed Petri net $\mathcal{U}(\mathcal{N}) = (P', T, F)$ where $P' = P_C \cup \{p^U | p \in P_T\}$ replaces
every trajectory place by a standard place, with initial marking $M_0^U = M_{C_0}$.
However, in general $\mathcal{U}(\mathcal{N})$ allows more markings and more runs than $\mathcal{N}$. Consider
the example of Figure 4, with configuration $C_0 = (M_0, B_0, \mathcal{T}_0)$ with $M_0(p_3) =
1, M_0(p_4) = M_0(p_5) = 0, \mathcal{T}_0(p_1) = (1,1), \mathcal{T}_0(p_2) = (2,2)$, and its translation
to a standard Petri net $\mathcal{U}(\mathcal{N})$ on the right of the Figure. One can see from this
example that in the initial configuration $C_0$, transition $\sigma_1$ is firable, but transition
$\sigma_2$ will never fire. On the other hand, in $\mathcal{U}(\mathcal{N})$, both transitions $\sigma_1$ and $\sigma_2$
can fire from $M_{C_0}$. This example shows that erasing time makes some new markings
reachable. Hence we cannot rely on a simple untiming of a trajectory net to
address reachability or coverability. We can further show that trajectory nets
are powerful enough to model a two-counter machine, yielding undecidability of
most problems.

**Theorem 1.** *Reachability, boolean reachability and coverability are undecidable for trajectory nets.*

*Proof (Sketch).* We can simulate the behavior of an unbounded two-counter ma-
chine with an unbounded trajectory net. Control places can represent counters.
From a configuration, urgency can be used to distinguish two behaviors: fire
immediately a particular transition if a counter place is filled, or wait and fire
a different transition if this place is empty. This is sufficient to encode a zero
test [22]. The complete encoding is provided in [15].□

A standard way to recover decidability of reachability and coverability in
timed extensions of Petri nets is to restrict to *bounded* nets, and define a sym-
bolic abstraction of timing information allowing a finite partition of the space of
configurations. For time Petri nets, where time is measured by clocks attached
to enabled transitions, [5] defines an abstraction called state classes, that are
equivalence classes for sets of configurations with identical markings and equiv-
alent constraints on the values of clocks. These constraints are called *domains*,
and can be compared to zones or regions of timed automata [3]. In the next
section, we consider state classes and domains for trajectory nets, and give a
sound abstraction of continuous values appearing in configurations.

# 4 Domains

In this section we define domains for trajectory nets. Domains are a way to
define symbolically the value of initial and remaining trajectory durations with
positive real valued variables. For a given configuration $C = (M, B, \mathcal{T})$, we have
two types of trajectories: blocked trajectories, and progressing ones. For blocked
trajectories, the remaining running time is known (it is 0), and the initial time
is of no use to define a position of an object: it is at distance 0 w.r.t the end
of the represented space. For progressing trajectories, i.e. trajectories in a place
$p \in P_T$ for which $\mathcal{T}(p)$ is defined, we have $\mathcal{T}(p) = (T_p, t_p)$. As already mentioned
in Section 3, we only need these two variables $T_p$ and $t_p$ to compute the speed
or the current position of an object, which are important information when
considering some safety properties.
**Definition 3 (Domains).** Let $\mathcal{N}$ be a trajectory net, with set of trajectory places $P_T$. Let $P \subseteq P_T$ represent places with progressing trajectories. Then, a domain for $\mathcal{N}$ with progressing trajectories in $P$ is a set of inequalities $D$ over variables $V_D = \{T_i, t_i | i \in P\}$, of the form:

$$ \alpha_i^1 \leq T_i \leq \beta_i^1 \quad \text{for all } i \in P \quad (1) $$

$$ \alpha_i^2 \leq t_i \leq \beta_i^2 \quad \text{for all } i \in P \quad (2) $$

$$ t_i - t_j \leq \gamma_{ij}^3 \quad \text{for all } i \neq j \quad (3) $$

$$ \alpha_i^4 \leq T_i - t_i \leq \beta_i^4 \quad \text{for all } i \in P \quad (4) $$

$$ \alpha_{ij}^5 \leq T_i - t_i + t_j \leq \beta_{ij}^5 \quad \text{for all } i \neq j \quad (5) $$

$$ -T_i + t_i + T_j - t_j \leq \gamma_{ij}^6 \quad \text{for all } i \neq j \quad (6) $$

where each type of inequality $(1-6)$ appears **exactly** once in $D$ for each $i \in P$ and for each pair of distinct places $i, j \in P$, and $\alpha_i^1, \alpha_i^2, \alpha_i^4, \alpha_i^5$. $\beta_i^1, \beta_i^2, \beta_i^4, \beta_i^5, \gamma_{ij}^3, \beta_{ij}^5, \gamma_{ij}^6$ are either constant values, $-\infty$, or $+\infty$.

Domains in Definition 3 are systems of linear inequalities, but inequalities of type (5) involve expressions with three variables, and inequalities of type (6) use expressions with four variables. Consequently, our domains are not two-dimensional, and differ from the domains proposed by [5]. Further, they **cannot be encoded using DBMs**. We will however show in the rest of the paper that these domains can be efficiently manipulated in polynomial time. Following the definitions of Section 2, we will say that a valuation $\mu: V_D \to \mathbb{R}$ for $V_D$ is a solution for $D$ iff replacing variables $T_i, t_i$ in $V_D$ by their values $\mu(T_i), \mu(t_i)$ yields a tautology, and denote by $[D]$ the set of all solutions for $D$. Slightly abusing our notation, we will write $\mathcal{T} \in [D]$ when the valuation $\mu_{\mathcal{T}}$ that associates variables $\{T_i, t_i\}$ with their respective values in $\mathcal{T}$ is a solution of $D$. We will say that two domains $D_1, D_2$ are equivalent iff $[D_1] = [D_2]$. Even if two domains are equivalent, they may have different representations. Indeed, consider a single pair of variables $T_1 = t_1$ whose values lie in the interval $[3, 4]$. We can represent the constraint on $T_1, t_1$ as $D_1 = \{3 \leq T_1 \leq 12; 0 \leq T_1 - t_1 \leq 0; 0 \leq t_1 \leq 4\}$. However the domain $D_2 = \{0 \leq T_1 \leq 4; 0 \leq T_1 - t_1 \leq 0; 3 \leq t_1 \leq 20\}$ represents the same set of solutions. We can show that a canonical form for domains exists (Proposition 1), and can be computed in polynomial time (Proposition 2).

**Definition 4.** Let $D = \{a_i \leq expr_i \leq b_i\}$ be a domain of the form given in Definition 3. Then, the canonical form for $D$ is a domain $D^* = \{a_i^* \leq expr_i \leq b_i^*\}$, where $a_i^*$ is the smallest value taken by $expr_i$ in $[D]$, and $b_i^*$ is the largest value taken by $expr_i$ in $[D]$.

**Proposition 1.** The canonical form of a domain $D$ is unique and preserves $[D]$.

*Proof (Sketch).* A domain $D$ is a set of inequalities of the form $a_i \leq expr_i$, and $expr_j \leq b_j$. A solution $\mu_S \in [D]$ is a map that associates a real value with every variable $t_i$ (resp. $T_i$). Let $\mu_S(expr_i)$ be the value obtained by replacing every
variable $t_i$ by $\mu_S(t_i)$ and $T_i$ by $\mu_S(T_i)$ in $expr_i$. The values $a_i^* = \min_{\mu_S \in [D]} \mu_S(expr_i)$ and $b_j^* = \max_{\mu_S \in [D]} \mu_S(expr_j)$ are unique, so $D^*$ is uniquely defined. Every expression of the form $a_i \le expr_i \le b_i$ can be equivalently rewritten as $a_i^* \le expr_i \le b_i^*$ because $a_i^* \le \mu(expr_i) \le b_i^*$ for every $\mu \in [D]$, and we have $a_i \le a_i^* \le b_i^* \le b_i$. A complete proof is given in [15]. □

As all domains over a fixed set of progressing trajectories have the same types of inequalities, and differ only by the constants used, a direct consequence of Proposition 1 is that two domains $D, D'$ are equivalent if and only if $D^* = D'^*$.

**Proposition 2.** *The canonical form for a domain D can be computed in PTIME.*

*Proof.* We perform the following linear transformation: $x_i = T_i - t_i$ and $y_i = -t_i$ to get a new set of inequalities:

$$ \begin{array}{l@{\qquad}l} \alpha_i^1 \le x_i - y_i \le \beta_i^1 & \alpha_i^4 \le x_i \le \beta_i^4 \\ -\beta_i^2 \le y_i \le -\alpha_i^2 & \alpha_{ij}^5 \le x_i - y_j \le \beta_{ij}^5 \\ y_j - y_i \le \gamma_{ij}^3 & -x_i + x_j \le \gamma_{ij}^6 \end{array} $$

Notice that our linear transformation is bijective. Hence, for any solution $\mu: \{T_i, t_i\} \to \mathbb{R}$ in the original domain, there exists a **unique** solution $\mu'$ such that $\mu'(x_i) = \mu(T_i) - \mu(t_i)$, $\mu'(y_i) = -\mu(t_i)$ and for any solution $\mu'$: $\{x_i, y_i\} \to \mathbb{R}$ in the new domain, there exists a **unique** solution $\mu$ such that $\mu(T_i) = \mu'(x_i) - \mu'(y_i)$, and $\mu(t_i) = -\mu'(y_i)$. Hence there is a bijection between the two domains.

Observe that this new domain is of dimension 2. It can hence be encoded as a DBM or a constraint graph, and finding a canonical form for this new domain can be done by computing the shortest paths in the constraint graph. The cost of this calculus is in $O(n^3)$ for $n$ variables. The optimal bounds obtained for the domain over variables $\{x_i, y_i\}$ are bounds for expressions of the form $x_i - y_i$, $x_i - y_j$, etc. that directly encode expressions of the original domain $D$ (for instance $x_i - y_i = T_i$, and $x_i - y_j = T_i - t_i + t_j$). The sharp bounds obtained for the new domain can hence be immediately used as optimal bounds for $D$, except for the expression of the form $-(\beta_i^2)^* \le y_i \le -(\alpha_i^2)^*$, where we need a sign inversion to obtain $(\alpha_i^2)^* \le t_i \le (\beta_i^2)^*$.

For a domain $D$ addressing properties of $k$ trajectories, the linear transformation of $D$ is in $O(k^2)$, as we have $3 \cdot k + 3 \cdot k^2$ inequalities $D$, and performing the transformation for each inequality takes constant time. Computing the canonical form of the new domain can be done in $O(k^3)$ time using the Floyd-Warshall algorithm, as the new domain has $2 \cdot k$ variables. Hence, the canonical form of $D$ can be computed in $O(k^3)$. Note that the constants obtained in the canonical form are linear combinations of $\alpha_i^s$ and $\beta_i^s$ with integer coefficients. □

Let $\mathcal{N}$ be a trajectory net, and let $P \subseteq P_T$ be the set of places containing progressing trajectories in initial configuration $C_0$. The initial domain $D_0$ for $\mathcal{N}$ and $P$ is the set:
$$D_0 = \begin{cases}
T_i^0 \le T_i \le T_i^0 & \text{for all } i \in P \\
T_i^0 \le t_i \le T_i^0 & \text{for all } i \in P \\
t_i - t_j \le \infty & \text{for all } i \neq j \\
0 \le T_i - t_i \le 0 & \text{for all } i \in P \\
-\infty \le T_i - t_i + t_j \le \infty & \text{for all } i \neq j \\
-T_i + t_i + T_j - t_j \le \infty & \text{for all } i \neq j
\end{cases}$$

Let $\mu_0$ be the valuation such that $\mu_0(T_p) = \mu_0(t_p) = T_p^0$ for every place where $T_0$ is defined. Obviously, $[D_0] = \{\mu_0\}$. The initial domain $D_0$ meets the requirements of Definition 3. To show that the form of domain of Definition 3 is sufficient to represent all domains of a net, it remains to show that the effect of a transition firing, or of a trajectory blocking after some delay $\delta$ as proposed in the semantics of Section 3 can be encoded through algebraic operations (variable changes, unions of inequalities and projections) that preserve the types of inequalities considered in Definition 3.

## 4.1 Successors after firing a transition

Let $D$ be a domain with set of progressing trajectories $P$. We want to compute the set of constraints on variables attached to progressing trajectories of the net after firing a transition $\sigma$. Let $p = \bullet(\sigma) \cap P_T$ and $p' = (\sigma) \bullet \cap P_T$. First, $\sigma$ can fire only if $p$ is an empty place (a trajectory in $p$ was formerly blocked), and $p'$ is also empty. According to our semantics, adding a trajectory in $p'$ means sampling a new trip duration $T_{p'} \in [\alpha_{p'}^s, \beta_{p'}^s]$ and adding in $p'$ a new progressing trajectory $(T_{p'}, T_{p'})$. The sampled value is totally independent from the values of variables in $D$, so the new set of constraint on progressing trajectories after firing of $\sigma$ is the set:

$$ \begin{aligned} \text{SuccF}(D, \sigma) = & D \cup \{\alpha_{p'}^s \le T_{p'} \le \beta_{p'}^s\} \cup \{\alpha_{p'}^s \le t_{p'} \le \beta_{p'}^s\} \cup \{0 \le T_{p'} - t_{p'} \le 0\} \\ & \cup \{t_{p'} - t_i \le \infty \mid i \in P\} \cup \{t_i - t_{p'} \le \infty \mid i \in P\} \\ & \cup \{-\infty \le T_{p'} - t_{p'} + t_i \le \infty \mid i \in P\} \\ & \cup \{-\infty \le T_i - t_i + t_{p'} \le \infty \mid i \in P\} \\ & \cup \{-T_{p'} + t_{p'} + T_i + t_i \le \infty \mid i \in P\} \\ & \cup \{-T_i + t_i + T_{p'} + t_{p'} \le \infty \mid i \in P\} \end{aligned} $$

One can immediately notice that if $D$ is a domain, then so is $\text{SuccF}(D, \sigma)$.

## 4.2 Successors after blocking a trajectory

Blocking a progressing trajectory $tr_p = (T_p, t_p)$ from a configuration occurs after elapsing $\delta = t_p$ time units, and is allowed if $\delta$ is the minimal duration among all progressing trajectories. We hence have to consider transformations on a domain $D$ occurring after a sequence of timed and discrete moves of the form $C \xrightarrow{\delta} C' \xrightarrow{\text{block}} C''$. Remark, from the semantics that $\delta = t_p$, so blocking of $tr_p$ can occur only if $t_p = \min\{t_j \mid \exists p_j \in P_T, \mathcal{T}(p_j) = (T_j, t_j)\}$. This requirement can be easily translated into a new constraint: trajectory $tr_p$ can be blocked
from some configuration satisfying domain $D$ iff $D^{p \le *} ::= D \cup \{t_p \le t_j \mid j \ne p \wedge (T_j, t_j) \text{ is a progressing trajectory}\}$ is satisfiable.

As a blocked trajectory does not constrain any more possible durations of other trajectories, the domain capturing the remaining constraints in configuration $C''$ is the projection on remaining variables once $t_p$ time units have elapsed. To obtain this set of constraints, we proceed as follows:

- We make a variable change. Let $t'_j$ denote a variable representing the new value of remaining travel time of trajectory $j$ after elapsing $t_p$ time units. Then we have $t'_j = t_j - t_p$. We hence replace every variable $t_j$ by $t'_j + t_p$ in every inequality of $D^{p \le *}$. Let us call $D'$ this new domain.

- We eliminate variables $T_p$ and $t_p$ from domain $D'$. This elimination can be done in polynomial time using the well-known Fourier-Motzkin algorithm (see [15] and [9]).

- We replace every occurrence of a variable $t'_j$ by an unprimed variable $t_j$ to obtain a successor domain $SuccB(D, p)$, and we compute its canonical form.

**Proposition 3.** Let $D$ be a domain of a trajectory net $\mathcal{N}$, and let $D'$ be a system of linear inequalities that is a successor of $D$ via construction of $SuccB(D, p)$ or $SuccF(D, \sigma)$. Then $D'$ is a domain of $\mathcal{N}$.

*Proof (Sketch).* $SuccF(D, \sigma)$ trivially satisfies this property, as it only adds constraints of the form $\alpha_i^S \le T_i \le \beta_i^S$, $\alpha_i^S \le t_i \le \beta_i^S$, and $T_i = t_i$. The proof for $SuccB(D, p)$ is more involved, as it requires eliminating variables for the blocked trajectory. Yet, during elimination, some inequalities are unchanged because they refer to $T_i$, and not to $t_i$. For other inequalities, combining expressions of the form $expr_j \le t_i$ and $t_i \le expr_k$ to obtain a new expression $expr_j \le expr_k$ during the elimination process either produces tautologies, or new expressions that are of the form of inequalities in Definition 3. A complete proof is given in [15]. □

# 5 Soundness, Completeness, Finiteness

Now that we have defined domains for trajectory nets, and shown that we can effectively compute a canonical representation for $SuccF(D, \sigma)$ the set of constraints that hold after firing a transition $\sigma$ and $SuccB(D, p)$ the constraints that hold after blocking a trajectory in place $p$ when starting from a domain $D$, we can define state classes.

**Definition 5.** A state class of a trajectory net $\mathcal{N}$ is a triple $SC = (M, B, D)$, where $M$ is a marking, $B$ is a subset of trajectory places with blocked trajectories, and $D$ is a domain of $\mathcal{N}$ in canonical form.

We can define a symbolic transition relation among state classes as follows:

- $(M, B, D) \xrightarrow{\text{Block } p} S (M, B', D')$ if $B' = B \cup \{p\}$, and $D'$ is the canonical representation of $SuccB(D, p)$, and
– $(M, B, D) \xrightarrow{\sigma} S (M', B', D')$ if $M[\sigma]M', B' = B \setminus \cdot(\sigma)$, and $D'$ is the canonical representation of $SuccF(D, \sigma)$.

We will write $(M, B, D) \xrightarrow{\sigma} S (M', B', D')$ if either $(M, B, D) \xrightarrow{Block p} S (M', B', D')$ or $(M, B, D) \xrightarrow{\sigma} S (M', B', D')$. We will denote by $Reach^S(M_0, B_0, D_0)$ the set of state classes that can be built inductively from the initial state class $D_0$ by application of the symbolic transition relation $\rightarrow_S$.

**Definition 6.** The state class graph of a trajectory net $\mathcal{N}$ is the transition system $SC(\mathcal{N}) = (Reach^S(M_0, B_0, D_0), \rightarrow_S, (M_0, B_0, D_0))$.

Notice that $SC(\mathcal{N})$ is defined even if $Reach^S(M_0, B_0, D_0)$ is not finite. We will say that a configuration $C = (M, B, \mathcal{T})$ matches with a state class $SC = (M', B', D)$ iff $M = M', B = B'$ and $\mathcal{T} \in [D]$.

**Definition 7.** A symbolic run of $\mathcal{N}$ is a sequence of state classes of the form $\rho^S = (M_0, B_0, D_0) \xrightarrow{e_0} (M_1, B_1, D_1) \xrightarrow{e_1} \dots$ such that for every index $i \ge 0$, $e_i \in \{\text{Block } p_i, \sigma_i\}$ and $(M_i, B_i, D_i) \xrightarrow{e_i} S (M_{i+1}, B_{i+1}, D_{i+1})$.

**Proposition 4 (Soundness).** Let $\rho^S = (M_0, B_0, D_0) \xrightarrow{e_0} (M_1, B_1, D_1) \xrightarrow{e_1} \dots$ be a symbolic run of a trajectory net $\mathcal{N}$. Then, there exists a run $\rho = (M_0, B_0, \mathcal{T}_0) \xrightarrow{e_0} (M_1, B_1, \mathcal{T}_1) \xrightarrow{e_1} \dots$ of $\mathcal{N}$ such that for every $i \ge 0$, $(M_i, B_i, \mathcal{T}_i)$ matches with $(M_i, B_i, D_i)$.

**Proposition 5 (Completeness).** Let $\rho = (M_0, B_0, \mathcal{T}_0) \xrightarrow{e_0} (M_1, B_1, \mathcal{T}_1) \xrightarrow{e_1} \dots$ be a run of a trajectory net $\mathcal{N}$. Then, there exists a symbolic run $\rho^S = (M_0, B_0, D_0) \xrightarrow{e_0} (M_1, B_1, D_1) \xrightarrow{e_1} \dots$ of $\mathcal{N}$ such that for every $i \ge 0$, $(M_i, B_i, \mathcal{T}_i)$ matches with $(M_i, B_i, D_i)$.

The proofs for Propositions 4 and 5 are obtained by induction on the length of runs, and are detailed in [15].

**Theorem 2.** Let $\mathcal{N}$ be a bounded trajectory net, with initial configuration $C_0$. Then the set of canonical domains that can be computed inductively from $D_0^*$ is finite.

*Proof (sketch).* A domain is defined by a set of inequalities. The number of inequalities depend only on the number of progressing trajectories, and these inequalities involve constants. We can prove that constants appearing in canonical domains of a trajectory net are linear combinations of constants appearing in $D_0$ and in intervals $[\alpha_i^s, \beta_i^s]$. It was also proved (see [5]) that the number of linear combinations of a finite set of constants in a rational interval $[A, B]$ is finite. It remains to show that this type of bounding interval exists for the values of constants $\alpha_i^1, \beta_i^1, \alpha_i^2, \beta_i^2, \gamma_{ij}^3, \alpha_i^4, \beta_i^4, \alpha_{ij}^5, \beta_{ij}^5, \gamma_{ij}^6$ appearing in domains of trajectory nets. This interval is $[-2 \cdot C_{max}, 2 \cdot C_{max}]$, where $C_{max}$ is the maximal value appearing in an interval $[\alpha_i^s, \beta_i^s]$. So, we get that constants in domains can take a finite number of values, and a finite number of inequalities can appear in domains. Let us denote by $I_0$ this set of possible inequalities. The set of possible domains is finite, since each domain is a subset of $I_0$. (all proof details are given in [15]□
Following Theorem 2, we can give an upper bound on the number of state classes in $SC(\mathcal{N})$. Let us first compute the size of $I_0$. Assuming that we consider only domains in canonical form, every constraint in $I_0$ is of the form $a \leq expr \leq b$, with $-2 \cdot C_{max} \leq a$ and $b \leq 2 \cdot C_{max}$. Assuming that all $\alpha_i^s$ and $\beta_i^s$ are rational numbers with a common denominator $d$, there exists at most $4 \cdot C_{max} \cdot d$ possibilities for values of $a$ and $b$ in expressions. Similarly, expression expr are of the form given in Definition 3, and there are hence $3 \cdot (|P_T| + |P_T|^2)$ expressions. The size of $I_0$ is hence $12 \cdot C_{max} \cdot d \cdot (|P_T| + |P_T|^2)$, and each domain is a subset of inequalities from $I_0$. This gives an upper bound on the number of domains, which is in $O(2^{|I_0|})$. In a state class, component $B$ is a subset of trajectory places, and hence there are at most $2^{|P_T|}$ possible values for $B$. Last, for a $K$ bounded trajectory net, the number of possible markings for control places is in $O(|P_C|^{K+1})$ [12]. The number of state classes is hence in $O(2^{|I_0|+|P_T|} \cdot |P_C|^{K+1})$.

# 6 Reachability, Coverability, Safety

An important property of the state class graph is that all solutions for domains that are reachable in $SC(\mathcal{N})$ are also reachable in $\mathcal{N}$. This immediately gives an algorithm to check coverability or reachability properties.

**Theorem 3.** *Given a state class $(M_n, B_n, D_n)$ reachable from initial state class $(M_0, B_0, D_0)$, and a solution $T_n \in [D_n]$, there exists a run in the original trajectory net that ends in configuration $(M_n, B_n, T_n)$.*

*Proof (Sketch).* As for Proposition 4), we can use an induction on the length of paths in the state class graph. (See details in [15]).□

**Theorem 4.** *Reachability, boolean reachability, and boolean coverability are decidable in PSPACE for bounded nets*

*Proof.* These problems can be solved by a non-deterministic exploration of the state class graph. Let us first consider reachability of a given configuration $(M, B, T)$. Assume that a state class $(M, B, D)$ such that $T \in [D]$ is reachable in $SC(\mathcal{N})$. Then, according to Theorem 3, there exists a run of $\mathcal{N}$ reaching $(M, B, T)$. Consider now the boolean reachability and coverability problems. Let $sc=(M, B, D)$ be a reachable state class. One can notice that the boolean marking $M_C$ is identical for every configuration $C$ matching $sc$. We hence denote this marking by $M_{sc}$, and compute it by assigning a token to a place $p_i \in P_T$ iff $T_i, t_i$ are variables used in $D$ or if $p_i \in B$. Then, deciding reachability (resp. coverability) of a marking $M$ consists in finding a state class $sc$ such that $M_{sc} = M$ (resp. $M_{sc} \geq M$).

As shown in Section 5, the size of the state class graph is exponential w.r.t. the number of places and w.r.t. the value on constants appearing in intervals attached to trajectory places. Encoding a state class can be done in $\log(|SC(\mathcal{N})|)$ hence in polynomial space, and reachability questions can be addressed in nlogspace w.r.t. the size of the graph. At each step of an exploration reaching a particular state class $SC_i = (M_i, B_i, D_i)$, checking $M = M_i, B = B_i, M = M_{SC_i}$ or $M \leq M_{SC_i}$
can be done in linear time w.r.t the number of places, and checking $\mathcal{T} \in [[D_i]]$
can be done in linear time w.r.t the number of inequalities in $D$ by replacing
every variable by its value in each inequality. As the number of inequalities in
canonical domains is quadratic w.r.t. the number of trajectory places, checking
$\mathcal{T} \in [[D_i]]$ can be done in PTIME. Hence, reachability boolean reachability, and
coverability can be checked in NPSPACE, which is equivalent to PSPACE by
Savitch's theorem [24].□

*Remark 1.* Notice that a trajectory net without trajectory places is a Petri net (transitions can fire as soon as their preset is filled, after any delay). Hence, reachability and coverability in trajectory nets are at least as hard as reachability and coverability in 1-safe Petri nets. These problems are known to be PSPACE-Complete [7,11].

**Corollary 1.** *Reachability, boolean reachability, and boolean coverability for bounded nets are PSPACE-Complete.*

*Proof.* PSPACE membership is proved by Theorem 4. As highlighted in Remark 1, a reachability or a coverability problem for 1-safe nets is also a reachability/coverability problem for trajectory nets (with empty set of trajectory places). As these two problems are PSPACE-Complete [7,11], we get the result.□

**6.1 Extending coverability to safety properties**

Reachability is often a too precise question and one is usually interested in properties that address ranges of values for positions of objects. Let us get back to the case study introduced in Section 3, namely avoidance of simultaneous dangerous situations in a metro network. Metro networks can be easily represented by trajectory nets: trajectory places represent track portions between two stations, or a finer partition of a physical network into track portions called *blocks*, transitions symbolize departures, arrivals etc. Obviously, metro networks have very strict safety requirements that must be guaranteed by physical equipments such as signals and brakes. Safety issues also appear at the operational level. At any instant, evacuation of passengers should be feasible with the lowest risks, and for that reason, operators want to avoid situations where more than *K* trains are in tunnels or on bridges.

Addressing such safety properties is neither a reachability nor a coverability
question: it requires that *at any instant*, all trajectories of trains avoid a *set of
unsafe positions*. Let $p \in P_T$ be a trajectory place, of length $H(p)$, and assume
that the track portion represented by $p$ contains a tunnel. We can easily define
two values $d_p^s$ and $d_p^e$ defining respectively the position of the entry and exit
of the tunnel in that track (for instance, in Figure 3, we have $d_p^s = 600$ and
$d_p^e = 400$). Let $\mathcal{T}p = (T_p, t_p)$. The function gives us the initial duration $T_p$ of
a trip from a station to the next one, the remaining time $t_p$ before the end of
this trip, but we can also compute the position $d_p$ of the considered train on
the track. We have assumed that all objects moving in a trajectory net have
a constant speed during the whole duration of a trajectory, sampled when the
object enters a place. Hence, $\frac{H(p)}{T_p} = \frac{d_p}{t_p}$ at any instant, and a train in place $p$ is in a tunnel iff the following property is satisfied:

$$ \text{Tunnel}(p) ::= d_p^e \le \frac{H(p) \cdot t_p}{T_p} \le d_p^s $$

Now assume that we want to avoid a situation where trains in a set of places $X = \{p_1, \dots, p_k\} \subseteq P_T$ are in tunnels at the same instant. It means that we have to avoid any configuration that satisfies the property

$$ \text{Unsafe}(X) ::= \bigcup_{p_i \in X} \text{Tunnel}(p_i). $$

The domains computed in the state class graph $\mathcal{SC}(\mathcal{N})$ are symbolic representations of configurations reached immediately after discrete moves. It can be the case that, after each discrete move, all trains are located before a tunnel in their respective track segment. Verifying safety of a train network does not amount to verifying that $[D \cup Unsafe(X)] = \emptyset$ for sets of places $X$ containing tunnels and for every reachable domain $D$. We need to consider how configurations depicted in $D$ evolve when elapsing time, i.e., build symbolic representations of configurations reached an arbitrary duration after a discrete move. Hence, we introduce time closure $S_\downarrow = (M, B, D_\downarrow)$ of a state class $S = (M, B, D)$.

**Definition 8 (Time Closure).** Let $S = (M, B, D)$ be any state class having a set of places with progressing trajectories $P_{pr} \subseteq P_T$. We introduce variables $\delta$ (to represent the timed move) and $t'_i$ for all $i \in P_{pr}$ (to represent time remaining in trajectories after a timed move of duration $\delta$). The time closure of $S$ is a 3-tuple $S_\downarrow = (M, B, D_\downarrow)$ with $D_\downarrow$ defined as:

*Case I: No transition is firable from the given marking $M$ and set of blocked trajectories $B$, and hence timed moves are allowed by the semantics of trajectory nets.* We have $D_\downarrow = D \cup \{0 \le \delta \le t_i \mid i \in P_{pr}\} \cup \{t'_i = t_i - \delta \mid i \in P_{pr}\}$

*Case II: There exists a firable transition for the given marking $M$ and set of blocked trajectories $B$, and hence timed moves are not allowed.* We hence have $D_\downarrow = D \cup \{\delta = 0\} \cup \{t'_i = t_i \mid i \in P_{pr}\}$.

The time closure of a state class $S = (M, B, D)$ is a symbolic representation of possible configurations reachable after timed moves of arbitrary duration $\delta$, including the configurations in domain $D$ (i.e., when $\delta = 0$). As explained above, a property of interest for metro networks is that no more than $K$ trains are in a tunnel at any given instant. We denote by $Unsafe'(X)$ the set of inequalities obtained by replacing, for every place $p \in X$ variable $t_p$ by $t'_p$ in $Unsafe(X)$. A state class $S = (M, B, D)$ is safe for places $p_1, \dots, p_K$ iff $[D_\downarrow \cup Unsafe'(p_1, \dots, p_K)] = \emptyset$. Verifying that a state class is safe for every subset of places of size $K$ amounts to asking that $[D_\downarrow \cup Unsafe'(X)] = \emptyset$ for every subset $X \subseteq P_T$ of places of size $K$ containing tunnels. Notice that the set of all $X$'s can be enumerated in $\log(|P_T|)$ space.

*Remark 2.* Non-emptiness of $D_\downarrow \cap Unsafe'(X)$ implies existence of a configuration violating the safety property, because all configurations in a state class $D$ are reachable, and hence all configurations in $D_\downarrow$ too. Hence, checking safety for
all state classes of SC($\mathcal{N}$) guarantees that the trajectory net does not violate the safety property. This gives us a method to check safety of a metro network modeled with a trajectory net using its state class graph.

Let $X = \{p_1, \dots, p_k\}$. The constraint $\text{Unsafe}(X)$ can be rewritten as
$$ \{d_{p_i}^e \le \frac{H(p_i) \cdot t_i'}{T_i} \le d_{p_i}^s \mid p_i \in X\} $$
and as every $T_i$ is a positive value, simplified to
$$ \text{get } \{d_{p_i}^e \cdot T_i \le H(p_i) \cdot t_i' \le d_{p_i}^e \cdot T_i \mid p_i \in X\} $$
One can immediately observe that this set contains only linear inequalities of dimension 2 involving $T_i$ and $t_i'$. Let us now consider $D_\downarrow$, defined for a set of places $P$ of progressing trajectories. It obtained by replacing $t_i$ by $t_i' + \delta$. It is hence a set of constraints of the form:

$$
\begin{align*}
\alpha_i^1 &\le T_i \le \beta_i^1 && \text{for all } p_i \in P \\
\alpha_i^2 &\le t_i' + \delta \le \beta_i^2 && \text{for all } p_i \in P \\
& t_i' - t_j' \le \gamma_{ij}^3 && \text{for all } p_i, p_j \in P \text{ with } i \neq j \\
\alpha_i^4 &\le T_i - t_i' + \delta \le \beta_i^4 && \text{for all } p_i \in P \\
\alpha_{ij}^5 &\le T_i - t_i' + t_j' \le \beta_{ij}^5 && \text{for all } p_i, p_j \in P \text{ with } i \neq j \\
-T_i + t_i' + T_j - t_j' &\le \gamma_{ij}^6 && \text{for all } p_i, p_j \in P \text{ with } i \neq j
\end{align*}
$$

**Remark 3.** Checking emptiness of $D_\downarrow \uplus \{d_{p_i}^e \cdot T_i \le H(p_i) \cdot t_i' \le d_{p_i}^s \cdot T_i \mid p_i \in X\}$ can be done by elimination of variables one after another, and stopping as soon as an inequality is unsatisfiable, or when all variables are eliminated. We can use a variable change as in Proposition 2, and get an equivalent system of dimension 2. Hence, checking satisfiability of $D_\downarrow \uplus \text{Unsafe}(p_1, \dots, p_k)$ can be done in PTIME.

**Proposition 6.** *Checking a safety property for a bounded trajectory net is PSPACE-complete.*

*Proof.* $\mathcal{N}$ violates a safety property of the form "no more than $K$ trains in a tunnel" iff there exists a reachable configuration $C = (M, B, \mathcal{T})$ such that $\mathcal{T} \models \text{Unsafe}(X)$ for some subset of places $X = \{p_1, \dots, p_K\}$ with tunnels. According to remark 2, this holds only if there exists a reachable state class $S = (M, B, D)$ such that $[[D_\downarrow \cup \text{Unsafe}'(X)]] \neq \emptyset$. We know from the decision procedures for reachability and coverability that exploration of all state classes can be done in PSPACE. Then, for each state class $S = (M, B, D)$ reached, we need to compute $D_\downarrow$ enumerate all subsets $X$ of $K$ places containing tunnels and with a progressing trajectory, and check emptiness of $D_\downarrow \cup \text{Unsafe}(p_1, \dots, p_K)$. Enumeration of subsets of places of size $K$ can be done in $\log(P_T)$ space. Following remark 3, (un)satisfiability of $D_\downarrow \cup \text{Unsafe}(p_1, \dots, p_K)$ can be verified in PSPACE. The hardness comes from a reduction of the coverability problems for 1-safe nets: if $C$ is a set of places to cover in a net $\mathcal{N}$, on can design a trajectory net $\mathcal{N}_T$ with one additional trajectory places $p_{T,c}$ per place in $C$ and such that $\bullet(p_{T,c}) = \bullet(c)$, $(p_{T,c})\bullet = (c)\bullet$ and set zones to avoid as the whole length of these places. Reaching a configuration with objects in $X = \{p_{T,c} \mid c \in C\}$ in $\mathcal{N}_T$ amounts to covering $C$ in $\mathcal{N}$. $\square$
# 7 Conclusion

We have considered an extension of Petri nets enhanced with time and linear functions depicting trajectories of moving objects. Most problems for this model are undecidable in general. However, as soon as the control part is bounded, the behaviour of the model can be abstracted to a finite state class graph, and coverability, reachability, and safety properties addressing distance issues can be decided in PSPACE. Finiteness of the state class graph of trajectory nets comes from bounds on the values of variables, and from the particular structure of domains, that are conjunctions of linear inequalities with at most 4 variables, and coefficients in {1, -1}. This structure is preserved by projection, and hence by the successor relation among state classes. Preliminary work shows that domains for trajectory nets are a form of regular polyhedra, that can be encoded by Totally Unimodular Matrices (TUM). This needs to be formally proved, but it would explain why our domains have interesting closure and algorithmic properties. An interesting research direction is to consider extensions of trajectory nets that preserve this nice and efficient domain structure.

As future work, several extensions of the model can be considered. We have defined a restricted model, mainly tailored to represent metro networks. The first restriction is that transitions have at most one trajectory place in their preset and in their postset. This last restriction was used to simplify notations and reading, and can be easily relaxed: one can imagine firing rules consuming several blocked trajectories, and similarly producing several new trajectories in the postset of a transition. The techniques shown in this paper easily adapt. It should also be possible to consider trajectories in 2D or 3D spaces.

The second restriction imposes that trajectories are simple linear functions, i.e. the speed of an object is sampled once, and remains constant until a trajectory gets blocked. One could easily improve trajectories using piecewise linear function depicting behavior of objects moving at varying speeds (this is the model proposed in [17], Chapter 5). This would be useful to describe acceleration and braking phases. We conjecture that this extension still allows to work with TUMs, as long as trajectory places contain at most one trajectory.

More involved improvements would be to consider trajectories specified by polynomials, or to allow more than one trajectory per place. The single trajectory restriction makes sense when modeling metro networks for instance, as many cities implement a fixed block traffic management policy, where tracks are partitioned in exclusive blocks that must be occupied by a single train at any instant. However, this type of management is progressively replaced by moving block policies, that allow several trains in a track segment provided they maintain safety distances. Relaxing the single trajectory restriction is also needed to model other situations such as road traffic. First experiments seem to show that a definition of domains for these two extensions require polynomial inequalities, i.e. expressions of the form $P(X) \le c$, where $P(X)$ is a multivariate polynomial. It is known that such domains are closed under projection [25]. However, variable elimination has a doubly exponential complexity [8]. Further, we conjecture that finiteness of domains does not hold any more in this new setting.
References

1. P.A. Abdulla and A. Nylén. Timed Petri nets and BQOs. In *ICATPN*, LNCS 2075, p.53-70, 2001.

2. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. *TCS*, 138(1):3–34, 1995.

3. R. Alur and D.L. Dill. A theory of timed automata. *TCS*, 126(2):183–235, 1994.

4. Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. The algorithmic analysis of hybrid systems. *Theor. Comput. Sci.*, 138(1):3–34, 1995.

5. B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. *IEEE Trans. Software Eng.*, 17(3):259–273, 1991.

6. V. Chandru. Variable elimination in linear constraints. *Comput. J.*, 36(5):463–472, 1993.

7. A. Cheng, J. Esparza, and J. Palsberg. Complexity results for 1-safe nets. *TCS*, 147(1&2):117–136, 1995.

8. G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In *Automata Theory and Formal Languages*, pages 134–183, 1975.

9. G. Dantzig and B. C. Eaves. Fourier-Motzkin Elimination and Its Dual. *J. Comb. Theory, Ser. A*, 14(3):288–297, 1973.

10. D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In *Automatic Verification Methods for Finite State Systems*, volume 407 of LNCS, pages 197–212, 1989.

11. J. Esparza. Decidability and complexity of Petri net problems - an introduction. In *Proc. of Petri Nets*, volume 1491 of LNCS, pages 374–428, 1998.

12. J. Esparza. Petri nets lecture notes. Technical report, 2019.

13. D. de Frutos-Escrig, V.V. Ruiz, and O. Marroquín Alonso. Decidability of properties of timed-arc Petri nets. In M. Nielsen and D. Simpson, editors, *Application and Theory of Petri Nets 2000, 21st International Conference, ICATPN 2000, Aarhus, Denmark, June 26-30, 2000, Proceeding*, volume 1825 of *Lecture Notes in Computer Science*, pages 187–206. Springer, 2000.

14. L. Hélouët and P. Agrawal. Waiting nets. In *Proc. of PETRI NETS 2022*, volume 13288 of LNCS, pages 67–89, 2022.

15. L. Hélouët and P. Contractor. Symbolic domains and reachability for nets with trajectories (long version). Technical report, Inria, https://inria.hal.science/hal-04528235, 2024.

16. N.D. Jones, L. H. Landweber, and Y. E. Lien. Complexity of some problems in Petri nets. *Theor. Comput. Sci.*, 4(3):277–299, 1977.

17. Karim Kecir. Performance Evaluation of Urban Rail Traffic Management Techniques. (Évaluation de Performances pour les Techniques de Régulation du Trafic Ferroviaire Urbain). PhD thesis, University of Rennes 1, France, 2019.

18. D. Lime and O.H. Roux. Model checking of time Petri nets using the state class timed automaton. *Discret. Event Dyn. Syst.*, 16(2):179–205, 2006.

19. E.W. Mayr. An algorithm for the general Petri net reachability problem. In *Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA*, pages 238–246. ACM, 1981.

20. P. M. Merlin. *A Study of the Recoverability of Computing Systems*. PhD thesis, University of California, Irvine, CA, USA, 1974.
21. C. Rackoff. The covering and boundedness problems for vector addition systems. *Theor. Comput. Sci.*, 6:223–231, 1978.

22. P.-A. Reynier and A. Sangnier. Weak time Petri nets strike back! In *Proc. of CONCUR 2009*, volume 5710 of LNCS, pages 557–571, 2009.

23. V. V. Ruiz, F. C. Gomez, and D. de Frutos-Escrig. On non-decidability of reachability for timed-arc Petri nets. In *PNPM*, pages 188–. IEEE Computer Society, 1999.

24. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. *Journal of Computer and System Sciences*, 4(2):177–192, 1970.

25. A. Tarski. A decision method for elementary algebra and geometry. Technical report, RAND Corporation, 1957.