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

Karim Kecir
email: karim.kecir@alstom.com

Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics

Keywords: Petri nets, unfolding, scheduling, realizability

This paper considers realizability of expected schedules by production systems with concurrent tasks, bounded resources that have to be shared among tasks, and random behaviors and durations. Schedules are high level views of desired executions of systems represented as partial orders decorated with timing constraints. Production systems (production cells,train networks. . . ) are modeled as stochastic time Petri nets STPNs with an elementary (1-bounded) semantics. We first propose a notion of time processes to give a partial order semantics to STPNs. We then consider boolean realizability: a schedule S is realizable by a net N if S embeds in a time process of N that satisfies all its constraints. However, with continuous time domains, the probability of a time process with exact dates is null. We hence consider probabilistic realizability up to α time units, that holds if the probability that N realizes S with constraints enlarged by α is strictly positive. Upon a sensible restriction guaranteeing time progress, boolean 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.

Introduction

Correct scheduling of basic operations in automated systems (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 QoS objectives. For instance, operating a metro network or a fleet of buses usually amounts to implementing at best a predetermined timetable to meet users needs. In many cases, schedules are designed in order to avoid congestion problems, and ease up recovery from minor delays that are part of the normal behavior of the system. Failing to implement a chosen schedule may then result in a loss of QoS, or even lead to congestion when delays accumulate. Schedules are high-level views for correct ordering of important operations in a system. They consider time issues such as delays between tasks, optimal dates, durations. . . in a production plan. They can be seen as partial orders among basic tasks, that abstract low-level implementation details, and are decorated with dates and timing constraints.

Designing a correct and optimal schedule for a system is a complex problem. On one hand, 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]. On the other hand, optimal solutions (for instance, w.r.t. completion date) are not necessarily the most probable nor the most robust ones: indeed, systems such as metro networks are subject to small delays (variations in trips durations from a station to another, passengers misbehavior. . . ). Delays are hence expected and considered as 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. Consequntly, optimal and realizable schedules are not necessarily robust enough if they impose tight realization dates to systems that are subject to random variations (delays in productions, faults. . . ). Note also that the size of timetabling problems for real systems running for hours cannot be handled in a completely automated way by tools, that usually have to be guided by experts to return quasi-optimal solutions. Hence, timetables design involves expert competences that differ from those needed to design systems.

