FMS-Workflow Modeling Based on P-Timed Stochastic Petri Net ()

Walid Ben Mesmia^{1}, Kamel Barkaoui^{2}, Mohamed Escheikh^{1}

^{1}Sys’Com-ENIT, Tunisia, ENIT, Le Belvédère, Tunis, Tunisia.

^{2}CEDRIC-CNAM, Paris, France.

**DOI: **10.4236/jsea.2023.169022
PDF
HTML XML
106
Downloads
558
Views
Citations

In this paper, we propose astochastic Petri net model P-timed Workflow (*WPTSPN*) to specify, verify, and analyze a business process (*BP*) of a Flexible Manufacturing System (*FMS*). After formalizing the semantics of our model, we illustrate how to verifysome of its properties (reachability, safety, boundedness, liveness, correctness, alive tokens, and security) in the P-Timed context. Next, we validate the relevance of the proposed model with* MATLAB* simulation through a specific *FMS *case study. Finally, we use a generalized truncated density function to predict the duration of a token’s sojourn (residence) in a timed place with respect to the sequence states of the global *FMS *workflow.

Keywords

WPTSPN, SPN, Workflow, FMS, P-Timed, Specification, Verification, Prediction

Share and Cite:

Mesmia, W. , Barkaoui, K. and Escheikh, M. (2023) FMS-Workflow Modeling Based on P-Timed Stochastic Petri Net. *Journal of Software Engineering and Applications*, **16**, 443-482. doi: 10.4236/jsea.2023.169022.

1. Introduction

On the one hand, in thispaper, we suggest a Workflow P-Timed Stochastic Petri Net model (*WPTSPN*) for a Flexible Manufacturing System (*FMS*) management process to describe and decide how business activities are carried out. Next, we show the generic (P-timed) characteristicsrelating to reachability, safety, boredness, liveness, properness, and alive-tokens, followed by a description of our model semantics. On the other hand, we propose an extension of stochastic Petri nets (SPNs). Weverify the properties of this model using a new notation and expressiveness-specific features related to the randomresidences of tokens in timed places. This allows us to detectex ecution failures linked either to FMS steps or to interactions between resources used in the business process. First, to introduce the application field of this work, we present the complexities and complicated dynamism of resource allocation and execution in the industrial process. FMS [1] modeling has been introduced for the analysis, verification, and optimization of a manufacturing system [2] [3] according to various criteria. The objective is to evaluate and compare the architectures of production systems to select the most suitable according to previously established decision criteria [2] . This process involves the use of formal models ensuring specification, analysis, evaluation, and verification [4] [5] .

So, production companies must develop a strategy that ensures control over their operations if they are to profit from the business process paradigm [1] . To achieve this, they must tend to totally or partially automate their processes because this method is apt to show the efficiency and tendency towards this objective [1] [5] . Several research works propose methodologies for modeling and automating business processes [4] [6] [7] [8] .

Second, the need to model an FMS to achieve automation, control, analysis, and optimization of the elementary activities that make up its representative business process [2] . A variety of business process modeling methods [9] (specification and representation) are used to practically specify work procedures from a global perspective to describe their operational requirements. We can mention among these methods the activity diagram UML (Unified Modeling Language), Chain Event-Driven Process [10] (*EPC*) and Business Process Modeling and Scoring (*BPMN*) [11] . We consider *BPMN* [11] [12] [13] [14] as a standard for process modeling. It provides a graphical notation-based representation for business process modeling [15] . To build a standard annotation and expressiveness to make a business process representation understandable and readable for the different users involved in procedures’ automation [16] [17] .

Despite the reality that specification and verification methods are widely used, their application to the business domain remains difficult [8] . This is related to the reasons that business analysts strive to formalize simple approaches to modeling and simulating their processes over a long period of time [18] . These approaches’ disadvantage, according to [8] [18] [19] , comes down to the need for operational expertise (manipulation and simulation). Furthermore, the representative model may deviate from the actual simulated due to the significant increase in the number of tests (time and simulation cost ratio) [8] [18] .

Third, the use of Petri Nets (*PNs*) to model an FMS management process [8] [18] [20] is justified as follows:

On one hand, industrial companies need a tool that simultaneously merges modeling and simulation processes. Also, this company’s type has a fundamental objective of economic competitiveness, which summarizes the satisfaction of customers’ tendencies with the changes in the environment [21] . Thus, this flexible and competitive aspect requires representation and control via the supply chain simulator and the use of modeling tools that guarantee an acceptable degree of comprehensibility and readability [21] . On second hand, it confirmed that (*PNs*) can represent a manufacturing system composed of simultaneous and synchronous activities set according to different levels of abstraction [22] [23] [24] . Any formalization based on the *PNs* [25] [26] [27] applied in the *FMS*, models the operational knowledge in the workshop, favoring a planning of the processes. So it provides a decision support tool [28] [29] [30] [31] . Additionally, *PNs* [22] [23] [24] [29] can model manufacturing systems at different levels of abstraction in a hierarchical manner identifying many strategic keys or control points [23] . Thus, *PNs* based models are used effectively to analyze control problems in real-time [23] [24] . These analyses are useful for understanding the behavioral aspect of real-time operations in an *FMS*. They effectively ensure a performance and systematic analysis by varying the parameters of the system represented.

We can list the works related to modeling *FMS* (Flexible Manufacturing System) with *PN* (Petri Nets) as follows:

· In [32] , the author uses the *PNs* in modeling and controlling the *FMS*. The control function is divided into two levels: their proposed model based on *PN* [32] represents the lower level of control for each device in a cell and the upper level which deals with a decision framework about priority sequencing to avoid collisions.

· In [33] [34] , the authors propose a model based on timed Petri nets (*TPN*) to model and analyze a production process. Also, they show an approach for translating TPN into linear algebraic equations. Evaluation and monitoring of production system performance can be done through the use of efficient algorithms to solve these last equations [33] [34] .

· In [35] [36] , a software package called Generalized Stochastic Petri-Net Analysis (*GSPNA*), is used to study the complex and dynamic behavior of a system. So, *GSPN* can achieve a more accurate and refined representation of a *FMS* than classical techniques such as network-based queuing [24] [35] - [39] .

On the other hand, the interest in orienting our proposed model towards the *P*-*timed* semantics of PNs [40] [41] [42] is summarized in the fact that they effectively ensure the analysis as well as the verification of the dynamic behaviors of the systems they model. The latter (*P*-*timed PN*) combines two different approaches to analyze the behavior and study the properties of a model: the time interval approach and the tokens-age approach. That is to say that the first allows a better study of the behavior while it is preferable to use the second for the analysis of the properties of the model. Moreover, our proposed extension of P-timed SPN orientation [43] [44] [45] is based on the assumption that all model transitions must be fired. Therefore, the arrival times of the tokens in the places that are synchronization transition entry places must be compatible. However, another advantage of this extension is that it randomly models (specifies) the minimum residence times and the maximum residence times of the tokens in all the places of the model (even those that are upstream of the synchronization transitions) [41] . This advantage is not possible with other classic PN models [35] [36] [46] [47] .

When we analyze the work related to modeling with Stochastic Petri Nets, we find:

· The authors [48] [49] [50] propose a model named *non*-*Markovian* *SPN*. They show that *Non*-*Markovian* *SPN* allows specifying the behavior of a system by representing the system more realistically. According to their modeling approach, each transition is characterized by a distributed random duration. This representation adopts bounded support laws with a predetermined probability density. Also, they use the maximum density method to estimate the firing time of the transitions [49] [50] .

· The authors [7] [19] propose a second level (refined representation) described by the intermediate locations (micro locations), the micro-transitions, and their firing preconditions according to a micro-level life cycle (token consumption phase, execution phase, and token production phase).

So our model based on P-timed SPN captures the random time requirements in the structure of the representative model of an FMS. In this work, we propose an extension of SPN with a P-timed orientation in specification and verification. The model referred to as Workflows P-Timed Stochastic Petri Nets (*WPTSPN*) enables life cycle specification and control of tokens circulating in the timed places according to sequences of transitions. This is fulfilled through granting to each places a dynamic residence interval. This residence time allocated to a place follows a law of probability determined via three possible densities (exponential, normal, and log-normal). To determine the average residence time granted to each token, we chose the gravity center of the density method, for precision accuracy. Hence, this model adopts the formal verification tools to conform to the P-timed orientation, knowing that such an orientation brings verification of the token's life cycle in timed places. From where we redefine a formalism of verification according to this semantics Thus, the model proposes a prediction approach of the delay related to the time of residence granted to the tokens in the timed places. In an *FMS* context, it should be noted that the delay in residence (stay) of the tokens in a place can mean the expiration time of primary material or semi-finished material. So, our work focuses on the Workflow performance aspect through Stochastic Petri Nets (*SPN*) [46] [47] [51] use. Hence, we propose a SPN extension, named Workflow P-Timed Stochastic Petri Net (*WPTSPN*), able to specify, check *FMS*-workflow, also predict time of stay (residence) in activity lifecycle.

In other words, we provide a P-timed SPN extension that provides expressive specification, verification, and performance analysis of *FMS* business processes. So, the *WPTSPN* makes it possible to represent the expressiveness of a *FMS* business process, to manage and monitor its phases, then to identify any type of execution failure, and to build scenarios of cooperation between actors and their roles in case of failure. Also, this model’ stochastic paradigm favors the delay prediction.

Knowing that several works related to the forecast of the risks of delay have elaborated:

· In the work orientation indicated in [16] , one must emphasize the need to sensitively manage business operations according to risk. In [52] there is a link to a recent survey on the question. According to this study, the majority of prior studies focused on that topic from a qualitative perspective. Some quantitative research methods have recently been offered. The risk indicators for non-compliance with deadlines are described in works [27] [52] and [53] . Also, the work in [7] investigates and analyzes the models’ goals, such as anomalous activity times, and forecasts a case of delay.

· The authors in [52] [53] provide a risk-based simulation prototype design that incorporates resource risks such as hardware failures and business process actor illnesses.

· The model in [7] , which is assumed to be stochastically validated, must include a monitoring system that captures and documents the business process stages, just as the models in [53] and [54] . In this hypothesis, the occurrence earlier-time is applied as an information source to generate an exact accuracy for the representative dynamic system.

Ultimately, P-timed PNs capture time requirements in the model structure. On the one hand, according to the P-timed semantics, it is necessary to assign to each token a local clock (a stopwatch) which measures the time from the moment of arrival in the place. On the other hand, the addition of these counters is useful to check and control the state of non-occurrence of dead tokens (violation of residence time constraints). Moreover, this state of a timed PN is characterized by the current marking and by the value of the clocks associated with the tokens. The latter has very negative consequences for the complexity of the analysis. However, this drawback is only due to the effective complexity of the modeled problem. In our approach, the tools enriching the model make it possible to calculate the cycle time, the times of firing, and the operating margins of the system in mono-periodic operation in residence and firing times. Based on the work performed in [47] and [50] , we extend our model with formal tools that ensure adaption to P-timed semantics. According to the splitted (division) mechanism, this model uses the analytical verification characteristics of the two-level transitions and their related micro-transitions. The density gravity center method is used to identify the firing duration and average random residency of a token in each model place, similar to the method used in [48] . Additionally, the current model adopts a strategy based on elapsed time randomly attached to tokens in timed places specified by randomly residence intervals. We note that randomly interpreting residency intervals is different from the approach in ff which interprets static stay intervals [47] [50] and [54] .

So our *WPTSPN* accomplishes a verification method based on checking model properties that are related to elapsed time which is randomly stay assigned to tokens in timed places like as in [30] [47] [50] [54] . We apply our model and its adjacent tools to an *FMS* example which corresponds to the production chain sub-section presented in [4] .

The remainder of this paper is divided into the following sections:

· The basic concepts of our proposed model are defined in Section 2;

· The suggested *WPTSPN* is depicted in Section 3;

· Section 4 focuses on the real-world implementation of our concept and related tools in the field of *FMS* Workflow;

· The final section summarizes our work and suggests future research directions.

2. Definitions and Basic Concepts

We define the concept set to introduce our paradigm and the associated formal tools to specify, verify and analyze a complex system such as a *FMS*-workflow.

2.1. Workflow

To present the strategic, organizational, and operational functions of the management process, we define *Workflow* [6] [7] . To understand and assess the existing parties in a socio-economic organization, it is crucial to understand the business processes in the organizational structure. They advocate for flexible information system design and deployment. These information systems’ technical foundation is the realization of new products through adaptation to change and market demands. Given the context of managing and guiding businesses, business process management is innovative. According to [5] a business process is any set of actions that include one or more types of input and offer a customer-satisfactory outcome. This definition covers the relationships’ semantics between the inputs and the outputs (pre-condition and post-condition) in a business process. So it is an abstraction of the concept of the process that becomes clear in this definition.

However, a workflow [12] [14] [55] ensures the automation of formal rules to restructure, simulate, and optimize the company’s business processes. According to [56] , the workflow optimization procedure, therefore, concerns the definition of the scheduling of fundamental interdependencies, the representation flexibility, at the time of the action, certain routes integrating the data specific to an instance particular process [18] [56] .

2.2. Petri Nets

In 1962, Carl Adam Petri innovated a formal modeling tool called the Petri Net [57] . They emerged as a powerful graphical tool for the representation of complex system and sequential mechanisms [57] . They have effectively been used for the specification, verification, and analysis of the behavior of complex systems [58] . With a variety of *PN*s [59] [60] [61] [62] application fields and their efficient uses to specify and verify the dynamic behavior of complex systems, *PN*s several classes have appeared in the literature. Using the advantages of the SPN to complex systems analysis and verification, we suggest a model that covers the life-cycle of the manufacturing process workflow. To specify, validate, and predict the execution delay associated with the duration of the tokens propagating within firing transitions, we propose a P-timed oriented extension of the SPN [63] [64] . This proposed model, as well as the tools for specification, verification, and evaluation, is presented in the following section.

3. Workflow P-Timed Stochastic Petri Net Model (WPTSPN)

