Loïc Hélouët
email: loic.helouet@inria.fr

Karim Kecir
email: karim.kecir@inria.fr

Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics (regular paper)

This paper considers realizability of schedules by stochastic concurrent timed systems. Schedules are high level views of desired executions represented as partial orders decorated with timing constraints, while systems are represented as elementary stochastic time Petri nets. We first consider logical realizability: a schedule is realizable by a net N if it embeds in a time process of N that satisfies all its constraints. However, with continuous time domains, the probability of a time process that realizes a schedule is null. We hence consider probabilistic realizability, of schedules up to some imprecision α, that holds if the probability that N logically realizes S with constraints enlarged by α time units is strictly positive. We show that upon a sensible restriction guaranteeing time progress, logical and probabilistic realizability of a schedule can be checked on the finite set of symbolic prefixes extracted from a bounded unfolding of the net. We give a construction technique for these prefixes and show that they represent all time processes of a net occurring up to a given maximal date. We then show how to verify existence of an embedding and compute the probability of its realization. * -→ m , τ iff there exists a sequence of moves leading from m, τ to m , τ . An initial configuration for N is a configuration m 0 , τ 0 where τ 0 attaches a sampled TTF to each transition enabled by m 0 .

Introduction

Correct scheduling of basic operations in automated systems such as manufacturing or transport systems is a way to manage at best available resources, avoid undesired configurations, or achieve an objective within a bounded delay. Following a predetermined schedule is also a way to meet qualitative objectives. This is for instance the case for metro networks, in which changes to predetermined schedules may cause network congestion and impact users satisfaction. Schedules provide high-level views for correct ordering of operations in a system, consider time issues and provide optimal dates for a production plan. They can be seen as partial orders among basic tasks, decorated with dates and timing constraints.

Designing a correct and optimal schedule for a system is a complex problem. Occurrence dates of events can be seen as variables, and correct and optimal schedules as optimal solutions (w.r.t. some criteria) for a set of constraints over these variables. Linear programming solutions have been proposed to optimize scheduling in train networks [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF][START_REF] D'ariano | Conflict resolution and train speed coordination for solving real-time timetable perturbations[END_REF]. The size of models for real systems that run for a full day call for approximated solutions and is usually addressed by experts. When a high-level schedule and the low-level system that implements it are designed in a separate way, nothing guarantees that the system is able to realize the expected schedule. This calls for tools to check realizability of a schedule by a system. One can notice that optimal and realizable schedules are not necessarily robust if they impose thight realization dates to systems that are subject to random variations (delays in productions, faults. . . ). In metro networks, trains delays are expected and are part of the normal behavior of the system. To overcome this problem, metro schedules integrate small recovery margins that avoid the network performance to collapse as soon as a train is late. Note also that for systems where time issues are defined with continuous variables, the probability to execute a given event at a precise date is zero. Furthermore, being able to realize a schedule does not mean that the probability to meet optimal objectives is high enough. Beyond logical realizability, a schedule shall hence be considered as realizable if it can be approached with a significant probability. This paper addresses realizability of schedules by stochastic timed systems. We define schedules as labeled partial orders decorated with dates and timing constraints, and represent systems with elementary stochastic time Petri nets (STPN for short), a model inspired from [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF]. We particularly emphasize on resources: non-availability of a resource (represented by a place) may block transitions. This leads to the definition of a blocking semantics for STPNs that forbids firing a transition if one of its output places is filled. We then propose a notion of realizability: a schedule S is realizable by a net N if S embeds in a symbolic process of N that meets constraints of S. We prove that upon some reasonable time progress assumption, realizability can be checked on a finite set of symbolic processes, obtained from a bounded untimed unfolding [START_REF] Kenneth | A technique of state space search based on unfolding[END_REF][START_REF] Esparza | An improvement of mcmillan's unfolding algorithm[END_REF] of N . Symbolic processes are processes of the unfolding with satisfiable constraints on occurrence dates of events. A symbolic framework to unfold time Petri nets was already proposed in [START_REF] Chatain | Symbolic diagnosis of partially observable concurrent systems[END_REF][START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF] but blocking semantics brings additional constraints on firing dates of transitions.

Embedding of a schedule in some process of N only guarantees logical realizability: the probabilty of a time process in which, at least, one event is forced to occur at a precise date is 0. We use transient analysis of STPNs [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF] to compute the probability that a schedule is realized by a symbolic time process of N up to imprecision of δ. This allows to compute the probability that N realizes S ± δ and define probabilistic realizability that holds if N realizes S ± δ with strictly positive probability.

The paper is organized as follows: Section 2 introduces schedules and our variant of stochastic time Petri nets with blocking semantics. Section 3 defines a notion of symbolic processes. Section 4 shows how to verify that a schedule is compatible with at least one process of the system and measure the probability of such realization. Due to lack of space, proofs and several technical details are omitted, but can be found in Appendix.

Schedules and Stochastic Time Petri Nets

A schedule describes causal dependencies among tasks, and timing constraints on their respective starting dates. Schedules are defined as decorated partial orders. We allow timing constraints among tasks that are not causally related.

Definition 1 (schedule).

A schedule over a finite alphabet A is a quadruple S N, →, λ, C where N is a set of nodes, → ⊆ N × N is an acyclic precedence relation, λ : N → A is a labeling of nodes, and C : N × N → Q >0 is a partial function that associates a time constraint to pairs of nodes. A dating function for a schedule S is a function d : N → Q ≥0 that satisfies all constraints of C and →: n, n ∈ → implies d(n ) ≥ d(n), and C(n, n

) = x implies d(n ) -d(n) ≥ x.
This model for schedules is inspired from [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF][START_REF] D'ariano | Conflict resolution and train speed coordination for solving real-time timetable perturbations[END_REF]. Intuitively, if C(n, n ) = x, then n cannot occur earlier than x time units after n, and if n, n ∈ →, then n (causally) precedes n . Constraints model the minimal times needed to perform tasks and initiate the next ones in production cells, the times needed for trains to move from a station to another, etc.

A schedule S is consistent if the graph N, → ∪ { n, n | C(n, n ) is defined} does not contain cycles. Obviously, consistent schedules admit at least one dating function. A frequent approach is to associate costs to dating functions and to find optimal functions that meet a schedule. A cost example is the earliest completion date. Optimizing this cost amounts to assigning to each node the earliest possible execution date. However, these optimal schedules are not the most probable ones. For the earliest completion date objective, if an event n occurs later than prescribed by d, then all its successors will also be delayed. In real systems running in an uncertain environment (e.g., with human interactions or influenced by weather conditions), tight timings are impossible to achieve. Finding a good schedule is hence a tradeof between maximization of an objective and of the likelihood to stay close to optimal realizations at runtime. We want to check whether a consistent schedule S with its dating function d can be realized by a system. Systems are described with a variant of Petri nets with time and probabilities, namely stochastic time Petri nets [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF]. We will show how to check that (S, d) is realizable by a net N , and then how to measure the probability that (S, d) is realized by N . Roughly speaking, an STPN is a time Petri net with distributions on firing times attached to transitions. As for Petri nets, the semantics of our model moves tokens from the preset of a transition to its postset. The time that must elapse between enabling of a transition and its firing is sampled according to the distribution attached to the transition. The major difference with [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF] is that we equip our STPNs with a blocking semantics. Due to blockings, stochastic time Petri nets are safe (1-bounded). This semantics restriction is justified by the nature of the systems we address: in production chains, places symbolize tools that can process only one item at a time. Similarly, when modeling train networks, an important security requirement is that two trains cannot occupy the same track portion, which can only be implemented with such a blocking semantics. Standard time or stochastic Petri nets do not assume a priori bounds on their markings. A way to force boundedness is to add complementary places to the original Petri net and then study it under the usual semantics [START_REF] Cortadella | Synthesizing Petri nets from state-based models[END_REF]. However, this trick does not allow to preserve time and probability issues in STPNs with blockings.

For simplicity, we only consider closed intervals of the form [a, b] with a < b and open intervals of the form [a, +∞). A probability density function (PDF) for a continuous random variable X is a function f X : R → [0, 1] that describes the relative likelihood for X to take a given value. Its integral over the domain of X is equal to 1. A cumulative distribution function (CDF) F X : R → [0, 1] for X describes the probability for X to take a value less than or equal to a chosen value. We denote by Σ pdf the set of PDFs, Σ cdf the set of CDFs, and we will only consider PDFs for variables representing durations, i.e., whose domains are included in R ≥0 . The CDF of X can be computed from its PDF as F X (x) = x 0 f X (y) dy. Given a finite set of places P , a marking is a function that assigns 0 or 1 token to each place p ∈ P .

Definition 2 (stochastic time Petri net). A stochastic time Petri net (STPN for short) is a tuple N = P, T, • (), () • , m 0 , eft, lft, F, W where P is a finite set of places; T is a finite set of transitions; • () : T → 2 P and () • : T → 2 P are pre and post conditions depicting from which places transitions consume tokens, and to which places they output produced tokens; m 0 : P → {0, 1} is the initial marking of the net; eft : T → Q ≥0 and lft : T → Q ≥0 ∪ {+∞} respectively specify the minimum and maximum time-to-fire that can be sampled for each transition; and F : T → Σ pdf and W : T → R >0 respectively associate a PDF and a strictly positive weight to each transition.

For a given place or transition x ∈ P ∪ T , • x will be called the preset of x, and x • the postset of x. We denote by f t the PDF F(t), and by F t the associated CDF. To be consistent, we assume that for every t ∈ T , the support of f t is [eft(t), lft(t)]. This syntax of STPNs is similar to [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], but we equip them with a blocking semantics, defining sequences of discrete transition firings, and timed moves. We will say that a transition t is enabled by a marking m iff ∀p ∈ • t, m(p) = 1. We denote by enab(m) the set of transitions enabled by a marking m.

For a given marking m and a set of places P , we will denote by m -P the marking that assigns m(p) tokens to each place p ∈ P \ P , and m(p) -1 tokens to each place p ∈ P . Similarly, we will denote by m + P the marking that assigns m(p) tokens to each place p ∈ P \ P , and m(p) + 1 tokens to each place p ∈ P . Firing a transition t is done in two steps and consists in: (1) consuming tokens from • t, leading to a temporary marking m tmp = m -• t, then (2) producing tokens in t • , leading to a marking m = m tmp + t • .