When a schedule and a low-level system description are designed separately, nothing guarantees that the system is able to realize the expected schedule. This calls for tools to check realizability of a schedule. One can expect systems designers and timetable experts to share a common understanding of the behavior of their system, so in general, the answer to a boolean realizability question should be positive. However, being able to realize a schedule does not mean that the probability to meet optimal objectives is high enough. Obviously, in systems with random delays, the probability to realize a schedule with precise dates is null. Beyond boolean realizability, a schedule shall hence be considered as realizable if it can be realized up to some bounded imprecision, and 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 (STPNs 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 give a formal operational semantics for STPNs, and show that this semantics can also be captured in a concurrent setting by time processes. We then propose a notion of realizability: a schedule S is realizable by an STPN N if S embeds in a time process of N that meets constraints on dates and causal dependencies of events in 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] Mcmillan | 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 a process of N only guarantees boolean realizability: the probabilty of a time process in which at least one event is forced to occur at a precise date is null. We use transient analysis techniques for STPNs as proposed in [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 an imprecision of α. This allows to show that N realizes S ± α with strictly positive probability, and then define a notion of probabilistic realizability.

The paper is organized as follows: Section 2 gives the main motivations for the models used in the paper, namely stochastic time Petri nets with a blocking semantics, and schedules. Section 3 gives an interleaved and a concurrent semantics to STPNs. Section 4 defines a notion of unfolding and symbolic process for STPNs. Section 5 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 Appendices.

Motivations

This section gives motivations for the models that are used in this paper. The context for this study is the modeling of automated systems with concurrently running tasks. In particular the models proposed hereafter can address production systems with a broad understanding of this term, ranging from automated production cells, to transport networks and human organizations. A typical example of such systems where concurrency is prominent is urban train systems, which motivated many features of our model, and in particular an unusual blocking semantics for stochastic time Petri nets.

A second topic addressed in this paper is accuracy of schedules. We want to ensure that a system with random perturbations can follow a predetermined schedule up to some bounded imprecision. Schedules are objects of everyday's life, and are both used as documentation for a system (for instance, bus and train schedules indicate to users when and where to pick up their transport), and to guide a system along behaviors that guarantee some quality of service. Though schedules are often perceived as linear orderings of actions, some scheduled events are causally related, and some other are independent (think for instance of tasks in a Gantt diagram, or buses moving in different parts of a city). Natural models for schedules should hence consider partial ordering.

A Petri net variant for urban train systems.

First of all, let us justify why concurrency models are preferable in the systems considered in this paper. Even in the case of finite resources, an optimized production system runs several subtasks concurrently. Consider for instance a manufacturing systems that transform objects with tools: each object is eventually produced according to a production flow. Objects productions are independent most of the time, except when a common resource needs to be used. This calls for the use of non-interleaved representation of processes. The same consideration applies for train systems: a train can continue its planned trip as long as the track ahead of it is not occupied by another vehicle. Considering a bi-directional network of n stations with p trains, one can rapidly have to consider more than n k states, which is not needed, as the decision for a train to move is mainly a local decision, that can be taken without knowing the status of the whole system (i.e. without maintaining a global state of the system). A non-interleaved model for these systems is hence preferable if the targeted applications do not call for calculus of global states of the system. In this paper, we will show that the targeted application (ensuring realizability of schedules) can be done with a concurrent semantics.

Urban train systems are usually composed of closed imbricated loops. Trains travel at predetermined speeds following a predetermined itinerary. They move from a station to another following a track. A network is hence not just a simple cycle: it contains forks, junctions, etc. Nevertheless, complex topologies can easily be captured by the flow relations of a Petri net. Consider for instance the example network of Petri nets are good models to represent workflows (e.g., to show how trains can move in a network), but are of little use without timing information and randomness. A frequent question asked for train networks is whether the service is properly ensured. This means in particular whether trains serve station at a regular enough pace, or in case departure dates of trains are very sparse, whether trains arrivals and departures match an expected timetable. Time: The second notion that a model for train systems must address is time. Several models of time have been proposed for timed concurrency models, and especially for Petri nets. Without claiming for exhaustiveness, one can cite at least time Petri nets [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] (TPNs for short), timed Petri nets (see for instance [START_REF] Razouk | Performance analysis using timed petri nets[END_REF]), and time Petri nets with multiple enablings (see for instance [START_REF] Boyer | Multiple enabledness of transitions in Petri nets with time[END_REF]). Time Petri nets associate a rational time interval I(t) = [l, u] or I(t) = [l, ∞) to every transition t in the system. The semantics of time Petri nets considers that a clock is attached to every transition, and reset every time the transition becomes enabled. A transition can fire only if its clock's value lays within the interval I(t). A particularity of this model is that time is not allowed to progress when a clock x t reaches the upper bound of interval I(t). This phenomenon is called urgency, and allows to model mandatory limits for execution dates. This is of particular interest to handle requirements such as: "A train has to leave at most 10 seconds after a departure order was given". Extensions of time Petri nets with multi-server semantics have been proposed to handle several enablings (instances) of each transition. In this paper, we consider a setting where trains are isolated from one another via a so-called fixed-block policy: track portions are reserved for one particular train. This prevents train from being too close from one another. Though this is not the only nor the most efficient way to avoid collision, this mechanisms is used in real systems1 . We discuss this issue further in details in this section. Nevertheless, with such a fixed block policy, one can address a train network at block level (i.e., attach a place to each portion of the network that can be entered by at most one train), and hence multi-enabling needs not be considered.

The second well-known timed variant of Petri nets is called timed Petri nets. In this model, markings associate a set of real values to places, and flow relations from places to transitions are constrained by intervals. Tokens are hence not blind tokens as in TPNs but rather ages: a newly created token has age 0, and a transition t can fire iff every place p in its preset contains a token satisfying the constraint attached to p and t. A drawback of this model is that transition firing is not urgent: a transition that can fire is not forced to fire, and once tokens in a place become too old to satisfy a constraint allowing them to leave the place, they can be forgotten (or not considered). A natural assumption is that trains are modeled as tokens. However, discarding tokens amounts to losing trains, which is an undesirable feature for the systems we consider. Hence, in the context of train systems, urgency seems to be an unavoidable feature. Solution to integrate urgency in timed Petri nets have been proposed [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF]. Though there must be way to avoid losses in timed Petri nets with adequate extensions, we will not follow this approach in this paper and use a model with urgency.

Randomness:

As soon as one is interested in performances of train systems, and not only in worst case scenarios, modeling randomness of these systems is essential. Indeed, train systems are subject to many random events: mechanical failures, bad weather conditions, passengers misconduct,... Some of these random events have huge impact on the network performance (hours of delay), but are usually rare. Recovering from such events usually calls for unusual means, and are not part of a normal schedule. One can see such highly impacting events as an issue that deals more with crisis management, where recovery scenarios have to be built to return to a normal situation. More frequent but hopefully less severe events in terms of time penalty occur at every instant in a network: leaves or ice on a track causing spinning effects, small delays in operations. . . Note that the time penalty due to such event is usually low. However, in urban train systems, where departures and arrivals occur at a high rate, accumulation of uncompensated delays happens very fast, and can result in undesirable phenomena (unexpected overtaking, bunching phenomena. . . ).

In this paper, we will only address frequent delays with low individual penalty. Assuming this, delays can be seen as deviations with respect to the expected most probable value, i.e., as noise. Note that changes with respect to the expected behavior of a particular train is not a change in the sequence of events occurring along its journey in a network (a train is supposed to follow its journey from its beginning to its end), but rather changes in the occurrence dates of events, or in the way several journeys are interleaved. A standard way to address noise is to define continuous probability distributions for the actual value that a duration (dwell time in stations, trip duration. . . ) may take.

For simplicity, we will consider that random durations appearing in our systems are sampled from 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 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. Several standard solutions can be used to model continuous distributions: Gaussian distributions, exponential laws. . . A drawback of Gaussian distributions is that, considering a duration as a randomly chosen value x around a pivot value a, Gaussian distribution attributes the same probability to event x < a and x > a. Intuitively, a train has the same probability to be late and to be in advance. Everyday's experience tends to show that the probability for a train to be delayed his higher, so Gaussian distributions does not match exactly the needs for asymmetric distributions in transport systems. In the rest of the paper, we will adopt distributions called truncated polyexponential functions, that have all the features needed to model random delays. A truncated polyexponential function is a function f (x) defined over an interval [a, b], such that b a f (x) dx = 1, and is a sum of K ∈ N weighted exponentials of the form:

f (x) = k∈1..K c k .x a k .e -λ k x if x ∈ [a, b] 0 otherwise 0.5 4 6 x f (x)
(x) = 0.58 • x 2 • e -1.7x + 0.29 • x 3 • e -1.
2x defined over domain [0.5, 6]. As already explained in [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], polyexponential functions can be used to model phase functions, that is functions where distributions have the shape of several bell-like curves centered around several pivot values. This is particularly interesting to represent with a single distribution speed profiles of trains, i.e., very different values corresponding to discrete choice of a targeted travel time perturbed by some noise. This ability allows to model sets of degenerate bells representing quasi-discrete distributions. Last, polyexponential functions compose well and are easy to manipulate: joint distributions are products of exponentials, projections on a variable or on a domain can be done as simple integrations, and remain polyexponential functions. Blocking Semantics: As already mentioned, we consider production systems with limited resources, and in the case of train systems, with strict security requirements. A safety headway requirement imposes that a train cannot enter a track portion if it is occupied by another train. Similar requirements can also be essential for production cells, where a tool usually processes one item at a time. Without care, one can design Petri nets that are not safe a priori (the contents of places is not always 1-bounded). To guarantee such safety requirement, we adapt the semantics of our nets in such a way that a transition cannot fire if its postet contains an already filled place. In an untimed setting, these nets are usually called elementary nets. We will however show that in a timed setting, elementary firing rules forces to adapdt the notion of urgency.

Stochastic time Petri nets:

The model that we use to represent timed concurrent systems is a variant of the stochastic Petri nets already proposed by [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], with a blocking semantics. Intuitively, a stochastic Petri net is a Petri net with time intervals attached to transitions, and probability density functions associated with these intervals.

Definition 1 (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)]. The semantics of STPNs can be summarized in a few lines: markings associates a certain number of tokens to places. A transition is enabled if places in its preset are filled. When a transition t becomes enabled, a value x t is sampled from the interval and the distribution attached to t. Then, this value decreases over time. A transition can fire as soon as its clock has reached 0, its preset is filled, and its postset is empty. We give a precise semantics for STPNs in section 3.

