Paper deep dive

Modelling and Analysis of Supply Chains using Product Time Petri Nets

Eric Lubat, Pierre-Emmanuel Hladik, Yoann Mateu, Rémi Sauvère

Year: 2026Venue: arXiv preprintArea: eess.SYType: PreprintEmbeddings: 45

Intelligence

Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 94%

Last extracted: 4/10/2026, 1:58:29 AM

Summary

This paper introduces a modular modelling approach for supply chains using Product Time Petri Nets (PTPNs). By representing subsystems independently and synchronizing them through transition labels, the authors address the complexity of geographically distributed manufacturing and assembly sites. The model explicitly incorporates a supply chain manager as a critical mobile resource and utilizes the TINA toolbox for state-space analysis to identify timing-related issues such as timelocks and infeasible configurations.

Entities (5)

Product Time Petri Nets · formalism · 100%TINA · software-tool · 100%Supply Chain Manager · resource · 95%BAZ · manufacturing-site · 90%TWINA · software-tool · 90%

Relation Signals (3)

Product Time Petri Nets → usedtomodel → Supply Chain

confidence 100% · Modelling and Analysis of Supply Chains using Product Time Petri Nets

TINA → verifies → Product Time Petri Nets

confidence 95% · verified using the TINA toolbox

Supply Chain Manager → coordinates → Supply Chain

confidence 90% · The supply chain manager as a critical shared and mobile resource

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Supply chains involve geographically distributed manufacturing and assembly sites that must be coordinated under strict timing and resource constraints. While many existing approaches rely on Colored Petri Nets to model material flows, this work focuses on the temporal feasibility of supply chain processes. We propose a modular modelling approach based on Product Time Petri Nets (PTPNs), where each subsystem is represented independently and the global behaviour emerges through synchronised transition labels. A key feature of the model is the explicit representation of the supply chain manager as a critical shared and mobile resource, whose availability directly impacts system feasibility. We analyse how timing constraints and managerial capacity influence the system behaviour, identifying configurations that lead to successful executions, timeouts, or timelocks induced by incompatible timing constraints. This approach enables systematic what-if analysis of supply chain coordination policies and demonstrates the relevance of PTPNs for modelling and analysing synchronised timed systems.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

44,239 characters extracted from source content.

Expand or collapse full text