The blocking semantics can be informally described as follows. A variable τ t is attached to each transition t of the net. As soon as the preset of a transition t is marked, τ t is set to a random value ζ t (called the time-to-fire of t, or TTF for short) sampled from [eft(t), lft(t)] according to f t . We will assume that every CDF F t is strictly increasing on [eft(t), lft(t)], which allows to use inverse transform sampling to choose a value (see for instance [START_REF] Rubinstein | Simulation and the Monte Carlo Method[END_REF] for details). Intuitively, this TTF represents a duration that must elapse before firing t once t is enabled. The value of τ t then decreases as time elapses but cannot reach negative values. When the TTF of a transition t reaches 0, then if t • is empty in m tmp , t becomes urgent and has to fire unless another transition with TTF 0 and empty postset fires; otherwise (if t • is not empty in m tmp ), t becomes blocked : its TTF stops decreasing and keeps a null value, and its firing is delayed until the postset of t becomes empty; in the meantime, t can be disabled by the firing of another transition. The semantics of STPNs is urgent: time can elapse by durations that do not exceed the minimal remaining TTF of enabled transitions that are not blocked. If more than one transition is urgent, then the transition that fires is randomly chosen according to the respective weights of urgent transitions. We formalize the semantics of STPNs in terms of discrete and timed moves between configurations that memorize markings and TTFs for enabled transitions.

Definition 3 (configuration of an STPN).

A configuration of an STPN is a pair C N m, τ where m is a marking, and τ : enab(m) → R ≥0 is a function that assigns a positive real TTF τ i τ (t i ) to each transition t i enabled by m. A transition t is enabled in a configuration m, τ iff it is enabled by m. Definition 4 (firable and blocked transitions). A transition t is firable in m, τ iff it is enabled by m, all places of its postset are empty in m -• t, and its TTF is equal to 0. We denote by fira( m, τ ) the set of firable transitions of m, τ . A transition t is blocked in m, τ iff it is enabled by m, its TTF τ (t) is equal to 0, and one of its postset places is marked in m -• t. We denote by blck( m, τ ) the set of blocked transitions in m, τ . Timed moves: A timed move m, τ δ -→ m, τ lets a strictly positive duration δ elapse. To be allowed, δ must be smaller or equal to all TTFs of transitions enabled by m and not yet blocked. The new configuration m, τ decreases TTFs of every enabled and non-blocked transition t by δ time units (τ (t) = τ (t) -δ). Blocked transitions keep a TTF of 0, and m remains unchanged.

Discrete moves:

A discrete move m, τ t -→ m , τ consists in firing a transition t from a configuration m, τ to reach a configuration m , τ . Discrete moves change the marking of a configuration, and sample new times to fire for transitions that become enabled after the move. To define the semantics of discrete moves, we first introduce newly enabled transitions.

Definition 5 (newly enabled transitions). Let m be a marking and t a transition enabled by m. A transition t is newly enabled after firing of t from m iff it is enabled by marking m = (m -• t) + t • and either it is not enabled by m -• t or t = t. We denote by newl(m, t) enab(m ) ∩ ({t} ∪ (T \ enab(m -• t))) the set of transitions newly enabled by firing of t from m.

The transition t fired during a discrete move is chosen among all firable transitions of m, τ . The new marking reached is m = (m -• t) + t • , and τ is obtained by sampling a new TTF for every newly enabled transition and keeping unchanged TTFs of transitions that were enabled by m and are still enabled by m .

For completeness, we give operational rules for moves of STPNs in Appendix A. We will write m, τ → m , τ iff there exists a timed or discrete move from m, τ to m , τ , and m, τ Let us now assign probabilities to STPN moves. Randomness in STPNs semantics mainly comes from sampling of TTFs. However, when several transitions are firable from a configuration, weights are used to determine the probability for a transition to fire first. Timed moves are achieved with probability 1: once TTFs are set, there is a unique configuration allowing discrete moves. In a move m, τ t -→ m , τ , m is built deterministically, but τ is obtained by sampling a random value ζ t for each newly enabled transition t. Each ζ t is chosen according to CDF F t , i.e., we have P(ζ t ≤ x) = F t (x) (for any x ∈ [eft(t), lft(t)]). When more than one transition is firable from m, τ , the transition that fires is randomly chosen, and each transition t k in fira( m, τ ) has a probability to fire P fire (t k ) = W(t k ) ti∈fira( m,τ ) W(t i ). Note that, as STPNs have continuous probability laws, the probability to choose a particular value ζ t is the probability of a point in a continuous domain and is hence null. However, in the next sections, we will consider probabilities for events of the form τ (t i ) ≤ τ (t j ), which may have strictly positive probability.

STPNs define sequences of moves

ρ = ( m, τ ei -→ m , τ ) i∈1...k
, where e i is a transition name in discrete moves and a real value in timed moves. Leaving probabilities for the moment, STPNs can also be seen as generators for timed words over T . A timed word over an alphabet A is a sequence a 1 , d 1 . . . a q , d q . . . in (A × R ≥0 ) * , where each a i is a letter from A, each d i defines the occurrence date of a i , and d 1 , . . . , d q is an increasing sequence of positive real numbers. Letting i 1 , . . . , i q denote the indices of discrete moves in ρ, we can build a timed word u ρ = a i1 , d 1 . . . a iq , d q ∈ (T × R ≥0 ) q that associates dates to transitions firings, where d 1 = j<i1 e j , and d j = d j-1 + ij-1<k<ij e k for j ∈ {2, . . . , q}. The timed language of an STPN N is the set L(N ) of timed words associated with its sequences of moves. We denote by L ≤D (N ) the set of words in L(N ) whose maximal date is lower than D.

As already highlighted in [START_REF] Aura | Time processes for time Petri-nets[END_REF] for TPNs, timed languages give a sequential and interleaved view for executions of inherently concurrent models. A non-interleaved semantics can be defined using time processes, i.e., causal nets equipped with dating functions. We recall that causal nets are finite acyclic nets of the form CN B, E, • (), () B, E, • (), () • is a causal net, and θ : E → R ≥0 associates a positive real date to transitions of the net, and is such that ∀e, e ∈ E with e • ∩ • e = ∅ we have θ(e) ≤ θ(e ). In time processes, places in B are called conditions, and transitions in E are called events. The depth of a time process is the maximal number of events along a path of the graph B ∪ E, • () ∪ () • . We will write e ≺ e iff e • ∩ • e = ∅, and denote by the transitive and reflexive closure of ≺.

Intuitively, conditions in B represent occurrences of places fillings, and events in E are occurrences of transitions firings. Given an STPN N , for every timed word u = a 1 , d 1 . . . a n , d n in L(N ), we can compute a time process TP u = B, E, • (), () • , θ . The construction described below is the same as in [START_REF] Aura | Time processes for time Petri-nets[END_REF]. It does not consider probabilities and, as the construction starts from an executable word, it does not have to handle blockings either. To differentiate occurrences of transitions firings, an event will be defined as a pair e X, t , where t is the transition whose firing is represented e and X is the set of conditions it consumes. Similarly, a condition is defined as a pair b p, e , where p is the place whose filling is represented by b, and e is the event whose occurrence created b.

We will denote by tr(e) the transition t attached to an event e, and by pl(b) the place p associated with a condition b. The flow relations are hence implicit: The time process TP u obtained from a timed word

u = t 1 , d 1 t 2 , d 2 . . . t k , d k ∈ L(N
) is built inductively as follows. We assume a dummy initial event ⊥ that initializes the initial contents of places according to m 0 . We start from the initial process TP 0 = B 0 , E 0 , θ 0 with a set of conditions B 0 = {(p, ⊥) | p ∈ m 0 }, a set of events E 0 = {⊥}, and a function θ 0 : {⊥} → {0}.

Let T P u,i = B i , E i , θ i be the time process built after i steps for the prefix t 1 , d 1 . . . t i , d i of u, and let t, d i+1 be the (i + 1) th entry of u. We denote by last(p, E i , B i ) the last occurrence of place p in TP u,i , i.e., the only condition b = p, e with an empty postset. Then, we have

E i+1 = E i ∪ {e}, where e = t, X with X = {b | b = last(p, E i , B i ) ∧ p ∈ • t} and B i+1 = B i ∪ { p, e | p ∈ t • }.
We also set θ(e) = d i+1 . The construction ends with TP u = TP u,|u| .

Figure 1-b is an example of a time process for STPN N 1 . In this example, event t j i (resp. condition p j i ) denotes the j th occurrence of transition t i (resp. place p i ). This time process corresponds to the time word u = t 1 , 5.5 t 2 , 8.1 t 1 , 8.1 ∈ L(N 1 ). It contains causal dependencies among transitions (e.g., from t 1 1 to t 1 2 ). Event t 2 1 cannot occur before t 1 2 as t 1 cannot fire as long as place p 2 is filled. However, this information is not explicit in the process. The timed language L(N ) of a TPN can be reconstructed as the set of linearizations of its time processes. In these linearizations, ordering of events considers both causality and dates of events: e must precede e = e in a linearization of a process if θ(e) < θ(e ) or if e e . With blocking semantics, some causality and time-preserving interleaving may not be a valid timed word of L(N ): in the process of Figure 1-b, t 2 1 cannot occur before t 1 2 , even if both transitions have the same date. To avoid wrong ordering among events with identical dates, one has to check whether the chosen ordering does not imply firing a transition that should be blocked in one of the reached configurations.

Unfolding of STPNs