To illustrate how such nets can be used, consider the piece of network in Figure 3. This piece of net represents a part of the train network in Figure 1. Places are used to represent tracks (tokens symbolize trains), and transitions model departures and arrivals of trains. Once at station D (represented by place P D ), a train can be controlled to move towards station E, it will then enter the track portion from D to E, represented by place P D,E , or it will follow another itinerary, and enter another track (represented by place P D,D ) to move towards station D. This decision is represented by transition t 2 . When a train is on its way to station E, entering station E (represented by place P E ) is symbolized by firing of transition t 3 . Decision to fire t 1 or t 2 is controlled by additional places (the dotted places P c1 and P c2 ). One can notice that firing t 1 empties P c1 and fills P c2 , and firing t 2 empties P c2 and fills P c1 . With such a simple controller, it is assumed that one train out of two goes from D to E, and the other goes from D to D. The distributions f 1 , f 2 , f 3 attached to transitions t 1 , t 2 , t 3 are represented in the right part of Figure 3. Intuitively, a train staying at station D will leave after a sojourn time comprised between 10 and 30 seconds, as long as its destination place is empty. Sojourn times in place P D have different distributions in interval [60, 80], depicted by function f 1 , f 2 , and that depend on whether the train leaves for station E or station D. The trip from D to E lasts between 130 and 140 seconds, and the distribution of trip duration is depicted by function f 3 . Now, if a train is ready to leave station D to go to E after a sufficient dwell time, but a train already occupies the track portion from D to E, then departure is forbidden. In our model, this is implemented by the blocking semantics that says that a transition can fire only when its postset is empty. In particular, in the model of Figure 3, this means that a token will enter place P D,E (resp. place P D,D ) at earliest 10 time units after P D was filled if P c1 (resp. P c2 ) contains a token. However, even if P c1 or P c2 always contain a token, there is no guarantee that the sojourn time of a token in P D is smaller than 80 seconds, despite urgency. Indeed, if places P c2 and P D,E are filled, transition t 1 has to for P D,E to be empty to fire, which may occur at earliest 130 seconds and at latest 140 seconds later. A possible execution for the STPN of Figure 3 is as follows. Assuming that the value sampled for t 1 is x t1 = 62, and the value sampled for t 3 is x t3 = 132, then clock x t1 expires after 62 time units, but t 1 cannot fire as place P D,E is filled.

Hence, one has to wait 132 time units, fire t 3 , and then fire t 1 . In terms of timed word, this execution can be represented as w = (t 3 , 132) • (t 1 , 132). Equivalently, one can describe this execution as a time process T P of N . Roughly speaking, a time process unfolds the net and associates an execution date to occurrences of transitions (the formal definition of time processes and their construction is given in Section 3). The time process corresponding to timed word w is given in Figure 4. Note on this example that even if the first occurrences of t 1 and t 3 seem to be concurrent (they occur at the same dates, and are not causally related), the blocking semantics imposes that t 1 3 fires before t 1 1 .

p 1 D t 1 1 132 p 1 D,E t 1 3 132 p 1 c1 p 1 c2 p 2 D,E p 1 E
Figure 4: Time process for the net of Figure 3 2.2. Schedules, timetables, and their realizability.

Blocking semantics allows to handle safety requirements for systems with critical resources. However, this semantics makes reasoning on systems harder. On our example of Figure 3, a possible wish of designers is that a trains stays no longer than 30 seconds at station D, and one train out of two goes to E.

The second requirement is easily implemented by the simple additional control represented by the dashed places and flows. However, nothing guarantees a priori the first requirement, i.e., that place P D,E is emptied at latest 30 seconds after a token entered P D . So, even if the model seems correct, trains may have to wait longer that expected a priori. The objective of this paper is to make sure that a system can implement a predetermined schedule. The principle of imposed schedule appear in many places of our everyday lives. Trains, metros, buses, follow predetermined schedules, also called timetables. The view that an everyday user of transports has of a schedule is only a partial view corresponding to the station where she catches a train or a bus, listing all possible departure hours. Now, this list of dates is simply a projection of more complex objects. Timetables describe a trajectory for every object: for instance the list of stops that a bus has to visit, and the arrival/departure dates from these stops. Distinct objects cannot use the same resource at the same date. Hence, although individual trajectories can be seen as very linear, and could for instance be modeled as timed words, dependencies exist: a train can enter a station only after its predecessor on the same line has left it.

The natural notion to encode timetable is hence that of partially ordered sets of events decorated with dates. Events represent the beginning/end of a task, the arrival/departure of a train or bus, etc. Partial ordering among events allows to account for linearity in individual trajectories and for causal dependencies due to exclusive resource use (a train can enter a station only after its predecessor has left). The dates decorating these partial order are dates that comply with the dependencies, and also with some physical characteristics of the modeled systems: a train move from a station S i to the following one S i+1 in its itinerary takes time, which shall be reflected by the dates attached to departures and arrivals at different stations.

A schedule can be seen as a solution for a set of constraints over variables representing dates of events. Even if a proposed solution satisfies all constraints attached to a system, it is usually a high-level view of the overall expected behavior of a system. This raises the question of whether a particular schedule can be effectively realized by the system. As schedules and systems models are descriptions of the same system, one can expect the answer to be positive in most of cases. However, solution returned by a solver for a constraint problem are optimal solutions w.r.t. some criteria, but not necessarily the most plausible nor the more robust ones. Indeed, for obvious reasons, one cannot ask a bus to reach each stop at the earliest possible date: such solution makes systems poorly robust to random delays, that necessarily occur in transport systems. Providing the ability to check that a schedule is realizable with reasonable chances is hence an essential tool to design schedules.