Our *WPTSPN* is an extension of the *SPN* that adds new components (timed places, tokens, and transitions) for the FMS-Workflow context. The basic formal concepts of the *WPTSPN* are covered in this section. The model’s basic characteristics are formulated, interpreted, and illustrated after it has been defined. In addition, this proposed model incorporates *WFMS* notions [55] [65] , with refinements attributed in [6] and [25] .

3.1. Model Definition

The Workflow P-Timed Stochastic Petri Net, denoted *WPTSPN*, is the 8-uplets:

*WPTSPN*:

=<*P*, *Tr*, *A*, *Sac*, *Ac*, *Typ*-*tk*, *GTyp*-*P*, *CardM*>

· $P={P}_{b}\mathrm{\text{\hspace{0.17em}}}\cup \mathrm{\text{\hspace{0.17em}}}{P}_{w}\mathrm{\text{\hspace{0.17em}}}\cup \mathrm{\text{\hspace{0.17em}}}{P}_{r}\mathrm{\text{\hspace{0.17em}}}\cup {P}_{f}$ , represents the finished set of places;

- ${P}_{b}$ : all initial places,

- ${P}_{w}$ : all workflow places,

- ${P}_{r}$ : all resource places,

- ${P}_{f}$ : all final places.

· $Tr=T{r}_{i}\mathrm{\text{\hspace{0.17em}}}\cup \mathrm{\text{\hspace{0.17em}}}T{r}_{d}\mathrm{\text{\hspace{0.17em}}}\cup T{r}_{s}$ , represents the finished set of transitions (non-empty finite set);

- $T{r}_{i}$ : immediate transitions set,

- $T{r}_{d}$ : determinstic transitions set,

- $T{r}_{s}$ : stochastic transitions set.

· *A*: set of Workflow-actors is non-empty finished;

· *Ac*: workflow activities finished set;

· *Sac*: finished set of Sub-activities associated with a Workflow-activity;

· *Typ*-*tk*: the representation by our model distinguishes between four token types (activity, sub-activity, actor, and any encapsulation of tokens) then the *Typ*-*tk*-function is in charge of this classification.