A time process emphasizes concurrency but only gives a partial order view of a single timed word. Many time processes of N 1 have the same structure as the process of Figure 1-b, but different dating functions. Indeed, there can be uncountably many time processes with identical structure, but different real dates. It is hence interesting to consider symbolic (time) processes, that define constraints on events dates instead of exact dates. Similarly, to avoid recomputing the structural part of each symbolic process, we will work with unfoldings, i.e., structures that contain all symbolic processes of an STPN, but factorize common prefixes. Symbolic unfoldings were already introduced for TPNs in [START_REF] Semenov | Verification of asynchronous circuits using time Petri net unfolding[END_REF] and later used in [START_REF] Chatain | Time supervision of concurrent systems using symbolic unfoldings of time Petri nets[END_REF]. In this section, we show how to unfold STPNs with blockings and extract symbolic processes out of this unfolding. Our aim is to find the minimal structure that represents prefixes of all symbolic processes that embed a schedule of known duration. We show that if a system cannot execute arbitrary large sets of events without progressing time, unfolding an STPN up to some bounded depth is sufficient.

Definition 7 (time progress

). An STPN N guarantees time progress iff there exists δ ∈ Q >0 such that ∀t ∈ T, i ∈ N, and for every time word

u = t 1 , d 1 . . . t i , θ 1 . . . t i+1 , θ 2 . . . t k , d k ∈ L(N ) where t i denotes the i th occurrence of t, we have θ 2 -θ 1 ≥ δ.
Time progress is close to non-Zenoness property, and is easily met (e.g., if no transition has an earliest firing time of 0). Any execution of duration ∆ of an STPN that guarantees time progress is a sequence of at most

|T | • ∆ δ transitions.
As in processes, unfoldings will contain occurrences of transitions firings (a set of events E), and occurrences of places fillings (a set of conditions B). We associate to each event e ∈ E positive real valued variables doe(e), dof(e) and θ(e) that respectively define the enabling, firability and effective firing date of the occurrence of transition tr(e) represented by event e. A constraint over var(E, B) is a boolean combination of atoms of the form x y, where x ∈ var(E, B), ∈{<, >, ≤, ≥} and y is either a variable from var(E, B) or a constant value. A set of constraints C over a set of variables V is satisfiable iff there exists at least one valuation v : V → R such that replacing each occurrence of each variable x by its valuation v(x) yields a tautology. We denote by SOL(C) the set of valuations that satisfy C.

Definition 8 (unfolding)

. A (structural) unfolding of an STPN N is a pair U E, B where E is a set of events and B a set of conditions.

Unfoldings can be seen as processes with branching. As for processes, each event e ∈ E is a pair e = • e, tr(e) where • e ⊆ B is the set of predecessor conditions of e (the conditions needed for e to occur).

A condition b ∈ B is a pair b • b, pl(b) where • b ⊆ E is
the predecessor of b, i.e., the event that created condition b. We assume a dummy event ⊥ that represents the origin of the initial conditions in an unfolding. Function • (), () • , pl() and tr() keep the same meaning as for time processes. The main change between processes and unfoldings is that conditions may have several successor events. Using relations ≺ and as defined for processes, we define the causal past of an event e ∈ E as ↑ e {e ∈ E | e e}. A set of events E ⊆ E is causally closed iff ∀e ∈ E , ↑ e ⊆ E . We also extend this notion to conditions. We say that two events e, e are in conflict, and write e e, iff • e ∩ • e = ∅. A set of events E ⊆ E is conflict free if it does not contain conflicting pairs of events. Similarly, we will say that two events e, e are competing iff tr(e) • ∩ tr(e ) • = ∅. Intuitively, competing events try to fill the same place.

Definition 9 (pre-processes of an unfolding). A pre-process of a finite unfolding U = E, B is a pair E , B such that E ⊆ E is maximal (i.e., there is no larger pre-process containing E , B ), causally closed and conflict free set of events, and B = • E ∪ E • . We denote by PE(U) the set of pre-processes of U.

We say that a condition b ∈ B is maximal in U = E, B or in a pre-process of U when it has no successor event (b • = ∅), and denote the set of maximal conditions of B by max(B). As for time processes construction, given a finite preprocess E , B ∈ PE(U), and a place p of the considered STPN, we denote by last(p, E , B ) the maximal occurrences of place p w.r.t. ≺ in E , B . A cut of a pre-process is an unordered set of conditions. We denote by Cuts(E, B) the set of cuts of pre-process E, B .

The unfolding of a net up to a fixed depth K is performed inductively, without considering time. We will then use this structure to find processes. Timing issues will be considered through addition of constraints on occurrence dates of events.

Structural unfolding: Following [START_REF] Esparza | An improvement of mcmillan's unfolding algorithm[END_REF], we build inductively unfoldings U 0 , . . . , U K . Each step k adds new events at depth k and their postset to the preceding unfolding U k-1 . We start with the initial unfolding U 0 ∅, B 0 , where B 0 = { ⊥, p | p ∈ m 0 }. Each induction step that builds U k+1 from U k adds new events and conditions to U k as follows. Letting U k = E k , B k be the unfolding obtained at step k, we have

U k+1 = E k ∪ Ê, B k ∪ B where Ê { B, t ∈ (2 B k × T ) \ E k | ∃ X, Y ∈ PE(U k ), B ⊆ Cuts(X, Y ), • t = pl(B)}, and B { e, p ∈ Ê × T | e = B, t ∈ Ê ∧ p ∈ t • }.
Intuitively, Ê adds an occurrence of a transition if its preset is contained in the set of conditions representing the last occurrences of places contained in some pre-process of U k , and B adds the conditions produced by Ê.

The structural unfolding of an STPN does not consider timing issues nor blockings. Hence, an (untimed) pre-process of PE(U K ) need not be the untimed version of a time process obtained from a word in L(N ). Indeed, urgent transitions can forbid firing of other conflicting transitions. Similarly, blockings prevent an event from occurring as long as a condition in its postset is filled. They may even prevent events in a pre-process from being executed if a needed place is never freed. We will show later that, once constrained, time processes of N are only prefixes of pre-processes in PE(U K ) with associated timing function. To introduce timing aspects, we now attach constraints on events and conditions of pre-processes as follows:

Constraints: Let U K = E K , B K be the unfolding of an STPN N up to depth K, and let E ⊆ E K be a conflict free and causally closed set of events, and

B = • E ∪ E • (B is contained in B K ).
We define Φ E,B as the set of constraints attached to events and conditions in E, B, assuming that executions of N start at a fixed date d 0 . Constraints must be set to guarantee that occurrence dates of events are compatible with the earliest and latest firing times of transitions in N , and that urgency or blocking is never violated. Let us first define the constraints associated with each condition b = e, p . Recalling that variable dob(b) represents the date at which condition b is created,

Φ E,B must impose that for every b ∈ B 0 , dob(b) = d 0 .
For all other conditions b = e, p , as the date of birth is exactly the occurrence date of e, we set dob(b) = θ(e) for every b = e, p . Thank to this equality, we need not use both variables θ(e) and dob(b) in our constraints. However, we will use both variables for readability purposes. Recall that dod(b) is a variable that designates the date at which a place is emptied by some transition firing, dod(b) is hence the occurrence date of an event that has b as predecessor. Within a conflict free set of events, this predecessor is unique. In the considered subset of conditions B, several conditions may represent fillings of the same place, and B can hence be partitioned into

B 1 B 2 • • • B |P | ,
where conditions in B i represent fillings of place p i . Due to blocking semantics, all conditions in a particular subset B i = {b i,1 , b i,2 , . . . , b i,k } must have disjoint existence dates, that is for every j, j ∈ {1, 2, . . . , k} with j = j , the intersection between [dob(b i,j ), dod(b i,j )] and [dob(b i,j ), dod(b i,j )] is either empty, or limited to a single value. This constraint can be encoded by the disjunction

no-overlap(b i,j , b i,j )    dod(b i,j ) ≤ dob(b i,j ) ∨ dod(b i,j ) ≤ dob(b i,j ) if b i,j • = ∅ ∧ b i,j • = ∅, dod(b i,j ) ≤ dob(b i,j ) if b i,j • = ∅ ∧ b i,j • = ∅, dod(b i,j ) ≤ dob(b i,j ) otherwise.
Note that if b j b j , then the constraint among events and transitions immediately ensures that dob(b j,i ) ≤ dod(b j,i ) ≤ dob(b j ,i ) ≤ dod(b j ,i ). However, we need to add a consistency constraint for every pair of concurrent conditions b i,j , b i,j that belong to the same B i . Hence, calling I(b i,j , E, B) the set of conditions that represent the same place as b i,j and are concurrent with b i,j in E, B , we have to ensure the constraint non-blocking(b i,j ) b i,j ∈I(bi,j ,E,B) no-overlap(b i,j , b i,j ). In words, condition b i,j does not hold during the validity dates of any concurrent condition representing the same place. This means in particular that a time process of N cannot contain two maximal conditions with the same place.

Let us now consider the constraints attached to events. An event e = B, t is an occurrence of a firing of transition t that needs conditions in B to be fulfilled to become enabled. Calling doe(e) the date of enabling of e, we necessarily have doe(e) = max{dob(b) | b ∈ B}. Event e is firable at least eft(t) time units, and at most lft(t) time units after being enabled. We hence have doe(e) + eft(t) ≤ dof(e) ≤ doe(e) + lft(t). However, execution of e does not always occur immediately when e is firable. Execution of e occurs after e is firable, as soon as the places filled by e are empty, i.e., e occurs at a date θ(e) that guarantees that no place in t • is occupied. This is guaranteed by attaching to every event e the constraints This formula can be translated in boolean combinations of inequalities over variables of var(E, B). Similarly, event e = B, t must occur before all its conflicting events. If an event e in conflict with e is executed, at least one condition in B is consumed, and e cannot occur in a time process containing e . We hence need the additional constraint e e notMoreUrg(e, e ) to guarantee that there exists no other event that is forced to occur before e due to urgency. We define notMoreUrg(e, e ) as the following constraint: Constraint notMoreUrg(e, e ) means that if e is in conflict with e, then at least one condition in • e is consumed before e can fire, or if e becomes firable before e fires, the urgent firing of e is delayed by blockings so that e can occur. As for constraint attached to blockings, notMoreUrg(e, e ) can be expressed as a boolean combination of inequalities. One can also notice that notMoreUrg(e, e ) can be expressed without referring to variables attached to event e nor e • , as doe(e ) = max bi∈ • e dob(b i ) and the intersection of I(b) and e • is void.