In many transport systems, schedules are only ideal behaviors of vehicles, that are realized up to some imprecision, and used mainly to guide the system. Systems such as bus fleets or metros often deviate from the expected timing prescribed by a timetable at peak hours. This deviation mainly concerns occurrence dates of events. Re-ordering of events is rare, and mainly occurs in case of a major failure of the system that forces working in a degraded setting, where following a timetable makes no sense. Systems are also adaptive: production cells can be equipped with controllers, bus drivers receive instructions to avoid bunching phenomena [START_REF] Bartholdi | A self-coordinating bus route to resist bus bunching[END_REF], and metro systems are controlled by regulation algorithms that help trains sticking to predetermined schedules. In this setting, a key question is to asses how much regulation and control is needed to make a system run as expected in its schedule. A first way to answer to this question is to ask the probability that a schedule is realized by the system. In this paper, we give ways to compute the probability that a schedule is realized up to some minor shift in occurrence dates of its events. This measure does not formally include a particular adaptation technique (control, regulation) to help a system stick to a predetermined schedule. However, this measure still makes sense, as it quantifies the need for correction to unregulated systems. Consider the example of Figure 5. This Figure represents the beginning of a schedule for three trains, where only departure dates are planned. The departures for each train are depicted as boxes, carrying a label of the form i : dJ, where i is the event number, and dJ means that this event is a departure from station J. Furthermore, an execution date is attached to each node. One can see on this drawing that schedules can be seen as partial orders organized along train trajectories. However, there are some dependencies among events from distinct trains: for instance, our schedule imposes that the second departure of the day at station D (event 6 : D) precedes departure 3 : C from station C. Similarly, 7 : E must precede 12 : D. One can notice that arrivals are not depicted in the schedule, that focuses on departures. Now, a sensible question is: can the network of Figure 1 realize this schedule? More precisely, can the Petri net designed for this network (with additional control places) realize such a schedule starting at 08 : 00 with a train at station A, a train at station C and a train at station F ? The answer to this question is not straightforward. Even if the answer is positive, the next step is to ask whether this schedule, with a tolerance of 1 min delay for each departure, is probable enough. If the answer is that the probability to realize our schedule is very low, then this schedule should not be considered as operational.

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 2 (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 trade-off between maximization of an objective and of the likelihood to stay close to optimal realizations at runtime. Realizability: Accuracy of schedules can be formally defined as follows: We want to check whether a consistent schedule S with its dating function d can be realized by a system, described as a stochastic time Petri net N . More formally, this amounts to verifying that there exists a timed execution T P of N and an interpretation function ψ mapping abstract events of S onto concrete events of T P , such that causally related events of S are causally dependent in T P and dates of events in T P meet the constraints on their abstract representation. In the rest of the paper, we show how to check realizability of a schedule by a STPN, and how to compute a lower bound on the probability that S is realized by N . This allows in particular to check that the probability of realization of a schedule is not null.

Semantics of Stochastic Time Petri Nets

Roughly speaking, an STPN is a time Petri net with distributions on firing times attached to transitions. The semantics of this model describes how tokens move 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. This model borrows its main features from [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], with the major difference that the semantics is blocking, i.e. it forces nets to remain safe (1-bounded), as in elementary nets. This restriction is justified by the nature of the systems we address: in production chains, places symbolize tools that process only one item at a time. Similarly, when modeling train networks, security requirement impose that two trains cannot occupy the same track portion. 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 all time and probability issues of the original net. Enforcing a bound via a blocking semantics is hence a practical way to guarantee a priori that models do not allow specification of undesired situations.

Let N = P, T, • (), () • , m 0 , eft, lft, F, W be a STPN. A marking of N is a function that assigns 0 or 1 token to each place p ∈ P . 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 described by timed and discrete moves among configurations, and can be described informally as follows. A variable τ t is attached to each transition t of the STPN. 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 value 0, 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, τ . An initial configuration for N is a configuration m 0 , τ 0 where m 0 is the initial marking of N , and τ 0 attaches a sampled TTF to each transition enabled by m 0 . We will write m, τ → m , τ iff there exists a timed or discrete move from m, τ to m , τ , and m, τ * -→ m , τ iff there exists a sequence of moves leading from m, τ to m , τ . Interested readers can find detailed operational rules for moves of STPNs in Appendix A. Consider the STPN N 1 of Figure 6, 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, τ (t 2 ) = 1.1, and 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. Once t 2 has fired, t 1 is urgent and firable, and immediately fires, at the same date.

p 1 t 1 [0, 6] p 2 p 3 t 2 [2, 8] p 1 1 t 1 1 5.5 p 2 1 p 1 2 t 2 1 8.1 t 1 2 8.1 p 3 1 p 1 3 p 2 2
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 discrete 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 according to the respective weight of each firable transition: 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 probabilities. 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 noninterleaved semantics can be defined using time processes, i.e., causal nets equipped with dating functions. We recall that causal nets are finite acyclic nets We will then drop flow relations and simply refer to time processes as triples TP = B, E, θ . 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.

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. We denote by TP u obtained from a timed word

u = t 1 , d 1 t 2 , d 2 . . . t k , d k ∈ L(N ).
It can be built incrementally by adding dates transitions one after another. We give a detailed construction in Appendix B.

Figure 6-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 interleavings may not be valid timed words of L(N ): in the process of Figure 6-b, t 2 1 cannot occur before t 1 2 , even if both transitions have the same date. A correct ordering among events with identical dates in a process T P u can however be found by checking that a chosen ordering does not prevent occurrence of other transitions.

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 6-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 introduced for TPNs in [START_REF] Semenov | Verification of asynchronous circuits using time Petri net unfolding[END_REF] and 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 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). The example of Figure 6 does not guarantee time progress as according to the semantics of STPNs, this net allows an arbitrary number of occurrences of transition t 1 to fire at date 0. However, such specification can be considered as ill-formed. Let us consider our motivating examples: in a production cell, the same kind of processing by a tool necessarily takes time, and conveying an item from a tool to another cannot either be instantaneous. Similarly, in train networks, some time must elapse between two consecutive arrivals of a train at a station, as well as between two consecutive arrivals/departures of the same train. Hence, real-life systems ensure properties that are often stronger than this time progress property. The example network of Figure 1 will hence necessarily contain exclusively transitions with rational intervals of the form [a, b] or [a, ∞), where a > 0. An interesting consequence of time progress is that any execution of duration ∆ of an STPN that guarantees time progress is a sequence of at most |T | • ∆ δ transitions. It means that for most of usual systems that run for a predetermined period (e.g., a metro network operate from 05:00 to 01:00), it is sufficient to consider behaviors of a model up to a certain number of events.

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. 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 difference 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 e ∈ E as ↑ e = {e ∈ E | e e}. A set of events E ⊆ E is causally closed iff ∀e ∈ E , ↑ e ⊆ E . This notion extends to conditions. 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. Two events e, e are competing iff tr(e) • ∩ tr(e ) • = ∅ (they fill a common 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 a maximal (i.e., there is no larger pre-process containing E , B ), causally closed and conflict free set of events, and B = • E ∪ E • . PE(U) denotes the set of pre-processes of U.

Unfolding an STPN up to 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.

Unfoldings can be built inductively, following the procedure proposed for instance in [START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF] and recalled in Appendix C. When building U 0 , . . . , U K , each step k adds new events at depth k and their postset to the preceding unfolding U k-1 . The construction starts with the initial unfolding U 0 = ∅, B 0 where

B 0 = { ⊥, p | p ∈ m 0 }.
The structural unfolding of an STPN does not consider timing issues nor blockings. Hence, an (untimed) pre-process of PE(U K ) needs 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. However, time processes of a net N can be built from processes of its untimed unfolding. 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 that satisfy requirement on dates that only depend on the considered pre-process. We re-introduce time in unfoldings by attaching constraints to events and conditions of pre-processes. 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 (i.e., defined over set of variables var(E, B)), assuming that executions of N start at a fixed date d 0 . Constraints in Φ E,B set to guarantee:

• (net constraints): occurrence dates of events are compatible with the earliest and latest firing times of transitions in N ,

• (causal precedence): if event e precedes event e , then θ(e) ≤ θ(e ).

• • (urgency): an urgent transition with empty postset fires if no other urgent transition fires before. And, in particular, for every event e ∈ E, there is no event that becomes firable and urgent before e.

Overall, Φ E,B is a boolean combination of inequalities. We do not detail its construction here: except for the additional constraint on place occupancy due to blocking semantics, it is almost the solution proposed by [START_REF] Chatain | Time supervision of concurrent systems using symbolic unfoldings of time Petri nets[END_REF]. Interested readers can also find a complete description of the construction of Φ E,B in Appendix D. 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 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, and make Φ E,B unsatisfiable. Consider for instance the 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 p Definition 10 (prefixes of an unfolding). Let PP = E, B be a pre-process of U K . A symbolic prefix of PP is a triple E , B , Φ E ,B where E ⊆ E is a causally closed set of elements contained in E, and

B = • E ∪ E • .
Symbolic prefixes are causally closed parts of pre-processes, but their constraints inherited from the unfolding U K may not be satisfiable. Let SPP = E , B , Φ E ,B be a symbolic prefix of pre-process PP = E, B . We will say that SPP is maximal w.r.t. urgent events firing iff no more event of PP have to belong to SPP. This property of SPP holds if every event f ∈ B • ∩ E that could have become urgent before the last date of all events in E was prevented from firing due to blocking. We show in Appendix D that this property of symbolic prefixes can be verified as unsatisfiability of a property Φ max (f ) for

every f ∈ B • ∩ E. Definition 11 (symbolic processes). A symbolic process of U K is a triple E s = E , B , Φ E ,B where E , B , Φ 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.

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 illustrated by the example of Figure 7, satisfiability of constraints is not monotonous: the constraints for processes in Fig 7-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: if a constraint associated with a prefix of size n is not satisfiable, appending a new event may introduce blockings that delay urgent transitions, yielding satisfiability of a constraint on a prefix of size n + 1. So, unsatisfiability of constraints cannot be used as a criterion to stop incremental unfoldings construction.

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 pre-processes, 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 that its processes are of depth at most H = D-d0 δ

• |T |.

Let b = e, p be a condition of an unfolding U n obtained at step n. Let block(b) be 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 in some bounded unfolding U K . 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 address the question of realizability of a high-level description of operations (a schedule S) by a system (described by a STPN N ). Considered in a purely boolean setting, this question can be rewritten as: is there an execution of N that implements S ? In many cases, a positive answer to this question is not sufficient: as STPNs are equipped with continuous probability distributions, the probability of a particular execution TP = E, B, θ is always 0. A sensible way to address realizability is a quantitative approach requiring that the set of executions of N implementing S has a positive probability. In this section, we first formalize the notion of realization of a schedule by an execution, and define boolean realizability. We then define probabilistic realizability, and sketch how an under-approximation of the probability to realize a schedule can be computed using a transient tree construction [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF]. First of all, the connection between high-level description of operations in S and their implementation in N is defined via 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 tracks, or to departure with different speed profiles, which is encoded with several transitions in an STPN. Realization functions hence relate actions in schedules to several transitions in an STPN. The condition r(a) ∩ r(a ) = ∅ 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. This allows in particular to define schedules that constrain dates for a subset of events, and leave dates of other events free from any constraint. In the context of a train network, this allows for the verification of realizability of schedules that focus on a subset of stations, e.g., requiring a departure from a choosen station every x minutes during a normal day of operation. 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) (embedding is consistent with labeling) ∀ n, n ∈→, ψ(n) ψ(n ) (causal precedence is respected) f ≤ ψ(min(n)), tr(f ) ∈ r(A) (embedding starts on 1st compatible events) ∀e ≤ f ≤ g, e = ψ(n) ∧ g = ψ(n ) ∧ tr(f ) ∈ r(A) (embedding "misses" ⇒ ∃n , f = ψ(n ) ∧ n → * n → * n no compatible event)
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 .