$Typ\text{-}tk\mathrm{:}tk\to \left\{\mathrm{1,2,3,4}\right\}\mathrm{;}\text{\hspace{0.17em}}\text{\hspace{0.17em}}tk\mapsto \{\begin{array}{l}\mathrm{1,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}tk\in A\\ \mathrm{2,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}tk\in Sac\\ \mathrm{3,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}tr\in Ac\\ \mathrm{4,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}tk\in uplet\end{array}$ (1)

· *GTyp*-*P*: the representation adopted by our model requires that we distinguish the ordinary places of a PN, those linked to the semantic workflow, and those endowed by a residence time. So, *GTyp*-*P*-function makes it possible to distinguish the model’s places.

$GTyp\text{-}P\mathrm{:}P\to \left\{o\mathrm{,\text{\hspace{0.17em}}}w\mathrm{,\text{\hspace{0.17em}}}r\mathrm{,\text{\hspace{0.17em}}}f\right\}$

$p\mapsto GTyp\text{-}P\left(P\right)=(\begin{array}{l}o\mathrm{,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}\left(\text{initialplace}\right)\\ w\mathrm{,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}\left(\text{workflowplace}\right)\\ r\mathrm{,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}\left(\text{resourceplace}\right)\\ f\mathrm{,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}\left(\text{finalplace}\right)\end{array}$ (2)

· *CdM*: the marking cardinality of a *WPTSPN* is a family indexed by the set of places *P*, such that tokens (*tk*) in place *p*:*M*(*p*) is an element of *CdM*(*M*(*p*)).

The proposed *WPTSPN* aims to represent (specify) a flexible production business process according to a P-timed orientation, to then check (verify) the model properties that coincide with the domain of application, and finally to predict the delay relating to the execution of an activity (firing a non-immediate transition of the model). So to achieve these ends, we enrich our model with formal functions.

3.2. Formal Tools Enriching the *WPTSPN* Model

In this subsection, we enriched our model with the functions to increase the analytical coverage according to the workflow semantics, P-timed orientation, and the random residence time assigned to the tokens during a sequence of firing transitions. These <*GDensity*, *GDistrib*, *TFringT*, *IRP*, *MST*, *GTruncated*, *MIP*, *MPO*, *MIT*, *MTO*> formal tools are defined as follows:

· *GDensity*: the probability density function of the *WPTSPN* components (tokens, and stochastic transitions) represents a stochastic probability density (Normal, Log-Normal, or Exponential).

$\begin{array}{l}GDensity\mathrm{:}\left(Ac\mathrm{\text{\hspace{0.17em}}}\cup Sac\mathrm{\text{\hspace{0.17em}}}\cup \mathrm{\text{\hspace{0.17em}}}T{r}_{s}\right)\times \left\{e\mathrm{,\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ln\right\}\to {\text{R}}^{+}\\ typ=\mathrm{\text{\hspace{0.17em}}}Typ\text{-}dist(\; k\; )\end{array}$

$\begin{array}{l}\left(k\mathrm{,\text{\hspace{0.17em}}}typ\right)\mapsto GDensity\left(k\right)=\\ (\begin{array}{l}typ=e\mathrm{,\text{\hspace{0.17em}}}\lambda \cdot {e}^{-\lambda x}\mathrm{\text{\hspace{0.17em}}}\left(\lambda \ge \mathrm{0,\text{\hspace{0.17em}}}x\ge 0\right)\mathrm{;}\\ typ=n\mathrm{,\text{\hspace{0.17em}}}1/\left(2\sqrt{2\pi}\right)\cdot {e}^{-1/2\cdot {x}^{2}}\mathrm{,}\left(x\ge {a}_{p}\right)\mathrm{;}\\ typ=ln\mathrm{,\text{\hspace{0.17em}}}1/x\sigma \sqrt{2\pi}\cdot {e}^{-\left({\left(\mathrm{ln}x-\mu \right)}^{2}/2{\sigma}^{2}\right)}\mathrm{,}\left(x\ge {a}_{p}\mathrm{,\text{\hspace{0.17em}}}\sigma \in {\text{R}}^{+}\mathrm{,\text{\hspace{0.17em}}}\mu \in \text{R}\right)\mathrm{.}\\ {a}_{p}=\mathrm{min}\left(IR{P}_{p}\right)\mathrm{\text{\hspace{0.17em}}\text{\hspace{0.17em}}}\left(\forall t{r}_{j}\in {}^{I}p\right)\text{\hspace{0.17em}}\text{and}\text{\hspace{0.17em}}\left(GTyp\text{-}P\left(p\right)\in \mathrm{\text{\hspace{0.17em}}}\left\{o\mathrm{,\text{\hspace{0.17em}}}w\right\}\right)\mathrm{.}\end{array}\end{array}$ (3)

· *GDistrib*: each *WPTSPN* component (tokens, and stochastic transitions) is assigned an arbitrary probability distribution (Normal, Log-Normal, or Exponential). This assignment is performed by the function *GDistrib*.

$\begin{array}{l}GDistrib\mathrm{:}\left(Ac\mathrm{\text{\hspace{0.17em}}}\cup \mathrm{\text{\hspace{0.17em}}}Sac\cup T{r}_{s}\right)\times \left\{e\mathrm{,\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ln\right\}\to {\text{R}}^{+}\\ typd=Typ\text{-}dist\left(k\right)\\ typ\text{-}k=Typ\text{-}tk(\; k\; )\end{array}$

$\begin{array}{l}\left(k\mathrm{,}typ\text{-}d\mathrm{,}typ\text{-}k\right)\mapsto GDistrib\left(k\right)=\\ (\begin{array}{l}typ=e\mathrm{,\text{\hspace{0.17em}}1}-{e}^{-\lambda x}\mathrm{\text{\hspace{0.17em}}}\left(\lambda \ge \mathrm{0,\text{\hspace{0.17em}}}x\ge {a}_{p}\right)\mathrm{;}\\ typ=n\mathrm{,\text{\hspace{0.17em}}}1/\left(2\sqrt{2\pi}\right)\cdot {\displaystyle {\int}_{-\infty}^{t}}\text{\hspace{0.05em}}\text{\hspace{0.05em}}{e}^{-1/2\cdot {x}^{2}}dx\mathrm{,}\left(x\ge {a}_{p}\mathrm{,\text{\hspace{0.17em}}}t\ge {a}_{p}\right)\mathrm{;}\\ typ=ln\mathrm{,\text{\hspace{0.17em}}}1/2+1/2\cdot er{f}^{-\left({\left(\mathrm{ln}x-\mu \right)}^{2}/2{\sigma}^{2}\right)}\mathrm{,}\\ \left(x\ge {a}_{p}\mathrm{,\text{\hspace{0.17em}}}\sigma \in {\text{R}}^{+}\mathrm{,\text{\hspace{0.17em}}}\mu \in \text{R}\mathrm{,\text{\hspace{0.17em}}}erf\mathrm{\text{\hspace{0.17em}}}\text{istheGausserrorfunction}\right)\mathrm{;}\\ {a}_{p}=\mathrm{min}\left(IR{P}_{p}\right)\mathrm{\text{\hspace{0.17em}}\text{\hspace{0.17em}}}\left(\forall t{r}_{j}\in {}^{I}p\right)\text{\hspace{0.17em}}\text{and}\text{\hspace{0.17em}}\left(GTyp\text{-}P\left(p\right)\mathrm{\text{\hspace{0.17em}}}\in \mathrm{\text{\hspace{0.17em}}}\left\{o\mathrm{,\text{\hspace{0.17em}}}w\right\}\right)\mathrm{.}\end{array}\end{array}$ (4)

· *TFringT*: Our model assigned three probability distributions (Normal, Log-Normal, or Exponential) to each stochastic transition [66] . This function makes it possible to determine each stochastic transition firing time, with *TFringT*-function, according to the distribution chosen. We use the gravity center method [48] which consists of taking the abscissa corresponding to the gravity center of the each stochastic density transition.

$\begin{array}{l}TFringT\mathrm{:}T{r}_{s}\times \left\{e\mathrm{,\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ln\right\}\to {\text{R}}^{+}\\ typ=Typ\text{-}dist\left(trs\right)\end{array}$

$\begin{array}{l}\left(trs\mathrm{,}typ\right)\mapsto TFringT\left(trs\right)=\\ (\begin{array}{l}typ=e\mathrm{,}\frac{{\displaystyle {\int}_{-\infty}^{t}}\left(\lambda \cdot {e}^{-\lambda x}\right)\mathrm{\text{\hspace{0.17em}}}\cdot \mathrm{\text{\hspace{0.17em}}}xdx}{{\displaystyle {\int}_{-\infty}^{+\infty}}\left(\lambda \cdot {e}^{-\lambda x}\right)dx}\mathrm{;}\\ typ=n\mathrm{,}\frac{{\displaystyle {\int}_{-\infty}^{+\infty}}\left(\left(1/\left(2\sqrt{2\pi}\right)\cdot {e}^{-1/2\cdot {x}^{2}}\right)\cdot x\right)dx}{{\displaystyle {\int}_{-\infty}^{+\infty}}\left(1/\left(2\sqrt{2\pi}\right)\cdot {e}^{-1/2\cdot {x}^{2}}\right)dx}\mathrm{;}\\ typ=ln\mathrm{,}\frac{{\displaystyle {\int}_{-\infty}^{+\infty}}\left(1/x\sigma \sqrt{2\pi}\cdot {e}^{-\left({\left(\mathrm{ln}x-\mu \right)}^{2}/2{\sigma}^{2}\right)}\cdot \mathrm{\text{\hspace{0.17em}}}x\right)dx}{{\displaystyle {\int}_{-\infty}^{+\infty}}\left(1/x\sigma \sqrt{2\pi}\cdot {e}^{-\left({\left(\mathrm{ln}x-\mu \right)}^{2}/2{\sigma}^{2}\right)}\right)dx}\mathrm{;}\\ \left(x\in {\text{R}}^{+}\mathrm{,}\lambda \in {\text{R}}^{+}\mathrm{,\text{\hspace{0.17em}}}\sigma \in {\text{R}}^{+}\mathrm{,\text{\hspace{0.17em}}}\mu \in \text{R}\right)\mathrm{.}\end{array}\end{array}$ (5)

· *IRP*: *IRP _{i}* function defines the static residence (stay) interval of the model’s places (initial or workflow). (
$\forall {p}_{i}\in \left({P}_{o}\cup {P}_{w}\right)\backslash GTyp\text{-}P\left({p}_{i}\right)\mathrm{\text{\hspace{0.17em}}}\in \left\{O\mathrm{,\text{\hspace{0.17em}}}w\right\}$ ). When it leaves the place
${p}_{i}$ , the output transitions firing becomes equal to
${b}_{i}$ . After this random time (
${b}_{i}$ ), the token will be “dead” and will no longer participate in the transitions validation. Formally

$IRP\mathrm{:}{P}_{o}\cup {P}_{w}\to {\mathbb{Q}}^{+}\cup \left({\mathbb{Q}}^{+}\times +\infty \right)$ ;

$\forall {p}_{i}\in {P}_{o}\cup {P}_{w}\backslash GTyp\text{-}P\left({p}_{i}\right)\in \left\{o\mathrm{,\text{\hspace{0.17em}}}w\right\}$ ;

${p}_{i}\to IR{P}_{i}=\left[{a}_{i}\mathrm{,\text{\hspace{0.17em}}}{b}_{i}\right]\text{\hspace{0.17em}}\text{\hspace{0.05em}}\text{with}\text{\hspace{0.17em}}0\le {a}_{i}\le {b}_{i}$ ;

$(\begin{array}{l}{a}_{i}=\mathrm{min}\left({a}_{i}\mathrm{,\text{\hspace{0.17em}}}{b}_{i}\right)\mathrm{\text{\hspace{0.17em}}}\left(\forall \mathrm{\text{\hspace{0.17em}}}tr\in {}^{I}p\right)\mathrm{;}\\ {b}_{i}=\mathrm{max}\left({a}_{i}\mathrm{,\text{\hspace{0.17em}}}{b}_{i}\right)\mathrm{;\text{\hspace{0.17em}}}\left(\forall \mathrm{\text{\hspace{0.17em}}}tr\in {}^{I}p\right)\mathrm{;}\end{array}$ (6)

· *MST*: (Mean Stay Time) Taking into account the specificity of the token’s type (activity or sub-activity) in places of our model. So, the *MST*-function calculates each token’s average stay time in timed locations and which are of type (initial or workflow). We associate time value, framed by the
$\mathrm{min}\left(TFringT\left(tr\right)\right)$ (
$\forall tr\in {}^{I}p$ ) and the
$\mathrm{min}\left(TfiringT\left(tr\right)\right)$ (
$\forall tr\in {p}^{O}\backslash \left(GTyp\text{-}P\left(p\right)\right)\in \left\{O\mathrm{,\text{\hspace{0.17em}}}w\right\}$ ,
$Typ\text{-}tk\left(M\left(p\right)\right)\in \left\{\mathrm{2,\text{\hspace{0.17em}}3,\text{\hspace{0.17em}}4}\right\}$ ), taking into account the random distribution assigned to each token in this place. Practically, we use the gravity center method [48] which determines the abscissa corresponding to the density attributed to the place in question.

$\begin{array}{l}MST\mathrm{:}\left(P\cup Ac\cup Sac\times T{r}_{s}\times \left\{e\mathrm{,\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ln\right\}\right)\to {\text{R}}^{+}\\ ty=GTyp\text{-}P\left(p\right)\in \left\{o\mathrm{,\text{\hspace{0.17em}}}w\right\}\\ typ=GTyp\text{-}dist\left(ttk\right)\\ ttk=Typ\text{-}tk\left(M\left(p\right)\right)\\ m=\mathrm{min}\left(TFringT\left(tr\right)\right)\forall tr\in {}^{I}p\\ M=\mathrm{min}\left(TFringT\left(tr\right)\right)\forall tr\in {p}^{O}\end{array}$

$\begin{array}{l}\left(p\mathrm{,\text{\hspace{0.17em}}}ty\mathrm{,\text{\hspace{0.17em}}}typ\mathrm{,\text{\hspace{0.17em}}}ttk\right)\mapsto MST\left(p\right)=\\ (\begin{array}{l}ty\in \left\{o\mathrm{,}w\right\}\mathrm{,\text{\hspace{0.17em}}}typ=\mathrm{\text{\hspace{0.17em}}}e\mathrm{,\text{\hspace{0.17em}}}ttk\in \left\{\mathrm{1,2}\right\}\mathrm{,\text{\hspace{0.17em}}}\frac{{\displaystyle {\int}_{m}^{M}}\left(\lambda \cdot {e}^{-\lambda x}\right)\mathrm{\text{\hspace{0.17em}}}\cdot \mathrm{\text{\hspace{0.17em}}}xdx}{{\displaystyle {\int}_{m}^{M}}\left(\lambda \cdot {e}^{-\lambda x}\right)dx}\mathrm{;}\\ ty\in \left\{o\mathrm{,}w\right\}\mathrm{,\text{\hspace{0.17em}}}typ=\mathrm{\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ttk\in \left\{\mathrm{1,2}\right\}\mathrm{,\text{\hspace{0.17em}}}\frac{{\displaystyle {\int}_{m}^{M}}\left(\left(1/2\sqrt{2\pi}\cdot {e}^{-1/2\cdot {x}^{2}}\right)\cdot x\right)dx}{{\displaystyle {\int}_{m}^{M}}\left(1/2\sqrt{2\pi}\cdot {e}^{-1/2\cdot {x}^{2}}\right)dx}\mathrm{;}\\ ty\in \left\{o\mathrm{,}w\right\}\mathrm{,\text{\hspace{0.17em}}}typ=\mathrm{\text{\hspace{0.17em}}}ln\mathrm{,\text{\hspace{0.17em}}}ttk\in \left\{\mathrm{1,2}\right\}\mathrm{,\text{\hspace{0.17em}}}\frac{{\displaystyle {\int}_{m}^{M}}\left(1/x\sigma \sqrt{2\pi}\cdot {e}^{-\left({\left(\mathrm{ln}x-\mu \right)}^{2}/2{\sigma}^{2}\right)}\cdot \mathrm{\text{\hspace{0.17em}}}x\right)dx}{{\displaystyle {\int}_{m}^{M}}\left(1/x\sigma \sqrt{2\pi}\cdot {e}^{-\left({\left(\mathrm{ln}x-\mu \right)}^{2}/2{\sigma}^{2}\right)}\right)dx}\mathrm{;}\\ \left(x\in \left[m\mathrm{,\text{\hspace{0.17em}}}M\right]\mathrm{,}\lambda \in {\text{R}}^{+}\mathrm{,\text{\hspace{0.17em}}}\sigma \in {\text{R}}^{+}\mathrm{,\text{\hspace{0.17em}}}\mu \in \text{R}\right)\mathrm{.}\\ m<\mathrm{min}\left(IRP\left(p\right)\right)\text{\hspace{0.17em}}\text{and}\text{\hspace{0.17em}}M<\mathrm{max}\left(IRP\left(p\right)\right)\mathrm{.}\end{array}\end{array}$ (7)

· *GTruncated*: We use a truncated density function to estimate and predict the delay related to the residence time of a token in a timed place. And for it to cover the densities allocated to the tokens’ residence time in each timed place. We define the generalized truncated density sojourn probability law of a timed place function as follows:

$\begin{array}{l}Truncated\mathrm{:}\left(P\cup T{r}_{s}\right)\mathrm{\text{\hspace{0.17em}}}\to \mathrm{\text{\hspace{0.17em}}}{\text{R}}^{+}\\ \left({t}_{0}\mathrm{,\text{\hspace{0.17em}}}t\right)\in TD\times TD\\ typ\in \left\{e\mathrm{,\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ln\right\}\\ ttk\in \left\{\mathrm{1,2,4}\right\}\\ \left(k\mathrm{,}typ\right)\mapsto GDensity\left(k\right)\\ \left(k\mathrm{,}typ\right)\mapsto GDistrib(\; k\; )\end{array}$

$\begin{array}{l}Truncated\left(k\mathrm{,}ttk\right)=\\ (\begin{array}{l}\mathrm{0,\text{\hspace{0.17em}}\text{\hspace{0.17em}}}t\le {t}_{0}\mathrm{,\text{\hspace{0.17em}}}GDistrib\left({t}_{0}\right)\le \mathrm{1;}\\ GDensity\left(t\right)/1-GDistrib\left({t}_{0}\right)\mathrm{,\text{\hspace{0.17em}}}t>{t}_{0}\mathrm{,\text{\hspace{0.17em}}}GDistrib\left({t}_{0}\right)<\mathrm{1;}\\ GDensit{y}_{\Delta}\left(t-{t}_{0}\right)\mathrm{,\text{\hspace{0.17em}}}GDistrib\left({t}_{0}\right)=\mathrm{1;}\end{array}\end{array}$ (8)

· Let *MIP*: the places input-transitions matrix:

$\left(P\times Tr\right)\to \left\{\mathrm{0,1}\right\}$ (9)

Such that:

$MIP\left({P}_{i}\mathrm{,\text{\hspace{0.17em}}}t{r}_{k}\right)=0$ , if ${}^{I}P\left({P}_{i}\mathrm{,\text{\hspace{0.17em}}}t{r}_{k}\right)=\varnothing $ , 1 if not

· Let *MPO*: the places output-transitions matrix :

$\left(P\times Tr\right)\to \left\{\mathrm{0,1}\right\}$ (10)

Such that:

$MPO\left({P}_{i}\mathrm{,\text{\hspace{0.17em}}}t{r}_{k}\right)=0$ , if ${P}^{O}\left({P}_{i}\mathrm{,\text{\hspace{0.17em}}}t{r}_{k}\right)=\mathrm{\text{\hspace{0.17em}}}\varnothing $ , 1 if not.

· Let *MIT*: the transitions input-places matrix:

$\left(Tr\times P\right)\to \left\{\mathrm{0,1}\right\}$ (11)

Such that:

$MIT\left(t{r}_{k}\mathrm{,}{P}_{i}\right)=0$ , if ${}^{I}Tr\left(t{r}_{k}\mathrm{,}{P}_{i}\right)=\varnothing $ , 1 if not

· Let *MTO*: the transitions output-places matrix:

$\left(Tr\times P\right)\to \left\{\mathrm{0,1}\right\}$ (12)

Such that:

$MTO\left(t{r}_{k}\mathrm{,}{P}_{i}\right)=0$ , if $T{r}^{O}\left(t{r}_{k}\mathrm{,}{P}_{i}\right)=\varnothing $ , 1 if not

The firing transitions semantics adopted by the *WPTSPN* model are defined in the next sections.

3.3. Firing Transitions Semantics Adopted by the *WPTSPN*

The firing semantics adopted by the *WPTSPN* depend on three factors: the static stay (residence) interval of the places at the transition input, the stochastic firing time, the average stay time of tokens in workflow entry places, and preconditions related to the interaction between the actors responsible for executing the activity represented by the transition. To explain this firing mechanism, we need to apply it to the context of the transition *tr*_{6}. According to Table 3, the transition *Tr*_{6} which represents the operation below (“Machine run”).

Figure 1 illustrates the *tr*_{6} transition and the mechanism of division (splitted) into three micro-transitions:
$\left\{t{r}_{6}^{c}\mathrm{,}t{r}_{6}^{w}\mathrm{,}t{r}_{6}^{p}\right\}$ .

The transition *tr*_{6} is stochastic according to the *WPTSPN*, so we assign a random value of firing time using
$tydt=GTyp\text{-}dis\left(t{r}_{6}\right)\in \left\{e\mathrm{,\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ln\right\}$ and
$TFringT\left(tydt\mathrm{,\text{\hspace{0.17em}}}t{r}_{6}\right)$ .

We note that according to the representation semantics of the WPTSPN: Let input places: ${}^{I}T{r}_{6}=\left\{{P}_{0}\mathrm{,}{P}_{7}\mathrm{,}{P}_{8}\right\}$ and output place: $T{r}_{6}^{O}=\left\{{P}_{10}\mathrm{,}{P}_{0}\mathrm{,}{P}_{8}\right\}$ .

· *P*_{0}: specifies the park of actors,
$GTyp\text{-}P\left({P}_{0}\right)=r$ ;

· *P*_{7}: specifies the both a machine bounded input and conveyor output buffer,
$GTyp\text{-}P\left({P}_{7}\right)=w$ ;

Figure 1. The *tr*_{6} transition and their micro-transitions and micro-places according to the division (splitted) mechanism of the *WPTSPN*.

· *P*_{8}: specifies place of the maintenance sub-process,
$GTyp\text{-}P\left({P}_{7}\right)=r$ ;

· *P*_{10}: specifies the end of workflow process
$GTyp\text{-}P\left({P}_{7}\right)=f$ ;.

It is assumed that non-workflow places (*P*_{0},* P*_{8}), *i.e*., resources, are not timed, so the tokens they store are always available, such as actors, primary materials, or semi-finished products. The timed place *P*_{7} is a workflow place dedicated to storing an activity or sub-activity type token (noted *tk*:
$Typ\text{-}tk\left(tk\right)=\in \left\{\mathrm{2,3}\right\}$ ). Then we assign a static interval of stay (residence):
$IRP\left({P}_{7}\right)=\left[{a}_{7}\mathrm{,}{b}_{7}\right]$ .

At the moment when the token named *tk* such that *Gtype*(*tk*) = 2 (*i.e*. of type *Sac*) instead of *p*_{7}, we assign it a stochastic value of stay using the density function (
${\tau}_{tk}=Gdensity\left(tk\mathrm{,}ty\right)$ ) where *ty* varies between the three possible distributions of the model
$\left\{e\mathrm{,\text{\hspace{0.17em}}}n\mathrm{,\text{\hspace{0.17em}}}ln\right\}$ . If there are several (*Gtype*(*tk*) = 2) type tokens, an average residence time is used using the
$MST\left({P}_{7}\right)$ function.

The firing semantics of a stochastic transition with timed places assumes that a time counter is triggered when a token arrives. Let t be the value of this time counter. We associate a token-life-cycle time named $\left({\tau}_{tk}\mathrm{,}t\right)$ . We discuss the following three cases:

·
${\tau}_{tk}<{a}_{i}\left({P}_{7}\right)$ ; so the *tk* token is not available.

·
$t\in \left[{a}_{7}\mathrm{,}{a}_{7}+{\tau}_{tk}\right]$ and (
${a}_{7}+{\tau}_{tk}<TFiring\left(T{r}_{6}\right)<{b}_{7}$ ); During *Tr*_{6} firing, *WPTSPN* detects the transition type via the function calls *Distinct*(*Tr*_{6}) = 3 and *GTyp*-*dist*(*Tr*_{6}) = *ln*. We know that the overall firing time value is determined by the function call *TFiringT*(*Tr*_{6}, *ln*). The transition firing *Tr*_{6}, which is in the sub activity executing charge *Sac*_{1}, consists in sequentially firing the three micro-transitions *Tr*_{6}* ^{c}*,
$T{r}_{6}^{w}$ and
$T{r}_{6}^{p}$ . The transition pre-condition
$T{r}_{6}^{c}$ is the

·
${\tau}_{k}>{b}_{7}$ ; so the *tk* token is dead. We note that the tokens which circulate in the three micro-transitions have the same behavior according to the static residence time. Note that each micro transition from the split mechanism inherits a behavior similar to the transition (splitted).

The main properties that generally studied the *WPTSPN* are verification and checking. First, verification consists in determining the techniques for deciding on each of them. Second, checking, which is based on the dynamic timed evolution to analayze and verify this model properties, is then presented.

3.4. *WPTSPN* Checking Formal Tools

The *WPTSPN* model can be used to qualitatively analyze the basic *FMS* properties to provide the dynamic behavioral aspects of complex systems. The *CdM* (marking cardinalities graph) associated with the model at any time in time represents the number and position of tokens concerning the places of the model. Firing a transition moves the model into a new marking cardinality. The marking cardinality of an *WPTSPN* helps to define which places are occupied and which are free.

The model adopts two verification approaches:

· Checking based on the elapsed time following a firing transitions sequence:

- Reachability (Accessibility): A *CdM*’ marking cardinality is said to be accessible from *CdM* if there are sequences of markings cardinalities (*CdM*_{0} to *CdM _{n}*) and transitions (
$t{r}_{0}$ to
$t{r}_{n}$ ,
$\forall \left(t{r}_{0}\mathrm{,}t{r}_{n}\right)\in \left(Tr\times Tr\right)$ ) such as
$Cd{M}_{i+1}$ is immediately accessible from

So reachability seems to be a tool for finding erroneous states, for practical problems the constructed graph usually has far too many states to compute. This allows us to detect execution failures of a business process (FMS) modeled by a *WPTSPN*.

- Safeness: An *WPTSPN* is safe if each of its places (
$\forall p\in P$ ) is safe. So, a place *p* is safe if it does not contain more than one token. The model transitions if it can fire infinitely often, so if there is always a fixed (necessarily infinite) firing sequence that ensures the execution of a workflow activity.

- Boundeness: A *WPTSPN* is said to be bounded if it is composed only of bounded places. A place (
$\forall p\in P$ ) is bounded if there is a limit on the tokens maximum number (
$CdM\left(p\right)\le K$ \(
$\forall p\in P,K>1$ )).

This property indicates that the system represented by a *WPTSPN* never risks exceeding the storage limits of semi-finished material, finished products, and workers… This property indicates that the system represented by a *WPTSPN* never risks exceeding the storage limits of semi-finished material, finished products, and workers…

- Conservativeness: A *WPTSPN* is said to be conservative if the tokens-number in the
$\forall CdM\in CdM$ remains constant.

It is obvious that conservativeness is a special case of structural delimitation and that coherence is a case of repetitiveness. Then this property can be partial, consistency and repetitiveness are the relaxations of the circulation of tokens in the places of the *WPTSPN*.

- Liveness: A transition is said to be alive if for each (
$\forall CdM\in \left(CdM\mathrm{,}WPTSPN\right)$ ) there is a firing sequence which brings the *WPTSPN* to a *CdM* in which this *tr* transition is fired. An *WPTSPN* is active if each transitions (
$\forall tr\in Tr$ ) are active. If the *WPTSPN* is activated and correct, this indicates that there are no deadlocks in the *FMS* operations.

- Properness: if the initial marking *CdM*_{0} is accessible from each marking (
$\forall CdM\in \left(CdM\mathrm{,}u\right)$ ) in the accessibility set, the *WPTSPN* is said to be proper.

This property verifies that the tokens which represent the actors (worker) return to their place of origin before the each firing model’s transition for which they will always be available at the future firing (excution of an activity workflow FMS).

· Checking is based on randomly residence intervals associated with the token in workflow-places and the token life-cycle:

We keep the verification properties related to the firing transitions context, and we add other definitions related to the *P*-*timed* *SPN* contexts that we adopt in this work. Let *DT* is a finite time domain; Let *t*: time in finished time domain (
$\forall t\in DT$ ); Let state characterizing the *WPTSPN* graph situation be defined by a doublet *SE* = <*CdM*, *Q*>, where:

· *CdM* is the same as the previous definition of the *WPTSPN* marking function,

· *Q* is a time-of-stay application which associates with each token *k* (
$\forall k\in \left\{SAC\cup AC\right\}$ ) in place
${p}_{i}$ (
$\forall {p}_{i}\in P\mathrm{\text{\hspace{0.17em}}}\backslash \mathrm{\text{\hspace{0.17em}}}Typ\text{-}tk\left(M\left({p}_{i}\right)\right)\in \left\{\mathrm{1,2,4}\right\}$ ) a real number
${q}_{i}^{k}$ where
${q}^{k}$ is the this token lifetime (the time elapsed since its arrival in place
${p}_{i}$ ). The
${q}_{i}^{k}$ associated with a token *k* in the place
${p}_{i}$ must be less than or equal to bi where
$\left[{a}_{i}\mathrm{,}{b}_{i}\right]$ is the Randomly residence interval associated with the place
${p}_{i}$ . This token *k* in the place
${p}_{i}$ is involved in the activation and validation of its *p ^{O}* transitions when
${q}_{i}^{k}$

Note that the lifetime
${q}_{i}^{k}$ of a token
$k\in \left(Ac\times Sac\right)$ (given by a local clock associated with it) is relative to this token arrival time in the place
${p}_{i}\backslash Typ\text{-}tk\left(M\left({p}_{i}\right)\right)\in \left\{\mathrm{1,2,4}\right\}$ . We suppose that the token *k* arrives in the place
${p}_{i}$ at the instant
$\tau $ (given by a global clock for example), this token time duration is equal to zero. At the absolute instant
${\tau}^{\prime}$ its lifetime is
${q}_{i}^{k}={\tau}^{\prime}-\tau $ . It participates in the validation of the output transitions of the place (
$\forall tr\in {p}_{i}^{O}$ which contains it, only from the instant
${\tau}^{\prime}=\tau \mathrm{\text{\hspace{0.17em}}}+\mathrm{\text{\hspace{0.17em}}}{a}_{i}$ , and it is dead from the instant
${\tau}^{\prime}>\tau \mathrm{\text{\hspace{0.17em}}}+\mathrm{\text{\hspace{0.17em}}}{b}_{i}$ . Then, a token is dead if its lifetime becomes strictly greater than the upper limit of the dynamic interval associated with its host place and if none of its exit transitions is validated at this time. Therefore, a transition can be activated and validated in the semantics of autonomous *PNs* and not in the *WPTSPN*’s semantics because of time constraints.

· A transition ( $tr\in T$ ) is potentially firable (validated in the semantics of model) from the state $SE\left(CdM\mathrm{,}Q\right)$ if and only if:

- It is validated within the meaning *WPTSPN*s in this state, that is to say
$\forall {p}_{i}\in {}^{I}tr\mathrm{;\text{\hspace{0.17em}}}CdM\left({p}_{i}\right)\mathrm{\text{\hspace{0.17em}}}\ge \mathrm{\text{\hspace{0.17em}}}Card\left(I\left({p}_{i}\mathrm{,}tr\right)\right)\mathrm{;\text{\hspace{0.17em}}}Typ\text{-}tk\left(M\left(p\right)\right)\in \left\{\mathrm{1,2,4}\right\}$ (*Card*: function which counts the tokens number in input flow or respectively output flow)
$\forall {p}_{i}\in {}^{I}tr$ , there is at least
$I\left({p}_{i}\mathrm{,}tr\right)$ tokens in the place such as:
$\mathrm{min}\left({b}_{i}\mathrm{\text{\hspace{0.17em}}}-\mathrm{\text{\hspace{0.17em}}}{q}_{i}^{k}\right)-\mathrm{max}\left(\mathrm{0,}\mathrm{max}\left({a}_{i}-{q}_{i}^{k}\right)\right)\ge 0$
$\left(\forall k\in \left\{SAC\cup AC\right\}\right)$ and
$\left[{a}_{i}\mathrm{,}{b}_{i}\right]$ is the dynamic interval associated with the place
${p}_{i}$ . In addition, there are no *j* tokens (which do not participate in firing the *tr* transition) such as:
$\left({b}_{i}\mathrm{\text{\hspace{0.17em}}}-\mathrm{\text{\hspace{0.17em}}}{q}_{i}^{k}\right)\le \mathrm{max}\left(\mathrm{0,}\mathrm{max}\left({a}_{i}\mathrm{\text{\hspace{0.17em}}}-\mathrm{\text{\hspace{0.17em}}}{q}_{i}^{k}\right)\right)$ .

- Otherwise, this token is *dead*. It is, then, associated with this place interval:
$\left[\mathrm{max}\left(0,\mathrm{max}\left({a}_{i}\mathrm{\text{\hspace{0.17em}}}-\mathrm{\text{\hspace{0.17em}}}{q}_{i}^{k}\right)\right),\mathrm{min}\left({b}_{i}\mathrm{\text{\hspace{0.17em}}}-\mathrm{\text{\hspace{0.17em}}}{q}_{i}^{k}\right)\right]$ .

Figure 2 illustrates the token life-cycle according to the firing semantics of the *WPTSPN*.

When we perform in the intersection of all these intervals (
$\forall p\in {}^{I}tr$ , we associate an interval), we select the interval in which the transition remains potentially firable. According to the state *SE* notion, from a given state, an infinite number of states is generally accessible. There are, therefore, two possibilities of having this new state from an earlier state:

- the time fluidity (time passage);

- the transition firing (the potential firing interval lower limit is equal to zero from this new state).

Figure 2. Token life-cycle according to the firing semantics of the *WPTSPN* model.

· The state *e*’ accessibility from a previous state *e* (
$\left(e\mathrm{,}{e}^{\prime}\right)\in SE\times SE$ ):

- by a
$\tau $ time-flow: we note
$e\left(CdM\mathrm{,}Q\right)\to {e}^{\prime}\left(Cd{M}^{\prime}\mathrm{,}{Q}^{\prime}\right)$ , is verifiable if:
$CdM\ne Cd{M}^{\prime}$ ,
$\forall k\in \left(SAC\cup Ac\right)$ in the
${p}_{i}\backslash Typ\text{-}tk\left(M\left({p}_{i}\right)\right)\in \left\{\mathrm{1,2,4}\right\}$ place,
${{q}^{\prime}}_{i}^{k}={q}_{i}^{k}+\tau $ ; where
${q}_{i}^{k}$ (respectively
${{q}^{\prime}}_{i}^{k}$ ) is the token *k* lifetime in state *e* (respectively in state *e*’) and
${b}_{i}$ is the dynamic interval upper bound associated with the place
${p}_{i}$ .

- by firing a transition
$t{r}_{i}$ if and only if:
$t{r}_{i}$ can be firing directly (the lifetimes of all the marks which validate
$t{r}_{i}$ are greater than or equal to the dynamic intervals lower bounds associated with their places) from *e*,
$\forall p\in {P}_{w}$ ,
$Cd{M}^{\prime}\left(p\right)=CdM\left(p\right)-CdM\left(I\left(p\mathrm{,}t{r}_{i}\right)\right)+CdM\left(O\left(t{r}_{i}\mathrm{,}p\right)\right)$ . When the tokens do not flow and keep the same lifetime in *e* and *e*’ (this is assumed to be an immediate transition), then we assume those tokens that are flowed or created have a lifetime (age) equal to zero. We note that the preceding firing rule allows us to determine the states and the state-space accessibility relations. The set of firing transitions’ sequences from the initial state characterizes the dynamic behavior of the *WPTSPN*.

According to the state analysis, either by time fluidity or by firing a transitions sequence, the *WPTSPN* verifiable properties are:

· An *WPTSPN* model’s state
$e\left(CdM\mathrm{,}Q\right)$ is tokens-alive if all of the tokens in *CdM* are alive.

· A *WPTSPN* is token-alive for an initial *CdM*_{0} marking (the initial state *e*_{0}) if all the markings accessible from *CdM*_{0} are token-alive states.

We adopt the hypothesis that if a token, in a cardinality marking a state accessible from *e*_{0}, is verified dead, the *WPTSPN* is dead tokens. Consequently, this dead token no longer participates in the transitions validation. There are two objectives through which we can verify the token death upstream of a synchronization transition *tr*:

- the tokens on circuits containing it do not arrive at a compatible time in its entry places ( $\forall p\in {}^{I}tr$ ),

- the tokens, on the transition elementary oriented paths from parallelism to *tr*, do not arrive at compatible instants upstream of the transition *tr*.

· A transitions firing sequence (made up of the transitions and the associated firing time $\left(\left(SE\mathrm{,\text{\hspace{0.17em}}}tr\right)\mathrm{;}\forall tr\in \left(T{r}_{s}\cup T{r}_{d}\right)\right)$ is called a token-liveness sequence (k-v-sequence) if and only if each of the states accessible ( $\forall e\in SE$ ) by this transition sequence is token-alive states.

· A transition firing sequence (*SE*, *u*) is repetitive if, for a state
$\exists e\mathrm{\text{\hspace{0.17em}}}\in \mathrm{\text{\hspace{0.17em}}}SE$ reachable from *e*_{0} (the initial state of graph states), *e* is accessible from *e* by the (*SE*, *u*) sequence transitions firing.

· A transition firing sequence (*SE*, *u*) is complete if it contains each of the transitions (
$u\subseteq Tr$ ) composing the *WPTSPN* model. The *WPTSPN* model checking P-timed properties definitions help to adopt the tow following assumptions in [30] :

- If an *WPTSPN* has a repetitive and complete (*tok*-*v*-*sequence*), then this model has at least one operation which results in a steady-state after a finite time.

- If an *WPTSPN* is boundless, alive, and alive-tokens then each operation of the model results in a steady-state after a finite time.

After verifying the *WPTSPN* model’s probabilities according to two P- and T-timed orientations, we show our formal mechanism for predicting of the delay relative to the residence time of sac-token in timed places.

3.5. Delay Prediction Relative to the Randomly Residence Time in Model Place

In this subsection, we demonstrate the specificity in the delay prediction that is related to the token’ randomly residence time assigned in the model’ timed places. We include the *Event*-*log* related to *WPTSPN* model to provide delay semantics in the activities’ description. Let *TD* represent the temporal domain associated with the state firing sequence *SE*.

So, we define an *Event Log* by *LEv* = (*SE*, *C*, *D*):

· *SE*: states’ firing sequence set,

· *C*: cases finite set where each case specifies an *FMS* business process instance,

· *D*:
$SE\to TD$ . A function to assign each event to time-space and classify it as a time function.

Each deterministic and stochastic transitions in the *WPTSPN* (
$tr\in \left(T{r}_{d}\mathrm{\text{\hspace{0.17em}}}\cup \mathrm{\text{\hspace{0.17em}}}T{r}_{s}\right)$ ) are covered by the set *SE*. And, each *SE*/*CdM* states in the event log contain the *C* set. We can utilize a time capture approach based on a probabilistic aspect to assure the prediction of the delay associated to task execution in the business processes represented by our model. As a result, this model was integrated with an event-log (*Eventlog** *: *LEv*) to predict remaining durations as well as the probability of execution delays. To induce the elapsed time required by the model, we use the same definition of a sequence of delays
$\left\{{d}_{0}\mathrm{,}{d}_{1}\mathrm{,}{d}_{2}\mathrm{,\text{\hspace{0.17em}}}\cdots \mathrm{,}{d}_{n}\right\}$ , where
$d\in TD$ is the time elapsed before the occurrence of *se*_{0} and *d _{i}* is the elapsed time between occurrences of
$s{e}_{i}$ and (
$\forall s{e}_{i}\mathrm{\text{\hspace{0.17em}}}\in \mathrm{\text{\hspace{0.17em}}}SE$ ) The prediction method is based on:

· The enrichment of places with probabilistic delays in order to determine the duration of an activity and the associated stay time.

· To determine the probability of a decision outcome, assign weights to places.

· The probability density function associated with stochastic places determines the randomly residence time distribution.

· Using an adjacent algorithm in the *WPTSPN* to predict the residence delay based on the elapsed time.

A monitoring system that collects and records the *FMS* business process steps is required for our *WPTSPN* to be stochastically verified. According to this assumption, the time since the previous occurrence represents an information source that benefits the preacher in acquiring precise accuracy for the model. With the duration distribution, it is possible to visualize the conditional impacts on the remaining time. The formal representation is as follows:

· $t\in TD$ : time space,

· $tr\in \left(T{r}_{d}\cup T{r}_{s}\right)$ : timed transition,

· ${P}_{i}\in {P}_{w}$ : timed place,

· $tk\mathrm{\text{\hspace{0.17em}}}\in Ac\mathrm{\text{\hspace{0.17em}}}\cup Sac$ : token,

· $GDistrib\left(k\right)k\in \left(P\cup T{r}_{d}\cup t{r}_{s}\right)$ : the duration distribution function,

· $GDensity\left(k\right)k\in \left(P\cup T{r}_{d}\cup t{r}_{s}\right)$ : The differential function $GDistrib\left(k\right)$ becomes the generalized density function.

· $Gtruncate{d}_{P}$ : the generalized truncated density function.

In a formal way, we denote that (
$t\in TD$ ) represents time, *tk* token (
$Typ\text{-}tk\left(tk\right)\in \left\{\mathrm{2,3,4}\right\}$ ) and (
${P}_{i}\in {P}_{w}$ ) is a timed place with the assigned static residence. Let (
${t}_{0}\in TD$ ;
${t}_{0}>0$ ) be *tr* the current place time sensor. Let *Gtruncated*_{Δ} be the *truncate* *delta* *function* which captures the entire probability mass at a single point.

We aim to build an algorithmic prediction solution based on the immediate detection of events. It is assumed that the duration of each stay place is purely isolated from other independent activities. This hypothesis allows us to simplify the forecasting process while remaining within the norms of other prediction approaches.

To perform the forecast on a state case, we build the forecast algorithm with six entries:

· business process model, its *states* *Graph* representative or markings cardinalities graph,

· current moment noted *t*_{0},

· minimum time limit: ${t}_{m}=Min\left(TFiringT\left(tr\right)\right)\left(\forall tr\mathrm{\text{\hspace{0.17em}}}\in {\mathrm{\text{\hspace{0.17em}}}}^{I}{P}_{i}\right)$ ,

· maximum time limit: ${t}_{M}=Min\left(TFiring\left(tr\right)\right)\left(\forall tr\mathrm{\text{\hspace{0.17em}}}\in \mathrm{\text{\hspace{0.17em}}}{P}_{i}^{O}\right)$ ,

· *Nbt*: activity Cases total number,

· activity current trace *c* which represents all the events observed up to the moment *t*_{0}.

The organizational chart illustrates the prediction process, which begins with a case activity search taking place in the model or one of its representative *SE* states. It’s a *SE* graph in the *WPTSPN* that specifies all of the observed events in this scenario.

Notation: we use the same concept which is an alignment method for localizing the current state in the business process model by adjusting the (place/transitions). The next step is to arrange the results of the probabilistic simulation (*t _{m}*,

We must notice that the remaining durations are estimated using the empirical estimation method.

4. Study Case: Flexible Manufacturing Systems

We show in this section the potential of a modeling approach based on the *WPTSPN* model via an application of industrial modeling. This approach is composed of the specification, the verification, and the delay prediction. In this case study, we use our *WPTSPN* to specify, verify, analyze, and simulate the production process.

In addition, the modeling of flexible manufacturing systems (*FMS*) in order to specify, analyze, verify, and optimize a manufacturing system according to different criteria. So it’s a performance study to detect any source of failure. This objective is summarized in a study to evaluate and compare several models of manufacturing systems by selecting the most suitable according to specific pre-selection criteria [64] . Our modeling process combines new formal tools specific to *WPTSPN*, with those of *SPN* [63] [64] to formulate a clear and expressive approach to specification, analysis, evaluation, and the checking process. Also, most *FMS*’ stochastic modeling studies [67] [68] have focused on steady-state analysis based on metrics such as throughput, productivity, and lifetime [4] [63] [64] [69] .

We note that the application of our model and its adjacent tools to an *FMS* example corresponds to the production chain section represented in [4] . In the present work, we rely on mixed specification, analysis, and verification between timed transitions, timed places (random residence time), and lifecycle tokens to detect delay sources. Our approach to modeling a flexible production chain based on the WPTSPN covers concepts related to delays, the temporal properties of transitions, and the circulation of tokens endowed with randomly timed life cycles (activities, sub-activities, actors, etc.).

The *FMS* system architecture [4] (See (Table 1)), modeled by *WPTSPN*, is composed of machines served by conveyor belts [4] . The raw material automatically comes from an unlimited buffer representing the raw material stockyard. The time between the arrival of these materials is distributed randomly. Knowing that the raw materials flow into the conveyor belt according to a strategy based on predictions of breakdowns. It is possible to assume that these two operations specify the movements on the conveyor chain. Firstly, the first operation is deterministic (with Delta Time) and designates the transport time between the pallet and the input buffer of the production machine, denoted (location 7) [4] . Suppose that the conveyor belt injects the raw materials into (slot 7) which specifies both a machine-limited input buffer and a conveyor output buffer. Thus, to synchronize logistics, the production system adopts a rule that blocks the conveyor belt when the location is saturated (two rooms in location 7). Secondly, the machine execution service is specified by operation 6. In parallel, the system estimates the lifetime according to a stochastic law. To simplify the calculations, we consider that the service is always available [4] . The control system assumes a breakdown/repair sub-process of the production chain: The time between two successive breakdowns distributed according to a normal distribution [4] .

Figure 3 illustrates the production chain [4] represented by Bizagi Modeler [70] adopting the BPMN 2.0 notification. Table 1 explains the business process steps (operations) represented by the *FSM* workflow. The Workflow Nets (*WF*-*Net*) notion [8] [71] , based on a Petri Net modeling, was introduced by Van Der Aalest [72] [73] . Also, the refinements made Van Der Aalest [6] [63] exploit the Petri Net criteria by behaving like an intuitive graphical language which results in Workflow models whose definition is clear and precise. We cannot leave the profile of an end-user in charge of generating Petri nets which are rather the expert’s language in the field of mathematical modeling. The conversion [72] [73] from a *WF*-*Net* to a Petri Net necessitates the interpretation of states (of a Role, a Resource, or a Tool) as “places” and operations (of the same model), usually represented by squares, as “transitions” [71] [72] [73] [74] .

4.1. *FMS* Specification by *WPTSPN*

We adopt a conversion manual method of the *WF*-*Net* (represented by *BPMN*) to *WPTSPN* using the terms adapted by [71] [72] [73] [74] .

Figure 3. Flexible manufacturing systems modeled based on *BPMN* 2.1 notation.

Table 1. Description of the *FMS*-business process steps.

· The application field is an *FMS*-Workflow.

· The set of $A\mathrm{\text{\hspace{0.17em}}}=\mathrm{\text{\hspace{0.17em}}}\left\{{A}_{1}\mathrm{,\text{\hspace{0.17em}}}{A}_{2}\mathrm{,\text{\hspace{0.17em}}}{A}_{3}\mathrm{,\text{\hspace{0.17em}}}{A}_{4}\mathrm{,\text{\hspace{0.17em}}}{A}_{5}\right\}$ : the actors set representing human resources allocated to a workflow.

· The workflow activities set named *AC* represents the finished product manufacture via an FMS business process.

· The set $SAC=\left\{sa{c}_{1}\mathrm{,}sa{c}_{2},\cdots \mathrm{,}sa{c}_{n}\right\}$ the sub-activities to be executed sequentially or in parallel according to a work scheduling strategy on the production multiple lines.

· Places Specification:

The set $\begin{array}{l}P=\left\{{P}_{0}\mathrm{,\text{\hspace{0.17em}}}{P}_{1}\mathrm{,\text{\hspace{0.17em}}}{P}_{2}\mathrm{,\text{\hspace{0.17em}}}{P}_{3}\mathrm{,\text{\hspace{0.17em}}}{P}_{4}\mathrm{,\text{\hspace{0.17em}}}{P}_{5}\mathrm{,\text{\hspace{0.17em}}}{P}_{6}\mathrm{,\text{\hspace{0.17em}}}{P}_{7}\mathrm{,\text{\hspace{0.17em}}}{P}_{8}\mathrm{,\text{\hspace{0.17em}}}{P}_{9}\mathrm{,\text{\hspace{0.17em}}}{P}_{10}\right\}\\ \text{\hspace{0.17em}}\text{\hspace{0.17em}}\text{\hspace{0.17em}}\text{\hspace{0.17em}}\text{\hspace{0.17em}}\text{\hspace{0.17em}}\text{\hspace{0.17em}}\cup \left\{{P}_{11}\mathrm{,\text{\hspace{0.17em}}}{P}_{12}\mathrm{,\text{\hspace{0.17em}}}{P}_{13}\mathrm{,\text{\hspace{0.17em}}}{P}_{14}\mathrm{,}{P}_{15}\mathrm{,\text{\hspace{0.17em}}}{P}_{16}\mathrm{,\text{\hspace{0.17em}}}{P}_{17}\mathrm{,\text{\hspace{0.17em}}}{P}_{18}\mathrm{,\text{\hspace{0.17em}}}{P}_{19}\mathrm{,\text{\hspace{0.17em}}}{P}_{20}\mathrm{,\text{\hspace{0.17em}}}{P}_{21}\mathrm{,\text{\hspace{0.17em}}}{P}_{22}\right\}\end{array}$ .

The model places, without taking into account the intermediate places, are explained by the Table 2.

The
$\left\{{P}_{11}\mathrm{,\text{\hspace{0.17em}}}{P}_{12}\mathrm{,\text{\hspace{0.17em}}}{P}_{13}\mathrm{,\text{\hspace{0.17em}}}{P}_{14}\mathrm{,\text{\hspace{0.17em}}}{P}_{15}\mathrm{,\text{\hspace{0.17em}}}{P}_{16}\mathrm{,\text{\hspace{0.17em}}}{P}_{17}\mathrm{,\text{\hspace{0.17em}}}{P}_{18}\mathrm{,\text{\hspace{0.17em}}}{P}_{19}\mathrm{,\text{\hspace{0.17em}}}{P}_{20}\mathrm{,\text{\hspace{0.17em}}}{P}_{21},{P}_{22}\right\}$ places set represents intermediate places set represents the intermediate places (micro-places) when we adopt the splitting approach for non-immediate transitions (like in [7] ). Such micro-places’ role is to avoid the loss of tokens during the transitions splitting as explained in [7] . In specifying the *FSM*, *P*_{1} is deemed as an initial place and *P*_{10} is a final place.

· Transitions Specification:

Like in [7] , the *WPTSPN* is liable to distinguish between the three transition types (immediate, deterministic and stochastic). Each stochastic or deterministic model transition is divided into three micro-transitions (*Tr ^{c}*,

Each model transition, whether stochastic or deterministic, is divided into

Table 2. Places specification.

three micro-transitions (*Tr ^{c}*,

· Tokens Specification:

Three different token types are adopted by our *WPTSPN*, which is an *FMS* business process representation:

- A firing sequence triggered by the presence of a *SAC*-*type* token named *sac*_{1} specifies the finished product cycle, from its primary form to its packaging. In other words, the FMS workflow represented by the WPTSPN, started by *P*_{1} is considered as begin place contains *sac*_{1}.

- To ensure the execution of the semi-automatic operations of the *FMS* workflow modeled by *WPTSPN*, we represent five types of tokens *A* having the execution agents’ role in the production section or the maintenance workflow. Place *P*_{0} is considered the workers’ park.

- An encapsulation tokens type comes from the places-entries of a non-immediate transition. This new token role guaranteed the non-loss of the tokens-entries during the division and the sequential micro-transitions firing.

4.2. *FMS* Model Represented by WPTSPN

In this subsection, with the development of the model *WPTSPN* representative

Table 3. The business process *FMS* transitions specification.

Table 4. Rates met description.

of the *FMS* business process. The specification phase is completed by this step which summarizes the previous subsection steps.

From the *FMS* workflow specified by our *WPTSPN* model representing an extension of model in [7] , we consider an abstraction with two levels:

· The first level presents the graphical *PN* representation via places, tokens randomly residence (stay), transitions, arc, tokens, and firing pre-conditions (see Figure 4(a)).

· According to a micro-level life cycle, the second level explains the micro places, micro-transitions, and their firing pre-conditions (tokens consumption phase, execution phase, and tokens production phase) (liken in [7] ).

To illustrate the micro-places and the micro-transitions, we present the abstraction-second level applied to the transition *Tr*_{6} in Figure 4(b). The Cardinality Marking Graph (Figure 5), State Graph based (Figure 6) on the timed places, Randomly residence (stay) time tokens, and tokens’ life-cycle shown earlier are helpful tools to interpret and verify the P-timed properties following a transitions firing sequence.

Figure 4. *FMS* business process represented with *WPTSPN* and *Tr*_{6} splitted into tree micro-transitions.

Figure 5. *FMS* represented by *WPTSPN* model cardinality marking graph.

4.3. FMS Model Checked Based on WPTSPN

The rules for conversion from a markings cardinalities graph *CdM* to a state graph *G*-*SE* are:

· each *CdM* is transformed into a state *e*;

· in case
$cd{M}_{i}$ comes from a
$cd{M}_{i-1}$ by firing an immediate transition of the *WPTSPN*, then a new state will not be considered and we associate a reversible arc in state
${e}_{i-1}$ .

Table 5 illustrates the correspondence between *SE* states and *cdM* markings and their generating transitions.

According to the markings cardinalities graph and the states graph associated with the *WPTSPN*, we notice:

· According to the workflow semantics of the FMS system modeled by WPTSPN, the arrival of a *sac*_{1} type token in the place considered initial. Then the state *e*_{0} and *cdM*_{0} are interpreted as the start of the *FMS* management process.

· The state *e*_{4} and *cdM*_{6} are interpreted as the end of the *FMS* workflow.

· According to the hypothesis of state stability during the firing of an immediate transition [63] , we observe that two *tr*_{3} and *tr*_{4} generate a state of temporal stability despite the change in the marking cardinality based on ordinary circulation tokens.

· The firing of the *tr*_{7} transition generates, according to the semantics of the workflow [6] , a change in the state of the sub-activity *sac*_{1} from in-execution to suspended.

· Each firing sequence comprising the two immediate transitions *tr*_{7} and *tr*_{8} generate a return to the (*cdM*_{5}, *e*_{2}), so it is a firing circuit.

· The study of markings cardinalities graph allows us to notice that it is possible to fire three transition sequences:
${s}_{1}\mathrm{\text{\hspace{0.17em}}}=\left\{t{r}_{1}\mathrm{,\text{\hspace{0.17em}}}t{r}_{2}\mathrm{,\text{\hspace{0.17em}}}t{r}_{3}\mathrm{,\text{\hspace{0.17em}}}t{r}_{4}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{7}\mathrm{,\text{\hspace{0.17em}}}t{r}_{8}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{6}\right\}$ ;
${s}_{2}=\left\{t{r}_{1}\mathrm{,\text{\hspace{0.17em}}}t{r}_{2}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{7}\mathrm{,\text{\hspace{0.17em}}}t{r}_{8}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{6}\right\}$ ;
${s}_{3}\mathrm{\text{\hspace{0.17em}}}=\left\{t{r}_{1}\mathrm{,\text{\hspace{0.17em}}}t{r}_{2}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{6}\right\}$ . The *s*_{3} firing sequence ends with a transition providing the finished product (the *sac*_{1} token instead

Table 5. Markings cardinalities, states, and generating transitions in *FMS* management process.

Figure 6. *FMS* business process represented by States Graph.

*P*_{10}), which contains no transition circuit, so its firing is assumed to be purely sequential.

The model’s properties are checked according to verification semantics based on *T*-*timed*:

· The *WPTSPN* associated with the *FMS* workflow for the firing sequence transition *s*_{3} is 9-*bounded*.

· The *WPTSPN* is not pure.

· The *WPTSPN* has no source transition.

· The transitions are *quasi*-*live* so the *WPTSPN* model is almost alive.

· Note that the *WPTSPN* has an accessibility problem when it reaches *cdM*_{6}.

· We see that *cdM*_{5} and *cdM*_{8} are equivalent to what a firing circuit shows.

· The marking cardinality *cdM*_{5} has no successor. So it’s a deadlock.

· The *WPTSPN* is *quasi*-*live*, non-conservativeness, not proper, not balanced, and not sound.

The model properties specificity verifying based on the *P*-*timed* semantics and the tokens cycle life carried following a behavioral simulation of the *FMS* business process. So, the following subsection is dedicated to simulating the tokens’ randomly timed behavior in the places at the *WPTSPN* sequence *s*_{3}.

4.4. *FMS* Model Simulation

A cardinality marking graph/state graph interpretation verifies that *cdM*_{6}/*e*_{4} is the final state of the *FMS* business process. We select the transitions in three sequences
${s}_{1}\mathrm{\text{\hspace{0.17em}}}=\left\{t{r}_{1}\mathrm{,\text{\hspace{0.17em}}}t{r}_{2}\mathrm{,\text{\hspace{0.17em}}}t{r}_{3}\mathrm{,\text{\hspace{0.17em}}}t{r}_{4}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{7}\mathrm{,\text{\hspace{0.17em}}}t{r}_{8}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{6}\right\}$ ,
${s}_{2}\mathrm{\text{\hspace{0.17em}}}=\left\{t{r}_{1}\mathrm{,\text{\hspace{0.17em}}}t{r}_{2}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{7}\mathrm{,\text{\hspace{0.17em}}}t{r}_{8}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{6}\right\}$ , and
${s}_{3}\mathrm{\text{\hspace{0.17em}}}=\left\{t{r}_{1}\mathrm{,\text{\hspace{0.17em}}}t{r}_{2}\mathrm{,\text{\hspace{0.17em}}}t{r}_{5}\mathrm{,\text{\hspace{0.17em}}}t{r}_{6}\right\}$ lead to the final state.

The *s*_{3} sequence is preferred to be simulated since it does not contain circuits. In our firing and randomly residence time analysis, we try to apply the method adopted by the *WPTSPN*.

· Let
$\left\{{e}_{0}\mathrm{,\text{\hspace{0.17em}}}{e}_{1}\mathrm{,\text{\hspace{0.17em}}}{e}_{2}\mathrm{,\text{\hspace{0.17em}}}{e}_{3}\mathrm{,\text{\hspace{0.17em}}}{e}_{4}\right\}$ : the states’ firing sequence corresponding to *s*_{3}.

· Let
$\left\{{P}_{0}\mathrm{,\text{\hspace{0.17em}}}{P}_{1}\mathrm{,\text{\hspace{0.17em}}}{P}_{2}\mathrm{,\text{\hspace{0.17em}}}{P}_{3}\mathrm{,\text{\hspace{0.17em}}}{P}_{4}\mathrm{,\text{\hspace{0.17em}}}{P}_{5}\mathrm{,\text{\hspace{0.17em}}}{P}_{6}\mathrm{,\text{\hspace{0.17em}}}{P}_{7}\mathrm{,\text{\hspace{0.17em}}}{P}_{8}\mathrm{,\text{\hspace{0.17em}}}{P}_{10}\right\}$ : the places’ subset is involved in the *s*_{3} firing sequence.

· Let *MIP*_{3}: the matrix of the places input-transitions involved in the transitions sequence *s*_{3}.

· Let *MPO*_{3}: the matrix of the places output-transitions involved in the transitions sequence s_{3}.

$MI{P}_{3}=\left(\begin{array}{cccc}0& 0& 0& 0\\ 0& 0& 0& 1\\ 0& 0& 0& 0\\ 1& 0& 0& 0\\ 0& 0& 1& 0\\ 0& 1& 0& 0\\ 0& 1& 0& 0\\ 0& 0& 1& 0\\ 0& 0& 0& 1\\ 0& 0& 0& 1\end{array}\right)$ $MP{O}_{3}=\left(\begin{array}{cccc}1& 0& 0& 0\\ 0& 0& 0& 1\\ 1& 0& 1& 0\\ 0& 1& 0& 0\\ 0& 1& 0& 0\\ 0& 0& 1& 0\\ 0& 0& 0& 0\\ 0& 0& 1& 1\\ 0& 0& 0& 1\\ 0& 0& 0& 0\end{array}\right)$

· Let *MIT*_{3}: the matrix of the transitions input-places involved in the transitions sequence *s*_{3}. Let *MTO*_{3}: the matrix of the transitions output-places involved in the transitions sequence *s*_{3}.

$MI{T}_{3}=\left(\begin{array}{cccccccccc}0& 1& 0& 0& 0& 0& 0& 0& 0& 0\\ 0& 0& 0& 1& 1& 0& 0& 0& 0& 0\\ 0& 0& 1& 0& 0& 1& 0& 0& 0& 0\\ 0& 0& 0& 0& 0& 0& 0& 1& 1& 0\end{array}\right)$

$MT{O}_{3}=\left(\begin{array}{cccccccccc}0& 0& 1& 1& 0& 0& 0& 0& 0& 0\\ 0& 0& 0& 0& 0& 1& 1& 0& 0& 0\\ 0& 0& 0& 0& 0& 0& 0& 1& 0& 0\\ 0& 0& 0& 0& 0& 0& 0& 0& 0& 1\end{array}\right)$

Thus, the simulated system evolution depends on different situations according to the densities types (Exponential, Normal, and Log-Normal). To calculate the firing time of each transition as well as the tokens’ random stay in each timed place, we target the transitions firing sequence *S*_{3}. A data collection specifying the parameters of our simulation solution must be provided as an input {*places*,* MIP*_{3}, *MPO*_{3}}, {*transitions*, *MIT*_{3}, *MTO*_{3}, *times* *at* *the* *latest*, *and* *firing* *rates*}, and the parameters related to the probability distribution type (
$\lambda \mathrm{\text{\hspace{0.17em}}}=\mathrm{\text{\hspace{0.17em}}0.6}$ ,
$\mu \mathrm{\text{\hspace{0.17em}}}=0.6$ and
$\sigma \mathrm{\text{\hspace{0.17em}}}=\mathrm{\text{\hspace{0.17em}}0.7}$ ). Table 6 illustrates our simulation transitions basic data.

After retrieving the input data, our simulation process follows the following steps:

· Step 1: The gravity center method [48] [50] which is used by the
$TFiringT\left(t{r}_{j}\right)$ (
$\forall t{r}_{j}\mathrm{\text{\hspace{0.17em}}}\in \mathrm{\text{\hspace{0.17em}}}{s}_{3}$ ) function, is used to determine the firing time for each transition in the firing sequence (*s*_{3}/*se*_{3}). This function returns three-time values, one for each density type (exponential, normal, and log-normal). The outcomes of this stage are presented in Table 7: (sorting time with the gravity center method according to the three types of distribution and their cumulative values).

We note:

- *EGFT*: Exponential Gravity Center Transition Firing Time;

- *NGFT*: Normal Gravity Center Transition Firing Time;

- *L-NGFT*: Log-Normal Gravity Center Transition Firing Time;

- *CEGFT*: Cumulative Exponential Center Transition Firing Time;

- *CNGFT*: Cumulative Normal Center Transition Firing Time;

- *CL-NGFT*: Cumulative Log-Normal Gravity Center Transition Firing Time.

· Step 2: In this simulation phase, we calculate the cumulative firing time (
$SFT=\mathrm{\text{\hspace{0.17em}}}{\displaystyle \sum}\left(TFiringT\left(t{r}_{j}\right)\right)$ ) for each transition
$t{r}_{j}$ in its firing sequence order (*s*_{3}/*se*_{3}). Also, for each transition, the three cumulative firing time values (see (Table 7)) are the basis for determining token dwell times. Then, for each timed place applied to the sequence, the lower bounds of the static stay intervals are determined from the matrix *MIP*_{3}. For each density type, the *MEFIP*_{3}, *MNFIP*_{3}, and *ML-NFIP*_{3} matrix are constructed to select each

Table 6. Simulation transitions basic input data.

Table 7. Each value of transitions gravity center firing time is expressed in minutes.

min-value row corresponding to the lower sac-token boundary at the current timed place (random residence).

$MEFI{P}_{3}=\left(\begin{array}{cccc}0& 0& 0& 0\\ 0& 0& 0& 51.80\\ 0& 0& 0& 0\\ 1.12& 0& 0& 0\\ 0& 0& 16.71& 0\\ 0& 5.02& 0& 0\\ 0& 5.02& 0& 0\\ 0& 0& 16.72& 0\\ 0& 0& 0& 51.80\\ 0& 0& 0& 51.80\end{array}\right)$

$MNFI{P}_{3}=\left(\begin{array}{cccc}0& 0& 0& 0\\ 0& 0& 0& 55.30\\ 0& 0& 0& 0\\ 0.79& 0& 0& 0\\ 0& 0& 18.17& 0\\ 0& 3.17& 0& 0\\ 0& 3.17& 0& 0\\ 0& 0& 18.17& 0\\ 0& 0& 0& 55.30\\ 0& 0& 0& 55.30\end{array}\right)$

$ML\text{-}NFI{P}_{3}=\left(\begin{array}{cccc}0& 0& 0& 0\\ 0& 0& 0& 67.47\\ 0& 0& 0& 0\\ 4.99& 0& 0& 0\\ 0& 0& 29.98& 0\\ 0& 14.98& 0& 0\\ 0& 14.98& 0& 0\\ 0& 0& 29.98& 0\\ 0& 0& 0& 67.47\\ 0& 0& 0& 67.47\end{array}\right)$

· Step 3: In this third phase, we fix a random residence interval upper limit, which is assigned to a token in each timed place occurring in the sequence s *s*_{3}/*se*_{3}. For each density type, the *MEFIT*_{3}, *MNFIT*_{3}, and *ML*-*NFIT*_{3} matrices are elaborated to select the minimum value of each column corresponding to the upper limit of the token’s stay.

$MEI{T}_{3}=\left(\begin{array}{cccccccccc}0& 1.12& 0& 0& 0& 0& 0& 0& 0& 0\\ 0& 0& 0& 5.02& 5.02& 0& 0& 0& 0& 0\\ 0& 0& 16.71& 0& 0& 16.71& 0& 0& 0& 0\\ 0& 0& 0& 0& 0& 0& 0& 51.80& 51.80& 0\end{array}\right)$

$MNI{T}_{3}=\left(\begin{array}{cccccccccc}0& 0.79& 0& 0& 0& 0& 0& 0& 0& 0\\ 0& 0& 0& 3.07& 3.17& 0& 0& 0& 0& 0\\ 0& 0& 18.17& 0& 0& 18.17& 0& 0& 0& 0\\ 0& 0& 0& 0& 0& 0& 0& 55.30& 55.30& 0\end{array}\right)$

$MNLI{T}_{3}=\left(\begin{array}{cccccccccc}0& 4.99& 0& 0& 0& 0& 0& 0& 0& 0\\ 0& 0& 0& 14.99& 14.99& 0& 0& 0& 0& 0\\ 0& 0& 29.98& 0& 0& 29.98& 0& 0& 0& 0\\ 0& 0& 0& 0& 0& 0& 0& 67.47& 67.47& 0\end{array}\right)$

After determining the randomly residence limits for each sac-token in *WPTSPN*’ timed place, we clarify that stochastically using the density functions according to the three distributions. Figure 7 represents the sac-token’ randomly residence distributions in the timed place *P*_{7}.

· The last step is summed up in determining for each place its three means of the stay time according to the gravity center method using the function $MST\left({P}_{i}\right)$ , ( $\forall {P}_{i}\in {s}_{3}$ ).

Table 8 illustrates the three randomly residence of all sac-token in the place *P*_{7}, its average residence times according to the three densities (exponential, Normal, and Log-normal), and a token *sac*_{1} cycle-life according to the time horizon.

Figure 7. Token random residence time in the place *P*_{7} according to the three densities.

Figure 8 specifies the process of determining the stay dynamic interval according to the place *P*_{7} and the decision about the token’s life-cycle, according to its time sensor value. The token *sac*_{1} arriving in the place *P*_{7} following the transition *tr*_{5} firing is equipped with an automatic time sensor. This time sensor can activate a perception operation of the Randomly residence and compare its value, triggered from the first moment in the place, with the *MST*(*P*_{7}).

The following subsection shows our delay detection and prediction process related to the randomly residence time in a firing sequence.

4.5. *FMS* Business Process Prediction Delay

The verification and simulation, allow us to detect a delay problem of the execution time relating to the operation op6 of the FMS business process, knowing that the latter is specified by the transition *tr*_{6}. So, we determine the cumulative

Table 8. Three randomly residence intervals of the token *sac*_{1} and their life cycle in the place *P*_{7}.

Figure 8. Process of determining the stay dynamic interval and the decision about the token’s life-cycle.

transition sequence firing time (*s*_{3}/*se*_{3}), after that, we check this delay indicated in the Figure 9. This figure illustrates the cumulative firing time, according to the three densities, for each transition making up the sequence. The delay detection step launches the prediction process linked to the tokens random residence in timed places. We apply the same prediction process to the micro-places, which are obtained following the division mechanism adopted by the model *WPTSPN*).

The model prediction approach requires converting the cardinality markings graph and/or the state sequence graph to *Event*-*log*: *Lev*, matching each *cdM*/*se* in Event. According to our *FMS* workflow simulation and verification results, firing sequence transitions denoted *s*_{3}/*se*_{3} create a delay risk in FMS execution. Therefore, we propose a delay prediction procedure based on the algorithmic aspect illustrated in Figure 8. Knowing that the delay causes the token death in timed places during the transitions firing sequence. So, we use a prediction process based on a density truncation with the three possible distributions. This last process is illustrated by Algorithm 1.

An illustrative example of the truncated randomly residence densities is applied to sac-token in *P*_{7} and shown in Figure 10. According to our model of transitions division approach (like in [7] ), it is possible to apply the truncating process at the second level (micro-places), as illustrated in Figure 11 and Figure 12.

Knowing that the two places (*P*_{17}, *P*_{18}) are considered as two micro-places preventing the splitting mechanism of the *tr*_{6} transition. As our model based on the no interpretation hypothesis of immediate transitions, then
$t{r}_{6}^{P}$ does not temporally generate interpretable micro-states.

So, the immediate micro-transition $T{r}_{6}^{p}$ densities’ truncation is not performed (like in [7] [48] ). The delay margin calculating the operation is based on subtraction between the time corresponding to the gravity center stay of the

Figure 9. The firing time of all transitions in *s*_{3}/*se*_{3} according to all densities adopted by the *WPTSPN* model.

Figure 10. The firing times of all transitions in *s*_{3}/*se*_{3} according to all truncated densities adopted by the *WPTSPN* model.

Figure 11. All the randomly residence densities in the micro-place *P*_{17} truncated.

Figure 12. All the randomly residence densities in the micro-place *P*_{18} truncated.

truncated density and the truncation time. After that, a statistical set is generated by observing the truncation operations on the densities. The empirical mean and empirical variance are determined for each density, with the confidence interval forming the aim around the truncation times delayed estimations. Since the statistical population number is reduced, we adopt the empirical estimate method in [7] and [75] .

Table 9 illustrates the prediction results based on our truncation process applied to *P*_{7}, *P*_{17} and *P*_{18} micro-places. Thus, we determine the delay margins for truncated density. To explore the numerical values meaning in Table 9, we note:

· *LST*: Lower Limit of Stay Interval;

· *TT*: Truncated Time or Gravity Center Stay Time;

· *EM*: Empirical Mean of Truncated Densities;

· *EMS*: Empirical Margin of Stay;

· *EL*: Empirical Likelihood;

· *CM*: Empirical Confidence Margin.

The temporal analysis of tokens’ random residence in timed places adopted by our *WPTSPN*, shows that if we use an exponential density, then the stay-delay tends towards stability. So, Figure 10 shows a uniformly distributed truncated stay density on the time horizon. According to Table 9, we notice that the stay margin distributed with the log-normal density gratitude is compared to that distributed with the normal one. Also, in the *FMS* business process evolution, the *tr*_{6} transition favors the end of production because of a maintenance sub-process. The proposed model applies the prediction tool to the micro-places which result from the transitions division mechanism. We note that the prediction process, oriented towards the P-timed context, requires retrospection on the past input transitions firing time, and a future vision (estimation) of the transitions firing time output.

Table 9. Three randomly time residence intervals in the places *P*_{7}, *P*_{17}, and *P*_{18} truncated.

5. Conclusions

In this article, we propose an extension of stochastic Petri nets [63] named *WPTSPN* and which combined with *Workflow-Nets* [6] . This extension endowedwith an orientation *P-Timed** * [30] [58] with (sojoun) residence times of the tokens determined randomly using the centers of gravity assigned to the density functions [31] . We apply their specification and verification approach in the context of the FMS Workflow [76] . In addition, the random residence time of tokens in timed places and the mechanism for triggering transitions are determined not only by the stochastic and deterministic aspects but also by other conditions adapted to the FMS context. The micro-steps are formally represented respectively by micro-places (micro-transitions [7] ) and sequentially concern the consumption, the execution of the task (sub-activity), and the production of tokens. The latter allows us to distinguish and locate, in a precisemanner, any type of execution failure. Our verification process adopted by the *WPTSPN* can bejustified by a state space based on the state graph, which represents firing sequences to control and localize shared resource conflicts.

We note that this model is enriched by formal tools based on the elapsed time to predict the remaining time and estimate the residence time (residence) of the tokens in the timed places during a firing sequence of a state. The residence time (stay) of the tokens in each model timed place, representative of an FMS, also indicates the expiration time of the primary or semi-finished material.

On the one hand, in our future work, we want to expand the expressiveness of the *WPTSPN* by incorporating the sharing of resource restrictions [76] , the interdependence between the time of activities [77] , and the performance evaluation of synchronous operations [30] [31] . This may be accomplished utilizing model transformation approaches, fluid Stochastic Petri Net models [26] , or *RecatNets* models [78] , which can be used to drive the tool to automatically change the development of the *BPMN* model into a *WPTSPN* like in [74] and [71] .

The *WPTSPN*, on the other hand, can be enriched with formal tools to cover a dynamic workflow context, ensuring the dynamic display of real-time performance and checking the dynamic workflow criteria to effectively assess the system’s strengths and weaknesses according to personalized criteria.

Conflicts of Interest

The authors declare no conflicts of interest regarding the publication of this paper.

[1] |
Alcacer, V. and Cruz-Machado, V. (2019) Scanning the Industry 4.0: A Literature Review on Technologies for Manufacturing Systems. Engineering Science and Technology, an International Journal, 22, 899-919. https://doi.org/10.1016/j.jestch.2019.01.006 |

[2] |
(2020) CGP Gestion de Production. https://www.cours-gratuit.com/cours-gestion/cours-sur-les-outils-de-la-gestion-de-production |

[3] | Courtois, A., Martin-Bonnefous, C. and Pillet, M. (2003) Gestion de production. 4 eme Edition, Editions d’Organization. |

[4] |
Ballarini, P., Barbot, B., Duflot, M., Haddad, S. and Pekergin, N. (2015) HASL: A New Approach for Performance Evaluation and Model Checking from Concepts to Experimentation. Performance Evaluation, 90, 53-77. https://doi.org/10.1016/j.peva.2015.04.003 |

[5] |
Weske, M. (2019) Business Process Management: Concepts, Languages, Architectures. Springer, Berlin. https://doi.org/10.1007/978-3-662-59432-2_1 |

[6] | Van der Aalst, W.M.P. and Van Hee, K. (2002) Workflow Management: Models, Methods, and System. The MIL Press, Cambridge. |

[7] |
Ben Mesmia, W., Escheikh, M. and Barkaoui, K. (2020) DevOps Workflow Verification and Duration Prediction Using Non-Markovian Stochastic Petri Nets. Journal of Software: Evolution and Process, 33, e2329. https://doi.org/10.1002/smr.2329 |

[8] | Sbai, Z. and Barkaoui, K. (2012) Verification Formelle des Processus Workflow Collaboratifs. Conference francophone sur les Systemes Collaboratifs, (SysCo’12), 5, 197-200. |

[9] | D’Ambrogio, A. and Zacharewicz, G. (2016) Resource-Based Modeling and Simulation of Business Processes. Proceedings of the 2016 Summer Computer Simulation Conference (SCSC 2016), Montreal, 24-27 July 2016, page. |

[10] |
(2020) CEDP Chain Event-Driven Process. https://www.wu.ac.at/erp/webtrainer/epc-webtrainer/theory |

[11] |
(2020) Object Management Group Business Process Model and Notation. https://www.omg.org/spec/BPMN/2.0 |

[12] |
(2020) BPMN 1.0 Business Process Model and Notation (BPMN)—Version 1.0 2020 URL. https://www.omg.org/spec/BPMN/1.1/PDF |

[13] |
Holzmann, G.J. (1997) The model checker SPIN. IEEE Transactions on Software Engineering, 23, 279-295. https://doi.org/10.1109/32.588521 |

[14] |
(2020) BPMN 2.0 Business Process Modeling Notation. https://www.omg.org/spec/BPMN/2.0/ |

[15] |
Kheldoun, A., Barkaoui, K. and Ioualalen, M. (2017) Formal Verification of Complex Business Processes Based on High-Level Petri Nets. Information Sciences, 385-386, 39-54. https://doi.org/10.1016/j.ins.2016.12.044 |

[16] |
Ciardo, G. (1995) Discrete-Time Markovian Stochastic Petri Nets. In: Stewart, W.J., Ed., Computations with Markov Chains, Springer, Boston, 339-358. https://doi.org/10.1007/978-1-4615-2241-6_20 |

[17] | Bocciarelli, P., D’Ambrogio, A., Giglio, A., Paglia, E. and Gianni, D. (2014) Empowering Business Process Simulation through Automated Model Transformations. 2014 Proceedings of the Symposium on Theory of Modeling and Simulation—DEVS Integrative M&S Symposium, Tampa, 13-16 April 2014, 39-45. |

[18] | Boucheneb, H. and Barkaoui, K. (2012) Parametric Verification of Time Workflow Nets. Proceeding of the 24th International Conference on Software Engineering and Knowledge Engineering SEKEC, San Francisco, 1-3 July 2012, 352-361. |

[19] | Ben Mesmia, W., Escheikh, M. and Barkaoui, K. (2019) DevOps Workow Specification Based on Non-Markovian Stochastic Petri Nets with Enhanced Expressiveness. COSI’2019, Tizi-Ouzou, 24-26 June 2019, 2-12. |

[20] | Yamaguchi, S., Yamaguchi, M. and Tanaka, M. (2008) A Soundness Verification Tool Based on the SPIN Model Checker for Acyclic Workflow Nets. The 23rd International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2008), Japan, 6-9 July 2008, 285-288. |

[21] |
Dumas, M., La Rosa, M., Mendling, J. and Reijers, H.A. (2018) Fundamentals of Business Process Management. Springer, Berlin. https://doi.org/10.1007/978-3-662-56509-4 |

[22] | Favrel, J. and Lee, K.H. (1985) Modelling, Analysing, Scheduling and Control of Flexible Manufacturing Systems. In: Falster, P. and Maxumder, R.B., Eds., Modelling Production Management Systems, Elsevier, Amsterdam, 279-288. |

[23] |
Cecil, J.A., Srihari, K. and Emerson, C.R. (1992) A Review of Petri-Net Applications in Manufacturing. The International Journal of Advanced Manufacturing Technology, 7, 168-177. https://doi.org/10.1007/BF02601620 |

[24] | Archetti, F. and Sciomachen, A. (1988) Representation, Analysis and Simulation of Manufacturing Systems by Petri-Net Based Models. In: Varaiya, P. and Kurzhanski, A.B., Eds., Discrete Event Systems: Models and Applications, Springer, Berlin, 162-178. |

[25] |
Cox, D.R. (1995) The Analysis of Non-Markovian Stochastic Processes by the Inclusion of Supplementary Variables. Mathematical Proceedings of the Cambridge Philosophical Society, 51, 433-440. https://doi.org/10.1017/S0305004100030437 |

[26] |
Trivedi, K.S. and Kulkarn, V.G. (1993) FSPNs: Fluid Stochastic Petri Nets. In: Ajmone Marsan, M., Ed., ICATPN 1993: Application and Theory of Petri Nets 1993, Springer, Berlin, 24-31. https://doi.org/10.1007/3-540-56863-8_38 |

[27] |
Ciardo, G., German, R. and Lindemann, C. (1994) A Characterization of the Stochastic Process Underlying a Stochastic Petri Net. IEEE Transactions on Software Engineering, 20, 506-515. https://doi.org/10.1109/32.297939 |

[28] | Krogh, B.H. and Srecnivas, R.S. (1987) Essenlially Decision Free Petri Nets for Real-Time Resource Allocation. Proceedings of 1987 IEEE International Conference on Robotics and Automation, Raleigh, 31 March-3 April 1987, 1005-1011. |

[29] | Colter, S.M., Woodward, A.T., fluck, A.A., Smith, R. and White, D.M. (1986) Extended Petri-Nets: The Language of Factory Automation? Proceedings of ISATA 1986: 15th International Symposium on Advances in Technology Education, Croydon, 1-20. |

[30] | Khansa, W., Aygalinc, P. and Denat, J.P. (1996) Structural Analysis of P-Time Petri Nets Computational Engineering in Systems Applications. CESA’96 IMACS Multiconference, Computational Engineering in Systems Applications, Lille, 9-12 July 1996, 127-136. |

[31] |
Calvez, S., Aygalinc, P. and Khansa, W. (1997) P-Time Petri Nets for Manufacturing Systems with Staying Times Constraints. IFAC Proceedings Volumes, 30, 1487-1492. https://doi.org/10.1016/S1474-6670(17)43571-3 |

[32] | Capkovic, F. (1995) A Petri Net-Based Approach to Synthesis of Control Systems for Discrete Event Dynamic Systems New Trends in Design of Control Systems 1994. Elsevier, 345-350. |

[33] |
DiLeva, A., Vernadat, F. and Bizier, D. (1987) Information Systems Analysis and Conceptual Database Design on Production Environments with M*. Computers in Industry, 9, 183-217. https://doi.org/10.1016/0166-3615(87)90037-6 |

[34] | Bruno, G. and Biglia, P. (1985) Performance Evaluation and Validation of Tool Handling in Flexible Manufacturing Systems Using Petri Nets. Proceedings of International Workshop on Timed Petri-Nets, Turin, July 1985, 64-71. |

[35] | Balbo, G., Chiola, G., Franceschinis, G. and Roet, G.M. (1987) Generalised Stochastic Petri Nets for the Performance Evaluation of FMS. Proceedings of IEEE International Conference on Robotics and Automation, Raleigh, 31 March-3 April 1987, 1013-1018. |

[36] | Narahari, Y. and Viswanadham, N. (1987) Performance Evaluation Using a Class of Petri-Nets with Deterministic and Exponential Firing Times. TENCON 87, 1987 IEEE Region 10 Conference: “Computers and Communications Technology toward 2000”, Seoul, 25-28 August 1987, 482-486. |

[37] |
Wadbwa, S. and Thrownc, J. (1988) Analysis of Collision Avoidance in Multirobot Cells Using Petri Nets. Robotersysteme, 4, 107-115. https://dblp.org/rec/journals/robotersysteme/WadhwaB88.bib |

[38] |
Martincz, J. and Silva, M. (1984) A Language for the Description of Concurrent System Modeled by Colored Petri Nets: Application to the Control of Flexible Manufacturing Systems. In: Chang, S.K., Ed., Languages for Automation, Springer, Boston, 369-388. https://doi.org/10.1007/978-1-4757-1388-6_18 |

[39] | Castelain, E., Corbel, D. and Gentina, J.C. (1985) Comparative Simulations of Control Processes Described by Petri-Nets. Proceedings of COMPINT 1985: Computer Aided Technologies, Quebec, 8-12 September 1985, 215-226. |

[40] |
Ammour, R., Leclercq, E., Sanlaville, E. and Lefebvre, D. (2017) Faults Prognosis Using Partially Observed Stochastic Petri Nets: An Incremental Approach. Discrete Event Dynamic Systems, 28, 247-267. https://doi.org/10.1109/WODES.2016.7497890 |

[41] |
Ajmone Marsan, M., Balbo, G. and Conte, G. (1984) A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems. ACM Transaction Computer Systems, 2, 93-122. https://doi.org/10.1145/190.191 |

[42] |
Choi, I., Song, M., Park, C. and Park, N. (2003) An XML-Based Process Definition Language for Integrated Process Management. Computers in Industry, 50, 85-102. https://doi.org/10.1016/S0166-3615(02)00139-2 |

[43] |
Lefebvre, D. (2017) Detection of Temporal Anomalies for Partially Observed Timed PNs. Mathematical Problems in Engineering, 2017, Article ID: 2821078. https://doi.org/10.1155/2017/2821078 |

[44] |
Lefebvre, D. (2017) Probability of Faults for Partially Observed Timed PNs with Temporal Constraints. 2017 IEEE 14th International Conference on Networking, Sensing and Control (ICNSC), Calabria, 16-18 May 2017, 103-108. https://doi.org/10.1109/ICNSC.2017.8000075 |

[45] |
Berthomieu, B. and Diaz, M. (1991) Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Transactions on Software Engineering, 17, 259-273. https://doi.org/10.1109/32.75415 |

[46] | Choi, H. (1993) Performance and Reliability Modeling Using Markov Regenerative Stochastic Petri Nets. Ph.D. Thesis, Graduate School of Duke University, Durham. |

[47] | Ciardo, G. and Lindemann, C. (1993) Analysis of Deterministic and Stochastic Petri Nets. Proceedings of 5th International Workshop on Petri Nets and Performance Models, Toulouse, 19-22 October 1993, 160-169. |

[48] |
Rachidi, S. (2019) Diagnostic des défauts dans les systèmes à évènements discrets soumis à des contraintes temporelles. Automatique/Robotique. Thèse de Doctorat, Normandie Université, Normandie, 26-30. https://tel.archives-ouvertes.fr/tel-02441760 |

[49] | Lefebvre, D., Rachidi, S., Leclercq, E. and Pigné, Y. (2018) Diagnosis of Structural and Temporal Faults for k Bounded Non-Markovian Stochastic Petri Nets. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 50, 3369-3381. |

[50] |
Lefebvre, D., Rachidi, S., Leclercq, E. and Pigné, Y. (2018) Temporal Fault Diagnosis for k-Bounded Non-Markovian SPN. 2018 5th International Conference on Control, Decision and Information Technologies (CoDIT), Thessaloniki, 10-13 April 2018, 271-276. https://doi.org/10.1109/CoDIT.2018.8394843 |

[51] | Dugan, J., Trivedi, K., Geist, R. and Nicola, V.F. (1984) Extended Stochastic Petri Nets: Applications and Analysis. Performance’ 84: Proceedings of the Tenth International Symposium on Computer Performance Modeling, Measurement and Evaluation, Paris, 19-21 December 1984, 507-519. |

[52] |
Ajmone Marsan, M., Balbo, G., Bobbio, A., Chiola, G., Conte, G. and Cumani, A. (1989) The Effect of Execution Policies on the Semantics and Analysis of Stochastic Petri Nets. IEEE Transactions on Software Engineering, 15, 832-846. https://doi.org/10.1109/32.29483 |

[53] |
Van Dongen, B.F., Crooy, R.A. and Van der Aalst, W.M.P. (2008) Cycle Time Prediction: When Will This Case Finally Be Finished? In: Meersman, R. and Tari, Z., Eds., On the Move to Meaningful Internet Systems: OTM 2008, Springer, Berlin, 319-336. https://doi.org/10.1007/978-3-540-88871-0_22 |

[54] |
Andreas Rogge, S. and Mathias, W. (2015) Prediction of Business Process Durations Using Non-Markovian Stochastic Petri Nets. Information Systems, 54, 1-14. https://doi.org/10.1016/j.is.2015.04.004 |

[55] |
WFMS (2020) Workflow Management System (WFMS). https://www.igi-global.com/dictionary/workflow-management-system-wfms/32777 |

[56] |
MP (2020) Processus-Management. https://www.pyx4.com/blog/3-familles-processus-management-realisation-support/ |

[57] | Petri, C.A. (1962) Kommunikation mit Automaten (Communication with Automata). Ph.D. Thesis, University of Bonn, Bonn. |

[58] |
Muratat, T. (1989) Petri Nets: Properties, Analysis and Application. Proceedings of the IEEE, 77, 541-580. https://doi.org/10.1109/5.24143 |

[59] |
Ramamoorthy, C.V. and Ho, G.S. (1980) Performance Evaluation of Asynchronous Concurrent Systems Using Petri Nets. IEEE Transactions on Software Engineering, SE-6, 440-449. https://doi.org/10.1109/TSE.1980.230492 |

[60] | Laftit, S. (1991) Graphes d’événements deterministes et stochastiques: Application aux systemes de production. Thèse de Doctorat, Université de Paris, Paris. |

[61] | David, R. and Alla, H. (1992) Du grafcet aux reseaux de Petri. Hermes Science Publications, Paris. |

[62] |
Dicesare, F., Harhalakis, G., Proth, J.M., Silva, M. and Vernadat, F.B. (1993) Practice of Petri Nets in Manufacturing. Chapman et Hall, London. https://doi.org/10.1007/978-94-011-6955-4 |

[63] |
Balbo, G. (2000) Introduction to Stochastic Petri Nets. In: Brinksma, E., Hermanns, H. and Katoen, J.P., Eds., EEF School 2000: Lectures on Formal Methods and PerformanceAnalysis, Springer, Berlin, 84-155. https://doi.org/10.1007/3-540-44667-2_3 |

[64] |
Ballarini, P., Gallet, E., Le Gall, P. and Manceny, M. (2019) Formal Analysis of the Wnt/β-Catenin through Statistical Model Checking. In: Margaria, T. and Steffen, B., Eds., ISoLA 2014: Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, Springer, Berlin, 193-207. https://doi.org/10.1007/978-3-662-45231-8_14 |

[65] | Thé Workflow Management Coalition Spécification (1999) Workflow Management Coalition Terminology and Glossary. Technical Report WFMC-TC-1011, Workflow Management Coalition, Brussels. |

[66] |
TimeNet (2020). https://timenet.tu-ilmenau.de/ |

[67] |
Ballarini, P., Djafri, H., Duflot, M., Haddad, S. and Pekergin, N. (2011) Petri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems. 2011 IEEE International Conference on Automation Science and Engineering, Trieste, 24-27 August 2011, 588-593. https://doi.org/10.1109/CASE.2011.6042488 |

[68] |
Narahari, Y. and Viswanadham, N. (1994) Transient Analysis of Manufacturing Systems Performance. IEEE Transactions on Robotics and Automation, 10, 230-244. https://doi.org/10.1109/70.282547 |

[69] | Buzacoott, J.A. and Shantikumar, J.G. (1993) Stochastic Models of Manufacturing Systems. Prentice-Hall, New Jersey. |

[70] |
Bizagi Modeler (2020) http://www.bizagi.com/en/products/bpm-suite/modeler/ |

[71] |
Mutarraf, U., Barkaoui, K., Li, Z.W., Wu, N. and Qu, T. (2018) Transformation of Business Process Model and Notation Models Onto Petri Nets and Their Analysis. Advances in Mechanical Engineering, 10, 168781401880817. https://hal.science/hal-02475788 |

[72] | van der Aalst, W.M.P. (1996) Three Good Reasons for Using a Petri-Net-Based Workflow Management System. In: Wakayama, T., Kannapan, S., Khoong, C.M., Navathe, S. and Yates, J., Eds., Information and Process Integration in Enterprises, Springer, Boston, 161-182. |

[73] |
van der Aalst, W.M.P. (1997) Verification of Workflow Nets. In: Azéma, P. and Balbo, G., Eds., ICATPN 1997: Application and Theory of Petri Nets 1997, Springer, Berlin, 407-426. https://doi.org/10.1007/3-540-63139-9_48 |

[74] |
Meghzili, S., Chaoui, A., Strecker, M. and Kerkouche, E. (2016) Transformation and Validation of BPMN Models to Petri Nets Models Using GROOVE. 2016 International Conference on Advanced Aspects of Software Engineering (ICAASE), Constantine, 29-30 October 2016, 22-29. https://ieeexplore.ieee.org/abstract/document/7843859/authors |

[75] |
(2020) Statistique: Estimation. https://www.math.u-bordeaux.fr/~mchabano/Agreg/ProbaAgreg1213-COURS2-Stat1.pdf |

[76] |
Barkaoui, K. and Petrucci, L. (1998) Structural Analysis of Workflow Nets with Shared Resources. In: van der Aalst, W.M.P., De Michelis, G. and Ellis, C.A., Eds., Workflow Management: Net-Based Concepts, Models, Techniques, and Tools (WFM’98): Proceedings of the Workshop, June 22, 1998, Lisbon, Portugal: WFM’98, Proceedings of the Workshop on Workflow Management. https://api.semanticscholar.org/CorpusID:60056523 |

[77] |
Barkaoui, K., Boucheneb, H. and Hicheur, A. (2009) Modelling and Analysis of Time-Constrained Flexible Workflows with Time Recursive ECATNets. In: Bruni, R. and Wolf, K., Eds., WS-FM 2008: Web Services and Formal Methods, Springer, Berlin, 19-36. https://doi.org/10.1007/978-3-642-01364-5_2 |

[78] |
Barkaoui, K. and Hicheur, A. (2012) Towards Analysis of Flexible and Collaborative Workflow Using Recursive ECATNets. In: ter Hofstede, A., Benatallah, B. and Paik, H.Y., Eds., BPM 2007: Business Process Management Workshops, Springer, Berlin, 232-244. https://doi.org/10.1007/978-3-540-78238-4_24 |

Journals Menu

Contact us

+1 323-425-8868 | |

customer@scirp.org | |

+86 18163351462(WhatsApp) | |

1655362766 | |

Paper Publishing WeChat |

Copyright © 2024 by authors and Scientific Research Publishing Inc.

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.