(e) = min{x ∈ R ≥0 | x / ∈ ]dob(b), dod(b)[ for some b ∈ I(b i ) ∧ x ≥ dof(e)}.
For causally closed sets of events and conditions E ∪B contained in some pre-process of U K , the constraint Φ E,B applying on events and conditions of E ∪ B is now defined as Φ E,B = x∈E∪B Φ E,B (x) where: e e notMoreUrg(e, e ) We can now define symbolic processes, and show how instantiation of their variables define time processes of N . Roughly speaking, a symbolic process is a prefix of a pre-process of U K (it is hence a a causal net) decorated with a satisfiable set of constraints on occurrence dates of events. Before formalizing symbolic processes, let us highlight three important remarks. Remark 1: an unfolding up to depth K misses some constraints on occurrence dates of events due to blockings by conditions that do not belong to U K but would appear in some larger unfolding U K , with K > K. We will however show (Prop. 1 and 2 that with time progress assumption, unfolding N up to a sufficient depth guarantees that all constraints regarding events with θ(e) ≤ D are considered. This allows to define symbolic processes representing the time processes of N that are executable in less than D time units. Remark 2: unfoldings consider depth of events, and not their dates. Hence if a process contains an event e occurring at some date greater than d, and another event e that belongs to the same pre-process and becomes urgent before date d, then e must belong to the process, even if it lays at a greater depth than e. Remark 3: Every pre-process E, B of U K equipped with constraint Φ E,B is not necessarily a symbolic process. Indeed, some events in a pre-process might be competing for the same resource. Consider for instance the net of Figure 3-a). Its unfolding is represented in b), and two of its (symbolic) processes in c) and d). For readability, we have omitted constraints. One can however notice that there exists no symbolic process containing two occurrences of transition t 3 , because conditions b 5 and b 6 are maximal and represent the same place p 2 . Note that symbolic prefixes define causally closed parts of pre-processes, decorated with constraints inherited from the unfolding U K , that may not be satisfiable.

∀b ∈ B, Φ E,B (b) = non-blocking(b) ∧        dob(b) = d 0 if b ∈ B 0 , and b is maximal, dob(b) = d 0 ∧ dob(b) ≤ dod(b) if b ∈ B 0 , dob(b) = θ( • b) if b / ∈ B 0 and b is maximal, dob(b) = θ( • b) ∧ dob(b) ≤ dod(b) otherwise. ∀e ∈ E, Φ E,B (e) =                doe(e) = max
Definition 11 (symbolic processes). A symbolic process of U K is a triple E s = E , B , Φ E,B where E , B is a symbolic prefix of some pre-process PP = E, B of U K , Φ E,B is satisfiable, and E is maximal w.r.t. urgent events firing in PP, that is for every f ∈ B • ∩ E, and letting C f = pl -1 (f • ) ∩ B denote the set of conditions whose place appears in the postset of e, the following constraint is not satisfiable.

Φ max (f )            Φ E ,B ∧ θ(f ) ≤ max e ∈E θ(e ) f fires before the last event in E' ∧ eft(f ) + max b∈ • f dob(b) ≤ θ(f ) (f is urgent) ∧ X∈2 C f max x∈X dod(x) ≤ θ(f ) ≤ min x∈C f \X dob(x)
(f is not blocked for the whole duration of the process)

Intuitively, Φ max (f ) indicates that the event f that is not in the symbolic process becomes urgent, is not blocked by conditions in B , and has to fire before the execution of the last event in E . If this constraint is satisfiable, then f should appear in the process.

A crux in the construction of symbolic processes of U K is to find appropriate maximal and causally closed sets of events with satisfiable constraints. This can be costly: as exemplified by the example of Figure 3, satisfiability of constraints is not monotonous: the constraints for processes in Fig 3-c) and d) are satisfiable. However, adding one occurrence of transition t 3 yields unsatisfiable constraints. Satisfiability of a prefix of size n hence does not imply satisfiability of a larger prefix of size n + 1. The converse implication is also false: when constraints of a prefix of size n are not satisfiable, appending new events may introduce new blockings and delays urgent transitions, yielding satisfiability of a constraint on a prefix of size n + 1. This means that satisfiability of constraints cannot be a criterion to stop unfolding.

Definition 12 (executions of symbolic processes). Let E s = E, B, Φ be a symbolic process of an unfolding U K . An execution of E s is a time process TP = E, B, θ where θ is a solution for Φ. For a chosen θ, we denote by E s θ = E, B, θ the time process obtained from E s . TP = E, B, θ is a time process of U K if there exists a symbolic process

E s = E, B, Φ of U K s.t. TP is an execution of E s .
Informally, symbolic pre-processes select maximal conflict-free sets of events in an unfolding. Symbolic processes extract executable prefixes from symbolic preprocesses, and executions attach dates to events of symbolic processes to obtain time processes. In the rest of the paper, we respectively denote by E s (U K ) and by E(U K ) the set of symbolic processes and time processes of U K .

We can now show that upon time progress hypothesis, unfoldings and their symbolic processes capture the semantics of STPNs with blockings. Given an STPN that guarantees time progress with a minimal elapsing of δ time units between successive occurrences of every transition, and given a maximal date D, we want to build an unfolding U D of N that contains all events that might be executed before D, but also all places and events which may impact firing dates of these events. We can show that U D is finite and its processes are of depth H = D-d0 δ • |T | at most. Let b = e, p be a condition of an unfolding U n obtained at step n. We denote by block(b) the set of conditions that may occur in the same process as b, represent the same place, and are not predecessors or successors of b in any unfolding U n+k obtained from U n .

Clearly, dates of birth and death of conditions in block(b) may influence the date of birth and death of b, or even prevent b from appearing in the same process as some conditions in block(b). However, in general, block(b) need not be finite, and at step n, block(b) is not fully contained in a pre-process of U n . Fortunately, upon time progress assumption, we can show that elements of block(b) that can influence dob(b) appear.

Proposition 1. Let N be a STPN guaranteeing time progress of δ time units (between consecutive occurrences of each transition). For every date D ∈ R ≥0 and condition b in an unfolding U n , there exists

K ≥ n s.t. {b ∈ block(b) | dob(b ) ≤ D} is contained in U K .
This proposition means that if some event cannot occur at dof(e) due to a blocking, then one can discover all conditions that prevent this firing from occuring in a bounded extension of the current unfolding.

Realizability of schedules

We can now describe a way to check whether a given schedule S, i.e., a highlevel description of operations of a system and of their timing constraints can be realized by a system represented as a STPN N depicting low-level operations and distributions over possible delays between enabledness and firing of transitions. First of all, the connection between the high-level view of operations in S and the lowest level implementation provided by N is defined through a realization function.

Definition 13 (realization function).

A realization function for a schedule S and an STPN N is a map r : A → 2 T that associates a subset of transitions from T to each letter of A, and such that ∀a = a ∈ A, r(a) ∩ r(a ) = ∅.

A realization function describes which low-level actions implement a high-level operation of a schedule. Each letter a from A can be interpreted as an operation performed through the firing of any transition from the subset of transitions r(a).

Allowing r(a) to be a subset of T provides some flexibility in the definition of schedules: in a production cell, for example, a manufacturing step a for an item can be implemented by different processes on different machines. Similarly, in a train network, a departure of a train from a particular station in the schedule can correspond to several departures using different track portions, which is encoded with several transitions in a net. Realization functions hence relate actions in schedules to several transitions in a net. The condition on realization functions prevents ambiguity by enforcing each transition to appear at most once in the image of r. Note that r(A) ⊆ T , that is the realization of a schedule may need many intermediate steps that are depicted in the low-level description of a system, but are not considered in the high-level view provided by a schedule. We will call transitions that belong to r(A) realizations of A.

Definition 14 (embedding, realizability). Let S = N, →, λ, C be a schedule, E s = E, B, Φ be a symbolic process of N and r : N → T be a realization function.

We say that S embeds into E s (w.r.t. r and d) and write S → E s iff there exists an injective function ψ : N → E such that:

               ∀n ∈ N, tr ψ(n) ∈ r λ(n) ∀ n, n ∈→, ψ(n) ψ(n ) f ≤ ψ(min(n)), tr(f ) ∈ r(A) ∀e ≤ f ≤ g, e = ψ(n) ∧ g = ψ(n ) ∧ tr(f ) ∈ r(A) ⇒ ∃n , f = ψ(n ) ∧ n → * n → * n
Intuitively, S embeds in E s iff there is a way to label every node n of S by a letter from r(λ(n)) and obtain a structure that is contained in some restriction of a prefix of E s to events that are realizations of actions from A and to a subset of its causal ordering. This way, a process respects the ordering described in S, does not "forget" actions, and does not "insert" realizations that are not the image by ψ of any high-level operation between two mapped realizations, or before the image by ψ of minimal nodes in the schedule. Note that there can be several ways to embed S into a process of N . i ∈ E S the set of possible embedding functions Ψ i {ψ i,0 , ψ i,1 , . . . , ψ i,Ni-1 } for which the constraints Φ ψi,j ,S,d are satisfiable.

To illustrate the construction of unfoldings and of processes, let us consider the example of figure 4. This simple toy example depicts two train carousels that serve stations. Line 1 serves stations A, B and C, and line 2 serves stations A , B and C . Both lines share a common track portion between stations B, C and B , C , and line 1 uses two trains. A possible required schedule is that one train leaves every 10 time units from station A on line 1, starting from date 10, and one train leaves station C every 10 time units, but starting from date 15. The leftmost picture shows the aspect of both lines and stations. The center picture is an STPN model for this example. We do not precise distributions, and focus on the structural unfolding, on the right of the example. One can notice on this picture that the topmost occurrence of place OK, that plays the role of a boolean flag in a critical section can be both consumed by occurrences t 1 1 and t 2 1 of transition t 1 . However, the second occurrence t 2 1 has an occurrence B 2 of place B in its preset, produced by t 1 6 . Due to blocking semantics, t 1 6 can fire only at dates greater that the date of death of the initial occurrence B 1 of B. As a consequence, no time process of the net can contain at the same time t 1 1 and t 2 1 , even if these transitions are not in conflict. Boolean satisfiability is not sufficient. Consider the net of Figure 5, and the two symbolic processes: one in which transition t 1 fires, and another one in which t 2 fires. The probability of the first process is the probability that a value v 1 sampled to assign a TTF for t 1 is smaller or equal to another value v 2 sampled independently to assign a TTF for t 2 . Clearly, the probability that v 1 ≤ v 2 is equal to the probabilty that v 1 ∈ [0, 1]. The probability of the second process is equal to the probability that v 1 ≥ v 2 , but the set of values allowing this inequality is restricted to a single