Definition 15 (realizability). Let d be a dating function for a schedule S = N, →, λ, C , r be a realization function. The pair (S, d) is realizable by E s = E, B, Φ (w.r.t. r) iff there exists an embedding ψ from S to E s , and furthermore,

Φ ψ,S,d = Φ ∧ n∈N θ ψ(n) = d(n) is satisfiable. (S, d) 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 .

For simplicity, we address realizability of a schedule with respect to a fixed dating function d. However, realizablity of a schedule S = N, →, λ, C with constraints C stands for realizability of any of the dating functions d meeting constraints C. Letting C ψ denote the conjunction of inequations obtained by replacing every map (i, j) → v in C by inequation θ(ψ(n j )) -θ(ψ(n i )) ≤ v, we will say that S is realizable by E s (w.r.t. r) iff there exists an embedding ψ from S to E s and Φ ψ,S,C = Φ ∧ C ψ is satisfiable. We write E s |= S when S is realizable by E s , and N |= S when S is realizable by N . Appendix G gives an algorithm to compute a set Ψ S,E s of embeddings of a schedule S in a process E s . As soon as an embedding ψ ∈ Ψ S,E s from S to a symbolic process E s is obtained, it suffices to prove that Φ ψ,S,d (resp. Φ ψ,S,C ) is satisfiable to prove that S is realizable by E s . Realizability hence consists in finding at least one symbolic process of N with an appropriate embedding in ψ ∈ Ψ S,E s . When a maximal occurrence date D for operations in S is provided, and when N guarantees time progress, such a process is a process of unfolding U K (where K is the bound given in Prop. 2). 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 i ∈ E S , the set of possible embedding functions Ψ i = {ψ i,0 , ψ i,1 , . . . , ψ i,Ni-1 } for which constraint Φ ψi,j ,S,d is satisfiable.