Maurice H. ter Beek and Gregor Gössler (Eds.): Proceedings of the 7th Workshop on Models for Formal Analysis of Real Systems (MARS’26) EPTCS 443, 2026, p. 23–39, doi:10.4204/EPTCS.443.3 © Lubat, Hladik, Mateu, Sauvère This work is licensed under the Creative Commons Attribution License. Modelling and Analysis of Supply Chains using Product Time Petri Nets Eric Lubat IRIT Université Toulouse Toulouse, France eric.lubat@irit.fr Pierre-Emmanuel Hladik Nantes Université, Ecole Centrale Nantes, CNRS, LS2N, UMR 6004, 44000, Nantes, France pierre-emmanuel.hladik@ls2n.fr Yoann Mateu Rémi Sauvère Supply chains involve geographically distributed manufacturing and assembly sites that must be co- ordinated under strict timing and resource constraints. While many existing approaches rely on Col- ored Petri Nets to model material flows, this work focuses on the temporal feasibility of supply chain processes. We propose a modular modelling approach based on Product Time Petri Nets (PTPNs), where each subsystem is represented independently and the global behaviour emerges through syn- chronised transition labels. A key feature of the model is the explicit representation of the supply chain manager as a critical shared and mobile resource, whose availability directly impacts system feasibility. We analyse how timing constraints and managerial capacity influence the system be- haviour, identifying configurations that lead to successful executions, timeouts, or timelocks induced by incompatible timing constraints. This approach enables systematicwhat-ifanalysis of supply chain coordination policies and demonstrates the relevance of PTPNs for modelling and analysing synchronised timed systems. 1 Introduction Supply chains involve a geographically distributed network of manufacturing and assembly sites. Key components such as electronic components are supplied by subcontractors, while final assembly is car- ried out in a factory. Coordination between these sites is tightly constrained by just-in-time logistics, strict quality control procedures, and shared critical resources. The role of the supply chain manager is essential in resolving these tightly constrained processes, particularly when quality deviations occur. Understanding how local timing deviations, such as a delay in a supplier site or a late modification propagate through the supply chain, is crucial to prevent bottlenecks, minimizing downtime, and optimiz- ing throughput. However, modelling such complex interactions often leads to monolithic, non-modular representations that are difficult to analyse, simulate, or reuse. In this work, our contribution is a benchmark based on a modular approach usingProduct Time Petri Nets(PTPNs) [12]. Each subsystem (e.g., a manufacturing site, a transport leg, or a quality control process) is represented by a separateTime Petri Net(TPN) [16], and synchronisation between subsystems is enforced through shared transition labels. This modular structure allows engineers to explore the global impact of local timing variations while preserving model modularity and supporting compositional analysis. Notably, the supply chain manager is explicitly modelled as a critical mobile resource, moving from supplier to supplier to process non-conformity acceptance and approve the delivery of critical parts. This modelling choice contrasts with more classical approaches based on TPNs or CTPNs (Colored Time Petri Nets) [10], in which the supply chain is typically represented as a monolithic model. 24Modelling and Analysis of Supply Chains using Product Time Petri Nets The proposed PTPN-based benchmark is intended to support analysis of supply-chain coordination policies. By varying parameters such as the number of suppliers, the number of managers, or timing bounds on production and validation activities, one can evaluate feasibility, detect deadlocks, and study the conditions under which coordination becomes impossible. Rather than aiming at the faithful repro- duction of a specific industrial system, the model provides a structured and parametric case study suitable for evaluating modelling and analysis techniques for synchronised timed systems. Our approach has been implemented in a tool called TWINA [12] (from one of the authors’ thesis) and verified using the TINA toolbox [8], with the toolselt[7], a state-event LTL (SE-LTL) checker. Using this model checker, we examine the states and transitions that lead to infeasible supply-chain configurations. The remainder of the paper is organized as follows. Section 2 reviews related work on supply-chain modelling with Petri Nets and timed formalisms. Section 3 recalls the definition and semantics of Time Petri Nets and Product Time Petri Nets. Section 4 presents the proposed supply-chain benchmark and its modular structure (available online 12 ). Section 5 reports experimental results obtained through model checking. Finally, Section 6 concludes and discusses perspectives for future work. 2 Related Work The modelling and analysis of supply chains have long been a topic of interest in both the modelisation and formal methods communities. In particular, Petri Nets and their timed extensions have been widely used to represent concurrency, synchronisation, and resource constraints in manufacturing and logistics systems [19]. Their formal semantics and graphical nature make them suitable to capture the complex interactions that arise in distributed industrial processes. Time Petri Nets (TPN) [16, 6] extend classical Petri Nets by associating temporal constraints with transitions, enabling the representation of processing times, transport delays, and waiting periods. As a result, they have been successfully applied to workflow modelling, performance evaluation, and the verification of time-critical systems. Several works by van der Aalst and collaborators [1, 2] address the modelling of supply chains and logistics processes using Petri Nets and workflow formalisms. These approaches focus on the correlation of events, the timing constraints between activities, and compliance with predefined temporal patterns. While such models effectively capture global behavioural constraints, they are typically expressed as monolithic nets, which can limit modularity and reuse when modelling large, geographically distributed supply chains. In particular, Bevilacqua et al. [15] employ Time-Coloured Petri Nets to model supply chain processes, where transition firing intervals encode production times, transportation delays, and managerial decision durations, allowing the analysis of system performance and coordination effects. Modularity and compositionality have been recurrent challenges in Petri Nets modelling, especially in a timing context [5]. Various approaches have been proposed to compose Petri Nets through shared places, transition fusion, or synchronisation labels. In the context of timed systems, however, synchro- nisation across multiple timed components often leads to significant state-space growth [17, 9], which complicates analysis. In contrast to existing approaches, this work builds on Product Time Petri Nets [12, 11], which enables the synchronised composition of multiple TPNs through shared transition labels. This allows each supplier, transport process, or decision authority to be modeled independently, while still capturing their temporal interactions. The proposed framework is particularly suited to study delay propagation 1 https://github.com/Darkelubat/SupplyChain 2 https://zenodo.org/records/18925093 Lubat, Hladik, Mateu, Sauvère25 and managerial resource contention in supply chains, as it preserves modularity at the modelling level and supports systematic experimentation with timing parameters. Our approach is closely related to classical scheduling techniques such as the Program Evaluation and Review Technique (PERT) [14], which models a project as a network of activities annotated with execution durations. In PERT analysis, the overall project duration is typically derived from the critical path, computed using conservative estimates of activity durations. Previous work on PTPN has already modelled factory systems in the context of diagnosability analysis for Time Petri Nets [13]. However, to the best of our knowledge, PTPN have not yet been applied to the analysis of supply-chain coordination and feasibility. In this work, we exploit this compositional modelling framework to analyse the temporal feasibil- ity of supply-chain coordination policies and to study the impact of timing constraints and managerial resource availability on the emergence of deadlocks. 3 Time Petri Nets and Product Time Petri Nets We describe our model, the TPN, and its extension, the PTPN, in the following section. For a more detailed description of the proof, semantics, execution and languages of PTPN, please refer to its intro- duction paper [12]. These definitions and semantic notions justify the use of SCG-based (State Class Graph [5, 4]) verification with TINA andseltin Section 5. This section constitutes the technical core that underpins the contribution of this paper, as described in Section 4. 3.1 Time Petri Net (TPN) and Product Time Petri Net (PTPN) ATime Petri Net(TPN) [16] is a net where each transition,t, is decorated with a (static) time interval I s (t)that constrains the time at which it can fire. A transition is enabled when there are enough tokens in its input places. Once enabled, transitiontcan fire if it stays enabled for a durationθthat is in the interval I s (t). In this case,tis saidtime enabled(we refer the reader to [12, 6] for details). More formally: Definition 1A TPN is a tuple⟨P,T,Pre,Post,m 0 ,I s ⟩in which:⟨P,T,Pre,Post⟩is a net (with P and T the set of places and transitions);Pre,Post:T→P→Nare the precondition and postcondition functions; m 0 :P→Nis the initial marking; andI s :T→Iis thestatic interval function. We useIfor the set of all possible time intervals. We consider that transitions can be tagged using a countable set of labels,Σ=a,b,.... We also distinguish the special constantε(not inΣ) for internal, silent transitions. In the following, we use a global labeling functionLthat associates a unique label inΣ∪εto every transition. The alphabet of a net is the collection of labels (inΣ) associated to its transitions. In general terms, the semantics of a TPN is a TTS structure⟨S,S 0 ,→⟩with only two possible kinds of actions: either a transitiontis fired, or a time delayθelapses. A transitiontcan fire from the state (m,φ)iftis enabled atmand firable instantly. We use an extension of TPN in which it is possible to fire several transitions “synchronously”. A Product TPN [12] (PTPN) is the composition(N,R)of a netN, with transitionsT, and a(product) relation,R, that is a collection offiring sets r 1 ,...,r n included inT(henceR⊆P(T), the powerset of T). The idea is that all the transitions in an elementrofRshould be fired at the exact same time. As a consequence, two transitions inrshould have the same labels (we should useL(r) =ato say they have a common labela) and not interfere with each other (they should not share a common input place). 26Modelling and Analysis of Supply Chains using Product Time Petri Nets Definition 2A Product TPN(N,R)is the pair of a net N=⟨P,T,Pre,Post,m 0 ,I s ⟩and a product relation R⊆P(T)such that, for every firing set r in R, transitions in r are independent and compatible: if both t 1 and t 2 are in r thenL(t 1 ) =L(t 2 )and for every place p in P,Pre(t 1 )(p)>0⇒Pre(t 2 )(p) =0. A firing set is a set of transitions that must fire together (e.g.,t 1 ,t 2 withL(t 1 ) =L(t 2 )). In a TPN, transitions are not merged; rather, they must fire synchronously in accordance with their timing constraints. Next, we summarize the behaviour of nets. Apart from the effect of the firing sets, the following definitions are quite standard, see for instance [3, 6]. Amarking mof a net⟨P,T,Pre,Post⟩is a mappingm:P→Nfrom places to natural numbers. A transitiontinTisenabledatmif and only ifm ̇ ⩾Pre(t), where ̇ ⩾is the pointwise comparison between functions. Pointwise comparison in Petri net markings refers to comparing two markings, place by place over the set of places. Astateof a PTPN is a pairs= (m,φ)in whichmis a marking, andφ:T→Iis a mapping from transitions to time intervals, also calledfiring domains. Intuitively, iftis enabled atm, thenφ(t)contains the dates at whichtcan possibly fire in the future. For instance, whentis newly enabled, it is associated to its static time intervalφ(t) =I s (t). Likewise, a transitiontcan fire immediately only when 0 is inφ(t) and it cannot remain enabled for more than its timespan,i.e.the maximal value inφ(t). We represent the state in a SCG structure like in [5]. The semantics of a PTPN is a (labelled) Kripke structure, or Time Transition System (TTS),⟨S,S 0 ,→ ⟩, with two possible kinds of actions: eithers a −→s ′ , meaning that a set of transitionstwith labelais fired froms; ors θ −→s ′ , withθ∈Q ≥0 (whereQ ≥0 denotes the set of non-negative rational numbers), meaning that we let a durationθelapse froms. A transitiontcan fire from state(m,φ)iftis enabled atm and firable instantly. When we fire a set of transitionsr=t 1 ,...,t n from state(m,φ), a transition k(withk̸=t) is said to bepersistentifkis also enabled in the markingm− ∑ t∈r Pre(t), that is if m− ∑ t∈r Pre(t) ̇ ⩾Pre(k). The other transitions enabled after firingrare callednewly enabled. Definition 3The semantics of a PTPN can be formally defined as(N,R), with N=⟨P,T,Pre,Post,m 0 ,I s ⟩, is the TTS⟨S,s 0 ,−→⟩, also denoted[[(N,R)]], where S is the smallest set containing s 0 and closed by−→ such that: — the initial state is s 0 = (m 0 ,φ 0 )whereφ 0 is the firing domain such thatφ 0 (t) =I s (t)for every t enabled at m 0 ; — the state relation→⊆S×(Σ∪ε∪Q ≥0 )×S is such that for all state(m,φ)in S (i) if r∈R with labels a and t is enabled at m and0∈φ(t)for all t∈r, then(m,φ) a −→(m ′ ,φ ′ ) where m ′ =m− ∑ t∈r Pre(t) + ∑ t∈r Post(t)andφ ′ is a firing function such thatφ ′ (k) =φ(k)for any persistent transition andφ ′ (k) =I s (k)elsewhere. (i) ifφ(t)−θis defined for all t enabled at m then(m,φ) θ −→(m,φ . −θ).φ(t)−θdenotes the interval obtained by subtractingθfrom both bounds. Transitions in the case(i)above are calleddiscrete; those labelled with delays (case(i)) are the continuous, or time elapsing, transitions. A Product TPN(N,R)allows to fire multiple transitions simultaneously, constrained by the relation R. Therefore TPN form a natural subset of PTPN, the one where every firing set has only one transition. More precisely, we can always interpret a TPNNwith transitionst 1 ,...,t n as the PTPN(N,R N ), where R N is the collection of singletont 1 ,...,t n . In the following, we often omit the product relation in a PTPN when it is not needed, or obvious from the context. We should also simply use the term net, or the symbolN, to refer to a Product TPN. Lubat, Hladik, Mateu, Sauvère27 3.2 Synchronous Product of PTPN We can define the product of two PTPN as follows: Definition 4Given two nets(N 1 ,R 1 )and(N 2 ,R 2 )with disjoint sets of places P 1 ,P 2 and transitions T 1 ,T 2 , their product(N 1 ,R 1 )× L (N 2 ,R 2 )is the PTPN(N,R)where N is the concurrent composition (juxtaposition) of N 1 with N 2 , the net⟨P 1 ∪P 2 ,T 1 ∪T 2 ,Pre,Post,m 1 0 ⊎m 2 0 ,I s ⟩withPre(t)(p) =Pre i (t)(p) if and only if t∈T i and p∈P i with i∈1..2, and0otherwise (same withPost); and the product relation R is such that: R= [ a∈L r 1 ∪r 2 |r i ∈R i ,L(r i ) =a,i∈1..2 ∪ [ a∈Σ ∪ε r|r∈R 1 ∪R 2 ,L(r) =a Unlike the conventionalsynchronous compositionoperator between Petri Nets, we do not merge transitions with the same labels but compose relations instead. But as with synchronisation, our goal is to define an operation that is acongruence, meaning that[[N 1 × L N 2 ]]is equivalent to[[N 1 ]]∥ L [[N 2 ]]where ∥ L denotes the classical synchronous product on labels for TPNs. 3.3 State Class Graph In this subsection, we would like to remind the result on thestate class abstractionmethod for TPNs, as defined by Berthomieu et al. [5]. AState Class Graph(SCG) is a finite abstraction of the timed transition system (TTS) of a net that preserves its markings and traces. The construction is based on the idea that temporal information in states (the firing domainφ) can be conveniently represented using systems of difference constraints [18]. Definition 5A state class C is defined by a tuple(m,D), where m is a marking and the firing domain D is described by a (finite) system of linear inequalities. In a domain D, we use variables x t ,y t ,...to denote a constraint on the value ofφ(t). A domain D is defined by a set of difference constraints in reduced form, that is inequalities of the kind:α i ≤x i , x i ≤β i and x i −x j ≤γ i,j , where i,j range over a given subset of “enabled transitions” and the coefficientsα,β andγare rational numbers. For a more detailed description of SCG in PTPN, please refer to its original publication [12] 3.4 Example of PTPN and timelock We consider the TPNsN 1 andN 2 shown in Figure 1, together with the SCG of the resulting PTPN shown in Figure 2. Both TPNs share the same alphabet,a,b. Therefore, in the resulting PTPN, transitions labelled with the same symbol are synchronized. The PTPN can thus be simplified into groups of transitions that must fire simultaneously. In this example, we obtain the following groups: t 0.1 ,t 0.2 ,t 1.1 ,t 1.2 ,t 3.1 ,t 1.2 ,t. All transitions within a given group must fire simultaneously. However, the groupt 3.1 ,t 1.2 has an empty firing domain:t 3.1 can fire only after 3 time units, whereast 1.2 must fire before 2 time units. Hence, these timing constraints are incompatible, which leads to atimelock. 28Modelling and Analysis of Supply Chains using Product Time Petri Nets p 1 p 2 p 0 t 0 .1 a [2,4] t 1 .1 b [1,2] t 3 .1 b [3,4] t × p 1 p 0 t 0 .2 a [2,4] t 1 .2 b [1,2] Figure 1:N 1 andN 2 before their product 12 0 t 0 .1|t 0 .2 t 1 .1|t 1 .2 t Figure 2: SCG of the PTPN ofN 1 andN 2 More generally, atimelockinduced by synchronisation occurs when the timing constraints of two or more synchronized transitions admit no common solution. In that case, the system reaches a temporal deadlock. Firing the unlabelled transitiontleads to a dead-end state, illustrating the timelock caused by incom- patible timing constraints. 4 Supply Chain Now that we have introduced the technical background on TPN and PTPN, we introduce the studied system: a distributed network of manufacturing and assembly sites, namely a supply chain. In this paper, the final assembly line, corresponding to the main factory, is calledBAZ(for Baziège, a town in Occitanie). Time units in the model represent days, reflecting the long time scales typically involved in supply chain processes. Our confidence in the model is supported both by prior research in the field and by the operational experience of one of the authors, who has worked as a supply chain engineer since 2019. This ensures that the model captures representative timing constraints and coordination behaviours commonly observed in practice. A supply chain represents the set of flows required to ensure product delivery. A product may be of various nature, such as a physical object, a service, or an information. Consequently, a supply chain may involve a wide range of activities such as manufacturing, shipping, maintenance operations, and financial transactions. A supply chain encompasses the combination of all resources and means (machines, work- force, information channels, financial flows, transportation, and quality management) that contribute to the execution of industrial processes. Poor coordination or mismanagement of any of these elements may Lubat, Hladik, Mateu, Sauvère29 directly impact process lead times. Every actor in the supply chain answers to a customer request. For example, suppliers deliver prod- ucts to manufacturers in response to purchase orders. All actors are interconnected and must be coor- dinated in order to satisfy the final customer’s demands. More specifically, raw material quality and delivery times must be managed so that the overall flow, from raw material production to product deliv- ery to the final customer meets the required time constraints. In addition to material flows, supply chains also involve financial flows (payments, contracts) and data flows (orders, acknowledgements, quality reports), which coordinates and constrains physical production and delivery processes. This strong cou- pling between concurrent activities, causal relations, and timing constraints naturally motivates the use of a Time Petri Net. A supply chain induces a global lead time, defined as the sum of the lead times of all supply-chain actors, from suppliers to delivery to the final customer. Each lead time is characterized by a best-case and a worst-case duration, representing the minimum and maximum time required to perform the cor- responding operation. In this work, only worst-case durations are considered, since early completion does not reduce the start time of subsequent operations. This assumption is consistent with a worst-case analysis of distributed industrial processes. Figure 3: Global view of our supply chain system 30Modelling and Analysis of Supply Chains using Product Time Petri Nets On this model (Figure 3) we have several subsystems: • Suppliers which are representing the different subcontractors manufacturing the different pieces of our product. • The main factory which handles the supply order and the modification demands. • The manager which coordinates and validates the different demands. All of them have interactions which will be represented as labelled transitions to be synchronised in our PTPN. • SO: Supply Order, the action of purchasing a product. • ACK: Acknowledgement. • MOD: Demand of modification for the piece in case of slight difference between the order and the produce piece. The produce is still up to the norm but not to the order. • Coordination and Validation: The Manager will be in the process of validation of pieces, with or without modification. We present the labelled transitions of the TPN such that each label indicates the source and desti- nation in the form ofty pe_source_destination. As an example,SO_BAZ_Siindicates a supply order (SO) from the main factory (BAZ) to the Supplier i (Si). The only exception is for the acknowledgment (ACK), for which we use a distinct labelling to emphasize the acknowledgment more prominently. In our supply-chain model, each actor is associated with an operation characterised by a bounded execution time, expressed through best-case and worst-case durations. The global supply-chain lead time is then obtained by aggregating the worst-case durations along the execution path from raw material suppliers to final delivery. This corresponds to a pessimistic timing analysis, analogous to worst-case critical-path evaluation in PERT [14]. By considering only worst-case durations, we adopt a conservative modelling approach that is well suited to industrial supply chains, where early completion of an operation does not necessarily reduce the start time of subsequent operations due to synchronisation constraints, inventory policies, or orga- nizational delays. This abstraction is consistent with both PERT-based reasoning and Time Petri Net semantics, and allows us to reason safely about global lead times in a distributed manufacturing context. From this perspective, the proposed TPN-based model can be seen as a generalisation of PERT networks, enriched with concurrency, synchronisation, and formal execution semantics. The timing intervals associated with transitions in our Time Petri Net model are intended to represent typical processing, transportation, and decision delays observed in supply chain operations, rather than precise measurements of a specific industrial system. This modelling choice is consistent with existing work on Timed Petri Net–based supply chain analysis, where time intervals are used to capture lead times, processing durations, and coordination delays between actors [15]. In addition, the selection of timing intervals in our model is informed by practical industrial experi- ence, as one of the authors is a supply chain engineer involved in operational planning and coordination activities. The chosen intervals therefore reflect representative values commonly encountered in practice and are used to support the analysis of temporal feasibility, synchronisation constraints, and bottleneck effects, rather than to reproduce a specific operational dataset. Now that we have presented our system as a general concept, we model the different subsystems as TPN representing their timing behaviour. Transitions are represented either as labelled (with their label in bold) or unlabelled (without a bold label). The absence of a timing constraint indicates that the transition has a timing interval of[0,∞]. Lubat, Hladik, Mateu, Sauvère31 4.1 Supplier The first TPN to produce was the supplier (see Figure 4). The supplier needs a supply order before becoming active, this order came from the main factory. The goal of the supplier is to produce a piece for a final product which would be produced in the main factory. Once the order is here, the supplier can decide to proceed toACK_S0_BAZ_SOto acknowledge the order and decide to do an inspection of the ordered product first viaINS. This can take from 1 to 7 days. Such an inspection is to ensure that actual manufacturing parameters could be used, or need to be updated to the latest industrial standard. These inspections are done by the supplier alone. Once the inspection is done and the ACK is sent, the supplier is producing the demanded supply, this takes time, from 6 to 10 days in our example. When the product is ready, if everything is up to the requirement, the supplier can send it via thePOK 10 transition, which is validated by an available manager. Otherwise, the supplier asks for a modification viaMOD_S0_BAZto ask for a modification of the contract. We do not account for the event of a failure of production here or the event of an unvalidated modification (which could lead to timeout). The focus is put on timing constraints studies. The manager is synchronised with this demand of modification and he is the one to accept it. The last transition of the Supplier isSY NCwhich synchronise this Supplier with other TPN to con- clude on the success of the whole system. This supplier can be adapted tonothers supplier by changing 0 for another number. 4.2 Manager The main goal of the manager is to validate one piece or allow for modification of the order. The supply chain cannot proceed without the explicit validation of a manager. It has two variables: •x: the number of managers which are available in theIDLEplace. •y: the upper bound of the modification of the supply order. This variable represents the maximum amount of time a manager could spend granting a modification which can be a bottleneck in the supply chain system. The manager presented in Figure 5 is for two suppliers (0 and 1). To add another supplier, there is a copy of the transitions and places for this new process. We focus on Supplier 0 in this case. The transitionValidation 0 is synchronised on the labelPOK0 which validates a piece produced by a supplier. A manager can also be unavailable (which could lead to atimelock, see Section 5). The transitionst 90 is synchronised onMOD_S0_BAZand is a demand of modification from a supplier. The manager then has to go to this supplier to check the modification and grant it with the transitiont 0 via the synchronised labelMOD_BAZ_S0. 32Modelling and Analysis of Supply Chains using Product Time Petri Nets MOD MOD_S0_BAZ [ 1 , 7 ] p 1 t 0 SO_BAZ_S0 SO 2 ACK IDLE INS 0 INS 2 ACK t 3 ACK_S0_BAZ_SO [ 1 , 7 ] Prod t 1 ACK_S0_BAZ_SO [ 1 , 7 ] product [ 6 , 10 ] MOD ? yesno POK 10 POK0 END POK 20 MOD_BAZ_S0 te SYNC INS : Inspection MOD : Modification Figure 4: TPN of a Supply Chain for Supplier 0 Lubat, Hladik, Mateu, Sauvère33 t 0 MOD_BAZ_S0 [2,y] t 90 MOD_S0_BAZ Validation 0 POK0 t 1 MOD_BAZ_S1 [2,y] t 91 MOD_S1_BAZ Validation 1 POK1 Su p plier 0 X IDLE Su p plier 1 Figure 5: TPN of X Managers for two supply chain The manager has a key role in allowing the flow of pieces from supplier to factory. 4.3 Factory Our factory (calledBAZin the TPN) is the entity asking for supply. We present in Figure 6 the Fac- tory behaviour for two suppliers. To handle more suppliers, we simply add one more path with a new identification (2 for Supplier 2 for example). A factory process begins by asking for a Supply Order (SO) via the first transition and the label SO_BAZ_S0. This step can take up to a day. At this point, the factory receives most of its informa- tion from the supplier (acknowledging the supply order) and the manager (acceptation modification via MOD_BAZ_Si) net, following their processes until the last transition. All of the factory paths are syn- chronised in thet e transition which is active when all of the suppliers are done handling the supply orders. This transition is urgent and it is represented as a[0,0]timing constraint. t 0 SO_BAZ_S0 [0,1] SO2ACK t 1 ACK_S0_BAZ_SO MOD0? MOD 0 MOD_S0_BAZ Modi f ication 0 POK 10 POK0 p 3 POK 20 MOD_BAZ_S0 te SYNC [0,0] IDLE 0 t 10 SO_BAZ_S1 [0,1] SO2ACK 1 t 11 ACK_S1_BAZ_SO MOD1? MOD 1 MOD_S1_BAZ Modi f ication 1 POK 11 POK1 p 4 POK 21 MOD_BAZ_S1 IDLE 1 Figure 6: TPN of the Factory for two suppliers 34Modelling and Analysis of Supply Chains using Product Time Petri Nets A key component of the Factory is that it almost orders the supply simultaneously. The goal of this paper was also to model-check some properties on our synchronised product. In the next section we are adding an ending net, calledend-of-lineto synchronise the overall system and check the viability of our supply chain model. 4.4 End-of-line The end-of-line net is synchronised at the end of the supply order via theSY NClabel. The single token in the Waiting place allows thetimeouttransition to have time elapse. The 210 days correspond to the accepted global supply-chain lead time by the factory. Once another token is put into the Waiting place, thet 0 transition became sensibilised. Since it is an urgent transition it must fire immediately. Thesuccess transition is checked to validate the viability of the supply chain. OK success success [0,0] Waiting t 1 SYNC t 0 [0,0] timeout [210,210] WaitSync 2 Figure 7: TPN end-of-line This net is more independent from the system since the only synchronisation is on the first transition. Now that we have introduced our net, we produce a full model via a PTPN product. 5 Experimental Results Our experiment follows several steps: • First, a model is generated from the TPN representing our supply chain. –The firing intervals of the manager transitions (with[2,y]) are considered as variables. –The number of managers and suppliers are also considered as a variables. • Second, we use a model checker to determine the feasibility of the resulting supply chain model. We synchronise our models following the process described in Figure 8. Since PTPNs are compos- able, the synchronisation is performed incrementally, net by net. First, the manager and the factory are synchronised, then each supplier is added one by one, and finally the TPN representing the end-of-line is incorporated. Lubat, Hladik, Mateu, Sauvère35 Figure 8: Process of Synchronisation of the TPN For a single supplier, a single manager, and a timing interval of[2,6]on the manager transitiont 0 , we obtain the SCG of the product, shown in Figure 9. Each state of this SCG encompasses both the marking and the firing domain of the underlying PTPN. This SCG represents a viable supply chain that always leads to successful delivery, as no deadlocks occur. Deadlocks would result from violations of timing constraints or insufficient managerial resources. 11 17 13 3 1221 0 14 15 16 4 6 7 5 10 9 8 t 0 SYNC t 0 SYNC MOD_BAZ_S0 POK0 MOD_S0_BAZ product t 0 SYNC success t 0 SYNC MOD_BAZ_S0 POK0 MOD_S0_BAZ product ACK_S0_BAZ_SO ACK_S0_BAZ_SO INS0 SO_BAZ_S0 Figure 9: SCG of the product To support reproducibility and reuse, the benchmark generator and the end-of-line Petri net are pub- licly available online 34 . Our benchmark was executed on an MSI GS70 equipped with an Intel Core i5 processor. We use TWINA to synchronise our TPNs using the following command: 3 https://github.com/Darkelubat/SupplyChain 4 https://zenodo.org/records/18925093 36Modelling and Analysis of Supply Chains using Product Time Petri Nets t w i n a − a u t f u s e . t p n TWINA processes the SCG defined in thefuse.tpnfile. If two transitions have the same label and name, TWINA adds a suffix to distinguish them (e.g.,t 0 ,t 0 becomest 0 .1,t 0 .2). We considered several configurations ranging from 1 to 3 suppliers. The synchronisation process may produce atimelock. In our setting, such a situation is not caused by a timeout but rather by an insufficient number of managers. One of the main variables in our model is the timing constraint applied to the Manager model. We vary the upper bound of the firing interval to determine when the model can no longer produce a success- ful execution. Failures may occur either because of a timeout (via thetimeouttransitions in the net) or because of atimelock, indicating that the timing constraints are too restrictive for the supply chain given the current number of managers. To detect these situations, we use the following formulas inselt: s e l t PTPN . k t z − f " < > [ ] s u c c e s s " −v s e l t PTPN . k t z − f " − d e a d \ / <> t i m e o u t " −v A single occurrence of a timeout is sufficient to conclude that it may occur, thereby rendering the supply chain non-viable. Ourseltformulas can be expressed both textually and in classical LTL notation as follows: 1. Success property:Does the success transition eventually hold forever? In LTL: ♢□success 2. Deadlock/Timeout property:Is there a deadlock or does a timeout eventually occur? In LTL: dead∨♢timeout Table 1 summarises the time required to compute the product. For each configuration, the table reports the output of the TWINA command, including the processing time, the number of classes, mark- ings, firing domains, and transitions composing the resulting PTPN model. Supplier1234 Time0.006s0.044s5.7s8m12s Classes18622421362760432 Marking9442391302 Firing Domains18588375852320772 Transitions211001987698385033 Table 1: Processing of the final PTPN depending on the number of Supplier While processing a synchronised supply chain system, two issues can arise: • The number of suppliers for a single manager will lead to management issues, so we scale it down for further experimentations and also test it with more managers. • Combinatorial explosion is still an issue when synchronising several TPNs. Lubat, Hladik, Mateu, Sauvère37 Supply chain feasibility Supplier12233 Manager11223 [2,y] [2,6]SuccessTimeLockSuccessTimeLockSuccess [2,15]SuccessTimeLockSuccessTimeLockSuccess [2,50]SuccessTimeLockSuccessTimeLockSuccess [2,60]SuccessTimeLockSuccessTimeLockSuccess [2,175]SuccessTimeLockSuccessTimeLockSuccess [2,180]TimeOutTimeOutTimeOutTimeOutTimeOut Table 2: Supply Chain feasibility depending on the number of Suppliers, Managers and timing con- straints We analysed our PTPN model usingPTPN.ktz. If one formula evaluate to a failure, we follow the counterexample provided byseltto identify atimelock. The results are summarised in Table 2, whereTimeOutdenotes a timeout of the supply order andTimelockindicates a deadlock arising from insufficient managerial resources. The main issue is that the manager is unable to handle more than one supplier at a time, which leads to atimelock. As discussed in Section 4, introducing slight timing differences in supply orders could allow a single manager to handle several suppliers more efficiently. Staggering supply orders reduces simultaneous demands on the manager’s modification transitions, thereby avoiding incompatible timing constraints that would otherwise lead to timelocks. To test this hypothesis, we modified the timing constraints on the first transitions of the factory as follows: •t 0 remains[0,1], •t 10 is set to[50,100]. The resulting measurements are reported in Table 3. Supply chain feasibility Supplier122 Manager112 [2,y] [2,6]SuccessSuccessSuccess [2,15]SuccessSuccessSuccess [2,50]SuccessSuccessSuccess [2,60]SuccessSuccessSuccess [2,175]SuccessTimeOutTimeOut [2,180]TimeOutTimeOutTimeOut Table 3: Supply Chain feasibility depending on the number of Suppliers, Managers, and timing con- straints with the New Staggered Supply Order As we can see, a better handling of supply orders clearly improves the manager’s ability to manage multiple suppliers. In some configurations, however,timeoutsnow occur because certain suppliers are 38Modelling and Analysis of Supply Chains using Product Time Petri Nets delayed enough to affect the overall system behaviour. The factory must therefore balance the ordering of supplies with the time required to perform the necessary modifications. 6 Conclusion In this paper, we proposed a modular approach for modelling and analysing supply chains based on Product Time Petri Nets. Each subsystem of the supply chain composed of suppliers, factory, and supply manager was modelled independently as a Time Petri Net, and their interactions were captured through synchronised transition labels. This compositional approach allows complex supply chain behaviours to be constructed incrementally while preserving precise timing semantics. A key aspect of our model is the explicit representation of the Supply Chain and supply Manager as a critical shared resource. This makes it possible to study not only delay propagation across sup- pliers, but also the impact of timing constraints and managerial availability on the overall feasibility of the supply chain. Using the TINA toolbox and LTL-based verification withselt, we showed how tim- ing constraints and resource allocation jointly influence system outcomes, leading either to successful completion, timeout failures, or timelocks induced by incompatible timing constraints. Our experimental results highlight several important insights. First, increasing the number of sup- pliers without increasing managerial capacity quickly leads to infeasible configurations, even in the ab- sence of explicit timeouts. Second, the timing of supply orders plays a crucial role: staggering orders can significantly improve feasibility by reducing contention on shared managerial resources. These ob- servations illustrate how PTPN-based models can support what-if analyses for supply chain design and decision-making. As expected, the synchronised composition of multiple timed components leads to a rapid growth of the state space, which currently limits exhaustive analysis to a small number of suppliers. However, this limitation does not affect the scalability of the modelling approach itself, which remains modular and reusable. Rather, it highlights the need for future work on compositional analysis techniques, partial- order reductions, or abstraction methods tailored to synchronised Time Petri Nets. Future work will explore several directions. First, we plan to extend the model to represent the flow of multiple pieces, rather than focusing solely on timing constraints. Second, additional supplier behaviours, with failures, rework loops, storage, alternative validation paths could be incorporated to in- crease realism. Finally, PTPN-based supply chain models provide a promising benchmark to investigate scalable verification techniques for synchronised timed systems. Acknowledgements We are grateful to Uli FAHRENBERG for discussing the modelling of Supply Chain, to Adrien VINEL for his insight on manufacturing, to Bernard BERTHOMIEU and Silvano DAL ZILIO for their help with the TINA toolbox. References [1] Wil M.P. van der Aalst (1994):Modelling and analysing workflow using a Petri-net based approach. Avail- able at https://api.semanticscholar.org/CorpusID:376304. [2] Wil M.P. van der Aalst (1998):The Application of Petri Nets to Workflow Management.Journal of Circuits, Systems, and Computers8, p. 21–66, doi:10.1142/S0218126698000043. Lubat, Hladik, Mateu, Sauvère39 [3] Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime & Olivier H Roux (2005):Comparison of the expressiveness of timed automata and time Petri nets. In:Formal Modeling and Analysis of Timed Systems (FORMATS),LNCS3829, Springer, doi:10.1007/978-3-540-85778-5_3. [4] B. Berthomieu & M. Diaz (1991):Modeling and Verification of Time Dependent Systems Using Time Petri Nets.IEEE Trans. on Software Engineering17(3), doi:10.1109/32.75415. [5] B. Berthomieu & M. Menasche (1983):An enumerative approach for analyzing time Petri nets. In:Proceed- ings IFIP. [6] B. Berthomieu, F. Peres & F. Vernadat (2006):Bridging the Gap Between Timed Automata and Bounded Time Petri Nets. In:Formal Modeling and Analysis of Timed Systems (FORMATS),LNCS4202, Springer, doi:10.1007/11867340_7. [7] B. Berthomieu, F. Peres & F. Vernadat (2007):Model Checking Bounded Prioritized Time Petri Nets. In: 5th Int. Symp. on Automated Technology for Verification and Analysis, LNCS, Springer, doi:10.1007/978- 3-540-75596-8_37. [8] Bernard Berthomieu, P.-O Ribet & Francois Vernadat (2004):The tool TINA – Construction of Abstract State Spaces for Petri Nets and Time Petri Nets.International Journal of Production Research42(14), doi:10.1080/00207540412331312688. [9] Franck Cassez & Olivier H Roux (2006):Structural translation from time Petri nets to timed automata. Journal of Systems and Software79(10), doi:10.1016/j.jss.2005.12.021. [10] Rong Liu, Akhil Kumar & Wil van der Aalst (2007):A formal modeling approach for supply chain event management.Decision Support Systems43(3), p. 761–778, doi:10.1016/j.dss.2006.12.009. Available at https://w.sciencedirect.com/science/article/pii/S0167923606002144. [11] Eric Lubat (2021):Synchronous Product of Time Petri Nets and its Applications to Fault-Diagnosis. Theses, INSA de Toulouse. Available at https://laas.hal.science/tel-03528121. [12] Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé & Audine Subias (2019):A State Class Construction for Computing the Intersection of Time Petri Nets Languages. In:Formal Modeling and Anal- ysis of Timed Systems (FORMATS),LNCS11750, Springer, doi:10.1007/978-3-030-29662-9_5. [13] Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé & Audine Subias (2020):A New Product Construction for the Diagnosability of Patterns in Time Petri Net. In:59th Conference on Decision and Control (CDC) 2020, Jeju Island (virtual conference), South Korea, doi:10.1109/CDC42340.2020.9303826. Available at https://laas.hal.science/hal-02989834. [14] D. G. Malcolm, J. H. Roseboom, C. E. Clark & W. Fazar (1959):Application of a technique for research and development program evaluation.Operations Research7(5), p. 646–669, doi:10.1287/opre.7.5.646. [15] Giovanni Mazzuto, Maurizio Bevilacqua & Filippo Emanuele Ciarapica (2012):Supply chain modelling and managing, using timed coloured Petri nets: a case study.International Journal of Production Research50(16), p. 4718–4733, doi:10.1080/00207543.2011.639397. arXiv:https://doi.org/10.1080/00207543.2011.639397. [16] Philip Merlin (1974):A study of the recoverability of computer systems.Ph. D. Thesis, Computer Science Dept., University of California. [17] F. Peres, B. Berthomieu & F. Vernadat (2011):On the Composition of Time Petri Nets.Discrete Event Dynamic Systems21(3), doi:10.1007/s10626-011-0102-2. [18] G. Ramalingam, J. Song, L. Joscovicz & R. E. Miller (1995):Solving Difference Constraints Incrementally. Algorithmica23, doi:10.1007/PL00009261. [19] Xiaoling Zhang, Qiang Lu & Teresa Wu (2009):Petri-net based application for supply chain management: An overview. In:IEEM 2009 - IEEE International Conference on Industrial Engineering and Engineering Management, doi:10.1109/IEEM.2009.5373050.

Instant research discovery