B B' C C' A D 1 2 B t1 BC t2 C t3 CA t4 A t5 AB t6 B' t7 BC' t8 C' t9 CD t10 D t11 DB t12 OK B 1 D 1 CA 1 t 1 1 t 1 11 t 1 4 BC 1 DB 1 A 1 t 1 2 t 1 12 t 1 5 C 1 B' 1 AB 1 OK 1 t 1 6 B 2 t 1 3 CA 1 t 1 4 t 1 7 t 2 1 A 1 BC' 1 BC 2 OK 2 t 2 7 t 3 1 BC 2 BC' 2
Fig. 4: A toy example : realizability of a partial schedule for two train carroussels with shared track portions.

point v 1 = 1, v 2 = 1.
Conforming to continous probability distribution semantics, the probability of this point is equal to zero. A schedule composed of a single node n with date 1 such that r(λ(n)) = {t 2 } is realizable according to Definition 14, but with null probability. A more accurate notion of realizability is to require that schedules embed into symbolic processes of U K with non-null probability. This raises a second issue: requiring a schedule to be realized with an exact timing also leads to realizations with null probabilities. Consider the former example: a schedule composed of a single node n, a realization function r s.t. r(λ(n)) = {t 2 }, and a dating function d s.t. d(n) = 2. Assign interval [0, 3] to transition t 1 in the net of Figure 5-a) and interval [START_REF] Aghasaryan | Fault detection and diagnosis in distributed systems: An approach by partially stochastic Petri nets[END_REF][START_REF] Carey | Ex ante heuristic measures of schedule reliability[END_REF] to transition t 2 . The probability that t 2 fires from the initial marking is equal to the probability that v 1 ≥ v 2 , which is not null (we will explain later how to compute the probability of such domain and the joint probability of v 1 , v 2 ), and is equal to the probability of the domain for values of v 1 , v 2 depicted by the colored zone in Figure 5-b). However, within this continuous domain of possible values, the probability to fire t 2 exactly at precise date 2 as required by dating function d is still null. We hence consider realizability of a schedule up to some admissible delay α. The constraint to meet once an injection ψ is found for a schedule S into a symbolic process E s hence becomes:

Φ ψ,S,d±α = Φ ∧ n∈N max(d(n) -α, 0) ≤ θ(ψ(n)) ≤ d(n) + α.

Definition 16 (probabilistic realizability).

A schedule with maximal date D is realizable with non-null probability iff there exists an embedding ψ of S into a symbolic process E s of U K s.t. P(E s ∧ Sol(Φ ψ,S,d±α )) > 0.

Intuitively, this definition requires that a symbolic process embeds S, and that the probability that this process is executed and satisfies all timing constraints imposed by the STPN and by the dating function is non-null. This probability can be evalu- ated using a transient execution tree, as proposed in [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF]. Roughly speaking, nodes of this tree are abstract representations of time domains for sampled values attached to enabled transitions (this is the usual notion of state class, already used in [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF][START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF] to analyze time Petri nets). In addition to state classes, transient tree nodes contain abstract representations of probability distributions. If the definition of distribution is appropriately chosen, for instance, using truncated sums of exponentials of the form

f (x) = c k x a k e -λ k x if x ∈ [a, b] 0 otherwise
then the distributions obtained by projection, multiplication, or variable elimination can still be encoded as sums of exponentials, and memorized using a finite set of parameters. The probability to fire a particular transition from a state and move to a successor node is computed as an integration over the time domains allowing this transition to fire first. The children of a node give a probabilistic distribution on possible classes of successor states. As time progress is guaranteeed in our model, a finite tree representing executions of an STPN or of one of its processes up to some bounded duration can be built. As explained in [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], the sum of probabilities attached to all paths of the tree can be used to compute the probability of some properties. In our case, the sum of probabilities of all paths that end with the execution of a chosen symbolic process gives the probability to realize this process. Details on the construction of this transient tree are provided in Appendix.

Conclusion