To illustrate the construction of unfoldings and of processes, let us consider the example of figure 8 Note 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 , which is a standard conflict. Note also that events t 1 4 and t 2 4 output a token in place A. Even if these events are not in conflict, due to non-blocking semantics, their firing dates may influence one another. The way operations of the schedule inject in a process of the net is symbolized by dotted lines. Notice that if t 5 1 has to fire at date 10, then according to intervals attached to transitions, t 1 4 has to fire at date 5. This means that there exists a unique way to guarantee a departure from station A at date 10, which is to sample the smallest trip durations from C to A and the smallest possible dwell time at station A. The probability of such kind of schedule with precise dates is obviously 0. BC t2 [START_REF] Boyer | Multiple enabledness of transitions in Petri nets with time[END_REF][START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF] C t3 [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF][START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] CA t4 [START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF][START_REF] Aura | Time processes for time Petri nets[END_REF] A t5 [START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF][START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] AB t6 [START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF][START_REF] Boyer | Multiple enabledness of transitions in Petri nets with time[END_REF] B' t7 [START_REF] Razouk | Performance analysis using timed petri nets[END_REF][START_REF] Aura | Time processes for time Petri nets[END_REF] BC' t8 [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF][START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] C' t9 [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF][START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF] CD t10 [START_REF] Boyer | Multiple enabledness of transitions in Petri nets with time[END_REF][START_REF] Aura | Time processes for time Petri nets[END_REF] D t11 [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF][START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF] DB t12 [START_REF] Aura | Time processes for time Petri nets[END_REF][START_REF] Doyen | Realizability of real-time logics[END_REF] The example of Figure 8 shows that boolean realizability characterizes an embedding that is consistent with time constraints, but not the probability to realize a schedule. Consider the STPN of Figure 9. This net has two symbolic processes: E s 1 in which transition t 1 fires, and E s 2 in which t 2 fires. The probability of process E s 1 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 probability that v 1 ∈ [0, 1] (and is hence equal to 1). The probability of the second process E s 2 is equal to the probability that v 1 ≥ v 2 , but the set of values allowing this inequality is restricted to a single point v 1 = 1, v 2 = 1. Conforming to continuous probability distributions semantics, the probability of this point, and consequently the probability of executing a time process that is consistent with constraints in E s 2 is 0. A schedule S composed of a single node n with a realization function such that r λ(n) = {t 2 } and a date d(n) = 1 are realizable according to Definition 14, but with null probability. This is not a surprise: requiring a schedule to be realized with an exact timing in a continuous probability setting leads to realizations with null probabilities. Let us slightly change the example of Figure 9-a). We now assign interval [0, 3] to transition t 1 in the STPN and interval [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF][START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF] to transition t 2 . We keep the same schedule S and realization function r, but require that d(n) = 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 explain in Appendix I how to compute the probability of such domain and the joint probability of v 1 , v 2 ), and is equal to the joint probability of values of v 1 , v 2 laying in domain v 1 ≥ v 2 depicted by the grey zone in Figure 9-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. Nevertheless, if t 2 is allowed to fire at date 2 with some imprecision α, then the probability to realize the expected schedule is equal to the integration of the joint probability distribution over the domain where (v 1 ≥ v 2 ) ∧ (2-α ≤ v 2 ≤ 2+α) (represented as a dashed part in Figure 9-b), which can be strictly positive if distributions attached to t 1 and t 2 are properly set. Note that requiring dates to be implemented up to some imprecision does not necessarily increase the probability to realize a schedule: in the example of Figure 9-a with intervals [0, 1] and [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 only way to realize the schedule S mentioned before with date d(n) = 1 is to execute the unique time process in which t 2 fires at date 1, and the probability of this process is null. More generally, the probability to realize a schedule when the embedding relation leaves a single possible occurrence date for at least one event in the chosen symbolic process is always null.

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 2 t 2 4 t 1 7 t 2 1 A 2 B'C' 1 BC 2 OK 2 t 2 7 t 3 1 BC 3 BC' 2
Boolean realizability is a first step to check that a schedule and an implementation are not totally orthogonal visions of a system. However, examples 8 and 9 demonstrate that it is not precise enough. They also show that boolean realizability up to imprecision still allows to consider sets of processes with null probabilities as realizations of a schedule. An accurate notion of realizability should require that schedules embed into symbolic processes of U K with strictly positive probability and up to some admissible imprecision on dates of events, bounded by some value α ∈ Q ≥0 . An operation x in a schedule should now be implemented by a occurrence t j i of a transition t at date θ(t j i ) ∈ [max(d(x) -α, 0), d(x) + α]. Once an injection ψ from a schedule S = N, →, λ, C to a symbolic process E s is found, the constraint to obtain realizability of a dating function d up to imprecision of α becomes:

Φ ψ,S,d±α = Φ ∧ n∈N max(d(n) -α, 0) ≤ θ(ψ(n)) ≤ d(n) + α.
One can similarly require constraints C in S to be realized up to imprecision of α, that is, require that constraints of the form d(n j ) -d(n j ) ≤ v imposed by map C are implemented in the low level net by a process satisfying a relaxed constraint of the form θ(ψ(n j ))-θ(ψ(n i )) ≤ v +α. This notion of realization up to bounded imprecision is more natural that boolean realizability. Indeed, for systems such as train networks, one cannot expect a schedule to be precisely realized (trains are subject to random delays), but rather that differences between realized and scheduled dates are usually not too important. Definition 16 (probabilistic realizability). Let d be a dating function with maximal date D for a schedule S = N, →, λ, C , r be a realization function. The pair (S, d) is realizable with non-null probability (w.r.t. r) up to imprecision α iff there exists an embedding ψ of S into a symbolic process E s of U K such that: P(E s ∧ Sol(Φ ψ,S,d±α )) > 0.

p 1 t 1 p 2 t 2 p 3 [0, 1] [1, 2] 0 1 2 3 4 0 1 2 3 4 v1 v2 v 1 = v 2
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 strictly positive. This probability can be evaluated 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 continuous probability distributions over the time domains defined by these classes. The probability to fire a particular transition from a state and move to a successor node is computed as an integration over the time domain allowing this transition to fire first. On the example of Figure 9 (with intervals [0, 3] and [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF][START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF], this corresponds to integration of a joint distribution for values v 1 , v 2 over the domain in grey. The distributions attached to transitions of STPNs are polyexponential functions. Beyond their expressive power, polyexponential functions are closed under projections, integrations, or multiplication. Further, (joint) distributions of clock values in a node can always be encoded as polyexponential functions. This way, one can iteratively build a tree whose nodes contain state classes and distributions over these classes. The parent-child relation is driven by which transition t fires from the parent node (this implies projecting existing values on a part of the class of the parent that allows firing t first), and which transitions are newly enabled after firing t (yielding re-sampling of TTFs for the newly enabled transitions). As time progress is guaranteed in our model, a finite tree representing executions of an STPN or of one of its processes up to some bounded duration can always be built. As shown in [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], after this transient tree construction the (sum of) probabilities attached to paths of the tree can be used to compute the probability of properties such as safety of a system within a bounded horizon. 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. If this probability is not null, then there is a positive probability to realize the considered schedule. Note that the computed value is only a lower bound for the exact probability to realize a schedule: indeed there can be more that one process realizing a schedule. However, computing the exact probability is rather involved, as distinct realizations of a schedule are not necessarily independent. Details on the construction of this transient tree are provided in Appendix H.

Conclusion

Related work: we have addressed realizability of partially ordered timed schedules by timed and stochastic concurrent systems with safety requirements. Realizability in a timed setting has formerly 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. This work could be used to answer a boolean realization question, by translating a schedule to a formula. However, this work of [START_REF] Doyen | Realizability of real-time logics[END_REF] lies in an interleaved setting: a sequential formula cannot differentiate interleaved and concurrent actions. It does not address randomness in systems and hence cannot quantify realizability. Scheduling of train networks was already addressed as a constraint satisfaction problem [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 solutions proposed in [START_REF] D'ariano | A branch and bound algorithm for scheduling trains in a railway network[END_REF] use a branch and bound algorithm to return an optimal schedule for the next 2 hours of operation of a train network, but do not consider randomness. Note however that this algorithm is efficient enough to be used online to guide decisions of a scheduling system. Stability of timetables in an environment with random perturbations was considered in [START_REF] Carey | Ex ante heuristic measures of schedule reliability[END_REF]: a schedule is considered as an immutable ordering on trains, and delays are modeled as probability distributions. Reliability of a given timetable (with fixed dates) is then defined via probability measures (probability that a given number of trains gets late by more than a fixed threshold. . . ).

Realizability is also close to diagnosis. 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 whose partial observation complies with the log. Considering a log as a schedule, the ability to compute a diagnosis implies realizability of this high-level log by the model. 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 seen as a sequence of discrete instants. Diagnosis was addressed for parameterized Petri nets in [START_REF] Chatain | Symbolic diagnosis of partially observable concurrent systems[END_REF].

The proposed solution unfolds a parameterized Petri net to find explanations for an observed log. Time Petri nets can be considered as a particular case of this parameterized model. [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 framework explains stream of time-stamped events as combinations of chronicles. Assembling chronicles is some kind of timed unfolding. However, event streams are not a concurrent model, and chronicles extraction does not consider randomness.

Schedulability can also be seen as conformance of an expected behavior (the schedule) to an implementation (the STPN model). Conformance was defined as a timed input/output conformance relation (tIOCO) relation between timed input/output automata in [START_REF] Krichen | Conformance testing for real-time systems[END_REF]. More precisely, timed automaton A 1 is in tIOCO relation with timed automaton A 2 iff after some timed word, the set of outputs produced by A 1 is included in the outputs produced by A 2 . This relation cannot 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 probabilities.

Assessment: 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, find symbolic processes of U K that embed the schedule, and then check that at least one of them has a strictly positive probability to be executed. In a purely boolean setting, this amounts to answering a satisfiability question for a combination of linear inequations, and in a probabilistic setting, this means computing a transient execution tree to obtain a quantitative answer. A first question is whether all these steps can be factorized. A second question is of course complexity of this algorithm.

A noticeable fact is that satisfiability of constraints associated with processs and embeddings and unfolding are rather distinct parts of the proposed method. Usually, unfoldings can be stopped as soon as some criterion is met (completeness for construction of finite prefixes [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF][START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF], satisfaction of a property. . . As shown in Section 4, due to blocking semantics, satisfiability of constraints is not monotonous w.r.t. the size of unfoldings, and hence cannot be used as a criterion 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. Regarding complexity, the size of unfoldings and hence of constraints associated with symbolic processes can grow exponentially with depth. However, these constraints can be simplified to refer only to event variables. One can also notice that atoms in constraints are rather simple inequalities. Hence, satisfiability of constraints could remain simple linear problems in most cases. However, due to blocking semantics, constraints also contain disjunctions. This may raise combinatorial issues and make satisfiability of constraint costly. The cost of the algorithm to compute realization probability for processes is also an issue. 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 process. This is obviously very costly. We are currently investigating ways to evaluate probabilities of symbolic processes in a non-interleaved setting. Note also that the algorithm designed so far only computes lower bounds for realization probability.

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 is 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, and not only lower bounds. by the next firable transitions at some point in an execution. We denote by Cuts(E, B) the set of cuts of pre-process E, B . Unfolding of a Petri net simply consists in successively appending transitions to already built processes, i.e. to cuts of these procvesses. Structural unfolding: Following [START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF], we inductively build 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 Ê.

Appendix D. Constraints to reintroduce time in processes

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 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 . Despite this equality, we will use both variables θ(e) and dob(b) for readability reasons. 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 event 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 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. In particular, 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 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: notMoreUrg(e, e ) = θ(e) ≥ doe(e )+lft(tr(e )) ⇒ tiled(e, e )∨ e ||e preempts(e , e ) 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.

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: Let SPP = E , B , Φ E ,B be a symbolic prefix of pre-process PP = E, B . Symbolic process SPP is maximal w.r.t urgent events firing iff no more event of PP have to belong to SPP. This property of SPP holds if every event f ∈ B • ∩ E that could have become urgent before the last date of all events in E was prevented from firing due to blocking. This property prefixes can be verified as a property Φ max (f ) that have to be satisfied for every f ∈ B

∀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
• ∩ E. Let C f = pl -1 (f • ) ∩ B denote
the set of conditions of B whose place appears in the postset of f . Then, SPP is maximal iff for every f ∈ B • ∩ 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 ) means that 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 Φ max (f ) is satisfiable, then f should appear in the process.

Appendix E. 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 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 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 ).

E s,0 = E 0 , B 0 , Φ 0 E s,1 = E 1 , B 1 , Φ
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 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.

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

Appendix J. 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. a ik x k 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 max example: 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 ) ∧ φ ∅

Figure 1 .

 1 This network is composed of 7 stations and bidirectional tracks. A train in the network can be scheduled to serve repeatedly stations A.B.C.D.E.F.G. Ḡ. F . Ē. D. C. B. Ā, or follow smaller loops A.B.C.D. D. C. B. Ā and D.E.F.G. Ḡ. F . Ē. D. The Petri net at the bottom part of Figure 1 can represent this network: places are used to represent stations or tracks between stations, and transitions model a possible move from a part of the network to a consecutive one. The flow relation of this net is almost isomorphic to the original network.

Figure 1 :

 1 Figure 1: Modeling trains flows in a network with Petri nets

Figure 2 :

 2 Figure 2: Expressing probability of a delay with a Gaussian distribution (plain line) and a polyexponential function (dashed line).

Figure 2

 2 Figure 2 illustrates the advantages of using polyexponential functions to model continuous distributions. The curves represented in this figure are a standard Gaussian distribution centered around value 4, and a polyexponential function f(x) = 0.58 • x 2 • e -1.7x + 0.29 • x 3 • e -1.2x defined over domain [0.5, 6]. As already explained in[START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF], polyexponential functions can be used to model phase functions, that is functions where distributions have the shape of several bell-like curves centered around several pivot values. This is particularly interesting to represent with a single distribution speed profiles of trains, i.e., very different

Figure 3 :

 3 Figure 3: Using STPNs to model trains moves

Figure 5 :

 5 Figure 5: A possible schedule for trains departures in the metro network of Figure 1

  Timed moves: A timed move m, τ δ -→ m, τ lets a strictly positive duration δ ∈ R 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 = m -• t + t • , τ . 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 already enabled by m and still enabled by m .

Figure 6 :

 6 Figure 6: a) An example STPN N 1 and b) a time process of N 1

  of the form CN = B, E, • (), () • , 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 = B, E, • (), () • is a causal net, and θ : E → R ≥0 associates a positive real date to transitions of net CN , 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. We 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: • 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}.

  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) (with values in R ≥0 ). 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.

  (no overlapping conditions): if b, b represent occurrences of the same place, then intervals [dob(b), dod(b)] and [dob(b ), dod(b )] have at most one common point,