Related work : This work addresses realizability of partially ordered timed schedules by timed and stochastic concurrent systems with blocking semantics. Realizability in a timed setting has been addressed as a timed game problem [START_REF] Doyen | Realizability of real-time logics[END_REF], with a boolean answer. The objective in this work is to check whether a player in a timed game has a strategy to ensure satisfaction of a formula written in a timed logic called Metric Interval Temporal Logic. Brought back to the setting of realizability of schedules, the work of [START_REF] Doyen | Realizability of real-time logics[END_REF] can be used to answer a boolean realization question, by translating a schedule to a formula. However, the work of [START_REF] Doyen | Realizability of real-time logics[END_REF] lies in an interleaved setting: a sequential formula can not differentiate interleaved and concurrent actions. It does not address randomness in systems and hence can not quantify realizability. Scheduling of train networks was already addressed as a contraint satisfaction problems [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF]. The input of the problem is given as an alternative graph (that can be seen as some kind of unfolding of a systems's behavior, decorated with time constraints. The algorithms provided by [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF] returns an optimal schedule for the next 2 hours of operation of a train network, using a branch and bound algorithm. However randomness was not addressed in this work. In [START_REF] Carey | Ex ante heuristic measures of schedule reliability[END_REF], stability of timetables with a stochatics model is considered.

Realizability is also close to diagnosis question: given a log (a partial observation of a run of a system), and a model for this system, diagnosis aims at finding all possible runs of the model of the system which partial observation complies with the log. Diagnosis was addressed for stochastic Petri nets in [START_REF] Aghasaryan | Fault detection and diagnosis in distributed systems: An approach by partially stochastic Petri nets[END_REF]. In this work, the likelihood of a process that complies with an observation is evaluated, and time is a seen as a sequence of discrete instants. Diagnosis was addressed for timed Petri nets in [START_REF] Chatain | Symbolic diagnosis of partially observable concurrent systems[END_REF], where unfolding of a timed Petri net is built to explain an observed log. [START_REF] Dousson | Extending and unifying chronicle representation with event counters[END_REF] proposes temporal patterns called chronicles that represent possible evolutions of an observed system. A chronicle is a set of events, linked together by time constraints. The diagnosis proposed is to explain stream of time-stamped events as combinations of chronicles. assembling chronicles can be seen as some kind of timed unfolding. However, the run to explain is not a concurrent model as for schedules, and chronicles do not address randomness in timed systems. Schedulability can also be seen as conformance of an expected behavior (the schedule) to an implementation (the Petri net model). Conformance was defined as a timed IOCO relation between timed input/output automata in [START_REF] Krichen | Conformance testing for real-time systems[END_REF]. More precisely, A 1 IOCO A 2 iff after some timed word, the set of outputs produced by A 1 is included in the outputs produced by A 1 . This relation can not be verified in general (as inclusion of timed automata languages is not decidable), but can be tested. Boolean realizability can be seen as some kind of conformance test. Note however that TIOCO is defined for an interleaved timed model without probabilization of transitions.

Conclusion:

The techniques described in this work first build an unfolding U K up to a depth K that depends on the maximal date appearing in the schedule, finds symbolic processes of U K that embed the schedule, and then checks that at least one of them has non-null probability. So far, we did not consider complexity issues. The size of an unfolding can grow exponentially w.r.t. its depth. Checking satisfiability of a set of constraints with disjunctions can also be costly. Satisfiability of constraints is not monotonous and hence cannot be used to stop unfolding. However, embedding verification and unfolding can be done jointly: one can stop a branch of unfolding as soon as a schedule does not embed in the pre-process on this branch. Most of the constraints presented in this paper can be simplified, and refer mainly to event variables. One can also notice that atoms in constraints are rather simple inequalities, which could simplify their verification. Computation of realization probability for processes can also be improved. We use the transient tree construction of [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], that builds a symbolic but interleaved representation of some processes. This is obviously very costly. We are currently investigating the possibility to attach probabilities to symbolic processes without computing an interleaved representation.

As future work, we would like to implement and improve this realizability verification framework, and use it as a basis to prove more properties. For instance, it might be interesting to prove that a schedule can be realized while ensuring that the overall sum of delays w.r.t the expected schedule does not exceed some threshold. Another improvement would be to provide means to compute an exact value for the realization probability. We are also interested in the design of controllers that maximize the probability of realization.

A Formal semantics of STPNs

Timed moves are formally defined by the following rule:

δ > 0 ∧ ∀t ∈ enab(m) \ blck( m, τ ), τ (t) ≥ δ ∧ τ (t) = τ (t) -δ ∧ ∀t ∈ blck( m, τ ), τ (t) = τ (t) m, τ δ -→ m, τ
A transition t is persistent after firing of t from m iff it is enabled in m, t = t , and t is enabled in m -• t. We denote by pers(m, t) = (enab(m) ∩ enab(m tmp )) \ {t} the set of persistent transitions after firing of t from m.

Discrete moves are formally defined by the following operational rule:

t ∈ fira( m, τ ) ∧ m = (m -• t) + t • ∧ ∀t i ∈ pers(m, t), τ (t i ) = τ (t i ) ∧ ∀t i ∈ newl(m, t), τ (t i ) ∈ [eft(t), lft(t)] m, τ t - → m , τ

B Proof of proposition 1

Proposition 1. Let N be a STPN guaranteeing time progress of δ time units (between consecutive occurrences of each transition). For every date D ∈ R ≥0 and condition b in an unfolding U n , there exists

K ≥ n s.t. {b ∈ block(b) | dob(b ) ≤ D} is contained in U K .
Proof. Consider a pre-process P P of U n , which depth is more than D δ .|T | events. Every event of the unfolding appended at depth i consumes conditions that were created at depth j < i, and at least one condition that was produced at step i of the unfolding. Hence, for every event e n and b n condition created at depth n, there exists a sequence b 0 < e 1 < b 1 < • • • < e n < b n of events and conditions of increasing depth (and also increasing dates). With the time progress assumption, we know that every consecutive pair of events representing the same transition occurs at lest at dates that differ by δ. Hence, an event created at depth n has an occurrence date of at least δ. n/|T | . The occurrence date of an event created at depth greater than D δ .|T | is hence greater than D. The number of events and conditions created at step n and appearing in the same pre-process of U n is finite (as creating an event uses exclusively at least one condition of the preceding step). It is hence sufficient to unfold a net up to depth D δ .|T | to obtain the (finite) set of conditions that refer to the same place as some condition b before a given date D.

C Proof of Proposition 2

Proposition 2. Let N be a STPN guaranteeing time progress of δ time units. The set of time processes executable by N in D time units are prefixes of time processes of U K , with K = D δ • |T | containing only events with date ≤ D.

Proof. We will show inclusion of the set of processes in the two directions. First of all, we define an ordering on symbolic processes. Let E s = E, B, Φ and E s = E , B , Φ be two symbolic processes. We will say that E s E s iff there exists an event e such that E = E ∪ {e }, B = B ∪ e • , and Φ = Φ |var(E,B) .

Lemma 1. Let E s be a symbolic process of unfolding U K , starting from m 0 , d 0 , that is satisfiable and complete. Let θ be one of its solutions guaranteeing ∀e ∈ E, θ(e) ≤ D. Then, there exists a sequence

E s,0 = E 0 , B 0 , Φ 0 E s,1 = E 1 , B 1 , Φ 1 • • • E s of symbolic processes of U K such that E 0 = ∅, B 0 = { ⊥, p | p ∈ m 0 } Φ 0 = {θ(⊥) = d 0 ∧ b∈B0 dob(b) = d 0 }
and θ is a solution for every E s,i and θ(e i ) ≤ θ(e i + 1).

Proof. We can show this property by induction on the size of prefixes of E s . The base hypothesis is straightforward, taking the sequence with only one symbolic process E s,0 without events. Suppose that this property is satisfied for symbolic processes up to size n, and consider a satisfiable and complete symbolic process E s,n+1 of size n + 1. Let θ n+1 denote a solution for this process. A growing sequence from E s,0 to E s,n+1 exists.In this sequence, the difference between E s,n+1 and E s,n is a single event e that is maximal in E s,n+1 w.r.t. ordering on events , and such that θ(e) ≥ θ(x) for every event x in E s,n+1 \ {e}, and θ(e) ≥ dob(b) for every b in E s,n+1 \ {e}. Let E n , B n denote the set of events in E s,n+1 \ {e}. Let us denote by Φ n+1|E n ,B n the restiction of Φ n+1 to variables attached to events and conditions E n , B n . One has to remove variables θ(e), dod(b) for every b ∈ • e, and dob(b) for every b ∈ e • using an elimination technique such as Fourier-Motzkin. Using the properties of elimination, θ satisfies Φ n+1 if and only if the restriction of θ to var(E n , B n ) satisfies Φ n+1|E n ,B n . However, the restriction of θ is exactly θ n , and as θ(e), dod(b) for b ∈ e • , and dod(b) for b ∈ • e are all greater than variables in var(E n , B n ), the elimination of variables is simply a projection on atoms that do not contain variables related to e, and Φ n+1|E n ,B n = Φ n .

Lemma 2. Given a symbolic process E s of U K , one of its solutions θ, and an ordering

E s,0 = E 0 , B 0 , Φ 0 E s,1 = E 1 , B 1 , Φ 1 • • • E s as above, then the word u E s ,θ = t 1 , θ(e 1 ) . . . t |E| , θ(e |E| ) is a timed word of L(N ).
Proof. Again we can prove this lemma by induction. The base case is obvious, as the empty word is a timed word of L(N ). Let us suppose that the property is satisfied up to n, that is for every process E n of size n and solution θ n meeting all constraints of E n , there exists an increasing sequence of prefixes of E n such that the word associated with this sequence is a timed word of L(N ).

Let us now consider a time process E n+1 with n + 1 events and one of its solutions θ n+1 . As in Lemma 1, one can find an event e n+1 and a process E n such that E n and E n+1 only differ by addition of this single event. There exists a timed word u n = e 1 , θ n+1 (e 1 ) . . . e n , θ n+1 (e n ) ∈ L(N ) corresponding to E n . This word may lead the net to any configurations in a set Conf n with identical markings, but distinct times to fire attached to transitions. However, as we know that θ n+1 meets all constraints of E n+1 , there exists a configuraton in Conf n whose times to fire allow firing of e n+1 at date θ(e n+1 ), and u n+1 = u n . e n+1 , θ(e n+1 ) ∈ L(N ).

Note that assuming time progress, the dates attached to an event of a process of U K that occur at a date smaller than D cannot be further constrained by addition of constraints coming from events that are not in U K . The two lemmas above hence allow to conclude that for a given symbolic process E s of unfolding U K , in which one considers events that occur before date D, and for each solution of E s , we have E s θ = T P u E s ,θ for some word u E s ,θ ∈ L(N ). Hence, the set of time processes of U K whose events occur before D is contained in the set of time processes T P (L ≤D (N )). All time processes of some pre-process of U K (and hence all time processes of unfolding U K ) can be built from a timed word that is executable by N in less than D time units, and are hence time processes of N .

We now have to prove the converse direction, i.e., every time process associated with a word u ∈ L ≤D (N ) is a time process of U K . Lemma 3. Let u ∈ L ≤D (N ). Then, T P (u) is a time process of U K .

Proof. We proceed by induction on the size of words. First, for the empty words, the time process with only initial conditions is clearly a time process of U K . Let us now assume that for every u n = e 1 , θ(e 1 ) . . . e n , θ(e n ) ∈ L ≤D (N ) of length n, T P (u n ) is a time process of U K . Let us consider a word u n+1 = e 1 , θ(e 1 ) . . . e n , θ(e n ) . e n+1 , θ(e n+1 ) ∈ L ≤D (N ). One can build a time process E u for u = e 1 , θ(e 1 ) . . . e n , θ(e n ) . Clearly, as u n+1 ∈ L ≤D (N ), word u leads from marking m 0 to a marking that enables e n+1 . Let e p1 , . . . , e p k denote the k events that produce the tokens that are consumed by e n+1 . If event e n+1 is a firing of some transition t that occurs exactly when its time to fire has expired, θ(e n+1 ) meets the constraint eft(t) + max{θ(e pi )} ≤ θ(e n+1 ) ≤ lft(t) + max{θ(e pi )}. In any case, we have ef t(t)+ max{θ(e pi )} ≤ θ(e n+1 ) (which is the only constraint w.r.t predecessors imposed by constraint in the unfolding. Similarly, let e b1 , . . . e bq denote the last events of u that free places in which t outputs some tokens (and hence may have blocked the execution of t before θ(e n+1 )). We have θ(e n+1 ) meets the constraint max({θ(e bi )}) ≤ θ(e n+1 ). Hence, any event that had to occur before θ(e n+1 ) (due to urgency, causality, or blockings) also appears in E u . Hence, θ witnesses satisfiability of a set of constraints over occurrence dates of events e 1 , . . . , e n , and one can safely append e n+1 = (B, t) to maximal places of E u , and obtain a symbolic prefix E un+1 (satisfiable, conflict free and complete). It now remains to show that E un+1 is a symbolic process of U K . As θ(e n+1 ) ≤ D, e n+1 appears in the unfolding of N at depth at most D δ , which is lower than

K = D δ • |T |.
Hence, E un+1 is an causally closed set of events that also contains all mandatory urgent transition firings and place unblockings whose set of constraints is satisfiable, and contained in U K , i.e., it is a symbolic process of U K .

D Algorithm to compute embeddings of a schedule in a process

Finding the set of embedding functions Ψ {ψ 0 , ψ 1 , . . . , ψ k } that satisfy the conditions of definition 14 is achieved building iteratively injective functions meeting the embedding requirements, by matching at every step minimal yet unexplored nodes of S with minimal unmatched nodes of E s . This construction is depicted in Algorithm 1. We will define an embedding function f as a set pairs of the form n, e , interpreted as f (n) = e. We define in particular the empty embedding f ⊥ , that is undefined for every node of N , and will be used as starting point of the algorithm. For a given function f , the function f ∪ n, e is the function that associates e to node n, and f (n ) to every other node n ∈ domain(f ).

E Stochastic state class tree

In this part of the appendix, we detail how to build a stochastic state class tree for a particular process of a stochastic Petri net with blocking seantics. The domain D of τ ¯is simply the domain of a class as defined in the usual state class graph construction of TPNs (see for instance [START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF][START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF]). It represents possible values for TTFs attached to transitions. As our STPN is bounded, the number of domains that can be generated inductively at construction time is finite (as proved by [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF]). Urgent and blocked transitions are also finite subsets of T . However, as shown in [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], the number of distributions that can be iteratively computed needs not be finite.

Definition 18 (transient stochastic state class tree).

A transient stochastic state class tree for an STPN N (that we shall call tree, for short) is a directed acyclic graph S V, •→ ∪ •→ where vertices in V are classes, edges in •→ represent firing transitions after (symbolically) elapsing time, and edges in •→ represent firings of urgent transitions. Every vertex in the tree has only one predecessor except for the root of the tree, denoted v 0 , that has no predecessor. Edges carry probabilistic informations on transitions firings and the sum of probabilities of all edges leaving the same vertex is equal to 1.

The construction of a tree starts from the initial class Σ 0 (with marking m 0 , a domain D 0 for the TTFs of transitions enabled in m 0 and all other components defined accordingly, see appendix E) and inductively computes edges and reachable classes. Edges Σ t,µ -→ Σ from a class Σ to a successor class Σ are labeled by a transition name t and by the probability µ to fire t from Σ, and are of two forms:

Firing after elapsing time:

A move Σ ti,µi •→ Σ from Σ = m, D, f τ ˜, blk, urg to Σ = m , D , f τ
˜, blk , urg , achievable with probability µ i , consists in firing transition t i after symbolically elapsing its TTF. Such a move is only allowed if urg = ∅ and the TTF τ i of t i is less than or equal to TTFs of all other transitions that could fire from Σ. The time domain D i from which t i can fire is hence D i D ∩ τj ∈τ ¯{τ i ≤ τ j }, and the probability of firing t i from Σ is

µ i = D i f τ ˜(x ˜) dx ˜. We have m = m -• t i + t i • .
The new domain D and distribution f τ ˜are computed as for STPNs with non-blocking semantics: Vector τ ˜is obtained by advancing time, removing variables of disabled transitions and adding those of newly enabled transitions [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], and then removing variables of transitions whose domain is the singleton {0}. The domain of a single variable τ i in a domain D over several variables can be obtained by eliminating all variables but τ i from D. As soon as a variable has domain {0}, the time to fire of the associated transition is necessarily zero, and the transition has to fire. It is then stored in the set of urgent transitions if it is not blocked, and in the set of blocked transitions otherwise. The set blk is obtained by removing from blk transitions that were disabled by firing of t i and transitions that are not blocked anymore in m thanks to the places freed by firing of t i (they become urgent), and adding transitions which are enabled in m with a firing domain in D that is {0}. Finally, the set urg contains all enabled transitions that became urgent when firing t i , i.e., transitions with firing domain {0} among enabled transitions, and formerly blocked transitions unblocked by t i .

Firing urgent transitions: In STPNs semantics, when more than one transition is firable from a configuration, their weights are used to compute the probability of firing each transition. This case can occur because of blocking semantics: an STPN can keep several transitions blocked, and firing a transition can also unlock several of them at the same time (all unblocked transitions become urgent). When a class Σ has urgent transitions (urg = ∅), only moves of the form Σ ti,µi

•→ Σ are allowed. They consist in firing a transition t i among urgent transitions in urg with probability µ i = W(t k ) tj ∈urg W(t j ). Components m , D and f τ ˜of the successor class are computed as for timed moves, with the only difference that no time elapses before the firing of t i . Set blk is obtained by removing from blk transitions that are unlocked or disabled by the firing of t i and adding those that become blocked in m , and urg' contains transitions from urg that were not disabled by firing of t i and transitions from blk that were unblocked when firing t i .

Transient trees are a priori infinite, but very often, one can work with a bounded horizon. This is our case when evaluating the probabilty of realization in U K . Let Ψ i {ψ i,0 , ψ i,1 , . . . , ψ i,n-1 } denote all possible embeddings of a schedule S into a symbolic process E s i of N . We denote by P(Φ ψi,j ,d±α ) the probability that N executes a time process E s i and realizes S within a precision of ±α when ψ i,j is the embedding of S in E s i . We adapt the tree construction to consider only E s i and embedding ψ i,j , and compute P(E s i ∧ Φ ψi,j ,d±α ). We build a tree whose vertices of the form Σ, S memorize a class and a suffix of E s

i not yet executed. We start from vertex Σ 0 , E s i . We create an edge Σ, S t k ,µ k ---→ (Σ , S ) representing firing of a transition t k if there is a minimal event e in the remaining suffix of E s i , and tr(e) = t k . S is the new suffix obtained by removing e from S. Σ is the successor class obtained after firing this transition from Σ. Edges are built as before in the tree, but with an additional constraint: edges with label t k , µ k and components m, D, f τ ˜, blk, urg of classes are built with the additional requirement that when creating an edge from an event e that is in the image of ψ i,j , the firing time domain is restricted to impose that e occurs in the time interval

I k = [max(0, d(ψ -1 i,j (e)) -α), d(ψ -1 i,j (e)) + α]. In this case, the probability of firing t k = tr(e) becomes µ k = D k ∩ D k f τ ˜(x ˜) dx ˜
, where D k is the part of D in which τ k -τ age (the firing date for e) belongs to I k . We stop developing a branch of the tree at vertices whose suffix does not contain events that are images of nodes in S via ψ i,j . The construction ends with a tree S i,j,α .

Transient tree S i,j,α measures the probability of solutions and of occurrence of a particular process. The probability P(E s i ∧ Φ ψi,j ,α ) is computed as P(E s i ∧ Φ ψi,j ,α ) = ρ∈Path(S i,j,α ) P(ρ) where Path(S i,j,α ) is the set of paths from Σ 0 , E s i to a leaf of S i,j,α , and the probability P(ρ) of a path ρ = Σ 0 ti,µi ---→ . . . ------→ Σ l that start at Σ 0 and end on a leaf Σ l is the product Π i∈{0,...,l-1} µ i . As soon as P(E s i ∧Φ ψi,j ,α ) > 0, S has a non-null probability to be realized (with a tolerance of ±α). Noticing that different embeddings yield disjoint paths in their respective transient stochastic state class trees, the probability for a schedule to be realized by a process is hence P(E s i |= S) = ψi,j ∈Ψi P(E s i ∧ Φ ψi,j ,α ). Finally, denoting by E(PP, S) the symbolic processes of a pre-process PP that embed S, the probability P(N |= S) is greater than max{P(E s i ∧ Φ ψi,j ,α ) | PP ∈ PE(U K ) ∧ E s i ∈ E(PP, S)}. It is difficult to obtain more than a lower bound for realization, as symbolic processes of E(PP, S) might have overlapping executions.

F Derivation of components of successor class

We hereafter provide details on how to compute components D and f τ ˜ of a class Σ obtained from a class Σ through a transition ti,µi

•→ . Derivation of components m , blk and urg has already been covered and need not further explanations.

We shall use the following notations:

given a time domain D delimiting the possible values of a set of variables x ¯= x 0 , x 1 , . . . , x N -1 , we will denote by D ↓ xi the projection of D that eliminates variable x i from x ¯. The elimination is done via the Fourier-Motzkin method detailed in Appendix G; given a vector x ¯= x 0 , x 1 , . . . , x N -1 , we denote by x ¯\ x i the vector x ¯from which variable x i is removed, with i ∈ {0, 1, . . . , N -1}; the addition of a scalar x 0 to each element of a vector x ¯= x 1 , x 2 , . . . , x n is simply written x ¯+ x 0 .

Fist of all, the initial class is Σ 0 m 0 , D 0 , f τ 0 ˜, blk 0 , urg 0 . Marking m 0 is the initial marking of the net, domain D 0 is a product of domains [ef t(t), lf t(t) for all transitions enabled in m 0 (their domain is not {0} as we have ef t(t) < lf t(t). Vector τ 0 ˜=< 0, τ 1 , τ enab(m0) is a vector representing elapsed time (in the inital class it must be 0, and times to fires of enabeled variables. As domains for τ i 's are not singletons, we can safely set blk 0 = ∅, and urg 0 = ∅. Probability of firing: A transition t i can fire from class Σ iff t i is enabled by m and no postset place of t i is occupied; that is ∀p ∈ t • , m(p) = 0. We also need its TTF τ i to be less than or equal to TTFs of all variables in τ ˜; transition t i will then fire from Σ with probability µ i , with:

µ i = D i f τ ˜(x ˜) dx Di
is the time domain from which t i shall fire with all its TTF less than or equal to every variable in τ ¯.

D i D ∩ t j ∈τ ¯{τ i ≤ τ j }
Precedence condition:

The assumption that t i fires before any other transition adds conditions on the time vector and thus leads to a new random variable τ ˜a distributed over D i according to the following conditional PDF:

f τ ˜a (x ˜) = f τ ˜(x ˜) µ i
Time elapsing and elimination: According to the semantics of STPNs, when t i fires, TTFs of activated transitions are decreased by the value of the TTF of t i , namely τ i . This yields a new random variable τ ˜b = τ ˜a -τ i distributed over the domain D b = D i ↓ τ i in which the variable attached to the fired transition t i is eliminated. The PDF of the new multivariate random variable τ ˜b is then:

f τ ˜b (x ˜) = Max i Min i f τ ˜a (x ˜+ x i , x i ) dx i
where Min i and Max i denote the bounds of the support of variable τ i .

Disabling: If the firing of t i disables a transition t j , variable τ j b has to be eliminated The same procedure is repeated for every disabled transition by the firing of t i . Let τ ˜c * , D c * and f τ ˜c * then respectively denote the resulting time vector, domain and PDF.

Newly enabling: If the firing of t i enables a transition t k , with PDF f t k over [eft(t k ), lft(t k )], then the new time vector, that we denote by τ ˜d, shall include an additional component τ k d and shall be distributed over D d = D c * × [eft(t k ), lft(t k )] according to the PDF:

f τ ˜d (x ˜, x k ) = f τ ˜c * (x ˜) × f t k (x k )
The same procedure is similarly repeated for every newly enabled transition to finally obtain the PDF of the successor class Σ .

G Fourier-Motzkin elimination method

The Fourier-Motzkin elimination method is an algorithm for eliminating variables from a system of linear inequalities. Let φ be a system of linear inequalities with variables x 1 , x 2 , . . . , x r where x r is the variable to be removed. φ can be written as are the sets of inequations where the coefficients of x r are respectively negative and positive, and φ ∅ is the inequations subsystem in which x r doesn't appear.

Eliminating the variable x r from φ refers to the creation of another system of inequations in which x r doesn't appear and which has the same solutions over the remaining variables. The original system can be written as Let φ be the following system of linear inequalities:

φ =                    α 1 ≤ x 1 ≤ β 1 α 2 ≤ x 2 ≤ β 2 α 3 ≤ x 3 ≤ β 3 -γ 21 ≤ x 1 -x 2 ≤ γ 12 -γ 31 ≤ x 1 -x 3 ≤ γ 13 -γ 32 ≤ x 2 -x 3 ≤ γ 23
Suppose that we want to eliminate the variable x 1 . We start by identifying φ ∅ , the subsystem of inequations in which x 1 doesn't appear, as follows:

φ =                    α 1 ≤ x 1 ≤ β 1 -γ 21 ≤ x 1 -x 2 ≤ γ 12 -γ 31 ≤ x 1 -x 3 ≤ γ 13 α 2 ≤ x 2 ≤ β 2 α 3 ≤ x 3 ≤ β 3 -γ 32 ≤ x 2 -x 3 ≤ γ 23      = φ ∅
We then isolate x 1 by rewriting the inequations left, as follows:

φ =          α 1 ≤ x 1 ≤ β 1 x 2 -γ 21 ≤ x 1 ≤ x 2 + γ 12 x 3 -γ 31 ≤ x 1 ≤ x 3 + γ 13 φ ∅
One can easily see that an equivalent solution of this system is the one where x 1 is bounded with the maximum value of its left bounds and the minimum of its right bounds in the system of inequations; adding to that φ ∅ .

φ ⇐⇒ max(α 1 , x 2 -γ 21 , x 3 -γ 31 ) ≤ x 1 ≤ min(β 1 , x 2 + γ 12 , ≤ x 3 + γ 13 ) ∧ φ ∅ Finally, eliminating x 1 consists in saying that the left bound is inferior or equal to the right bound and we get the following:

φ ⇐⇒ max(α 1 , x 2 -γ 21 , x 3 -γ 31 ) ≤ min(β 1 , x 2 + γ 12 , ≤ x 3 + γ 13 ) ∧ φ ∅

Fig. 1 :

 1 Fig. 1: a) An example STPN N 1 and b) a time process of N 1Consider the STPN N 1 of Figure1, and suppose that N 1 is in configuration m, τ , with m(p 1 ) = 1, m(p 2 ) = m(p 3 ) = 0, τ (t 1 ) = 5.5. From this configuration, one can let 5.5 time units elapse, and then fire t 1 . After this firing, the STPN reaches marking m with m (p 1 ) = m (p 2 ) = 1, m (p 3 ) = 0. New TTFs d 1 , d 2 are sampled for t 1 , t 2 , leading to a configuration m , τ , where τ (t 1 ) = d 1 and τ (t 2 ) = d 2 . Let us suppose that d 1 = 1.5 and d 2 = 2.6. Then one can let 1.5 time units elapse, but after this timed move, transition t 1 cannot fire, as place p 2 contains a token. N 1 is hence in a configuration m , τ , where τ (t 1 ) = 0 and τ (t 2 ) = 1.1, where t 1 is blocked. After letting 1.1 time units elapse, transition t 2 can fire, leading to marking m (p 1 ) = m (p 3 ) = 1, m (p 2 ) = 0, and transition t 1 immediately fires at the same date.

•e

  = {b | e = X, t ∧ b ∈ X}, and similarly e • = {b | b = p, e }, and for b = p, e , • b = e and b • = {e ∈ E | b ∈ • e}. We will then drop flow relations and simply refer to time processes as triples TP B, E, θ .

  Similarly, we associate to each condition b positive real valued variables dob(b) and dod(b) that respectively represent the date of birth of the token in place pl(b), and the date at which the token in place pl(b) is consumed. We denote by var(E, B) the set of variables e∈E doe(e) ∪ dof(e) ∪ θ(e) ∪ b∈B dob(b) ∪ dod(b).

  θ(e) = dob(b 1 ), θ(e) = dob(b 2 ), . . . , θ(e) = dob(b k ), where {b 1 , b 2 , . . . b k } = e • , and constraints non-blocking(b 1 ), non-blocking(b 2 ), . . . , non-blocking(b k ). Last, as semantics of STPN is urgent, once firable, e has to fire at the earliest possible date. This is encoded by the constraint θ

Fig. 2 :

 2 Fig. 2: Constraints on dates of birth of tokens in a shared place. Written differently, θ(e) = dof(e) if b∈I(b1)∪...I(b k ) dof(e) ≤ dob(b), and min{dod(b) | ∀b ∈ bi∈e • I(b i ), dod(b) / ∈ ]dob(b ), dod(b )[} otherwise.

  notMoreUrg(e, e ) θ(e) ≥ doe(e ) + lft(tr(e )) ⇒ tiled(e, e ) ∨ e ||e preempts(e , e ) where tiled(e, e ) free(e ) ∩ [doe(e ) + lft(tr(e )), θ(e)] = ∅, e ||e refers to event that are concurrent with e in the considered set of events, free(e ) = R ≥0 \ {[dob(b), dod(b)] | ∃b ∈ e • , b ∈ I(b )} is the set of intervals in which places attached to conditions in e • are empty, and preempts(e , e ) θ(e ) ≤ min(]doe(e ) + lft(tr(e )), θ(e)[ ∩ free(e )) means e disabled e by consuming a condition in • e .

  b∈ • e dob(b) ∧ doe(e) + eft(tr(e)) ≤ dof(e) ≤ doe(e) + lft(tr(e)) ∧ dof(e) ≤ θ(e) ∧ b∈ • e dod(b) = θ(e) ∧ b∈e • θ(e) = dob(b) ∧

Fig. 3 :

 3 Fig.3: An STPN with conflicts and blockings a), its symbolic unfolding b), and two of its symbolic processes c) and d).