Figure 7 :

 7 Figure 7: 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.

  . This toy example depicts two train carousels: line 1 serves stations A, B and C, and line 2 serves stations D, B and C . Both lines share a common track portion between stations B, C and B , C , and line 1 uses two trains. The up left picture shows the aspect of both lines and stations, and the bottom left figure a STPN model of this network (we do not show distributions). Stations are represented by places labeled by station names, and track portions between two stations by places labeled by pairs of letters representing the connected stations (e.g., place CA represents the track from C to A). Transitions consuming tokens from a station place represent trains departures, and transitions consuming tokens from a track place are arrivals. A possible required schedule (middle of the figure) is that one train leaves every 10 time units from station A on line 1, starting from date 10, and one train leaves station B every 10 time units, but starting from date 15. Arrivals of trains and departures from other stations are not represented, and are hence not constrained. Departures from A are nodes labeled by d A and departures from B are nodes labeled by d B . The righmost part of the figure is a structural unfolding of the net. We set r(d A ) = {t 5 } and r(d B ) = {t 7 }.

Figure 8 :

 8 Figure 8: Realizability of a schedule for a metro network with two lines and a shared track.

Figure 9 :

 9 Figure 9: a) An example STPN b) A domain for τ (t 1 ), τ (t 2 ) allowing firing of t 2 , assuming I(t 1 ) = [0, 3] and I(t 2 ) = [1, 4].

  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 .

  every event e the constraints θ(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 STPNs is urgent, once firable, e has to fire at the earliest possible date. This is encoded by the constraint θ(e) = min{x ∈ R ≥0 | x / ∈ ]dob(b), dod(b)[ for some b ∈ I(b i ) ∧ x ≥ dof(e)}.Figure D.10 shows the effect of blocking and possible free firing dates for some event with a condition b in its postset. The top of the figure is a part of a pre-process, with conditions b, b 0 , b 1 , b 2 referring to the same place p 1 . Suppose that values of variables [dob(b i ) and dod(b i )] for i ∈ 0, 1, 2 are already known. The situation is depicted by the drawing at the bottom of Figure D.10. Horizontal lines represent real lines, and line portion between brackets represent intervals [dob(b i ), dod(b i )] for i ∈ 0, 1, 2. Accoridng to the considered pre-process, we have I(b) = {b 0 , b 1 , b 2 }. Then [dob(b), dod(b)] have to be fully inscribed in one of these thick segments of the Figure. An event with b in its postset (as event e in the pre-process at the top of the Figure) can occur only at dates contained in these thick segments. 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.

1 )Figure D. 10 :

 110 Figure D.10: Constraints on dates of birth of tokens in a shared place.

  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) ∧ e e notMoreUrg(e, e ) Let us now address maximality of symbolic prefixes wrt urgent events firing.

2 Proposition 2 .

 22 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. Appendix F. Proof of Proposition 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.

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 ˜, x j ) dx jThe 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 overD 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 1535 finally obtain the PDF of the successor class Σ .

φ

  can be written asφ + ∧ φ -∧ φ ∅ where φ -= m i=1 -x r ≤ b i -

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 ) ∧ φ ∅

  • • • 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 ).

https://en.wikipedia.org/wiki/Railway signalling Fixed block

Appendix A. Formal semantics of STPNs

Timed moves are formally defined by the following rule:

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:

Appendix B. Construction of time processes

The time process TP u obtained from a timed word

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

We also set θ(e) = d i+1 . The construction ends with TP u = TP u,|u| .

Appendix C. Structural unfolding of a STPN

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 pre-process 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 . Preprocesses of an unfolding are conflict free sets of events and conditions. They represenyt potential processes (executions) of N when timing constraints are forgotten. A cut of a pre-process is an unordered set of conditions. As this set of conditions originates from a pre-process, conditions in a cut have no conflicting events in their causal past. They represent place contents that can be consumed 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

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 .

Appendix G. 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 ).

Appendix H. 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. where m is a marking, τ ˜= τ age , τ ¯ is a vector where τ age is the opposite of the elapsed time and D is a domain for τ ˜. τ ¯= τ 0 , τ 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.

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. // the set of solutions is initially empty

// the exploration starts from the undefined map

// f is an embedding else F := F \ {f }; // we will explore extensions of partial embedding f Min E,f := min E \ image(f ) ; 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 Appendix J;

• 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:

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:

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