Proposition 2 .

 2 Let N be a STPN guaranteeing time progress of δ time units. The set of time processes executable by N in D time units are prefixes of time processes of U K , with K = D δ • |T | 2 containing only events with date ≤ D.

Fig. 5 :

 5 Fig. 5: a) An example STPN b) A domain for τ (t 1 ), τ (t 2 ) allowing firing of t 2 .

Algorithm 1 :

 1 Computation of embeddings of a schedule in a symbolic process input: a schedule S = N, →, λ, C , a symb. process E = E, B, Φ ;Ψ := ∅;// the set of solutions is initially emptyF := {f ⊥ };// the exploration starts from the undefined mapwhile F = ∅ do choose f ∈ F ; Min S,f := min → N \ domain(f ) ;if Min S,f = ∅ then ; // all nodes of S have an image in E Ψ := Ψ ∪ {f };// f is an embedding else F := F \ {f }; // we will explore extensions of partial embedding f Min E,f := min E \ image(f ) ;Found := false; while Min S,f = ∅ ∧ Found = false do choose n ∈ Min S,f ; Min S,f := Min S,f \ {n}; cand := {e ∈ Min E,f | tr(e) ∈ r λ(n) ∧ ∀n ∈ dpred → (n), f (n ) e}; if Cand = ∅ then F := F ∪ e∈Cand {f ∪ n,e }; // update f with pairs n, e that meet the matching criteria and add the new functions to candidate embeddings Found := true; end end end end

t l- 1

 1 ,µ l-1

  from the time vector, yielding a new vector τ ˜c = τ ˜b \τ j b distributed over D c = D b ↓ τ j b j ) dx j

φ-x r ≤ b i - r- 1 k=1a ik x k and φ + = n i=1 x r ≤ b i - r- 1 k=1a

 11 + ∧ φ -∧ φ ∅ where φ -= m i=1 ik x k

a 1 k=1a 1 k=1a 1 k=1a

 111 ik x k ) ≤ x r ≤ min i=1,...,n (b i -rik x k ) ∧ φ ∅ Which, by eliminating x r , gives max i=1,...,m (-b i + rik x k ) ≤ min i=1,...,n (b i -rik x k ) ∧ φ ∅ Example 1.

  [START_REF] Aghasaryan | Fault detection and diagnosis in distributed systems: An approach by partially stochastic Petri nets[END_REF], and suppose that N 1 is in configuration m, τ , with m(p 1 ) = 1, m(p 2 ) = m(p 3 ) = 0, τ (t 1 ) = 5.5. From this configuration, one can let 5.5 time units elapse, and then fire t 1 . After this firing, the STPN reaches marking m with m (p 1 ) = m (p 2 ) = 1, m (p 3 ) = 0. New TTFs d 1 , d 2 are sampled for t 1 , t 2 , leading to a configuration m , τ , where τ (t 1 ) = d 1 and τ (t 2 ) = d 2 . Let us suppose that d 1 = 1.5 and d 2 = 2.6. Then one can let 1.5 time units elapse, but after this timed move, transition t 1 cannot fire, as place p 2 contains a token. N 1 is hence in a configuration m , τ , where τ (t 1 ) = 0 and τ (t 2 ) = 1.1, where t 1 is blocked. After letting 1.1 time units elapse, transition t 2 can fire, leading to marking m (p 1 ) = m (p 3 ) = 1, m (p 2 ) = 0, and transition t 1 immediately fires at the same date.

  • , where for every b ∈ B, |b • | ≤ 1 and | • b| ≤ 1. Intuitively, a causal net contains no conflict (pairs of transition with common places in their presets) nor place receiving tokens from more than one transition.

	Definition 6 (time process). A time process is a tuple TP	CN, θ , where
	CN

  Definition 15 ((boolean) realizability). Let d be a dating function for a schedule S, r be a realization function. S is realizable by E s (w.r.t. r and d) iff there exists an embedding ψ from S to E s , and furthermore, Φ ψ,S,d Φ ∧

n∈N θ ψ(n) = d(n)

is satisfiable. S is realizable by N (w.r.t. r and d) iff there exists a symbolic process E s such that S is realizable by E s .

We write E s |= S when S is realizable by E s , and N |= S when S is realizable by N . Appendix D gives an algorithm to compute a set Ψ S,E s of embeddings of a schedule S in a process E s . Once Ψ S,E s is obtained, it remains to show that for at least one embedding ψ ∈ Ψ S,E s , Φ ψ,S,d is satisfiable to prove that S is realizable by E s . We can then compute the set of symbolic processes E S {E s 0 , E s 1 , . . . , E s N -1 } of U K that embed S and similarly for each E s

  , τ 1 , . . . , τ N -1 is a vector of random variables with support D ↓τage representing the possible TTFs of transitions enabled by marking m s.t. for every τ i in τ ¯, the elimination of all other variables from D yields a non-empty set of possible values that is different from {0}; f τ ˜is a PDF over D, blk is a set of blocked transitions, and urg is a set of urgent transitions.

	Definition 17 (transient stochastic state class). A transient stochastic state
	class (or class for short) of an STPN N is a tuple Σ is a marking, τ ˜ τ age , τ is a vector where τ age is the opposite of the elapsed time m, D, f τ ˜, blk, urg where m ¯ and D is a domain for τ ˜. τ ¯ τ 0