Keywords: Verification, Modal specification, Workflow net/Petri net, Constraint solving, Reduction

1.1/ Context and Motivations

Our ability to attain fitness goals through complexly organized, situationally-tailored, instrumental sequences of behaviours is one of the defining trait of our human nature [START_REF] Devore | The reconstruction of hominid behavioral evolution through strategic modeling[END_REF]. Human progress is essentially based on the improvement of the processes designed to attain fitness goals (e.g., survive, reproduce). In modern times, the organisation of such processes into logically coherent systems, called rationalization, has led to major improvements. For example, the rationalization of manufacturing processes has promoted the industrial revolution, an important and beneficial mark of progress [START_REF] Ashton | The industrial revolution 1760-1830[END_REF]. In a broader context, the rationalization of goal-oriented processes gave raise to the notion of workflows.

Intuitively, a workflow describes the set of possible runs of a particular process by specifying the series of activities that are necessary to complete it. More precisely, the Workflow Management Coalition [START_REF] Coalition | Terminology & glossary[END_REF], a global organization of adopters, developers, consultants, analysts, as well as university and research groups engaged in workflow-based development, defined workflow as: The automation of a process, in whole or part, during which documents, information or tasks are passed from one participant (i.e. a person or an automated process) to another for action (i.e. activities), according to a set of procedural rules.

Nowadays workflows are extensively used by companies and organisations in order to improve organizational efficiency, responsiveness and profitability by managing the tasks and steps of business processes [Schäl, 1996, Lawrence, 1997, Fischer, 2003, Van Der Aalst et al., 2004].

To effectively use and manage workflows, companies rely more and more on workflow management systems which provide an infrastructure for the set-up, execution and monitoring of a defined sequence of tasks, arranged as a workflow. A great diversity of application domains exist today that use workflow management systems on a daily basis in order to control their business processes. These include office automation, healthcare, telecommunications, manufacturing and production, finance and banking, just to name a few.

Workflows modelling is one of the most important steps in managing workflows. It aims at mapping out the different activities involved in processes so that they can be understood, evaluated, and improved. On the one hand, well designed workflows allow business processes to become more efficient, compliant, agile and visible by ensuring that every process step is explicitly defined and optimized for maximum productivity. On the other hand, faulty workflows often result in financial losses as well as in failure to provide services.

With the increasing use of workflows for modelling crucial business processes, the verification of specifications, i.e. of desired properties of workflows, becomes mandatory to ensure that such processes are properly designed and reach the expected level of trust and quality. For this reason, in the last two decades, companies have been putting more stress on the analysis of their business processes in order to maintain a competitive level while complying with a high quality of services.

Workflow analysis can be carried out by informal approaches such as workshops in which the interested stakeholders can discuss and point to possible issues in the defined workflows. However, the growing complexity of the modelled processes requires new advanced methods and dedicated analysis tools to achieve automation, reliability as well as scalability of the workflow analysis and verification steps.

Many workflow modelling languages have been proposed to model workflows (e.g., UML activity diagrams [START_REF] Dumas | Uml activity diagrams as a workflow specification language[END_REF], BPMN [White, 2004], Event-driven Process Chains [START_REF] Scheer | Process modeling using event-driven process chains[END_REF]). Among them, workflow nets [van der Aalst, 1998], a particular class of Petri nets [Petri, 1962], have become one of the standard ways to model and analyse workflows.

A workflow net is typically used as an abstraction of a workflow, notably modelling its controlflow dimension. The success of modelling workflows as Petri nets can be explained by several reasons. First, Petri nets are a graphical language, as a result they are intuitive and easy to learn. Second, Petri nets are very expressive: they allow the modelling of complex workflows exhibiting concurrencies, conflicts, as well as causal dependencies of activities (i.e tasks). Finally and most importantly, Petri nets have a clear and precise formal definition of their semantics. This enables their validation and verification within the framework of formal methods [START_REF] Clarke | Formal methods: State of the art and future directions[END_REF], a set of mathematically based languages, techniques, and tools for specifying and verifying such systems.

While most workflow nets verification problems are known decidable [Esparza, 1998], their complexity is often very high due to the large expressiveness provided by Petri nets. For instance, the reachability problem (i.e. the problem of determining whether a given state is reachable), a central problem to which many others reduce to, is known to be decidable. However, it requires exponential space and therefore exponential time [Lipton, 1976].

To assist engineers in their specification and validation activities, modal specifications [Larsen, 1989] have been designed to allow loose specifications with restrictions on transitions of complex systems. Those specifications are notably used within refinement approaches for workflows development, a top-down design approach to workflows modelling which consists in iteratively (i.e. step by step) refining a model by adding further details until a sufficient level of description is obtained. More precisely, in the context of workflow specification, modal specifications allow the definition of necessary or admissible behaviours to which the considered workflow model must conform. Modal specifications are usually expressed over a single transition of the considered system. As pointed out to us by workflow modellers of the study cases considered in this thesis, this is quite limiting. The issue is that, in real-life, the expression of complex modal behaviours involving several transitions and their causalities is needed. This thesis addresses this issue and presents extended modal specifications -a modal logic expressing complex modal behaviour involving several transitions and dealing with their causalities.

The verification of behavioural properties, such as modal specifications, are usually performed through model checking [START_REF] Clarke | Model checking[END_REF]. Model checking is a verification technique that explores all possible system states in a brute-force manner. It aims at verifying the validity of a desired behavioural property (the specification) via an exhaustive -explicit or symbolic -enumeration of all the reachable states and transitions between them. The complexity of such an approach can be worse than primitive recursive space due to the state explosion problem [Valmari, 1998]. This renders model checking and other techniques based on state space exploration intractable on large instances of workflow nets.

On the one hand, verifying behavioural properties of workflows is a very complex task which requires exponential computational resources with respect to the size of their modelling by workflow nets. On the other hand, the size of companies workflows is growing at a very fast pace as companies become larger, more complex, and rely more and more on workflow management systems to deal with an evermore precise and detailed range of business processes.

The main challenge faced during the development of verification approaches is therefore this inerrant complexity with respect to the size of the considered workflow nets. Indeed, complete and efficient verification tools for the general case are currently out of reach. However, to cope with this issue, different approaches have been considered. A first one consists in considering less expressive subclasses of workflow nets for which efficient verification procedures can be designed [Van der Aalst, 1997]. This method has been thoroughly investigated [van der [START_REF] Van Der | Soundness of workflow nets: classification, decidability, and analysis[END_REF] and is based on compromises between expressiveness of the workflow models and the complexity of their analysis. While large subclasses of workflow nets with manageable analysis complexity have been identified (e.g., free-choice workflow nets), this approach strongly limits the range of workflow behaviour that can be modelled. A second approach consists in designing verification heuristics. Such procedures (e.g., [START_REF] Vanhatalo | Faster and more focused control-flow analysis for business process models through sese decomposition[END_REF], Wimmel et al., 2011]) aim to efficiently handle a large range of usual workflow nets by guiding the explicit or implicit state space exploration. These procedures, which are not necessary complete, have shown their efficiency in operational contexts [START_REF] Vanhatalo | Faster and more focused control-flow analysis for business process models through sese decomposition[END_REF], Wimmel et al., 2011, Esparza et al., 2014, Esparza et al., 2015]. They are often based on the design of abstract models approximating the considered workflow net behaviour. The construction of such abstract models relies primarily on powerful abstraction mechanisms. This thesis addresses the verification of extended modal specifications in line with this second approach.

Recent advances in the development of constraint solving tools offer an unprecedented opportunity for the efficient automation of analysis tasks [START_REF] Prasad | A survey of recent advances in sat-based formal verification[END_REF], Rybalchenko, 2010]. Existing constraint solvers present a real opportunity to leverage these advances for solving hard program analysis problems [START_REF] Gulwani | Program analysis as constraint solving[END_REF] such as the problems faced during workflow nets analysis. Constraint-based algorithms are composed of two main steps. In a first step, the validity of a property of interest is formulated as a constraint system (i.e. a set of constraints over a set of variables ranging over their domains) through an automated process, called constraint generation. In a second step, this constraint system is solved to determine the validity of the considered property. This second step is executed using a third party constraint solver. Such a separation of concerns -constraint generation versus constraint solving -can liberate the designer of the verification tool from the tedious task of creating a dedicated algorithm by beneficing from the maturity and efficiency of existing constraint solvers.

On the basis of the above, this thesis presents contributions made to the verification of modal specifications of workflow nets based on powerful abstractions and the use of constraint solving.

The research questions we will address are summarized in the next section.

1.2/ Research Questions

As previously introduced, this work is motivated by the challenges raised during the analysis of workflow described by workflow nets. More precisely, it considers the following research questions:

RQ 1 How to effectively express modal behaviour of workflow nets involving several transitions and their causalities?

In the context of workflow nets, modal specifications are usually expressed over a single transition of the system under analysis. This is quite limiting as the expression of complex modal behaviour involving several transitions and their causalities is needed in real-life.

RQ 2 How to effectively verify the validity of such modal specifications by leveraging the efficiency of existing mature constraint solvers?

The design of a constraint system based framework enabling the verification of modal specifications, which express complex modal behaviours involving several transitions and their causalities, will benefit from the use of existing mature and efficient constraint solvers.

RQ 3 Which abstraction mechanisms are appropriate and relevant with respect to verification of such modal specifications?

As stated in the previous section, the verification of modal specifications is a hard verification problem. Due to its inerrant complexity with respect to the size of the considered workflow nets, powerful abstractions preserving the validity of modal specifications are needed to efficiently handle a large range of usual workflow nets.

1.3/ Contributions to this Thesis

This section briefly describes the contributions made to this thesis in order to address the research questions introduced in the previous section.

To address RQ 1 , we first define a modal logic, over workflow nets, enabling the description of modal behaviour involving several activities and their causalities [START_REF] Bride | Constraint solving for verifying modal specifications of workflow nets with data[END_REF]. This modal logic stems from the observation that while basic modal specifications are useful, they usually lack expressiveness for real-life applications, as only individual transitions are concerned with. This modal logic is then further extended to handle workflow nets extensions (e.g., workflow nets with data). To this end, additional constraints on the initial and final states as well as on the data associated to transition firing are considered [START_REF] Bride | Constraint solving for verifying modal specifications of workflow nets with data[END_REF].

In a second step, to address RQ 2 , we describe a novel constraint-based framework for modelling workflow nets executions. In this framework, several over-approximations of the correct executions of workflow nets are defined as constraint systems. We also define a constraint system whose solution space under-approximates the set of correct executions of workflow nets. Solutions of this latter constraint system are called segments. They model partial executions whose existence is guaranteed through structural analysis. Furthermore, we show that the concatenation of such segments can be used to model any correct executions of workflow nets. This constraint-based framework is used to verify the validity of modal specifications expressed within the previously defined modal logic by leveraging the efficiency of mature constraint solvers. These results have been published in [START_REF] Bride | Verifying modal workflow specifications using constraint solving[END_REF]. We then proceed to explicitly describe how our modal specification description and verification methodology can be applied to a more abstract notion of workflow nets that we define. This abstract notion of workflow nets notably includes workflow nets with data on which the proposed approach can be carried out as published in [START_REF] Bride | Constraint solving for verifying modal specifications of workflow nets with data[END_REF].

In a third step, to address RQ 3 , we portray reduction methods based on powerful abstraction mechanisms in order to reduce the size of analysed workflow nets while preserving the behavioural properties of interest. To this end, we present workflows nets reduction rules strongly preserving generalised soundness, an essential and necessary correctness property that must be satisfied by workflow nets. The presented reduction rules extend existing reduction rules and therefore enable a greater reduction of workflow nets. We show how they are used as powerful pre-processing steps to the verification of generalised soundness as well as to the verification of modal specifications.

Finally, as a practical contribution to RQ 2 and RQ 3 , these approaches have been implemented and experimentations have been carried out in order to validate them. We introduce and discuss convincing experimentations carried out over real-life industrial study cases in order to illustrate the relevance and effectiveness of the proposed modal specification verification approach. Furthermore, we present an empirical evaluation of effectiveness, efficiently and scalability of the proposed modal specification verification approach over workflow nets of growing size and complexity. This experimental work has been published in [Bride et al., 2016a[START_REF]Workflow nets verification: SMT or CLP?[END_REF]. Finally, we also describe experimental results supporting the benefits provided by the presented reduction methods to the verification of workflow net behavioural properties such as generalised soundness and correctness with respect to modal specifications.

1.4/ Outline

This thesis dissertation is organised according to the following outline.

In Chapter 2, we provide a review of some mathematical notions and notations used throughout this thesis. We also review some elements of the state of the art regarding Petri nets, workflow nets and existing approaches for their analysis as well as constraint systems together with approaches for their resolution.

In Chapter 3, we define extended modal specifications, a modal logic which extends usual modal specifications by enabling the description of necessary or admissible behaviour involving several activities and their causalities. We then, in a first step, define an innovative constraint system based framework to model executions of workflow nets. This framework is then used to verify extended modal specifications. In a second step, we define abstract workflow nets, an abstract notion of workflow nets which notably provides a generalisation of Petri nets, and of coloured Petri nets.

The previously defined framework based on constraint systems is then applied to such an abstract notion of workflow nets to provide an extended modal specification verification method to analyse not only ordinary workflow nets but also coloured workflow nets and similar extensions.

In Chapter 4, powerful reduction methods preserving properties of interest such as generalised soundness and correctness of a given extended modal specification are presented. We then portray pre-processing steps based on these reduction techniques reducing workflow nets size, so that the analysis of preserved properties can be carried out on smaller instances.

In Chapter 5, we present dedicated tools implementing the approaches defined in Chapters 3 and 4, and we detail and discuss experimental results obtained over real-life industrial study cases and benchmarks in order to assess their value.

Chapters 6 and 7 respectively draw general conclusions and gives directions for future work.

Intuitively, a set is a collection of distinct objects. Throughout this manuscript, standard notation for sets and operations are used.

The empty set is denoted by ∅, element inclusion (i.e. element membership) by ∈, set intersection by ∩, set union by ∪, set difference by \, set inclusion by ⊆, and strict set inclusion by ⊂. We denote the set of natural numbers by N, and the set of integers by Z.

The number of elements in a finite set A is called the cardinality, and is denoted by |A|.

The Cartesian product allows a new set to be created from existing sets.

Definition 1: Cartesian Product

The Cartesian product of two sets A and B, denoted A × B, is the set of ordered pairs

{(a, b) | a ∈ A, b ∈ B}.
Correspondences between two sets are defined by binary relations.

A binary relation

f ⊆ A × B is called a partial function, denoted f : A B if ∀ (a 1 , b 1 ), (a 2 , b 2 ) ∈ f, a 1 = a 2 ⇒ b 1 = b 2 . The notation f (a) = b signifies that (a, b) ∈ f . A partial function f : A B is called a function, denoted by f : A → B, if Dom(A) = A.
An enumerated collection of objects in which repetitions are allowed is called a sequence.

Definition 3: Sequence

A sequence S is an enumerated collection of objects from a set A in which repetitions are allowed. It is defined as a function f S : D → A where D ⊆ N \ {0}. By convention, for i ∈ D, the i th element of S is denoted S i = f S (i).

A binary operation over a set A is a function : A × A → A that combines two elements of A (called operands) to produce another element of A. By convention, let a 1 , a 2 ∈ A, we denote (a 1 , a 2 ) by a 1 a 2 . The binary operation is said to be an associative binary operation if and only if ∀ a 1 , a 2 , a 3 ∈ A, (a 1 a 2 ) a 3 = a 1 (a 2 a 3 ) and is said to be a commutative binary operation if and only if ∀ a 1 , a 2 ∈ A, a 1 a 2 = a 2 a 1 .

A monoid is a set that has an identity element together with an associative binary operation.

Definition 4: Monoid

Let A be a set and be a binary operation over A. (A, ) is a monoid if and only if:

-is an associative binary operation, and -there exists 0 A ∈ A, an identity element, such that ∀ a ∈ A, a 0 A = 0 A a = a.

A commutative monoid is a monoid whose associative binary operation is commutative.

For example, the natural numbers N form a commutative monoid under addition (identity element zero), or multiplication (identity element one).

Any commutative monoid (A, ) is endowed with its algebraic preordering ≤ A defined by ∀ a 1 , a 2 ∈ A, a 1 ≤ A a 2 ⇔ ∃ a 3 ∈ A, a 1 a 3 = a 2 .

Graph Theory

A set together with a binary relation over itself forms a directed graph.

Definition 5: Directed Graph

A directed graph G is a tuple N, A where N is a set of nodes and A ⊆ N × N is a set of directed arcs.

A directed graph whose set of nodes can be divided into two disjoint sets such that directed arcs do not relate two nodes of the same set, is called a bipartite directed graph.

Definition 6: Bipartite Directed Graph A bipartite directed graph G is a directed graph N 1 ∪ N 2 , A where N 1 ∩ N 2 = ∅ and A ⊆ N 1 × N 2 ∪ N 2 × N 1 .
A sequence of directed arcs which connect a sequence of nodes is called a path.

Definition 7: Path

Let G = N, A be a directed graph and n ∈ N. A path σ : {1, .., n} → N of length n in G is a finite sequence of nodes such that ∀ i ∈ {1, .., n -1}, (σ(i), σ(i + 1) ∈ A.

2.1.2/ Petri Nets

Petri nets, also known as place/transition nets, are a basic model of parallel and distributed systems proposed by Carl Adam Petri [Petri, 1962]. They allow modelling of discrete event systems exhibiting behaviours such as concurrency, conflict, and causal dependency between events in a readable graphical and/or a formal manner, and several important verification problems, like reachability or soundness, are known to be decidable [Esparza, 1998]. They are widely used to model concurrent processes in theoretical computer science. They are also used to describe chemical reactions, manufacturing processes, supply chains, and so on.

A Petri net is a directed bipartite graph, in which the nodes represent transitions (i.e. events that may occur, graphically depicted by bars) and places (i.e. conditions, graphically represented by circles). A transition (i.e. an event) may have any numbers of input places and output places which respectively represent the pre-condition and the post-condition of the considered transition.

Formally an ordinary Petri net is defined as follows.

Definition 8: Ordinary Petri net

An ordinary Petri net N is a tuple P, T, F where:

-P is a finite set of places, -T is a finite set of transitions (P ∩ T = ∅), -F ⊆ (P × T ) ∪ (T × P) is a finite set of arcs, also called the flow relation of N.

The nodes from which an arc runs to a node g are called the input nodes of g and are denoted by • g. Likewise, the nodes to which arcs run from a node g are called the output nodes of g and are denoted by g • . Formally, let g ∈ P ∪ T and G ⊆ P ∪ T we have:

g • = {g |(g, g ) ∈ F} G • = ∪ g∈G g • • g = {g |(g , g) ∈ F} • G = ∪ g∈G • g
A marking of a Petri net, representing the number of tokens on each place, is a function M : P → N. It evolves during its execution since transitions change the marking of a Petri net according to the following firing rules. A transition t is enabled in a marking M a if and only if ∀p ∈ • t, M a (p) ≥ 1. When an enabled transition t is fired, it consumes one token from each place of • t and produces one token for each place of t • . Formally, the firing of a transition t, enabled in a marking M a , results in a new marking M b defined as follows: The first chemical reaction, modelled by transition t 1 , is the reaction between carbon (C) and dioxygen (O 2 ) which produces carbon dioxide (CO 2 ). The second chemical reaction, modelled by transition t 2 , is the reaction between sodium hydroxide (NaOH) and carbon dioxide (CO 2 ) which produces sodium bicarbonate (NaHCO 3 ). The marking of figure 2.1(a) models a situation where one atom of carbon, one molecule of dioxygen, and one molecule of sodium hydroxide are present. In this marking the transition t 1 is enabled and firing it leads to the marking depicted by figure 2.1(b) which models a situation where one molecule of carbon dioxide and one molecule of sodium hydroxide are present, in this marking transition t 2 is enabled.

∀ p ∈ P, M b (p) =              M a (p) + 1, if p ∈ t • \ • t M a (p) -1, if p ∈ • t \ t • M a (p), otherwise (
For clarity, modelling efficiency and convenience, ordinary Petri nets can be generalised by associating weight to arcs, leading to the notion of generalised Petri nets.

Definition 9: Generalised Petri net

A generalised Petri net N is a tuple P, T, F, W where:

-P, T, F is an ordinary Petri net, and -W : F → N is a function that assigns a weight to each arc.

In the context of a generalised Petri net a transition t is enabled in a marking M a if and only if ∀p ∈ • t, M a (p) ≥ W(p, t). When an enabled transition t is fired, it consumes W(p, t) token(s) from each place p of • t and produces W(t, p) token(s) for each place p of t • . Formally, the firing of a transition t, enabled in a marking M a , results in a new marking M b defined as follows: Note that generalised Petri nets and ordinary Petri nets have the same expressive power as a generalised Petri net can always be transformed into an ordinary Petri net, however the resulting ordinary Petri net is in general more complex than the generalised one.

∀ p ∈ P, M b (p) =                    M a (p) + W(t, p) -W(p, t), if p ∈ t • ∩ • t M a (p) + W(t, p), if p ∈ t • \ • t M a (p) -W(p, t), if p ∈ • t \ t • M a (p), otherwise (
Let N = P, T, F (resp. N = P, T, F, W ) be an ordinary Petri net (resp. a generalised Petri net). The Petri net N is said to be pure (i.a. self-loop-free) if and only if ∀(x, y) ∈ (P×T )∪(T ×P), (x, y) ∈ F ⇒ (y, x) F.

Let x ∈ P ∪ T , we denote [x] the cluster of x defined as the smallest subset of P ∪ T such that

x ∈ [x], p ∈ [x] ∩ P ⇒ p • ⊆ [x] and t ∈ [x] ∩ T ⇒ t • ⊆ [x]. The set of clusters of N is denoted as C(N) = {[x] | x ∈ P ∪ T }.
Finally, it can be noted that Petri nets can also be viewed as vector addition systems [Leroux, 2011] as well as special kind of 2automata [Burroni, 1993].

2.1.2.1/ Matrix Representation of Petri nets

Ordinary as well as generalised Petri nets can be represented using their matrix form.

A matrix is a rectangular array of elements of a set. Let A be a set and n, m ∈ N, we denote by A (n,m) the set of matrices of n rows and m columns of elements of the set A. Let a ∈ A (n,m) , i ∈ {1, .., n} and j ∈ {1, .., m}, we denote by a i, j the element of a at the i th row and j th column.

Let N = P, T, F (resp. N = P, T, F, W ) be an ordinary (resp. a generalised) Petri net such that P = {p 1 , .., p |P| } and T = {t 1 , .., t |T | }.

In matrix form, a marking M of N is represented by a matrix M ∈ N (|P|,1) such that:

∀i ∈ {1, .., |P|}, M i,1 = M(p i ) A transition t is represented by a matrix t ∈ N (|T |,1) such that: ∀i ∈ {1, .., |T |}, t i,1 =        1, if t = t i 0, otherwise
The structure of N is represented by its pre-incidence matrix W -∈ N (|P|,|T |) and its post-incidence matrix W + ∈ N (|P|,|T |) such that:

∀ i ∈ {1, .., |P|}, ∀ j ∈ {1, .., |T |}, W - i, j =        1(resp. W(p i , t j )), if (p i , t j ) ∈ F 0, otherwise ∀ i ∈ {1, .., |P|}, ∀ j ∈ {1, .., |T |}, W + i, j =        1(resp. W(t j , p i )), if (t j , p i ) ∈ F 0, otherwise
In this representation, a transition t is enabled in a marking M a if and only if:

M a ≥ W - * t (2.1)
When an enabled transition t is fired in a marking M a it leads to a new marking M b such that:

M b = M a -W - * t + W + * t (2.2)
Assuming N is pure, equation 2.2 can be written as:

M b = M a + W * t (2.3)
where W = W + -W -is called the incidence matrix of N.

It follows that N can be fully described by the tuple W -, W + . Likewise, if N is pure then it can be fully described by the tuple W .

2.1.3/ Petri Nets Behavioural Properties

This section presents Petri nets behavioural properties in which we are interested.

In the context of Petri nets, one of the most important analysis problem, on which most verification problems are based, is called the reachability problem. The reachability problem is stated as follows: Given a Petri net N and M 0 an initial marking of N, can a given marking M of N be obtained from the marking M 0 after the firing of a sequence of transitions?

The conditions of a transition firing and its effects on the marking of a Petri net have been described in Section 2.1.2. Let M a and M b be two markings and t a transition of a Petri net N, we denote M a t -→ M b the fact that transition t is enabled in marking M a , and firing it results in the marking M b . The marking M b is denoted as directly reachable from M a by transition t.

Let M 1 , M 2 , .., M n be markings and σ = t 1 , t 2 , .., t n-1 a sequence of transitions of a Petri net N,

we denote M 1 σ -→ M n the fact that M 1 t 1 -→ M 2 t 2 -→ .. t n-1 ---→ M n .
The marking M n is then said to be reachable from M 1 by the sequence of transitions σ. We denote R N (M) the set of markings of N reachable from a marking M.

Definition 10: Reachability Problem

Given M a marking of a Petri net N whose initial marking is the marking M 0 , the reachability problem is the problem of deciding whether M ∈ R N (M 0 ). Many relevant behavioural properties can be expressed and evaluated through the resolution of the reachability problem, notably safety properties. It has been shown that the reachability problem for Petri nets is decidable [Kosaraju, 1982, Leroux, 2011] but requires at least exponential space (and therefore time) to be solved in the general case [Lipton, 1976].

Another behavioural property of interest is called the boundedness property. An ordinary Petri net N = P, T, F (resp. a generalised Petri net N = P, T, F, W ) together with its initial marking M 0 is said k-bounded (or simply bounded) if and only if the number of tokens in each place does not exceed a finite number k for any markings reachable from M 0 .

Definition 11: Boundedness

Let N = P, T, F (resp. N = P, T, F, W ) be an ordinary Petri net (resp. a generalised Petri net) whose initial marking is the marking

M 0 . The Petri net N is bounded if and only if ∃ k ∈ N, ∀ M ∈ R N (M 0 ), ∀ p ∈ P, M(p) ≤ k.
The last behavioural property considered is called the liveness property. With respect to the firing rule, a transition t is dead at marking M if it is not enabled in any marking M reachable from M. A transition t is live if it is not dead in any marking reachable from the initial marking. A Petri net is said live if each of these transition is live.

Definition 12: Liveness

Let N = P, T, F (resp. N = P, T, F, W ) be an ordinary Petri net (resp. a generalised Petri net) whose initial marking is the marking M 0 . The Petri net N is live if and only if

∀ t ∈ T, ∀ M ∈ R N (M 0 ), ∃ M a , M b ∈ R N (M), M a t - → M b .

2.1.4/ Petri Nets Subclasses

The need of considering classes of Petri nets sufficiently powerful with respect to their expressive capability has led to the definition of several subclasses of Petri nets. All such subclasses are defined only on the basis of structural characteristics. The four main Petri net subclasses are, in the order of growing expressiveness, defined as follow.

Definition 13: State Machine

Let N = P, T, F be an ordinary Petri net, N is a state machine (SM) if and only if:

∀t ∈ T, | • (t)| = |( • t)| = 1.
A state machine is an ordinary Petri net without concurrency, but with possible conflicts among transitions. Figures 2.3

∀p ∈ P, | • (p)| = |( • p)| = 1.
A marked graph is an ordinary Petri net without conflict, but there can be concurrency. Let N = P, T, F be an ordinary Petri net, N is a free choice net (FC) if and only if:

∀p ∈ P, (| p • |≤ 1) ∨ ( • (p • ) = {p}).
A free choice net is an ordinary Petri net where there can be both concurrency and conflict, but not at the same time.

∀p 1 , p 2 ∈ P, p • 1 ∩ p • 2 = ∅ ⇒ (p • 1 ⊆ p • 2 ) ∨ (p • 1 ⊇ p • 2 ).
An asymmetric choice net is an ordinary Petri net where there can be both concurrency and conflict, but not symmetrically. While Petri nets allow the modelling of most of real-life processes their specification ability and expressiveness can be improved. To this end, many extensions have been proposed. Some of them are completely backwards-compatible (i.e. are equivalent to Petri nets) and focus on improving the modelling capability of Petri nets while conserving the same expressiveness (e.g., Coloured Petri nets [Jensen, 1987] with finite colour's domains), whereas some others improve the expressive power of Petri nets (e.g., timed Petri nets [Ramchandani, 1974] which associate time with the firing of transitions).

The following sections present three Petri net extensions considered in this thesis: hierarchical Petri nets, coloured Petri nets and weighted transitions Petri nets.

2.1.5.1/ Hierarchical Petri Nets / Refinement

Modelling large and intricate Petri nets can be a difficult task and requires powerful structuring mechanisms [Dittrich, 1989]. Fortunately, similarly to modular programming, Petri nets can be designed using other Petri nets as building blocks [Fehling, 1991, Marechal et al., 2013, Marechal et al., 2015]. This modelling method enables modellers to substitute places and transitions by whole Petri nets (i.e. building blocks) while preserving properties of interest (e.g., liveness, boundedness).

To represent the models produced by such modelling method, hierarchical Petri net are used. Formally, a hierarchical Petri net is recursively defined as follows.

Definition 17: Hierarchical Petri Nets

The set H of hierarchical Petri nets is recursively defined as H ∈ H ⇔ H = P h , T h , F h where:

-

P h ⊆ H is a finite set of places, -T h ⊆ H is a finite set of transitions, -F h ⊆ (P h × T h ) ∪ (T h × P h ) is a set of arcs.
Hierarchical Petri nets are the support for an efficient modelling methodology called stepwise refinement [START_REF] Suzuki | A method for stepwise refinement and abstraction of petri nets[END_REF]. Through the definition of a precise semantics of hierarchical Petri nets, stepwise refinement of Petri nets is a top-down approach to Petri nets development which consists in iteratively (i.e. step by step) refining a Petri net by substituting transitions and places by whole Petri nets until a sufficient level of detail is achieved. Each step of the refinement process transforms an abstraction of the modelled process (i.e. a Petri net with several details left-out) into a more precise abstraction of the modelled process. The inverse process of refining is called abstraction.

Petri nets obtained through stepwise refinement can be viewed as Petri nets with multiple layers of detail. In this way, stepwise refinement consists in explicitly giving a hierarchical abstraction of the modelled Petri net.

Note that, in the context of stepwise refinement of Petri nets, the semantic of hierarchical Petri nets is defined with respect to the construction of underlying Petri nets. Therefore, the use of hierarchical Petri nets focuses on improving the modelling capability of Petri nets while conserving the same expressiveness.

The main advantage of such a development is the possibility to derive properties of interest by construction. By imposing a precise semantics of hierarchical Petri nets as well as conditions on the building blocks used, each successive refinement can be proved to preserve properties of interest, such as liveness and boundedness [START_REF] Suzuki | A method for stepwise refinement and abstraction of petri nets[END_REF]].

2.1.5.2/ Coloured Petri Nets

Coloured Petri nets [Jensen, 1987] are an extension of Petri nets where data are assigned to the tokens and can be modified by transitions based on their contents. For data (also called colours) of finite domains they are equivalent to Petri nets with respect to their expressiveness. However they may have more succinct representations and may be more convenient for modelling.

Let Ξ be a non-empty set of data-types (also called colours), where each data-type is a set of data-values. We denote L(V, W) the space of linear maps from V to W, and O the zero map.

Definition 18: Coloured Petri net

A coloured Petri net (CPN) is a tuple P, T, C, W where:

-P is a finite set of places, T is a finite set of transitions, such that P ∩ T = ∅, --→ M b , and the reachability relation is defined as the reflexive and transitive closure of the direct reachability.

-C : P ∪ T → Ξ is the colour-function, -W -: P × T → L(Ξ, Ξ) is the pre-incidence function, -W + : P × T → L(Ξ, Ξ)
-(p 1 , t 1 ) : C 1 → C 1 such that W -(p 1 , t 1 )([v 1 , v 2 , v 3 ]) = [v 1 , v 2 , v 3 ]. Its post- incidence function is defined as W + (t 1 , p 2 ) : C 1 → C 2 such that W + (t 1 , p 2 )([v 1 , v 2 , v 3 ]) = [v 1 , v 2 , v 3 ]
. Suppose an initial marking M a such that M a (p 1 ) = [2, 0, 1] and M a (p 2 ) = [0, 0, 0], a marking where place p 1 contains two tokens of value 1 and one token of value 3, and place p 2 contains no token. The transition instance (t, [1, 0, 1]) is enabled in M a , and firing it results in a marking M b such that M a (p 1 ) = [1, 0, 0] and M a (p 2 ) = [1, 0, 1], a marking where place p 1 contains one token of value 1, and place p 2 contains one token of value 2 and one token of value 6.

Note that coloured Petri nets with finite colour domains and ordinary Petri nets have the same expressiveness. Indeed coloured Petri net with finite colour domains can always be transformed into an ordinary Petri net, however the resulting ordinary Petri net is in general more complex than the coloured one.

While Petri nets capture the essential process flows, they often get very large and complex when additional information is provided to refine the basic models. However, such refined models are often required to specify desired behaviours. In this context, using coloured Petri nets allows specifiers to incorporate data into tokens of the system model, e.g., characteristics to treated cases in the context of workflows, which enables them to represent complex behaviour in a concise manner.

2.1.5.3/ Weighted Transitions Petri Nets

Weighted transitions Petri nets are an extension of Petri nets. They associate weights with transitions via a weight function. This enables performance analysis.

A weight function is defined within a framework where (C, + C ) is a commutative monoid. We denote O C the minimal element of C. Let N = P, T, F be an ordinary workflow net, a weight function of N is a total function C : T → C assigning a weight to each transition.

Let N w = N, C be the weighted transitions Petri net formed from the ordinary Petri net N by associating a weight function C with it. The weight of a transition t is then given by C(t). Let M a , M b be markings of N, and σ a transition sequence such that M a σ -→ M b , the weight associated with the execution σ is given by the execution weigh function C defined by

C(σ) = t∈T O t (σ) * C(t)
where O t (σ) is the number of occurrences of t in σ 2.1.6/ Workflow Nets Workflow nets (WF-nets) are special cases of Petri net introduced by W.M.P. van der Aalst [van der Aalst, 1998]. They are used to model the control-flow dimension of a workflow. They allow the modelling of complex workflows exhibiting concurrencies, conflicts, as well as causal dependencies of activities (i.e tasks). The different activities are modelled by transitions, while causal dependencies are modelled by places and arcs. For instance, the Petri nets depicted in Figures 2.9(a), 2.9(b) and 2.9(c) are workflow nets respectively illustrating the structure of causal dependency, conflict and concurrency of two distinct tasks. Let us notice that, in the context of workflows, as places correspond to conditions, specifiers are used to considering ordinary Petri nets [van der Aalst, 1998]. -N has two special places i and o, where • i = ∅ and o • = ∅, and -for each node n ∈ (P ∪ T ), there exists a path from i to o passing through n.

The places i and o respectively correspond to the beginning and termination of the processing of a case. Let N = P, T, F be a workflow net and k ∈ N \ {0} be a number of cases. The beginning of the processing of k cases corresponds to the initial marking M i(k) such that:

∀ p ∈ P, M i(k) (p) =        k, if p = i 0, otherwise
Analogously, the termination of the processing of k cases corresponds to the final marking M o(k) such that:

∀ p ∈ P, M o(k) (p) =        k, if p = o 0, otherwise A sequence of transitions σ is an (partial) execution of N if there exist M a , M b two markings of N such that M a σ -→ M b . A correct execution of N is an execution σ such that M i(k) σ -→ M o(k) . The behaviour of N is defined as the set Σ k of all its correct executions σ such that M i(k) σ -→ M o(k) .
Given a transition t and an execution σ, the function O t (σ) is the number of occurrences of t in σ.

Example 5: Workflow net example: On-demand order delivery

To illustrate the use cases of workflow nets, let us consider the business process associated with an on-demand order delivery company such as a Pizza delivery company. Textually this process is described as follows. The process starts when receiving a call from a client. The client then proceeds to, in any order, state his order as well as some personal information (e.g., name, address). Once a client stated his order, the order is prepared then delivered. When presented with his order, a client can present one or several promotional coupons before paying his order using either a credit card or by cash. The process finishes upon receiving payment. This process can be modelled by a workflow net as shown in Figure 2.10. Figure 2.10: On-demand order delivery workflow net

2.1.7/ Workflow Nets Equivalences

Comparing the behaviour of workflow nets is a task which relies on the definition of equivalences. Let N = P, T, F be a workflow net and k ∈ N \ {0} be a number of cases. We present two kinds of equivalences. The first kind, called strong trace equivalence, compares workflow nets with respect to all of their transitions.

The behaviour of N for the processing of k cases, denoted Σ k , is defined as the set of all its correct executions. Formally,

Σ k = {σ | M i(k) σ -→ M o(k) }
The strong trace set of N, denoted Γ(N), is defined as:

Γ(N) = ∪ k∈N\{0} Σ k
Two workflow nets are said to be strong trace equivalent if and only if their strong trace sets are equal. Formally,

Definition 20: Strong Trace Equivalence

Let N 1 = P 1 , T 1 , F 1 and N 2 = P 2 , T 2 , F 2 be two workflow nets. N 1 and N 2 are strong trace equivalent if and only if Γ(N 1 ) = Γ(N 2 ).

N, denoted M 1 , .., M n-1 , such that M a t 1 = ⇒ S M 1 t 2 = ⇒ .. t n-1 = == ⇒ M n-1 t n = ⇒ S M b .
The behaviour of N for the processing of k cases with respect to the set of transitions S , denoted Σ S k , is defined as:

Σ S k = {σ | M i(k) σ = ⇒ S M o(k)
The weak trace set of N with respect to the set of transitions S , denoted Γ S (N), is defined as:

Γ S (N) = ∪ k∈N\{0} Σ S k
Two workflow nets are said to be weak trace equivalent with respect to a set of transitions if and only if their weak trace sets with respect to this set of transitions are equal. Formally,

2.1.8/ Workflow Nets Soundness

In the context of workflow nets, a well-established correctness feature that all workflows should verify is called soundness [van der Aalst, 1998]. It states that beside structural properties given by the definition of workflow nets, a sound workflow net describes a procedure that will terminate eventually (option to complete), and that when it does there is a token in place o and all of the other places are empty (proper completion). Additionally, a sound workflow net may not contain dead transitions. This correctness criteria constitute an underlying property of workflow nets that has to be verified in order to ensure correct executions.

Definition 22: Soundness [van der Aalst, 1998[START_REF] Van Der | Soundness of workflow nets: classification, decidability, and analysis[END_REF] Let N = P, T, F be a workflow net, N is sound if and only if: 1) ) (proper completion), and

-∀M ∈ R N (M i(1) ), M o(1) ∈ R N (M) (option to complete), -∀M ∈ R N (M i(1) ), (M(o) > 0) ⇒ (M = M o(
-∀t ∈ T, ∃M, M ∈ R N (M i(1) ), M t - → M (no dead transitions).
Note that if we assume fairness -transitions that are enabled infinitely often will fire eventually -then the first requirement implies that eventually the final making is reached. As argued in [van der Aalst, 1998], the fairness assumption is reasonable in the context of workflow management. Indeed, all choices are made implicitly or explicitly by applications, humans or external actors which should not introduce infinite loops.

To apply the notion of soundness to workflow nets handling multiple cases at once, the notion of k-soundness introduced in [START_REF] Barkaoui | Workflow soundness verification based on structure theory of Petri nets[END_REF] (also known as structural soundness) extends the classical soundness to the processing of k cases and is proved to be decidable [T ¸iplea et al., 2005].

Definition 23: k-soundness [START_REF] Barkaoui | Workflow soundness verification based on structure theory of Petri nets[END_REF] Let N = P, T, F be a workflow net, and k ∈ N. N is k-sound if and only if:

-∀M ∈ R N (M i(k) ), M o(k) ∈ R N (M) -∀t ∈ T, ∃M, M ∈ R N (M i(k) ), M t - → M
Furthermore, a workflow net is said generalised sound if it is k-sound for all k ∈ N. Generalised soundness is also proved to be decidable [Van Hee et al., 2004].

Definition 24: Generalised Soundness [START_REF] Barkaoui | Workflow soundness verification based on structure theory of Petri nets[END_REF] Let N = P, T, F be a workflow net, N is generalised sound if and only if:

∀k ∈ N, N is k-sound 2.1.9/ Stepwise Refinement of Worflow Nets
In Section 2.1.5.1, we defined hierarchical Petri nets and their relation to stepwise refinement, a powerful development method which consists in iteratively substituting places and transitions of a Petri net by whole Petri nets (i.e. building blocks) while preserving properties of interest (e.g., liveness, boundedness) until the desired level of detail is achieved. Such construction is often native to workflow modelling standard. For instance, in BPMN [Allweyer, 2016], processes can contain sub-processes which are themselves processes. This allows modellers to start with a simple model of the considered process (i.e. a rough abstraction of the process) composed of abstract activities. Such activities are then iteratively detailed by the processes which model them until a sufficient level of detail is reached. Doing so enables modellers to get a general idea of the process, recognize correlations, and identify where the weak points are early, concerns that are essential to reliable and effective process modelling.

In the context of workflow nets, this leads to a simple and intuitive stepwise refinement method based on the substitution of transitions and places by whole workflow nets which preserves generalised soundness [Van Hee et al., 2003].

A composed workflow net built using this method has special transitions/places that represent several whole (composed or not) workflow nets. Such composed workflow nets can then be viewed as hierarchical Petri nets, called hierarchical workflow nets and representing workflow nets with multiple layers of detail.

Intuitively, a single task (i.e. a single transition) on a higher level can become a sequence of subtasks (i.e. a sequence of transitions) involving choices and concurrencies. Likewise, a resource (i.e. a token) meeting a condition (i.e. at some place) can require a sequence of subtasks (i.e. a sequence of transitions) involving choices and concurrencies to be executed between the moment they meet the condition and the moment they are available by other tasks.

Formally, a hierarchical workflow net is recursively defined as follow.

Definition 25: Hierarchical Workflow Nets

The set W of hierarchical workflow nets is recursively defined as W ∈ W ⇔ W = P h , T h , F h where:

-

P h ⊆ W is a finite set of places, -T h ⊆ W is a finite set of transitions, -F h ⊆ (P × T ) ∪ (T × P) is a finite set of arcs, -the Petri net P h , T h , F h is a workflow net or P h = T h = F h = ∅
The semantics of a hierarchical workflow net W is defined with respect to its underlying Petri net which assumes standard Petri nets semantics. Formally, let N 1 = P 1 , T 1 , F 1 and N 2 = P 2 , T 2 , F 2 be two workflow nets, there exist two basic refinement operations.

The first refinement operation is the place refinement of a place p ∈ P 1 with a workflow net N 2 which produces a new workflow net N = N 1 ⊗ p N 2 built by replacing the place p by the workflow net N 2 : p is removed from N 1 , the input transitions of p (i.e. Data: W = P h , T h , F h a hierarchical workflow net Result: N = P, T, F the workflow net underlying W Function underlying(W = P h , T h , F h )

N = P h , T h , F h ; forall the S = P s , T s , F s ∈ P h ∪ T h do if P s ∅ then N = N ⊗ S underlying(S ); end end return N
Algorithm 1: Construction of the workflow net underlying a hierarchical workflow net By analogy with spacial dimensions, the presented refinement operations -place refinement and transition refinement -are called vertical refinement operations. This is because, given W = P h , T h , F h a hierarchical workflow net, refinement operations, called horizontal refinement operations, can modify its flow relation (i.e. F h ) or add/remove nodes without modifying any of its nodes (i.e. the hierarchical workflow nets in the set P h ∪ T h ) and super-nodes (i.e. the hierarchical workflow nets whose set of nodes contains W). In the context of Petri nets, horizontal refinement operations are also called synthesis rules. Several synthesis rules are presented in Section 2.2.3.2 page 36, as well as in the contribution of this thesis in Section 4.1 page 68.

As previously said, a major advantage of stepwise refinement development method is its ability to preserve properties of interest. For example, the previously presented refinement operations -place refinement and transition refinement -are known to preserve generalised soundness [Van Hee et al., 2003].

Formally, let N 1 = P 1 , T 1 , F 1 and N 2 = P 2 , T 2 , F 2 be two generalised sound workflow nets, then ∀ n ∈ P 1 ∪ T 1 , N 1 ⊗ n N 2 is a generalised sound workflow net.

While hierarchical workflow nets do not add any expressiveness to workflow nets, they greatly simplify the modelling work by allowing to model small parts of the whole process described as (hierarchical) workflow nets that are then composed into a hierarchical workflow net. It also fosters the re-usability of (hierarchical) workflow nets, a key notion which allows rapid development of new hierarchical workflow nets based on a sound library of generic (hierarchical) workflow nets developed previously.

Note that, in the context of stepwise refinement using place refinements and transition refinements, the hierarchical workflow nets are explicitly given by the modellers. In a broader context, hierarchical workflow nets can be automatically and efficiently constructed from workflow nets through their decomposition [START_REF] Vanhatalo | Faster and more focused control-flow analysis for business process models through sese decomposition[END_REF], Polyvyanyy et al., 2011, Koehler et al., 2014].

2.1.10/ Modal Specification

To help engineers in their specification and validation activities, modal specifications [Larsen, 1989] have been designed to allow loose specifications of models under development. Modal specifications impose restrictions on the possible refinements by indicating whether activities are necessary or admissible. Those specifications are notably used within refinement approaches for software development. Modalities allow underspecification of certain activities which must be or may be present in later refinements. They provide a flexible tool for workflow development as decisions can be delayed to later steps of the development life cycle, when performing workflow refinements (Section 2.1.9).

In the framework of Petri nets, modal specifications allow specifiers to indicate that a transition (i.e. an activity) is necessary or just admissible. This concept provides two kinds of transitions: the must-transitions and the may-transitions [START_REF] Elhog-Benzina | Refinement and asynchronous composition of modal petri nets[END_REF]. More precisely, in the context of workflow nets, a may-transition (resp. must-transition) is a transition fired by at least one execution (resp. all the executions) of the process modelled by a workflow net.

Definition 26: Modal Workflow net

A modal workflow net M is a tuple N, T where:

-N = P, T, F is a workflow net, and -T ⊂ T is a set of must-transitions.

The set of may-transitions is the set of transitions T of N.

Formally, let M = P, T, F , T be a modal workflow net, we have:

t ∈ T ⇔ ∃ σ ∈ Σ 1 , O t (σ) > 0, and t ∈ T ⇔ ∀ σ ∈ Σ 1 , O t (σ) > 0
Example 8: Illustration of a modal specification For example, consider the on-demand order delivery workflow net described in Figure 2.10 page 22. Some activities of this workflow are necessary (e.g., Client States Order, Deliver Order) whereas some activities of this workflow are admissible (e.g., Client Presents Coupon). More precisely, an example of a modal specification of this workflow is given by the definition of the set of must-transitions containing the following transitions: Receive Client Call, Client States Order, Client States Personal Informations, Prepare Order, Deliver Order.

2.2/ Analysis of Petri Nets

Beside being a computational modelling suited to the descriptions of complex systems exhibiting causal dependencies, conflicts and concurrencies, Petri nets rely on a strong theoretical and formal background allowing modellers to draw important conclusions about the modelled systems without having to resort to the time and cost ineffective trial and error prototyping. Thereby modellers can answer questions about what the modelled system behaviour is supposed to be under specific operational conditions, what properties are inherent to the structure of the net, what to expect and what not to expect from the system during operation.

When it comes to analysing Petri nets, there exist three major approaches:

-Behavioural approach -based on the construction of reachability (coverability) graphs, -Structural approach -based on the matrix representation of Petri nets and algebraic techniques as well as on topological features, and -Reduction (abstraction) approach -based on transformations simplifying Petri nets (e.g., reducing the size of Petri nets)

On the one hand, the first approach essentially relies on the enumeration of all reachable markings. It can by applied to arbitrary Petri nets but is limited to small instances of Petri nets due the complexity arising from the state-space explosion. On the other hand, the two other approaches are not as generic but have been shown to be very powerful over specific subclasses of Petri nets or specific cases.

The following sections briefly describe these three approaches.

2.2.1/ Behavioural Approach

As previously said, the behavioural approach essentially relies on the enumeration of all markings reachable from an initial state. The result of such an enumeration is stored in a labelled graph where nodes represent markings, and each arc represents a transition firing which transforms a marking into another.

Let N = P, T, F be an ordinary Petri net, and M 0 : P → N be an initial marking of N. The reachability graph RG(N, M 0 ) of the ordinary Petri N with initial marking M 0 is a rooted, directed graph V, E, v 0 where:

-V = R N (M 0 )
is the set of nodes (i.e. each marking of N reachable from the initial marking M O is a node), v 0 = M 0 is the root node (i.e. the initial marking M O of N is the root node), and

-E = { M, t, M |M, M ∈ V, t ∈ T, M t - → M }
is the set of arcs (i.e. the firing of transitions between markings of N reachable from the initial marking M O ).

Reachability graphs aim at representing the underlying semantics of Petri nets from which analysis can be carried out on. However, such representation may be infinite whenever the considered Petri net is unbounded.

To overcome this issue, one can represent the reachability graph by mean of abstraction. A wellknown abstract reachability graph is the coverability graph [START_REF] Karp | Parallel program schemata[END_REF]. The main idea of the coverability graph is to represent infinite parts of the reachability graph where some places become unbounded in a finite number of nodes thus leading to finite over-approximation of the reachability graph.

CHAPTER 2. STATE OF THE ART

While many properties can be checked using the coverability graph (e.g., boundedness, dead transition) others may not in general be checked due to the the fact that it defines an overapproximation (e.g., reachability, liveness).

In particular, the coverability graph can be used to decide whether a workflow net is sound as well as modal specifications validity.

The reachability graphs and the coverability graphs of Petri nets (resp. workflow nets) provide the basis of a verification technique called model checking. Model checking is a verification technique that explores all possible states of a system in a brute-force manner [START_REF] Clarke | Model checking[END_REF]. It aims at verifying the validity of a desired behavioural property (the specification), usually expressed in temporal logic such as Linear Temporal Logic [START_REF] Gabbay | On the temporal analysis of fairness[END_REF] or Computation Tree Logic [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF], via an exhaustive explicit or symbolic enumeration of all of the reachable states and transitions between them. If the property is found not to hold in all system executions, a counterexample is produced, consisting of a trace of the model from a start state to an error state in which the specification is violated, providing a very helpful approach for debugging the system design. Examples of Petri nets model checkers include LoLA [Schmidt, 2000] and TINA [Berthomieu* et al., 2004].

However, a main challenge of model checking is the state explosion problem [Valmari, 1998]. Indeed, the complexity of the algorithm constructing the reachability graph as well as the coverability graph can be worse than primitive recursive space. This renders model checking intractable on large instances of Petri nets (resp. workflow nets).

2.2.2/ Structural Approach

This section presents the structural approach used to analyse Petri nets. Structural analysis techniques are mainly based on the static structure of a Petri net, and aim at deriving links between the topological structure of a Petri net and its behaviours. They mainly revolve around algebraic techniques applied to the matrix representation of Petri nets.

The following sections describe the main features linked to the structural analysis of Petri nets.

2.2.2.1/ State Equation

From the matrix representation of Petri nets (Section 2.1.2.1 page 14), one would like to give an algebraic description of how the markings of Petri nets change (evolve).

Let N = P, T, F (resp. N = P, T, F, W ) be an ordinary (resp. a generalised) Petri net such that P = {p 1 , .., p |P| } and T = {t 1 , .., t |T | }.

Assuming, without loss of generality, that N is pure, then N is fully described by its incidence matrix W.

Let M a , M b be two markings of N and t a transition of N. By definition of the firing rule we have:

M a t - → M b ⇔ M b = M a + W * t ≥ 0 (2.4)
The right hand side of the equivalence in equation 2.4 is a state equation: it relates an actual state M a , to a next state M b obtained after firing transition t.

Next, this equation is extended to consider transition sequences.

Let σ be a transition sequence of N, in matrix form, σ is represented as a matrix σ ∈ N (|T |,1) such that ∀i ∈ {1, .., |T |}, σ i,1 = O t i (σ).

Building up on equation 2.4 by using the distributivity property of the multiplication operator ( * ) we obtain the state equation:

M a σ -→ M b ⇒ M b = M a + W * σ ≥ 0 (2.5)
Similarly to the right hand side of the equivalence in equation 2.4, the right hand side of the equivalence in equation 2.5 is a state equation: it relates an actual state M a , to a next state M b obtained after firing transition sequence σ.

Equation 2.5 is called the state equation of N, also known as the fundamental equation of N.

Intuitively, the state equation considers, based on the structure of N, the transition sequences such that for each place of N the number of tokens produced added to the tokens present in the starting marking of the place is equal to the number of tokens consumed added to the tokens present in the reached marking of the place. Note that the order in which the transitions involved in the transition sequences are fired is not considered by the state equation.

It provides a necessary condition to the existence of a transition sequence σ starting from marking M a and leading to marking M b . However, it is important to note that it does not provide a sufficient condition to the existence of a transition sequence σ starting from marking M a and leading to marking M b . More precisely, a non-negative integer solution of the equation M b = M a + W * σ does not imply that a transition sequence σ such that M a σ -→ M b exists.

Solutions satisfying the state equation of N that do not correspond to valid executions of N are called spurious solutions. The existence of spurious solutions is one of the main problems in the utilization of algebraic linear techniques to analyse the behaviour of a Petri net.

Let us note that the state equation is the basis of a reachability analysis approach based on the concept of counterexample guided abstraction refinement (CEGAR) [START_REF] Clarke | Counterexample-guided abstraction refinement[END_REF]. In essence, [START_REF] Wimmel | Applying cegar to the petri net state equation[END_REF] iteratively analyses spurious solutions of the state equation and add constraints that exclude a solution found to be spurious but do not exclude any consistent solutions.

2.2.2.2/ Structural Invariants

This section describes the different structural invariants that arise from the study of the incidence matrix of Petri nets. Structural invariants are structural features independent of the initial marking of a Petri net from which behavioural properties can be inferred.

Let N = P, T, F (resp. N = P, T, F, W ) be an ordinary (resp. a generalised) Petri net such that P = {p 1 , .., p |P| } and T = {t 1 , .., t |T | }. Assuming, without loss of generality, that N is pure, then N is fully described by its incidence matrix W. There exist two main categories of invariants: T-invariants and P-invariant.

Definition 27: T-invariant

Let I ∈ Z (|T |,1) be a matrix such that I 0, I is a T-invariant of N if and only if:

W * I = 0 (2.6) A T-invariant I is called a T-semiflow if and only if: ∀i ∈ {1, .., |T |}, I i,1 ≥ 0 (2.7)
The support of a T-invariant I, noted || I||, is defined as:

|| I|| = { t i | I i,1 > 0 } (2.8)
Intuitively, a T-invariant of N indicates a possible loop in the net, i.e. a sequence of transitions which does not change the marking of N.

Theorem 1: T-invariant Property

Let M 0 be the initial marking of N, M be a marking of N and σ a transition sequence such that

M 0 σ -→ M. M = M 0 if and only if σ is a T-invariant of N.
The Petri net N is said to be covered by T-invariants if and only if, for each transition t ∈ T , there exists I, a T-invariant of N, such that t ∈ || I||. The boundedness and liveness of N can be inferred from T-invariants as follows.

Theorem 2: T-invariants Covered Petri Net Property

If N is covered by T-invariants then N is bounded and live.

Definition 28: P-invariant |P|) be a matrix such that I 0, I is a P-invariant of N if and only if:

Let I ∈ Z (1,
I * W = 0 (2.9) A P-invariant I is called a P-semiflow if and only if: ∀i ∈ {1, .., |P|}, t 1,p ≥ 0 (2.10)
The support of a P-invariant I, noted || I||, is defined as:

|| I|| = { p i | I 1,i > 0 } (2.11)
Intuitively, a P-invariant corresponds to a set of places whose weighted token count is a constant for any reachable marking.

Theorem 3: P-invariant Property

Let M 0 be the initial marking of N and M ∈ R N M 0 be a marking of N. If I is a P-invariant of N then:

I * M 0 = I * M (2.12)
This way, P-invariants are notably used to prove mutual exclusion of places.

The Petri net N is said to be covered by P-invariants if and only if, for each place p ∈ P, there exists I, a P-invariant of N, such that p ∈ || I||. The boundedness of N can be inferred from P-invariants as follows.

Theorem 4: P-invariant Covered Petri Net Property

If N is covered by P-invariants then N is bounded.

Let us note that any linear combination of P-invariants (resp. T-invariants) is a P-invariant (resp. T-invariant).

2.2.2.3/ Siphons and Traps

Siphons and traps are interesting features that can, as invariants, be used to infer behavioural properties of a Petri net.

Let N = P, T, F (resp. N = P, T, F, W ) be an ordinary (resp. a generalised) Petri net.

Definition 29: Siphon

Let N ⊆ P such that N ∅:

-N is a siphon if and only if

• N ⊆ N • .
Intuitively, a siphon is a subset of places such that every input transition of a place is an output transition of some other places.

Lemma 1: Siphon property [Murata, 1989] An unmarked siphon cannot be marked.

Definition 30: Trap

Let N ⊆ P such that N ∅:

-N is a trap if and only if

N • ⊆ • N.
Intuitively, a trap is a subset of places such that every output transition of a place is an output transition of some other places.

Lemma 2: Trap property [Murata, 1989] A marked trap cannot be unmarked.

We note that in the case of ordinary Petri nets, the presence of P-semiflows is linked with the presence of traps and siphons.

Lemma 3: P-Semiflow Siphon/Trap link property [START_REF] Li | Deadlock Resolution in Automated Manufacturing Systems: A Novel Petri Net Approach[END_REF] Let N = P, T, F be an ordinary Petri net. A function ω : P → N is a P-semiflow of N if and only if ||ω|| the support of ω (i.e. ||ω|| = {p ∈ P|ω(p) > 0}) is a trap and a siphon.

In the case of free-choice nets, there is a well-known relation between traps/siphons and liveness based on the evaluation of the so called siphon-trap property.

Definition 31: Siphon-Trap Property

Let N be a Petri net, N is said to satisfy the siphon-trap property (STP) if and only if:

-every siphon of N contains a marked trap.

Theorem 5: Free-Choice Nets liveness [Murata, 1989] Let N be a free-choice Petri net. N is live if and only if N satisfies the siphon-trap property.

In the case of arbitrary Petri nets, the Siphon-Trap property can be linked to behavioural property as follows.

Theorem 6: Siphon-Trap conclusions [Murata, 1989] Let N be a Petri net.

-If N is live then N satisfies the siphon-trap property.

-If N satisfies the siphon-trap property then N does not contain dead locks (i.e. all reachable markings enable at least one transition).

2.2.2.4/ Analysis of Workflow Nets

In this section we focus on the structural analysis techniques used to verify the soundness (resp. ksoundness, generalised soundness) property of workflow nets as presented in [Van der Aalst, 1997, Barkaoui et al., 2007, Van Hee et al., 2004].

Given a workflow net N = P, T, F , the goal is to structurally decide whether N is k-sound.

To this end, the k-closure of a workflow net N, noted N * k , is defined as follows.

Definition 32: k-closure of a Workflow Net

Let N = P, T, F be a workflow net. The k-closure of N, noted N * k is defined as a generalised Petri net P * , T * , F * , W * where:

-

P * = P, -T * = T ∪ {t * }, -F * = F ∪ {(o, t * ), (t * , i)}, -∀ f ∈ F, W * ( f ) = 1, and -W * (o, t * ) = W * (t * , i) = k.
It is proved that the k-soundness property of a workflow net can be reduced to the liveness and boundedness of the corresponding k-closure Petri net.

Theorem 7: k-soundness via k-closure [START_REF] Barkaoui | Workflow soundness verification based on structure theory of Petri nets[END_REF] A workflow net N is k-sound if and only if its k-closure Petri net N * k is live and bounded.

This allows structural analysis to be applied to the determination of the k-soundness property of a workflow net.

In the case of free-choice workflow nets, this leads to a polynomial time algorithm capable of deciding k-soundness [START_REF] Barkaoui | Workflow soundness verification based on structure theory of Petri nets[END_REF] based on the following theorem.

Theorem 8: Free-choice k-soundness [START_REF] Barkaoui | Workflow soundness verification based on structure theory of Petri nets[END_REF] Let N be a workflow net such that its k-closure Petri net N * k is a free-choice Petri net. The workflow net N is k-sound if and only if N * k is covered by P-semiflows and satisfies the siphon-trap property.

However, in the general case this analysis only defines sufficient conditions for k-soundness based on the following theorem. For some subclasses of workflow nets (e.g., free choice workflow nets), it has been shown that classical soundness, i.e. (weak) 1-soundness, implies generalised soundness [START_REF] Ping | On 1-soundness and soundness of workflow nets[END_REF].

In the context of arbitrary workflow nets, generalised soundness has been proved decidable and a decision procedure has been given in [Van Hee et al., 2004]. This procedure relies on the fact that a workflow net N is generalized sound if and only if a certain batch workflow net N can be derived from it, and N is generalized sound. The derivation is straightforward and only uses structural analysis of the net. Further, verifying the generalized soundness of N is reduced to a finite number of proper termination checks in N . We also note that in [START_REF] Van Hee | Verifying generalized soundness of workflow nets[END_REF] the procedure described in [Van Hee et al., 2004] is improved by reducing the size of needed proper termination checks.

2.2.3/ Reduction Approach

This section presents an approach based on successive application of Petri net transformation rules preserving properties of interest (e.g., liveness, boundedness).

The main idea behind this approach is to iteratively apply a set of Petri net transformation rules (called a kit), each one reducing the size of the analysed Petri net while preserving the subset of properties to be analysed until the reduced Petri net is irreducible with respect to the considered set of transformation rules (i.e. until a fixed point is reached). The obtained irreducible Petri nets can be so simple that the properties under study can be trivially checked. Otherwise, further analysis are required to conclude.

The main advantage of this method is its ability to reduce the size of Petri nets under analysis while preserving a subset of their properties (e.g., liveness, boundedness). It follows that this approach is mainly considered as a pre-processing step to standard analysis approaches such as the one presented in Sections 2.2.1 page 29 and 2.2.2 page 30 enabling them to be carried out on instances smaller than the original ones.

2.2.3.1/ Formalization

Formally, a Petri net transformation rule φ is defined as a binary relation over Petri nets. It is fully described by the conditions of application under which it can be applied to a source Petri net, and the construction algorithm that is applied to the source Petri net to form a target Petri net.

Let N, Ñ be two Petri nets and φ a transformation rule, the fact that φ is applicable to N and that applying φ to N results in Ñ, is denoted (N, Ñ) ∈ φ.

A Petri net transformation rule φ is called a Petri net reduction rule if for all (N, Ñ) ∈ φ, the number of nodes (i.e. the number of places and transitions) of Ñ is strictly smaller than the number of nodes of N. Conversely, a Petri net transformation rule φ is called a Petri net synthesis rule if for all (N, Ñ) ∈ φ, the number of nodes of Ñ is strictly greater than the number of nodes of N.

Note that refinement operations such as place refinement and transition refinement (Section 2.1.9 page 25) are synthesis rules. Likewise, reduction rules are abstraction operations.

Let ψ be a Petri net property such as liveness or boundedness, we denote N | = ψ the fact that the Petri net N satisfies ψ.

If for all Petri nets N and Ñ such that

(N, Ñ) ∈ φ, N | = ψ ⇒ Ñ | = ψ, φ is said to preserve ψ. If the reverse holds as well (i.e. Ñ | = ψ ⇒ N | = ψ), then φ is said to strongly preserve ψ.
The relation over Petri nets induced by a set of Petri net transformation rules is called a kit. Let Φ be the kit induced by n Petri net transformation rules φ 1 , .., φ n , Φ defines a binary relation over Petri nets such that (N, Ñ)

∈ Φ ⇔ ∃i ∈ {1, .., n}, (N, Ñ) ∈ φ i .
If a kit is induced by a set of Petri net reduction rules, it is called a reduction kit. Likewise, if a kit is induced by a set of Petri net synthesis rules, it is called a synthesis kit.

We say that Φ (strongly) preserves ψ if and only if ∀i ∈ {1, .., n}, φ i (strongly) preserves ψ.

Finally, Φ * denotes the transitive closure of Φ, where (N 0 , N m ) ∈ Φ * if and only if there exists a sequence (φ 1 , N 1 ), ..,

(φ m , N m ) such that ∀ i ∈ {1, .., m}, (N i-1 , N i ) ∈ φ i .

Lemma 4: Kit Property Preservation

Let ψ be a Petri net property, Φ a kit, which strongly preserves ψ, and N, Ñ be two Petri nets such that (N, Ñ) ∈ Φ * , then one has:

-

N | = ψ ⇔ Ñ | = ψ
Suppose that Φ is a reduction kit, Φ is said to be a complete reduction kit with respect to the property ψ if and only if there exists an atomic Petri net N Atomic (i.e. an irreducible Petri net) such that N Atomic | = ψ and ∀ N | = ψ, (N, N Atomic ) ∈ Φ * . Conversely, suppose that Φ is a synthesis kit, Φ is said to be a complete synthesis kit with respect to the property ψ if and only if there exists an

atomic Petri net N Atomic such that N Atomic | = ψ and ∀ N | = ψ, (N Atomic , N) ∈ Φ * .

2.2.3.2/ Well-known reduction rules

This section presents an overview of well-known reductions rules preserving boundedness and liveness, two properties closely related to the soundness of workflow nets (Section 2.2.2.4 page 34). Note that we restrict this section to rules whose conditions of applications are structurally defined and that are applicable to workflow nets.

In [Murata, 1989], six reduction rules strongly preserving boundedness and liveness are given.

From those six rules only five are applicable to workflow nets. Figure 2.15 depicts these six reduction rules: Every net fragment shown on the left can be reduced to the fragment on the right while preserving boundedness and liveness.

Note that many tools implement these reduction rules as a pre-processing step to analysis. For example, before the analysis of soundness, Woflan [START_REF] Verbeek | Woflan 2.0 a petri-net-based workflow diagnosis tool[END_REF]] -a Petri net based work- [Murata, 1989] flow diagnosis tool -can apply these five reduction rules in order to reduce the size of the analysed workflow net.

In [START_REF] Desel | Free choice Petri nets[END_REF], three reduction rules preserving boundedness and liveness are presented and proved to be complete over the subclass of free-choice Petri nets. The first rule, denoted φ A is depicted by Figure 2.16.

Figure 2.16: Reduction Rule φ A of [START_REF] Desel | Free choice Petri nets[END_REF] The second rule, denoted φ S , states that a place p can be removed from a Petri net N = W with at least two places if p is not an isolated place (i.e. • p ∪ p • ∅), and p is linearly dependent of a distinct set of places (i.e. there exists Λ ∈ N (1,|P|) such that Λ (1,p) = 0 and Λ * W = W (p, ) where W (p, ) is the row of W corresponding to place p).

The third rule, denoted φ T , states that a transition t can be removed from a Petri net N = W with at least two transitions if t is not an isolated transition (i.e. • t ∪ t • ∅), and t is linearly dependent of a distinct set of transitions (i.e. there exists Λ ∈ N (|T |,1) such that Λ (t,1) = 0 and W * Λ = W ( ,t) where W ( ,t) is the column of W corresponding to transition t).

As previously mentioned, this kit is a complete kit over the subclass of free-choice Petri Net with respect to boundedness and liveness. Thus, any bounded and live free-choice Petri nets can be reduced to an atomic Petri net defined as N Atomic = {p}, {t}, {(p, t), (t, p)} . As a result, we can use these rules on the k-closure of a free-choice workflow net to determine whether this free-choice workflow net is k-sound.

Numerous other authors have investigated reduction rules for Petri nets [Berthelot, 1987, Lee-Kwang et al., 1987], notably in the context of workflow nets [START_REF] Voorhoeve | Ad-hoc workflow: problems and solutions[END_REF], Sadiq et al., 2000, Lin et al., 2002, Lohmann et al., 2009, Hichami et al., 2014]. Furthermore, similar approaches have been applied to other languages such as EPCs [Kindler, 2004, van Dongen et al., 2005, van Dongen et al., 2007] and BPMN [START_REF] Goldman | On graph reduction for qos prediction of very large web service compositions[END_REF]. Finally let us note that reduction rules have also been applied for the analysis of Petri net extensions such as time Petri nets [START_REF] Sloan | Reduction rules for time petri nets[END_REF] and coloured workflow nets [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF].

2.3/ Constraint Systems

This section defines the notion of constraint system and provides an overview of the resolution techniques used to decide their satisfiability.

2.3.1/ Definition

Constraint systems model mathematical problems defined by a finite set of constraints (properties) over a finite set of variables with values ranging over their respective domains.

Formally, a constraint system is a tuple Ω =< X, D, C > where X is a set of variables {x 1 , . . . , x n }, D is a set of domains {d 1 , . . . , d n }, where d i is the domain associated with the variable x i , and C is a set of constraints {c 1 (X 1 ), . . . , c m (X m )}, where a constraint c j involves a subset X j of the variables of X.

An interpretation (also called a model) of a constraint system Ω is an assignment to every variable of a value from its domain. Formally, an interpretation is defined by a valuation function v assigning to each variable x i of X a value from its domain d i . An interpretation v satisfies (i.e. is consistent with respect to) a constraint c(X) of C if the projection of v on X is in c(X).

An interpretation v of a constraint system Ω is said to satisfy the constraint system Ω (i.e. v is a solution of Ω), noted Ω | = v, if and only if v is an interpretation such that all the constraints C are satisfied. A constraint system Ω is said consistent or satisfiable if and only if there exists an interpretation v satisfying (i.e. consistent with respect to) all the constraints C.

Constraint systems thus model NP-complete problems as search problems where the corresponding search space is the Cartesian product space d 1 × . . . × d n .

Determining the consistency/satisfiability of constraint systems has been the focus of a lot of research work [START_REF] Bordeaux | Propositional satisfiability and constraint programming: A comparative survey[END_REF], Biere et al., 2009, Oliveras, 2014].

In this thesis we restrict ourselves to the use of constraint systems over finite domains for which recent advances in resolution methods provide an efficient resolution regarding satisfiability.

Two approaches can be distinguished to solve this problem, namely Logic Programming and more specifically Constraint Logic Programming (CLP) over Finite Domains [Tsang, 1993] and Satisfiability Modulo Theories (SMT) over the theory of non-linear integer arithmetic [De Moura et al., 2011].

2.3.2/ Constraint Logic Programming (CSP)

Constraint satisfaction problems [Tsang, 1993] over finite domains are typically solved using a form of search. The most used techniques are based on variants of backtracking, constraint propagation, and local search.

A constraint system can be solved using generate-and-test paradigm (GT) that systematically generates each possible value assignment and then it tests whether it satisfies all the constraints. An other search paradigm, considered more efficient, is the backtracking paradigm (BT) that is the most commonly used algorithm. The backtracking paradigm is based on a recursive algorithm maintaining a partial interpretation. It proceeds as follows, first, all variables are unassigned. At each step, an unassigned variable is chosen, and all possible values are assigned to it in turn. For each value, the consistency of the partial interpretation with respect to all constraints is checked. If the partial interpretation is found consistent a recursive call is performed otherwise the algorithm backtracks to the previous variable. Whenever a complete interpretation is found consistent the algorithm can conclude that the constraint system is satisfiable.

The problem of most search algorithms based on backtracking is the occurrence of many backtracks to alternative choices, which degrades the efficiency of the system. Moreover, the efficiency of backtracking algorithms depends considerably on the order in which variables and their values are considered for instantiations. To cope with this issue various heuristics exist for dynamic or static ordering of values and variables. Further, several variants of backtracking exist. For example, backjumping [START_REF] Dechter | Backjump-based backtracking for constraint satisfaction problems[END_REF] allows saving part of the search by backtracking more than one variable in some cases. Constraint learning [START_REF] Bayardo | A complexity analysis of spacebounded learning algorithms for the constraint satisfaction problem[END_REF] infers and saves new constraints that can be later used to avoid part of the search. Look-ahead [START_REF] Frost | Look-ahead value ordering for constraint satisfaction problems[END_REF] attempts to foresee the effects of choosing a variable or a value, sometimes determining in advance whether a partial interpretation is consistent.

The late detection of inconsistency is the main disadvantage of GT and BT paradigms. Therefore constraint propagation techniques has been introduced to prune the search space. They are methods that enforce a form of local consistency, which are conditions related to the consistency of a group of variables and/or constraints turning a problem into one that is equivalent but is usually simpler to solve. The most known and used forms of local consistency are arc consistency, hyper-arc consistency, and path consistency [Kumar, 1992].

Well-known CSP solvers include Opturion CPX, OR-Tools, and SICStus Prolog [START_REF] Carlsson | SICStus Prolog user's manual[END_REF].

Let us note that a lot of work has been done [START_REF] Melzer | Checking system properties via integer programming[END_REF], Desel, 1998, Schmidt, 2001, Soliman, 2008[START_REF] Bourdeaud | Incremental integer linear programming models for Petri nets reachability problems[END_REF], Kleine et al., 2010, Wimmel et al., 2011] in order to model and to analyse the behaviour of Petri nets by using equational approaches that can be handled by constraint logic programming.

2.3.3/ Satisfiability Modulo Theories (SMT)

Constraint systems with variables over finite domains can be translated into first-order formulae over the theory of non-linear integer arithmetic so that their satisfiability can efficiently be checked using the satisfiability modulo theories approach [De Moura et al., 2011].

Satisfiability modulo theories consists of deciding the satisfiability of a first-order formula with respect to a background theory. Two main approaches are distinguished, the eager approach and the lazy approach.

The eager approach is based upon the translation of SMT instances into equisatisfiable Boolean SAT instances, so that off-the-shelf SAT solver can be used. The lazy approach, used by most SMT solvers, is based on a DPLL search with theory-specific solvers [START_REF] Nieuwenhuis | Solving sat and sat modulo theories: From an abstract davis-putnam-logemann-loveland procedure to dpll (t)[END_REF]], called T -solvers, that handle conjunctions of predicates from a given theory T . In this approach boolean reasoning is handled by a DPLL-based SAT solver which interacts with a T -solver. The Tsolver handles the theory T reasoning and check the feasibility of conjunctions of theory predicates passed on to it from the DPLL-based SAT solver as it explores the boolean search space of the formula.

Well-known SMT solvers include Z3 [De Moura et al., 2008] and CVC4 [START_REF] Barrett | Cvc4. In Computer aided verification[END_REF].

In the context of Petri net analysis a lot of approaches using SMT resolution have been investigated [START_REF] Monakova | Verifying business rules using an SMT solver for BPEL processes[END_REF], Esparza et al., 2014, Pólrola et al., 2014, Esparza et al., 2015].

In this first part, we provided a review of some mathematical notions and background notations used throughout this thesis. We also reviewed some elements of the state of the art regarding Petri nets, workflow nets and existing approaches for their analysis as well as constraint systems together with approaches for their resolution. Based on these elements, the following part introduces the contributions made to this thesis. To assist engineers in their specification and validation activities, modal specifications [Larsen, 1989] have been designed to allow loose specifications of models under development (Section 2.1.10 page 28). This chapter presents an approach to the verification of modal specifications.

The first section deals with ordinary workflow nets. It defines extended modal specifications, an extension of modal specifications that enables the description of complex modal properties expressing requirements on several transitions and on their causalities. It then describes an original modelling of workflow nets as constraint systems. The proposed modelling follows the wellknown schema of divide and conquer. The main idea is to decompose modelled executions in segments defined over conflicts-free (i.e. marked graph) subnets, allowing the structural verification of their correctness in order to guaranty that the modelled executions are correct. It concludes by applying this modelling methodology to the verification of extended modal specification of workflow nets.

The second section deals with the generalisation of the approach defined in the first section to handle abstract Petri net, a suited abstract representation notably able to model ordinary, generalised and coloured Petri nets. It begins with the formal definition of abstract workflow nets, defining the largest model representation on which the modelling of executions presented in the first section can be extended. It then generalises the concept of extended modal specifications over ordinary workflow nets to the realm of abstract workflow nets. Based on these definitions it follows by presenting the constraint system used to model executions of abstract workflow nets as the composition of 43 segments verifiable structurally. Finally it exposes how abstract extended modal specifications can be verified on the basis of the previously described executions modelling.

The constraint based modelling approach we define presents several advantages compared to explicit or symbolic state space based verification techniques described in Section 2.2.1 page 29:

-The search is quite focussed from the beginning as we traverse the solution space of the state equation rather than the underlying semantic labelled transition systems of workflow nets;

-There is in most case no need to explicitly compute the ordering of all transitions composing executions, instead only the ordering of segments composing executions is required;

-The method may perform well when verifying the conformity of workflow nets with respect to necessary and inadmissible behaviours thanks to adequate use of over-approximations;

-The computation workload is shifted to existing mature and efficient constraint solving tools (Section 2.3 page 38).

The third and final section concludes this chapter by summarising the contributions made to the verification of modal specifications.

3.1/ Over Ordinary Workflow Nets

This section aims to present a verification method that enables the verification of modal specifications over ordinary workflow nets. It first defines extended modal specifications over ordinary workflow nets, an extension of modal specifications required to express requirements on several transitions and on their causalities. It then aims at defining a generic framework based on the modelling of ordinary workflow nets executions through constraint systems (Section 2.3 page 38). Finally, it presents how this generic framework is used to verify the (in)validity of extended modal specifications over ordinary workflow nets.

3.1.1/ Extended Modal Specification

Modal specifications of workflow nets (as presented in Section 2.1.10 page 28) allow specifiers to indicate that a specific transition is necessary or just admissible.

While basic modal specifications are useful, they usually lack expressiveness for real-life applications, as only individual transitions are concerned with.

Example 9: Illustration of the limits of basic modal specifications

Consider the on-demand order delivery workflow net described in Section 2.1.6 page 21.

One would like to specify that a modal property of this workflow net is the fact that a client must pay his order either using a credit card or by cash. However, as this requirement concerns behaviour involving two distinct transitions, it cannot be expressed using basic modal specifications as presented in Section 2.1.10.

Therefore, we propose to extend modal specifications to express requirements on several transitions and on their causalities.

To this end, the language S (N) of well-formed modal specification formulae associated to a workflow net N = P, T, F is defined as follows.

Definition 33: Well-formed Modal Specification Formulae

Let N = P, T, F be a workflow net where T = {t 1 , .., t n }. The language S (N) of wellformed modal specification formulae associated to a workflow net N is defined by the following grammar of axiom A:

A → (A ∧ A) | (A ∨ A) | (¬A) | B B → t 1 | .. | t n
The domain of a well-formed modal specification formula m, denoted Domain(m), is the set of transitions appearing in the formula (i.e. the leafs of the abstract syntax tree of m).

These well-formed modal specification formulae allow specifiers to express modal properties about workflow nets correct executions.

Let σ ∈ Σ 1 be a correct execution of N and m a well-formed modal specification formula, we denote σ | = m the fact that the modal property expressed by m is satisfied by the execution σ.

Formally, given t ∈ T and

A 1 , A 2 ∈ S (N), we have σ | = t ⇔ O t (σ) > 0, σ | = (A 1 ∧ A 2 ) ⇔ σ | = A 1 ∧ σ | = A 2 , σ | = (A 1 ∨ A 2 ) ⇔ σ | = A 1 ∨ σ | = A 2 , and σ | = (¬A 1 ) ⇔ ¬(σ | = A 1 ).
Similarly to the way a transition can be characterized as a may-transition or a must-transition, any modal specification formula m ∈ S (N) can be interpreted as a may-formula or a must-formula.

On the one hand, a may-formula describes a modal property that has to be ensured by at least one correct execution of the considered workflow net. On the other hand, a must-formula describes a modal property that has to be ensured by all the correct executions of the considered workflow net.

Further, given a well-formed may-formula (resp. must-formula) m ∈ S (N), the workflow N satisfies m, written N | = may m (resp. N | = must m), when at least one (resp. all) correct execution(s) of N satisfies (resp. satisfy) the modal property expressed by m.

Formally, given m ∈ S (N):

N | = may m ⇔ ∃ σ ∈ Σ 1 , σ | = m, and
N | = must m ⇔ ∀ σ ∈ Σ 1 , σ | = m.
Note that the set of may-formulae forms a subset of Computation Tree Logic (CTL) formulae interpreted over finite traces where only the possibly operator (i.e. along at least one path) is used. Likewise the set of must-formulae forms a subset of CTL formulae where only the inevitably operator (i.e. along all paths) is used [START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF], De Giacomo et al., 2013, Westergaard, 2011].

Example 10: Illustration of an extended modal specification formula

To illustrate the use of extended modal specification formula let N be the on-demand order delivery workflow net considered in Example 9. The fact that a client must pay his order either using a credit card or by cash can be specified by the following must-formula: m = Client Pays By Cash ∨ Client Pays By Credit Card whose domain is Domain(m) = {Client Pays By Cash, Client Pays By Credit Card}. It follows that, in order to be valid with respect to this specification, N has to satisfy the must-formula m (i.e. N | = must m).

Note that, N does indeed satisfy the must-formula m.

The previous definitions of the syntax and semantic of may-formulae and must-formulae allow us to define what we call an extended modal specification as follows.

Definition 34: Extended Modal Specifications

Let N = P, T, F be a workflow net. An extended modal specification of N is a tuple a must , A may where:

a must is a must-formula, and -A may is a set of may-formulae.

Note that, in this definition, only a single must-formula is needed while a set of may-formulae is needed. This is due to the fact that given

A 1 , A 2 ∈ S (N), N | = must A 1 ∧ N | = must A 2 ⇔ N | = must (A 1 ∧ A 2 ) whereas N | = may A 1 ∧ N | = may A 2 N | = may (A 1 ∧ A 2 ).
Given a workflow net N, we say that N satisfies (i.e. is conform to) an extended modal specification a must , A may , noted N | = a must , A may , if and only if:

N | = must a must , and
∀ a may ∈ A may , N | = may a may .
We defined extended modal specifications over workflow nets, an extension of modal specifications that enables the description of complex modal properties expressing necessary or admissible behaviour involving several transitions and their causalities. The next section describes constraint systems which aim at modelling correct workflow net executions in order to enable the verification of such extended modal specifications.

3.1.2/ Modelling Executions of Workflow Nets

This section exposes the modelling of correct executions of ordinary workflow nets through their decomposition into segments verifiable structurally.

We begin by considering the well-known state equation, also known as the fundamental equation (Section 2.2.2.1 page 30). The state equation has been used earlier for verification purposes. It has been notably considered in the analysis of safety properties [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF] as well as reachability [Schmidt, 2001, Wimmel et al., 2011].

Definition 35: State Equation Constraint System

Let N = P, T, F be a workflow net and M a , M b two markings of N, the state equation constraint system S(N, M a , M b ), associated with it, is:

-∀p ∈ P, ν(p) = t∈p • ν(t) + M b (p) = t∈ • p ν(t) + M a (p)
where ν : P ∪ T → N is a valuation function.

The solutions of the constraint system of Definition 35 are related to the execution of N as stated by Theorem 10.

Theorem 10: Reachability Necessary Condition

Let N = P, T, F be a workflow net. If M a * -→ M b then there exists a valuation satisfying

S(N, M a , M b ). Proof. Suppose M a * - → M b , by definition there exists σ = t 1 , t 2 , ..., t n such that M a t 1 -→ M 1 t 2 -→ M 2 t 3 -→ .. t n-1 ---→ M n-1 t n -→ M b .
Let ν : P ∪ T → N be defined as follows:

-∀t ∈ T, ν(t) = O t (σ) -∀p ∈ P, ν(p) = j∈{1,2,...,n-1}∪{a,b} M j (p)
As the workflow N is an ordinary Petri net, the sum of the tokens in all markings of a place is equal to the sum of the occurrences of transitions producing (resp. consuming) a token at this place plus the number of token(s) in marking M b (resp. M a ).

Therefore ∀p ∈ P, j∈{1,2,...,n-1}∪{a,b} M j (p) = t∈p • O t (σ) + M b (p) = t∈ • p O t (σ) + M a (p). By definition of ν, it follows that ∀p ∈ P, ν(p) = t∈p • ν(t) + M b (p) = t∈ • p ν(t) + M a (p). Consequently, ν is a valuation satisfying S(N, M a , M b ).
More precisely, the constraint system S(N, M a , M b ) models the fact that for each place p of N, the number of token(s) entering p plus the number of token(s) in M a (p) is equal to the number of tokens leaving p plus the number of token(s) in M b (p). Let ν be a valuation function satisfying S(N, M a , M b ), ν aims at modelling a transition sequence σ such that ∀t ∈ T, O t (σ) = ν(t). However, there is no guarantee that there exists such σ corresponding to an execution of N reaching the marking M b from the marking M a . Solutions of S(N, M a , M b ) which do not correspond to an execution of N are called spurious solutions. Indeed, spurious solutions can appear because the order of transition firing is not taken into account in the modelled execution. In this workflow, the transition t 2 has to consume a token produced by t 1 in p 1 , likewise transition t 1 has to consume a token produced by t 2 in p 2 . As two transitions cannot fire simultaneously from an initial marking M i , transitions t 1 and t 2 are dead transitions. It follows that there exists no correct execution of N 1 (i.e. σ, M i σ -→ M o ). However, the following valuation

ν 1 such that ∀ n ∈ {i, p 1 , p 2 , o, t 1 , t 2 }, ν 1 (n) = 1 is a valuation satisfying S(N 1 , M i , M o )
that does not correspond to any correct execution of N 1 and is therefore a spurious solution.

Nevertheless, as stated by Theorem 10, if there is no valuation satisfying S(N, M a , M b ) then the marking M b is not reachable from marking M a . In this sense the constraint system S(N, M a , M b ) defines an over-approximation of all the executions of N reaching the marking M b from the marking M b .

In order to dismiss the spurious solutions of S, we propose to refine it. To do so, we consider the modelled executions subnets structural features.

Let ν be a solution of the constraint system S(N, M a , M b ), the subnet associated with it is an ordinary Petri net such that only the places and transitions of N involved by the valuation ν are considered. Note that we also remove the places which have a greater or equal number of tokens in the marking M a (resp. M b ) with respect to the number of tokens consumed from (resp. produced in) those places.

Definition 36: State Equation Solution Subnet

Let N = P, T, F be a workflow net, M a , M b two markings of N, ν :

P ∪ T → N a satisfying valuation of S(N, M a , M b ), U + : P → N a function such that ∀p ∈ P, U + (p) = t∈p • ν(t) and U -: P → N a function such that ∀p ∈ P, U -(p) = t∈ • p ν(t).
We define the subnet sN(ν) = sP, sT, sF as an ordinary Petri net where: By Lemma 1 page 33, we can infer that the subnet sN(ν) of a non spurious solution ν of S(N, M a , M b ) does not contain a trap nor a siphon. Indeed, as a marked trap cannot be unmarked and places marked in the final marking M b have been removed, sN(ν) cannot contain a trap. Likewise as an unmarked siphon cannot be marked and places of sN(ν) must have at least a token consumed, sN(ν) cannot contain a siphon.

-sP = {p ∈ P | ν(p) > 0 ∧ (U + (p) > M a (p) ∨ U -(p) > M b (p))} -sT = {t ∈ T | ν(t) > 0}, and -sF = {(a, b) ∈ F | a ∈ (sP ∪ sT ) ∧ b ∈ (sP ∪ sT )}
(p) = p∈G t∈p • ν(t) = p∈G t∈ • p ν(t). It implies p∈G t∈p • ∩G • ν(t) + p∈N t∈p • ∩sT G • ν(t) = p∈N t∈ • p∩G • ν(t) + p∈N t∈ • p∩sT G • ν(t) that can be simplified as p∈N t∈p • ν(t) = p∈N t∈ • p∩G • ν(t) + p∈N t∈ • p∩sT G • ν(t) because ∀p ∈ N.p • ∩ sT G • = ∅. Let G be a trap (i.e. G • ⊆ • G) such that G is not a siphon (i.e. • G G • ). Thus, one has p∈N t∈p • ν(t) = p∈N t∈ • p∩G • ν(t) implying p∈N t∈p • ν(t) = p∈N t∈p • ν(t) + p∈N t∈ • p∩sT G • ν(t). We fi- nally have ∀p ∈ N. • p ∩ sT G • = ∅ because ∀t ∈ sT.ν(t) > 0. This implies • G ⊆ G • , a contradiction. (⇐) The proof that if G is a siphon then G is a trap, is similar.
Example 14: Illustration of the property stated by Theorem 11 This property is verified by sN(ν 1 ), the valuation defined in Example 11, as the trap {p 1 , p 2 } identified in Example 13 is also a siphon.

According to Theorem 11, one can decide the presence of siphons and traps in a subnet by deciding about the presence of siphons only (or equivalently to the presence of traps only). Alternatively, one can decide the presence of siphons and traps in a subnet by deciding about the presence of P-semiflow (Lemma 3 page 33).

The presence of siphons in an ordinary Petri net can be decided by evaluating the satisfiability of the following constraint system.

Theorem 12: Siphon Presence Constraint System

Let N = P, T, F be an ordinary Petri net and B(N) the constraint system defined as follows:

-

∀p ∈ P, ∀t ∈ • p. p ∈ • t ξ(p ) ≥ ξ(p) -p∈P ξ(p) > 0
where ξ : P → {0, 1} is a valuation function. N contains a siphon if and only if there is a valuation satisfying B(N).

Proof. (⇐) Let ξ be a valuation satisfying B, and

G ⊆ P such that ξ(p) = 1 ⇔ p ∈ G. Then ∀p ∈ G, ∀t ∈ • p, p ∈ • t ξ(p ) ≥ 1, which implies • G ⊆ G • . Consequently, G is a siphon. (⇒) Suppose that G is a siphon (i.e. • G ⊆ G • ) then the valuation ξ(p) defined as ξ(p) = 1 if p ∈ G,
and 0 otherwise, satisfies B(N).

Using the constraint system S together with the constraint system B leads to the definition of the constraint system Q as follows.

Definition 37: State Equation + Absence of Siphon Constraint System Let N = P, T, F be a workflow net and M a , M b two markings of N, the constraint system Q(N, M a , M b ), associated with it, is:

-S(N, M a , M b ) | = ν -ξ such that B(sN(ν)) | = ξ where ν : P ∪ T → N is a valuation function.
While many of the spurious solutions of S(N, M a , M b ) are discarded from the solutions of Q(N, M a , M b ), the latter constraint system still defines an over-approximation of the valid execution of N leading to M b from M a . This is due to the fact that the absence of traps and siphons in the subnets of solutions of Q(N, M a , M b ) is only a necessary but not a sufficient condition to the existence of a valid execution of N leading to M b from M a .

n ∈ {i, p 2 , o, t 1 , t 2 , t 3 , t 4 , t 5 , t 6 , t 7 }, ν 2 (n) = 1 and ∀ n ∈ {p 1 , p 3 , p 4 }, ν 2 (n) = 2, is a valuation satisfying Q(N 2 , M i , M o ).
However, the transition t 2 of this workflow N 2 is a dead transition from the initial marking M i . Indeed, to be enabled, the transition t 2 requires the presence of two tokens (one in place p 1 and one in place p 4 ), but the initial marking only has one token and the only transition creating a token is t 3 which requires a token to be produced by t 2 in place p 2 . Therefore there exists no execution σ such that

M i σ -→ M o and O t 2 (σ) > 0. It follows that ν 2 is a spurious solutions of Q(N 2 , M i , M o ).
While defining an over-approximation might be useful for the verification of safety properties, in our case, we want to be able to models any executions of a workflow net with enough precision in order to verify extended modal specifications.

To further refine Q so that sufficient conditions can be defined structurally, additional constraints are needed. We propose to consider solution ν of Q(N, M a , M b ) such that sN(ν) is a marked graph (Section 2.1.4). The resulting constraint system is denoted D.

Definition 38: State Equation + Absence of Siphon + MG Constraint System

Let N = P, T, F be a workflow net and M a , M b two markings of N, the constraint system D(N, M a , M b ), associated with it, is:

-∀p ∈ P, t∈ • p ν(t) ≤ 1 ∧ t∈p • ν(t) ≤ 1 -Q(N, M a , M b ) | = ν where ν : P ∪ T → N is a valuation function.
The solutions of the constraint system of Definition 38 are related to the execution of a workflow net N as stated by Theorem 13.

M ∅ such that ∀ p ∈ sP, M ∅ (p) = 0). Therefore, ∀ p ∈ sP there exists t pre ∈ • p, t post ∈ p • such that ν(t pre ) > 0 ∧ ν(t post ) > 0 and ∀ σ such that M ∅ σ -→ M ∅ is an execution of sN(ν) we have O t post (σ) = 1 ⇒ O t pre (σ) = 1. By induction, it follows that there exists σ such that M ∅ σ -→ M ∅ an execution of sN(ν) where ∀t ∈ T such that ν(t) > 0, we have O t (σ) = 1. We conclude that there exists σ such that M a σ -→ M b is an execution of N where ν | = σ.
As stated by Theorem 13, any solution of D(N, M a , M b ) models at least one valid execution of N leading to M b from M a . Note the solutions of D are abstractions of the executions they model as the ordering of the transitions they involve is not explicitly computed. However, as N might not belong to the subclass of marked graph, not all valid executions of N leading to M b from M a can be modelled by solutions of D(N, M a , M b ). In this sense, the solutions of D(N, M a , M b ) define an under-approximation of the valid executions of N leading to M b from M a .

We call segment every execution modelled by the constraint system D. We now propose to decompose any execution of a workflow net into such segments. The resulting constraint system is denoted U.

Definition 39: k-segment Execution Constraint System

Let N = P, T, F be a workflow net, M a , M b two markings of N, and k ∈ N a number of segments, the constraint system U(N, M a , M b , k), associated with it, is:

-∃ M 1 , ν 1 , D(N, M a , M 1 ) | = ν 1 -∀ i ∈ {2, .., k -1}, ∃ M i , ν i , D(N, M i-1 , M i ) | = ν i -∃ ν k , D(N, M k-1 , M b ) | = ν k -∀ n ∈ P ∪ T, ν(n) = i∈{1,..,k} ν i (n) where ν : P ∪ T → N is a valuation function.
The solutions of the constraint system of Definition 39 are related to the execution of a workflow net N as stated by Theorem 14.

By definition there exists

M 1 , .., M k-1 such that M a t 1 -→ M 1 ..M k-1 t k -→ M b .
As the firing of a single transition t can be modelled by a valuation ν t : P ∪ T → N satisfying S and the associated subnet sN(ν t ) is a marked graph without siphon composed of only transition t, we can infer that ν t is also a valuation satisfying D. It follows that there exists ν 1 , ..,

ν k such that D(N, M a , M 1 ) | = ν 1 , .., (N, M k-1 , M b ) | = ν k . Let ν : P ∪ T → N be a valuation function such that ∀ n ∈ P, ν(n) = i∈{1,..,k} ν i (n). By definition of U, we can conclude that U(N, M a , M b , k) | = ν and ν | = σ. (⇐) Follows from Theorem 13.
By Theorem 14, every execution composed of at most k segments and leading to a marking M b from a marking M a of a workflow net N can be modelled by the constraint system U(N, M a , M b , k).

n ∈ P ∪ T, ν(n) = ν f irst (n) + ν second (n) + ν third (n) is a solution of the constraint sys- tem U(N, M i , M b , 3
) and therefore a model of a correct execution of N. The places and transitions present in each figure correspond to the places and transition which valuation is equal to 1. The dashed elements are the elements not present in the subnet associated with the considered valuations. This illustrates how workflow nets complete executions can be broken down into pieces we call segments whose validity is guaranteed by the structural analysis of their subnets.

We described how ordinary workflow nets correct execution can by modelled through the definition of constraint systems. More precisely we showed how every execution could be modelled by segments verifiable structurally. The next section describes how the previously defined modelling can be used to verify extended modal specifications over ordinary workflow nets.

3.1.3/ Verifying Extended Modal Specifications

Let us recall that modal specifications enable the description of complex modal properties expressing admissible or necessary behaviour involving several transitions and their causalities. Such admissible and necessary behaviours are respectively defined by may-formulae and must-formulae.

Intuitively, a workflow net N is valid with respect to a may-formula m if and only if there exists a correct execution σ of N such that the modal property expressed by m is satisfied by the execution

σ (i.e. N | = may m ⇔ ∃ σ ∈ Σ 1 , σ | = m).
Likewise a workflow net N is valid with respect to a must-formula m if and only if there does not exist a correct execution σ of N such that the modal property expressed by ¬m is satisfied by the execution σ (i.e.

N | = must m ⇔ σ ∈ Σ 1 , σ | = (¬m)).
When determining whether or not a workflow net satisfies the modal properties of interest, we distinguish two decision problems. The first one, called the K-bounded validity of a modal formula, only considers executions formed by K segments, at most. The second one, called the unbounded validity of a modal formula, deals with executions formed by an arbitrary number of segments; it generalises the first problem.

In our approach, verifying modal formulae as defined in Section 3.1.1 page 44 relies on their expression by constraints.

Given N = P, T, F a workflow net and m ∈ S (N) a modal property, we build the associated constraint system, noted C(N, m), by replacing every terminal symbol t ∈ T of m by ν(t) > 0, where ν : P ∪ T → N is a valuation function.

Example 17: Illustration of the expression by constraints of a modal formula

Let N be the on-demand order delivery workflow net described in Section 2.1.6 page 21. The modal property m which states the fact that a client pays his order either using a credit card or by cash can be defined as m = Client Pays By Cash ∨ Client Pays By Credit Card. By replacing every terminal symbol t ∈ T of m by ν(t) > 0, we obtain the following constraint system: C(N, m) = ν(Client Pays By Cash) > 0 ∨ ν(Client Pays By Credit Card) > 0 where ν : P ∪ T → N is the valuation function.

Upon the expression of a modal property by a constraint system, we build a constraint system extending the constraint system U(N, M i , M o , k) which models the correct execution of N composed of at most k segments.

Definition 40: k-segment Modal Execution Constraint System

Let N = P, T, F be a workflow net, k ∈ N a number of segments, and m ∈ S (N) a modal property, the associated constraint system V(N, k, m) is defined as follow:

-

U(N, M i , M o , k) | = ν -C(N, m) | = ν
where ν : P ∪ T → N is a valuation function.

The solutions of the constraint system of Definition 40 are related to the execution of a workflow net N as stated by Theorem 15. Proof. Follows from Theorem 14.

By Theorem 15, there exists a correct execution of N composed of at most k segments satisfying a modal property m ∈ S (N) if and only if there exists a valuation satisfying the constraint system V(N, k, m). It follows that we can determine the K-bounded validity of a modal property m, by determining the satisfiability of V(N, K, m). Consequently let m be a may-formula (resp. a mustformula), the workflow net N is said to be K-bounded valid with respect to m if and only if By Theorem 16, the K-bounded validity of an extended modal specification can de determined through the evaluation of the satisfiability of the corresponding constraint system.

∃ ν, V(N, K, m) | = ν (resp. ν, V(N, K, ¬m) | = ν).
We continue by demonstrating that for K sufficiently large, the K-bounded validity of an extended modal specification is equivalent to its unbounded validity.

Theorem 17: Existence of K max

Let N = (P, T, F) be a workflow net, Rmust the set of all well-formed must-formulae not satisfied by N, and R may the set of all well-formed may-formulae satisfied by N. There exists K max such that:

-∀ f ∈ Rmust , ∃ ν, k ≤ K max , V(N, k, ¬m) | = ν, and -∀ f ∈ R may , ∃ ν, k ≤ K max , V(N, k, m) | = ν.
Proof. Sketch. The set of correct executions of a workflow net is possibly infinite. This is due to the fact that T-invariants (i.e. sequence of transitions σ such that M σ -→ M) could be fired indefinitely. However, when considering the verification of modal formulae, we are only interested in the presence or absence of transitions in correct executions (i.e. the number of their firings does not matter). Therefore considering the set of correct executions where T-invariants are allowed to fire at most once is enough to check the validity of modal formulae. This restricted set of correct executions is finite. As a consequence, there exists K max such that every execution of this set can be modelled by K max segments, at most.

We presented an approach enabling the verification of (extended) modal specifications over ordinary workflow nets through the modelling of their executions by constraint systems. In the next section, this approach is generalised to the realm of abstract Petri nets, an abstract notion of Petri nets including ordinary, generalised and coloured Petri nets.

3.2/ Over Abstract Workflow Nets

The goal of this section is to generalise the verification method of modal specifications presented in the previous section to the realm of abstract workflow nets, a suited abstract representation notably able to model ordinary, generalised and coloured Petri nets. After formally defining abstract workflow nets as well as their abstract extended modal specification, this section generalises the modelling framework presented in the previous section to enable its use over abstract workflow nets. It then describes how this modelling framework is used to verify the (in)validity of extended modal specifications over abstract workflow nets.

3.2.1/ Abstract Petri Nets

This section introduces the notion of Abstract Petri nets (APN) which provides a generalisation of Petri nets (Section 2.1.2 page 11), and of coloured Petri nets (Section 2.1. 5.2 page 19). This definition of abstract Petri nets is closely related to other more complex notions of abstract Petri nets such as the definition of [Padberg, 1999]. It aims at defining the largest model in which the modelling of execution we will present and upon which our verification method is based can be applied. The definition of the structure and semantics of abstract Petri nets is analogous to the definition of the structure and semantics of Petri nets (Section 2.1.2 page 11) and coloured Petri nets (Section 2.1.5.2 page 19). The state of an abstract Petri net is given by its marking, as proposed in the next definition. Let g P ∈ P, g T ∈ T, G P ⊆ P and G T ⊆ T . We use the following notations:

-

g • P = {t|W + (g P , t) O D } and • g P = {t|W -(g P , t) O D }, -g • T = {p|W + (p, g T ) O D } and • g T = {p|W -(p, g T ) O D }, -G • P = ∪ g∈G P g • , and • G P = ∪ g∈G P • g, -G • T = ∪ g∈G T g • , and • G T = ∪ g∈G T • g.
The markings of an abstract Petri net evolve when transition instances are firing. Let D be the Grothendieck group of D (i.e. the most general commutative group that arises from D by introducing additive inverses). Without loss of generality, let us suppose an abstract Petri net with no self loop, i.e. ∀p, p • ∩ • p = ∅, where P = {p 1 , .., p n } and T = {t 1 , .., t m }. This abstract Petri net can be represented by its corresponding incidence matrix W ∈ L(D, D ) (n,m) where:

∀p ∈ P, M b (p) = M a (p) -D W -(p, t)(d) + D W + (t, p)(d).
W i, j = W + (t j , p i ) -D W -(p i , t j ).
Let M be a marking, it can be represented by a marking vector M ∈ D (n,1) where M i,1 = M(p i ). Likewise, let (t, d) be a transition instance, it can be represented by a transition instance vector T ∈ D (m,1) where:

T j,1 =        d, if t j = t O D , otherwise
Let denote the generalised matrix-multiplication where each product is replaced by a function

composition (i.e C = A B ⇔ C i, j = Σ(A i,k • B k, j )). For M a (t,d)
---→ M b , we have:

M b = M a + W T (t,d) .
We denote T (t,d) the transition instance vector representing the transition instance (t, d), and σ | = T the fact that T = T (t 1 ,d 1 )

+ D .. + D T (t n ,d n ) .
In the context of abstract Petri nets, we define abstract workflow nets, a generalisation of workflow Petri nets (Section 2.1.6 page 21).

Definition 44: Abstract Workflow Net

Let AN = P, T, W -, W + be an abstract Petri net. The abstract Petri net AN is an abstract workflow net if and only if:

-AN has two special places i and o where • i = ∅ and o • = ∅, and -for each node n ∈ (P ∪ T ) there exists a path from i to o passing through n.

We denote M i the set of initial markings of an abstract workflow net where:

M i ∈ M i ⇔ M i (i) > O D ∧ ∀ p ∈ P \ {i}, M i (p) = O D .
Likewise we denote M o the set of final markings of an abstract workflow net where:

M o ∈ M o ⇔ M o (o) > O D ∧ ∀p ∈ P \ {o}, M o (p) = O D .
A correct execution of an abstract workflow net is an execution

M i σ -→ M o , where M i ∈ M i and M o ∈ M o .
The behaviour of AN is defined as the set Σ of all its correct executions.

Next, we proceed to explicitly show that Petri nets (Section 2.1.2 page 11), and coloured Petri Net nets (Section 2.1.5.2 page 19) are abstract Petri nets. Furthermore, we introduce weighted transitions abstract workflow nets, an extension of abstract workflow nets, that associates weights to transition instances in order to enable performance analysis.

Petri Nets as Abstract Petri Nets

A ordinary/generalised Petri net (Section 2.1.2 page 11) is an abstract Petri net defined within the framework where D is the set N of natural numbers, + D is the standard addition operation over N, and ≤ D is the standard less-than-or-equal relation over N.

Let N = P, T, F, W be a generalised Petri net, N is an abstract Petri net aP, aT, W -, W + where:

-the set of place P and aP are the same (P = aP), -the set of transition T and aT are the same (T = aT ), -the pre-incidence function is defined by

W -(p, t)(x) = W(p, t) * x if (p, t) ∈ (F ∩ (P × T ) and W -(p, t)(x) = O otherwise, -the post-incidence function is defined by W + (t, p)(x) = W(t, p) * x if (t, p) ∈ (F ∩ (T × P) and W + (t, p)(x) = O
C i from C 1 × .. × C u and Π C i be the projection of C 1 × .. × C u from C i .
Let N = (P, T, C, W) be a coloured Petri net, N is an abstract Petri net aP, aT, W -, W + where:

-the set of place P and aP are the same (P = aP),

-the set of transition T and aT are the same (T = aT ),

-the pre-incidence function is defined by

W -(p, t) = Π C(p) • W(t, p) • π C(p) ,
-the post-incidence function is defined by

W + (t, p) = Π C(p) • W(t, p) • π C(p) ,
-a transition instance (t, d) is then seen as the transition t associated with the binding π C(t) (d). Its incidence matrix is defined as: [[v1, v2, v3] v1, v2, v3]] . The abstract Petri net corresponding and equivalent to this coloured Petri net is composed of the same three places and transition, and its incidence matrix is defined as: [([v1, v2, v3], [0, 0, 0]) → ([-v1, -v2, -v3], [0, 0, 0]), ([v1, v2, v3],

→ [-v1, -v2, -v3], [v1, v2, v3] → [
[0, 0, 0]) → ([0, 0, 0], [v1, v2, v3])] .

Weighted Transition Abstract Workflow Nets

Analogously to weighted transition Petri nets (Section 2.1.5.3 page 21), weighted transitions abstract workflow nets are an extension of abstract workflow nets. They associate weights to transition instances in order to be able to perform performance analysis.

They rely upon the definition of a weight function defined within a framework where (C, + C ) is a commutative monoid. We denote O C the minimal element of C.

Let AN = P, T, W -, W + be an abstract workflow net, a weight function of AN is a total function C : T × D → C assigning a weight to each transition instances.

Let AN w = AN, C be the weighted transition abstract workflow net formed from the abstract workflow net AN associated with its weight function C.

The weight of a transition instance (t, d) is then given by C(t, d). Let M a , M b be marking of AN, and T a transition instance sequence such that M a T -→ M b , the weight associated to execution T is given by the execution weigh function C defined as C(T ) = t∈T T (t) * C(t).

We defined abstract workflow nets and presented their relation to workflow nets, and coloured workflow nets. The next section focuses on the definition of extended modal specifications over abstract workflow nets.

3.2.2/ Extended Abstract Modal Specification

This section introduces extended modal specification over abstract workflows net.

It generalises the concept of extended modal specifications over ordinary workflow nets to the realm of abstract workflow nets. The main additions are that modal properties, beside considering constraints over the transitions involved in correct executions and their relations, consider constraints on the initial markings, the final markings, as well as the transition instances.

To this end, the language S (AN) of well-formed modal specification formulae associated with an abstract workflow net AN = P, T, W -, W + is defined as follows.

Let be e ∈ D (l,c) where l, c ∈ N, we denote F(e, l, c) the set of formulae defined by the following grammar of axiom A, where i ∈ 1..l, j ∈ 1..c, and G is the axiom of the grammar of elements of D:

-A → (A ∧ A)|(A ∨ A)|(¬A)|B -B → C ≤ D C -C → D + D D -D → e i, j |G
Given m ∈ F(e, l, c), we denote e | = m the fact that e satisfies m, where ∧, ∨, ¬, and ≤ D assume standard semantics. Using this, a marking vector M can be constrained by a formula m ∈ F(M, n, 1), and a transition vector T can be constrained by a formula m ∈ F(T , m, 1).

Definition 45: Well-formed Abstract Modal Specification Formulae Let AN = P, T, W -, W + be an abstract workflow net. The language S (AN) of wellformed modal specification formulae of AN is defined by the following grammar of axiom A:

-A → (A ∧ A)|(A ∨ A)|(¬A)|B -B → t[e]
where t ∈ T and e ∈ F(d, 1, 1) with d a variable of domain D.

These well-formed abstract modal specification formulae allow specifiers to describe abstract workflow nets behaviour based on the transition instances involved.

Formally, let m ∈ S (AN) be a well-formed abstract modal specification formula and T the transition instance vector of a correct execution of AN, we denote T | = m the fact that the behaviour expressed by m is satisfied by the transition instance vector T . Formally, given t[e] where t ∈ T and e ∈ F(d, 1, 1) with d is a variable of domain D, we have

T | = t[e] ⇔ T i,1 | = e[d/T i,1
] where t i = t and e[d/T i,1 ] is the formula e, where all occurrences of d are replaced by T i,1 . Further, given

A 1 , A 2 ∈ S (AN), we have T | = (A 1 ∧A 2 ) ⇔ T | = A 1 ∧T | = A 2 , T | = (A 1 ∨A 2 ) ⇔ T | = A 1 ∨T | = A 2 , and T | = (¬A 1 ) ⇔ ¬(σ | = A 1 ).
Next, we extend well-formed abstract modal specification formulae in order to consider constraints on the initial markings as well as the final markings.

To this end, we define the set of well-formed extended abstract modal specification formulae as follows.

Definition 46: Extended Abstract Modal Specification Formulae

Let AN = P, T, W -, W + be an abstract workflow net. The set of well-formed extended abstract modal specification formulae of AN, noted S e (AN), is defined by the set of tuple cM i , cM o , m where:

-cM i ∈ F(M i , m, 1) are the constraints on the initial marking, -cM o ∈ F(M o , m, 1) are the constraints on the final marking, m ∈ S (AN) is the constraint on the transition instances and their relations defined by a well-formed abstract modal specification formula.

These well-formed extended abstract modal specification formulae allow specifiers to express abstract modal properties about abstract workflow nets correct executions.

Formally, let M i ∈ M i be an initial marking of AN, M o ∈ M o be a final marking of AN, σ be a correct execution of AN such that M i σ -→ M o , and T be a transition instance vector such that σ | = T , we say that a well-formed extended abstract modal specification formula m = cM i , cM o , m is satisfied by the correct execution σ if and only if

T | = m ∧ M i | = cM i ∧ M o | = cM o .
Every modal property expressed by a well-formed extended abstract modal specification formula can be interpreted as a may-formula (resp. must-formula), describing a behaviour that has to be ensured by at least one (resp. all) correct execution(s) of the specified abstract workflow net.

Formally, an abstract workflow AN satisfies a may-formula f may = cM i-may , cM o-may , m may , noted AN | = may f may , if and only if

∃ σ ∈ Σ, M i ∈ M i , M o ∈ M o , M i σ -→ M o ∧ σ | = T ∧ T | = m may ∧ M i | = cM i-may ∧ M o | = cM o-may . Further, an abstract workflow AN satis- fies a must-formula f must = cM i-must , cM o-must , m must , noted AN | = must f must , if and only if ∀ σ ∈ Σ, M i ∈ M i , M o ∈ M o , M i σ -→ M o ∧ σ | = T ∧ T | = m may ∧ M i | = cM i-may ∧ M o | = cM o-may .
Analogously to the way extended modal specifications are defined for ordinary workflow nets, we define abstract extended modal specifications for abstract workflow nets as follows.

Definition 47: Abstract Extended Modal Specification Let AN = P, T, W -, W + be an abstract workflow net. An abstract extended modal specification of AN is tuple a must , A may where:

a must is a must-formula, and -A may is a set of may-formulae.

Given an abstract workflow net AN, we say that AN satisfies (i.e. is conform to) an abstract extended modal specification a must , A may , noted AN | = a must , A may , if and only if: Note that in the case where AN is an abstract workflow nets extended with performance indicators (i.e. AN is a weighted transition abstract workflow net, Section 3.2.1 page 58), abstract extended modal specification can be further extended by considering constraints on the total weight of correct executions.

N | = must a must ,
To this end, a may-formula f may = cM i-may , cM o-may , m may (resp. a must-formula f must = cM i-must , cM o-must , m must is extended by a constraint cC ∈ F(w, m, 1) where w is the execution weight associated with the modelled executions.

It follows that a may-formula f may (resp. a must-formula f must ) extended by considering a constraint cC on the total weights of correct executions is satisfied by a weighted transitions abstract workflow net AN if and only if there exists a correct execution satisfying f may (resp. all correct executions satisfy f must ) such that its (resp. their) total weight satisfies cC.

3.2.3/ Modelling Executions of Abstract Workflow Nets

This section aims at modelling correct executions of abstract Petri net (Section 3.2.1 page 55) by a constraint system which is then solved to validate or invalidate some properties of interest. This modelling is similar to the modelling previously proposed to model correct executions of ordinary workflow nets.

We begin with the generalisation of the state equation to the domain of abstract workflow nets.

= M a + D (W T (t 1 ,d 1 ) )+ D ..+ D (W T (t n ,d n ) ) which is equivalent to M b = M a + D W (T (t 1 ,d 1 ) + D .. + D T (t n ,d n ) ) as is distributive.
We denote the constraint system of Theorem 18 by S a (M a , M b ). This constraint system defines an over approximation of the executions reaching M b from M a . Indeed, analogously to S defined over workflow nets, S a does not consider the order in which transitions are fired, which leads to spurious solutions.

We continue and refine solutions of S a using structural features of their associated subnets composed of places (except places only marked in the initial marking, and places only marked in the final marking), transitions, and arcs involved in the solution of S a .

As we are only interested in the structure of such subnets, it is sufficient to build them as ordinary Petri nets, i.e. using arc weight less or equal to 1.

Definition 48: Subnet of a solution of S a Let AN = P, T, W -, W + be an abstract workflow net, M a , M b be two markings of AN and T be a solution of the constraint system S a (M a , M b ) of AN. Let E + = W + T and E -= W -T . We define the subnet sAN(T ) = sP, sT, sF an ordinary Petri net where:

-sP = {p ∈ P | (O D < D E + (p) ∧ M a (p) < D E + (p)) ∨ (O D < D E -(p) ∧ M b (p) < D E -(p))} -sT = {t ∈ T | O D < D T (t)} -sF = {(p, t) | p ∈ sP ∧ t ∈ sT )} ∪ {(t, p) | t ∈ sT ∧ p ∈ sP)}
We know from the previous section that if the subnet of a solution to S a contains a siphon or a trap then this solution is a spurious solution. We also know that the subnet of a solution to S a contains a siphon (resp. a trap) if and only if it is also a trap (resp. a siphon). Using these rules to refine S a eliminates a large number of its spurious solution.

Definition 49: State Equation + Absence of Siphon Constraint System

Let AN = P, T, W -, W + be an abstract workflow net, and M a , M b be two markings of AN, the constraint system Q a (AN, M a , M b ) associated with it is:

-

S(N, M a , M b ) | = T -ξ such that B(sAN(ν)) | = ξ
where T : T → D is a valuation function.

However, the set of solutions of S a (M a , M b ), whose subnets contain no siphon, equivalently no trap or no P-semiflow (i.e. solutions of Q a (M a , M b )), still defines an over approximation of the executions reaching M b from M a .

To further refine the solutions Q a , we need to restrict the structure of their subnets. We propose to restrict them to the class of marked graphs (Section 2.1.4 page 16). This structural restriction is sufficient to guarantee the existence of at least an execution for every solution.

Definition 50: State Equation + Absence of Siphon Constraint + MG System

Let AN = P, T, W -, W + be an abstract workflow net, and M a , M b be two markings of AN the constraint system D a (AN, M a , M b ), associated with it, is:

-

Q(N, M a , M b ) | = T -sAN(T ) = sP, sT, sF is a marked graph (i.e. ∀p ∈ sP, | • p |≤ 1∧ | p • |≤ 1)
where T : T → D is a valuation function.

The solutions of the constraint system of Definition 50 are related to the execution of an abstract workflow net AN as stated by Theorem 19. We call a segment any executions modelled by D a and proceed to model any executions as the composition of segments.

Definition 51: k-segment Abstract Execution

Let AN = P, T, W -, W + be an abstract workflow net, M a , M b be two markings of AN and k ∈ N, the constraint system U a (AN, M a , M b , k), associated with it, is:

-∃ M 1 , ν 1 , D a (AN, M a , M 1 ) | = T 1 -∀ i ∈ {2, .., k -1}, ∃ M i , T i , D a (N, M i-1 , M i ) | = T i -∃ T k , D a (N, M k-1 , M b ) | = T k -∀ n ∈ T, T (n) = i∈{1,..,k} T i (n)
where T : T → D is a valuation function.

The solutions of the constraint system of Definition 51 are related to the execution of an abstract workflow net AN as stated by Theorem 20. By definition there exists M 1 , ..,

M k-1 such that M a t 1 -→ M 1 t 2 -→ .. t k-1 ---→ M k-1 t k -→ M b .
As the firing of a single transition instance t can be modelled by a valuation T t : T → D satisfying S a and the associated subnet sN(T t ) is a marked graph without siphons composed of only the transition t, we can infer that T t is also a valuation satisfying D a . It follows that there exist T 1 , ..,

T k such that D(N, M a , M 1 ) | = T 1 , .., (N, M k-1 , M b ) | = T k . Let T : T → N be a valuation function such that ∀ p ∈ T, ν(p) = i∈{1,..,k} T i (p). By definition of U a , we can conclude that U a (AN, M a , M b , k) | = T and σ | = T .
(⇐) Follows from Theorem 19.

The constraint system U enables the modelling of finite executions of abstract workflow nets by considering their initial and final markings, and their sequences of transition instances.

This section presented a modelling framework which enables the modelling of abstract workflow nets through the construction of constraint systems. The next section takes advantage of this modelling to verify (extended) abstract modal specifications.

3.2.4/ Verifying Extended Abstract Modal Specifications

Analogously to the previous section, this section describes how the modelling of correct executions of an abstract workflow net can be used to verify the validity of an abstract extended modal specifications.

To this end, the following constraint system uses the constraint system U a to model only correct executions of AN composed of k ∈ N segments satisfying a given abstract modal property.

Definition 52: k-segment Abstract Execution

Let AN = P, T, W -, W + be an abstract workflow net, k ∈ N, and f = cM i , cM o , m be an abstract modal formula of AN, the constraint system V a (AN, k, f ) associated with it is:

-M i | = cM i -M o | = cM o -U a (AN, M i , M o , k) | = T -T | = m where (M i , M o , T ) : (P → D, P → D, T → D) is a valuation function.
It follows that there exists a correct execution, composed of at most k ∈ N segments, of AN, an abstract workflow net, such that it satisfies an abstract modal formula f if and only if the constraint system V a (AN, k, f ) is satisfiable.

Let f = cM i , cM o , m be an abstract modal formula of an abstract workflow net AN. To verify the K-bounded validity of f interpreted as a may-formula, it is sufficient to determine the existence of a correct execution modelled by K segments with an initial marking satisfying cM i , a final marking satisfying cM o and with the behaviour satisfying m. Therefore, a may-formula f is K-bounded valid with respect to AN if and only if V a (AN, k, f ) is satisfiable.

Similarly, determining the K-bounded validity of f interpreted as a must-property, can be done by determining the non-existence of a correct execution modelled by K segments with an ini-tial marking satisfying cM i , a final marking satisfying cM o where the behaviour of ¬(m) is satisfied. Therefore, a must-formula f is K-bounded valid with respect to AN if and only if V a (AN, k, cM i , cM o , ¬m ) is not satisfiable.

Finally, in the case where AN is an abstract extended with performance indicators (i.e. AN is a weighted transitions abstract Petri net, Section 2.1.5.3 page 21), we need to consider the constraint cC given over the total execution weight. To this end, note that the total weight of an execution modelled by U a (N, M a , M b , k) | = T is given by C(T ) = t∈T T (t) * C(t). Therefore it is necessary to add the following constraint to U a (N, M a , M b , k): C(T ) | = cC.

3.3/ Synthesis

This chapter presented an approach to the verification of modal specifications.

It defined extended modal specifications, an extension of modal specifications that enables the definition of modal behaviour involving several transitions.

An innovative modelling framework of workflow nets (resp. abstract workflow nets) executions has also been defined. This modelling framework is based on the definition of several constraint systems. More precisely, it defines constraint systems whose solution space over-approximate the set of correct executions of workflow nets (resp. abstract workflow nets). Each of this over-approximation is built by refining the previous one starting from a well-known approximation: the state equation. Further, it also defined a constraint system whose solution space underapproximates the set of correct executions of workflow nets (resp. abstract workflow nets). This latter constraint system is then used to define segments of execution (i.e. partial execution structurally verifiable). It then proceeded to demonstrate that the concatenation of such segments could be used to model any correct executions of workflow nets (resp. abstract workflow nets).

One of the advantages of this modelling is that the search is quite focussed from the beginning as we traverse the solution space of the state equation and its refinements rather than the underlying semantic labelled transition systems of workflow nets. Another advantage of such modelling is that only the segments ordering is computed, the transitions ordering within segments is not. Therefore, this modelling is adapted to the verification of properties where only the presence or absence of transitions is considered (e.g., extended modal specifications).

Finally, it presented how such modelling framework is used to verify the (in)validity of extended modal specifications over workflow nets (resp. abstract workflow nets). This verification approach, based upon the previously presented modelling may perform well when verifying the conformity of workflow nets with respect to valid must-formulae as well as invalid may-formulae, thanks to adequate use of over-approximations. Furthermore, this extended modal specification verification approach requires the use of constraint systems satisfiability checks which can be handled by third party constraint solvers. This allows the proposed verification method to benefit from existing mature and efficient constraint solvers.

In order to enhance verification approaches such as the one presented in this chapter, the following chapter presents powerful reduction methods preserving properties of interest such as generalised soundness and correctness of a given modal specification. It also presents how these reduction methods can be employed as pre-processing steps to reduce workflow nets size in order to verify the preserved properties on smaller instances. The development of large and intricate workflow nets can be a difficult task which requires powerful structuring mechanisms [Dittrich, 1989]. It also forces modellers to follow strict abstraction patterns in order to produce quality workflow nets [van der Aalst et al., 2000]. To cope with these development difficulties, stepwise refinement (Section 2.1.9 page 25) is often used to ensure reliability and ease verification.

Verification of workflow nets is an a posteriori approach: given a workflow net, it checks whether properties (e.g., generalised soundness, extended modal specification) hold. Although for workflow nets these properties are known to be decidable [Esparza, 1998[START_REF] Van Der | Soundness of workflow nets: classification, decidability, and analysis[END_REF], their verification is a very time consuming task due to its high complexity (EXPSPACE) with respect to the size of the workflow net under analysis [Lipton, 1976].

Unfortunately, most often, the abstraction mechanisms, used by modellers of workflow nets, are not explicitly given beside the clear advantages they bring to their analysis.

As seen in Section 2.2.3 page 35, reduction rules have the ability to reduce workflow nets size while strongly preserving properties of interest. This allows the analysis of studied properties to be performed on reduced workflow nets, in many cases, greatly decreasing its complexity by alleviating state explosion of their state space, which undermines state exploration methods.

More generally, reduction rules are abstraction operations: they reduce the level of details of workflow nets. They aim at capturing the abstraction mechanisms used by modellers of workflow nets. It follows that the inversion of reduction rules (i.e. synthesis rules) are refinement operations. Conceptually, this leads to an analysis paradigm where the analysis of workflow nets is substituted by the analysis of their constructions.

The first section of this chapter presents reduction rules strongly preserving generalised soundness over workflows nets, an essential and necessary correctness property that must be satisfied by workflow nets.

Afterwards, the second section describes how these reduction rules can be used to efficiently semidecide generalised soundness.

The third section introduces pre-processing steps reducing workflow nets size so that the analysis can be carried out on smaller instances. More specifically, it highlights how reduction methods can be applied as pre-processing steps to the verification of extended modal specifications over workflow nets.

Finally, the last section concludes this chapter.

4.1/ Φ * : A workflow nets reduction kit

This section defines Φ * , a kit of reduction rules over workflow nets that strongly preserve generalised soundness (Definition 24 page 25).

In Section 2.2.2.4 page 34 we saw that the k-soundness of a workflow net is equivalent to the liveness and boundedness of its k-closure. Therefore, known reduction rules (Section 2.2.3.2 page 36) which strongly preserve liveness and boundedness of Petri nets also strongly preserve generalised soundness of workflow nets. Conversely, the reduction rules introduced in this section strongly preserve liveness and boundedness.

The reduction kit defined in this section generalises and adapts previously known reduction rules (Section 2.2.3.2 page 36) to the realm of workflow nets. They extend the range of workflow nets reducible in such a way.

The presented reduction rules are applicable to arbitrary workflow nets and are not restricted to subclasses. Further, their conditions of application are defined solely on the structure of the considered workflow nets. This allows their application to be performed statically in an efficient manner. Also, note that each rule's conditions of application describe an infinity of workflow patterns (i.e. structural configurations) to which they can be applied.

In what follows, each workflow net reduction rule is defined by describing the conditions of application under which it can be applied to a source workflow net N = P, T, F , and the construction algorithm which is applied to N to produce a target workflow net Ñ = P, T , F .

For clarity, every rule is illustrated by figures depicting two of the possible applications of this rule. The first one only considers the plain element of the figure and corresponds to the minimal pattern. The second one considers both the mandatory (plain) and the optional (dashed) elements, and corresponds to a possible extended pattern. In this way, figures are not exhaustive but aim to ease the understanding of the rules that are formally described by the related conditions of application and the construction algorithms.

There are a total of six rules presented in the following subsections: one removing a place (R 1 ), two removing a transition (R 2 , R 3 ), two removing a place and a transition (R 4 , R 5 ), and finally one removing a strongly connected component: (R 6 ).

R 1 : Remove Place

We define φ RemoveP , a workflow net reduction rule, which strongly preserves generalised soundness and consists in removing a place for which there exists a set of places with the same input transitions as well as the same output transitions. Places removed in such a way are called redundant places as they do not modify the set of correct executions of a workflow net.

This rule generalises the Fusion of Parallel Places rule described in [Murata, 1989] and the Abstraction of Parallel Places rule described in [START_REF] Hichami | An approach of optimisation and formal verification of workflow petri nets[END_REF]. This rule can also be viewed as an adaptation of the rule φ S of [START_REF] Desel | Free choice Petri nets[END_REF] (i.e. one of the three reduction rules proved to be complete with respect to the subclass of free-choice Petri nets) to the context of ordinary workflow nets.

The inverse of this rule is the only synthesis rule able to add a single place to a workflow net while preserving generalised soundness and is notably used to introduce concurrency. In the context of Petri net, a self-loop place (i.e. a place p such that • p = p • ) can be added without compromising liveness and boundedness. However, this requires changing the initial marking which is not possible in the context of workflow nets. Nonetheless, a generalisation of this rule could be applied to an extension of workflow nets modelling resources by marked places. Conditions on N:

-∃ p ∈ P \ {i, o} -∃ G = {g 1 , .., g n } ⊆ P \ {i, o, p} -p • = G • -• p = • G -∀i, j ∈ {1, .., n}, i j ⇒ • g i ∩ • g j = g • i ∩ g • j = ∅ Construction of Ñ: -p • = {ot 1 , .., ot n } -outArc = {p} × p • -• p = {it 1 , .., it m } -inArc = • p × {p} -P = P \ {p} -T = T -F = F \ (inArc ∪ outArc) Figure 4.1: Reduction rule φ RemoveP (R 1 )
The soundness of φ RemoveP , with respect to generalised soundness, is given by the following theorem.

Theorem 21: Soundness of φ RemoveP φ RemoveP is a workflow net reduction rule which strongly preserves generalised soundness.

Proof. (Sketch). Let f : ( P → N) → (P → N) be a bijective function such that f (M)(g) = M(g) for all g ∈ P and f (M)(p) = M(g 1 ) + .. + M(g n ). By conditions on N, every transition that produces (resp. consumes) a token in any of the places of G also produces (resp. consumes) a token in p. Consequently, ∀k ∈ N one has:

M ∈ R Ñ (M Ñ i(k) ), M Ñ o (k) ∈ R Ñ (M) ⇔ f (M) ∈ R N (M N i(k) ), M N o (k) ∈ R N ( f (M))
, and transitions ot 1 , .., ot n , it 1 , .., it m of N are not dead if and only if transitions ot 1 , .., ot n , it 1 , .., it m of Ñ are not dead.

R 2 : Remove Transition

We define φ RemoveT , a workflow net reduction rule, which strongly preserves generalised soundness and consists in removing a transition for which there exists a set of transitions having the same input and output places. Intuitively, the transitions removed by this rule are transitions which firing can be simulated by the firing of a sets of other transitions. This rule is an original rule generalising the Fusion of Parallel Transitions rule of [Murata, 1989] and the Abstraction of Parallel Transitions rule of [START_REF] Hichami | An approach of optimisation and formal verification of workflow petri nets[END_REF]. This rule is an adaptation of the rule φ S of [START_REF] Desel | Free choice Petri nets[END_REF] to the realm of ordinary workflow nets with no restriction on their subclasses. Indeed, outside the scope of free-choice workflow nets, additional constraints are required to ensure that the removed transitions are live. To this end, the liveness of a transition to be removed in such a way is inferred from the liveness of a source transition, a transition that, when fired, enables the transition to be removed. Note that this requirement could be relaxed. Instead of requiring the presence of a source transition, one could require the presence of a sequence of transitions, where each successive transition is enabled by the firing of the previous ones, such that the firing of this sequence of transitions enables the transition to be removed.

The inverse rule of this reduction rule is a synthesis rule able to add a single transition to an arbitrary workflow net based on its structure while preserving generalised soundness and is used to introduce choice.

The reduction rule φ RemoveT is pictured in Figure 4.2 and formally described below.

Let D be a set of places, we define the function ϑ : D → (P → N) such that:

∀ d ∈ P, ϑ(D)(d) =        1, if d ∈ D 0, otherwise
Let f 1 , f 2 , f 3 : P → N be three functions, we overload the operator +,and = such that

f 3 = f 1 + (-) f 2 ⇔ ∀p ∈ P, f 3 (p) = f 1 (p) + (-) f 2 (p)
. Function ϑ is used to compare inputs and outputs of a set of transitions. Note here that this function does not consider self-loop transitions, a desired property as self-loop transition can be added to places (see φ RemoveS T reduction rule, introduced in the next subsection).

Conditions on N:

-∃ t ∈ T -∃ G = {g 1 , .., g n } ⊆ T \ {t} -ϑ t = ϑ(t • ) -ϑ( • t) -ϑ G = ϑ(g • 1 ) + .. + ϑ(g • n ) -ϑ( • g 1 ) -.. -ϑ( • g n ) -ϑ t = ϑ G -∀i, j ∈ {1, .., n}, i j ⇒ ( • g i ∩ • g j = g • i ∩ g • j = ∅) -(∃ t s ∈ T \ ({t} ∪ G), ∀g ∈ G, • g ⊆ t • s ) ∨ (|G| = 1)
Construction of Ñ:

-

t • = {op 1 , .., op n 1 } -outArc = {t} × t • -• t = {ip 1 , .., ip n 2 } -inArc = • t × {t} -P = P -T = T \ {t} -F = F \ (inArc ∪ outArc) Figure 4.2: Reduction rule φ RemoveT (R 2 )
The soundness of φ RemoveT , with respect to generalised soundness, is given by the following theorem.

Theorem 22: Soundness of φ RemoveT φ RemoveT is a workflow net reduction rule which strongly preserves generalised soundness.

Proof. (Sketch). Let us suppose that ϑ t = ϑ G . By conditions on N, for all k in N, and

∀M N in R N (M N i(k)
), transition t is enabled if and only if transitions g 1 , .., g n are also enabled. Moreover, the firing of t must result in the same marking as the successive firing of transitions g 1 , .., g n in any order. It follows that ∀k

∈ N, M ∈ R N (M N i(k) ), M N o (k) ∈ R N (M) ⇔ M ∈ R Ñ (M Ñ i(k) ), M Ñ o (k) ∈ R Ñ (M). To conclude, suppose |G| = 1, then t is not dead in N if and only if g 1 is not dead in Ñ. Alternatively, suppose (∃ t s ∈ T \ ({t} ∪ G), ∀g ∈ G, • g ⊆ t •
s ), then t is not dead in N if and only if t s is not dead in Ñ.

R 3 : Remove Self-loop

We define φ RemoveS T , a workflow net reduction rule, which strongly preserves generalised soundness and consists in removing a transition whose input places are its output places. This original rule generalises the Self-Loop Transition rule described in [Murata, 1989]. Similarly to rule φ RemoveT , the liveness of a transition removed by this rule also needs to be inferred from the existence of a source transition (alternatively a source sequence of transitions).

Furthermore, the inverse of this reduction rule is a synthesis rule able to add a single transition to an arbitrary workflow net based on its structure while preserving generalised soundness. It is typically used to introduce choice and repetitive tasks. Conditions on N:

-∃ t ∈ T -t • = • t -∃ t s ∈ T \ {t}, • t ⊆ t • s ∨ • t ⊆ • t s Construction of Ñ: -outArc = {t} × t • -inArc = t • × {t} -P = P -T = T \ {t} -F = F \ (inArc ∪ outArc) Figure 4.3: Reduction rule φ RemoveS T (R 3 )
The soundness of φ RemoveS T , with respect to generalised soundness, is given by the following theorem.

Theorem 23: Soundness of φ RemoveS T φ RemoveS T is a workflow net reduction rule which strongly preserves generalised soundness.

Proof. (Sketch). By conditions imposed on N, we know that the firing of transition t does not change the markings of N in which it is enabled. It follows that ∀k

∈ N, M ∈ R N (M N i(k) ), M N o (k) ∈ R N (M) ⇔ M ∈ R Ñ (M Ñ i(k) ), M Ñ o (k) ∈ R Ñ (M)
. Notice that t is not dead in N if and only if t s is not dead in Ñ.

R 4 : Remove Transition Place

We define φ RemoveT P , a workflow net reduction rule, which strongly preserves generalised soundness and consists in removing a place and its only input transition. Intuitively, this rule consists in removing a place p and its only input transition t by merging transition t with the output transitions of place p.

The φ RemoveT P rule is displayed in Figure 4.4(a), 4.4(b) and formally described below.

Conditions on N:

-∃ p ∈ P \ {i, o}

-• p = {t} -t • {p} ⇒ ∀ ot ∈ p • , • ot = {p} ∧ t • ∩ ot • = ∅ -t • = {p} ⇒ ∀ ot ∈ p • , • t ∩ • ot = ∅ ∧ (∃ ot ∈ p • , • ot = {p} ∨ ∀ ip ∈ • t, ip • = {t})
Construction of Ñ:

- This rule generalises the Post-Fusion rule of [Berthelot, 1987, Sloan et al., 1996].

t • \ p = {op 1 , .., op n 1 } -• t = {ip 1 , .., ip n 2 } -p • = {ot 1 , .., ot n 3 } -outT = {t} × t • \ p -inT = • t × {t} -outP = {p} × p • -inArc = • t × p • -outArc = p • × t • \ p -P = P \ {p}, -T = T \ {t} -F = (F ∪ inArc ∪ outArc) \ ((t, p) ∪ inT ∪ outT ∪ outP) (a) t • = {p} (b) t • {p}
The inverse of this rule is a synthesis rule introducing a sequence of tasks (adding a task that has to be accomplished before others) and able to factor common input/output places of a set of transitions.

The soundness of φ RemoveT P , with respect to generalised soundness, is given by the following theorem.

Theorem 24: Soundness of φ RemoveT P φ RemoveT P is a workflow net reduction rule which strongly preserves generalised soundness.

Proof. (Sketch). In N the transitions ot 1 , .., ot n 3 have to consume a token in place p. All tokens consumed in place p have to be produced by transition t, which consumes a token in places ip 1 , .., ip n 2 and produces a token in places op 1 , .., op n 1 and p. Thus, ot 1 , .., ot n 2 have to consume a token in ip 1 , .., ip n 2 and produce a token in op 1 , .., op n 1 . Conversely, the same analysis holds on Ñ, we conclude that N is generalised sound if and only if Ñ is generalised sound.

R 5 : Remove Place Transition

We define φ RemovePT , a workflow net reduction rule, which strongly preserves generalised soundness and consists in removing a place and its only output transition. Intuitively this rule consist in removing a place p and its only output transition t by merging transition t with the input transitions of place p.

The φ RemovePT rule is displayed in Figure 4.5(a), 4.5(b) and formally described below.

Conditions on N: This rule generalises the Pre-Fusion rule of [Berthelot, 1987, Sloan et al., 1996] as well as the reduction rule φ A of [START_REF] Desel | Free choice Petri nets[END_REF].

-∃ p ∈ P \ {i, o} -p • = {t} -• t {p} ⇒ ∀ it ∈ • p, it • = {p} ∧ • t ∩ • it = ∅ ∧ ( • it) • = {it} -• t = {p} ⇒ ∀ it ∈ • p, t • ∩it • = ∅ Construction of Ñ: -t • = {op 1 , .., op n 1 } -• t \ p = {ip 1 , .., ip n 2 } -• p = {it 1 , .., it n 3 } -outT = {t} × t • -inT = • t \ p × {t} -inP = • p × {p} -inArc = • t \ p × • p -outArc = • p × t • -P = P \ {p}, -T = T \ {t} -F = (F ∪ inArc ∪ outArc) \ ((p, t) ∪ inT ∪ outT ∪ inP) (a) • t = {p} (b) • t {p}
The inverse of this rule is a synthesis rule introducing a sequence of tasks (adding a task that have to be accomplished after others) and able to factor common input/output places of a set of transitions.

The soundness of φ RemovePT , with respect to generalised soundness, is given by the following theorem.

Theorem 25: Soundness of φ RemovePT φ RemovePT is a workflow net reduction rule which strongly preserves generalised soundness.

Proof. (Sketch). In N the transitions it 1 , .., it n 3 have to produce a token in place p. All tokens produced in place p have to be consumed by transition t, which consumes a token in places ip 1 , .., ip n 2 and p, and produces a token in places op 1 , .., op n 1 . Thus, it 1 , .., it n 3 have to consume a token in ip 1 , .., ip n 2 and produce a token in op 1 , .., op n 1 . Conversely, the same analysis holds on Ñ, we conclude that N is generalised sound if and only if Ñ is generalised sound.

R 6 : Remove Ring

We define φ RemoveR , a workflow net reduction rule, which strongly preserves generalised soundness, and consists in merging places among a ring. A ring is a set of places strongly connected by transitions with a single input place and a single output place. The transitions forming the ring are also removed. Intuitively, tokens among the places of a ring can freely move from a place of the ring to an other, therefore they might as well be on the same place.

This rule is an original one, its inverse rule is a synthesis rule which transforms a place into a ring, distributing its input and output transitions among the places of the introduced ring. Conditions on N: The soundness of φ RemoveR , with respect to generalised soundness, is given by the following theorem.

-∃ {p 1 , .., p n } ⊆ P -∃ {t 1 , .., t m } ⊆ T -∀ i ∈ {1, .., m}, | • t i | = |t • i | = 1 -∀ i, j ∈ {1, .., n}, • p i ∩ • p j = p • i ∩ p • j = ∅ -∀ i, j ∈ {1, .., m}, ∃ σ : {1, .., k} → {p 1 , .., p n } ∪ {t 1 , .., t m } a path of length k such that σ(1) = p i ∧ σ(k) = p j ∧ ∀ x ∈ {1, .., k -1}, (σ(x), σ(x + 1)) ∈ F Construction of Ñ: -ringArc = (({p 1 , .., p n } × {t 1 , .., t m }) ∪ ({t 1 , .., t m } × {p 1 , .., p n })) ∩ F -inT = • p 1 ∪ .. ∪ • p n -outT = p • 1 ∪ .. ∪ p • n -removedA = ((inT × {p 1 , .., p n }) ∪ ({p 1 , .., p n } × outT )) ∩ F -addA = (inT × p) ∪ (p × outT ) -P = (P ∪ p) \ {p 1 , .., p n } -T = T \ {t 1 , .., t m } -F = (F ∪ addA) \ removedA
Theorem 26: Soundness of φ RemoveR φ RemoveR is a workflow net reduction rule which strongly preserves generalised soundness.

Proof. (Sketch). By conditions imposed on N, tokens among the places p 1 , .., p n of a ring can freely move from a place of the ring to an other by firing a sequence of transitions formed with transitions t 1 , .., t m . It follows that each token produced (resp. consumed) by an input (resp. output) transition of a place in the ring will eventually be (resp. has been), after (resp. before) the firing of a possibly empty sequence of transitions formed with transitions t 1 , .., t m , consumed (resp. produced) by any output (resp. input) transitions of a place of the ring. Likewise, in Ñ each token produced (resp. consumed) by an input (resp. output) transition of p will be (resp. has been) consumed (resp. produced) by an output (resp. input) transition of p. It follows that N is generalised sound if and only if Ñ is generalised sound.

In this section we defined six reduction rules which together constitute a generic generalised soundness preserving reduction kit. These rules generalise the rules previously presented in the literature [Berthelot, 1987, Murata, 1989, Sloan et al., 1996, Voorhoeve et al., 1997, Sadiq et al., 2000, Lin et al., 2002, Desel et al., 2005, Hichami et al., 2014] thereby extending the range of workflow nets reducible in such a way.

The next sections present two applications of this reduction kit: a generalised semi-decision procedure and a pre-processing step towards the verification of (extended) modal specifications.

4.2/ Semi-Decision of Generalised Soundness

This section proposes an algorithm based on the workflow nets reduction kit Φ * described in the previous section, for semi-deciding the generalised soundness of workflow nets.

Our approach is based on Lemma 4 page 36. This lemma allows us to infer the validity of a property of a workflow net from its transformed instance as long as the transformation rules applied to obtain it strongly preserve this property.

The reduction kit Φ * strongly preserves generalised soundness. Let N and Ñ be two workflow nets such that (N, Ñ) ∈ Φ * then the workflow N is generalised sound if and only if the workflow net Ñ is generalised sound. Furthermore, it is trivial that the workflow net N Atomic = {i, o}, {t}, {(i, t), (t, o)} (i.e. a workflow net composed of a single transition whose input place is the initial place and output place is the final place) is generalised sound.

It follows that if (N, N Atomic ) ∈ Φ * then the workflow net N is generalised sound. Unfortunately, the reduction kit Φ * is not complete with respect to generalized soundness over ordinary workflow nets. This leads to the design of an algorithm to semi-decide whether a workflow net N is generalised sound. This algorithm proceeds by iteratively trying to apply any of the reduction rules of Φ * to the input the workflow net N until a fix-point is reached (none of the reduction rules can be applied). If the workflow net produced by these reductions equals N Atomic , one can conclude that N is generalised sound. Otherwise, one cannot directly conclude about generalised soundness, but the reduced workflow net is saved to be further analysed using classical techniques such as model-checking. This procedure is described by Algorithm 2 which is based on: (i) the set of workflow net reduction rules Φ = {R 1 , .., R 6 }, (ii) an auxiliary function size(N), which returns the number of nodes of a workflow net N at each iteration step, (iii) a function T ryApplyRule(φ, N), which returns either Ñ if the rule φ can be applied to N to produce Ñ, or N otherwise, and (iv) save(N), a function that saves N.

Theorem 27: Termination of Algorithm 2

The procedure described by Algorithm 2 terminates.

Proof. (Sketch). Every rule applied by Algorithm 2 strictly reduces the number of nodes of N. None of the applied rules can produce a workflow net with less than one node. Thus it always terminates when no workflow net reduction rules can be applied, and either provides an atomic sound net or saves the reduced workflow net. The procedure described by Algorithm 2 is sound.

Proof. (Sketch). The set of workflow net reduction rules strongly preserves generalised soundness. By Theorem 4 page 36, the procedure described by Algorithm 2 is sound.

The application of this algorithm is illustrated by Figure 4.7. This figure depicts the sequence of workflow nets obtained by applying the reduction rules indicated by the labels of the large arrows linking them. The large arrows labelled R i * indicate that the transformation R i is sequentially applied many times to the source workflow net to produce the target one. The nodes coloured in red are the nodes of the source workflow net that are deleted by the reduction rule(s) applied to produce the target one. Whenever the applied rule is R 1 (resp. R 2 ) the places (resp. transitions) which are equivalent to the deleted node(s) are coloured in green. The last workflow net obtained is the atomic workflow net. Therefore, we can conclude that each workflow net depicted by Figure 4.7 is generalised sound.

We described how the workflow nets reduction kit described in Section 4.1 page 68 can be used to semi-decide the generalised soundness of workflow nets. Moreover, it is important to note that, in the case where this procedure cannot conclude, all was not done in vein as the produced workflow net size is most likely reduced. Furthermore, useful error diagnostics are given in the form of an irreducible graph. This makes the presented procedure a valuable pre-processing step towards further workflow net soundness analysis.

The following section reuses this concept and defines restrictions on the workflow nets reduction kit described in Section 4.1 page 68. These restrictions enable them to preserve the (in)validity of (extended) modal specifications in order to be used as a pre-processing set towards their verification.

4.3/ Preprocessing Modal Specification Verification

In Section 3.1.3 page 53 we presented a verification method to verify the (in)validity of extended modal specifications (Section 3.1.1 page 44) through the evaluation of the satisfiability of constraint systems. This method principally relies on the definition of over-approximations (e.g., the state equation) which are then refined through the composition of under-approximations. However, the used over-approximations are quite complex. For example, the existence of a solution to the state equation (Section 2.2.2.1 page 30) of a workflow net is an NP-complete problem. This has the effect of making this method intractable for large workflow nets.

Nonetheless, in Section 2.1.9 page 25, a vertical abstraction mechanism is defined through two vertical abstraction operations: Place refinement and Transition refinement. This abstraction mechanism leads to the definition of hierarchical workflow nets representing workflow nets with multiple layers of detail. When the analysed workflow net is developed by stepwise refinement using Place refinement and Transition refinement, this hierarchical workflow net is explicitly given by the modellers. In a broader context, hierarchical workflow nets can be automatically and efficiently constructed (e.g., by detecting strongly connected components) from workflow nets through their decomposition [START_REF] Polyvyanyy | Connectivity of workflow nets: the foundations of stepwise verification[END_REF], Vanhatalo et al., 2007, Koehler et al., 2014].

The presented extended modal specification verification method, as most analysis tools, is not able to directly deal with hierarchical workflow nets. Instead, it takes as input the underlying workflow nets of hierarchical workflow nets. However, not all levels of detail of a hierarchical workflow net are required in order to infer the (in)validity of a given extended modal specification. It follows that the construction of a dedicated underlying workflow net, which preserves the (in)validity of a given extended modal specification, constitutes a vertical abstraction mechanism able to reduce the size of the workflow net under analysis. Furthermore, in Section 4.1 page 68, a reduction kit able to abstract workflow nets in order to reduce their size while preserving generalised soundness is presented. It allows an horizontal abstraction of workflow nets at an higher level. This reduction kit is particularly well-adapted to the reduction of workflow nets designed through refinement, a development approach which notably uses modal specifications.

It follows that adapting the reductions rules used by this reduction kit in order to preserve the (in)validity of a given extended modal specification constitutes an horizontal abstraction mechanism able to reduce the size of the workflow net under analysis.

Such abstraction mechanisms, used as pre-processing steps of the verification of a given extended modal specification, enlarge the range of workflow nets that can be analysed. Indeed, due to the exponential nature of the verification method with respect to the size of the workflow net under analysis, any reduction of the size of the workflow net under analysis should significantly improve the efficiency of the verification method.

Conceptually, this kind of approaches can be seen as a slicing approach [START_REF] Rabbi | A model slicing method for workflow verification[END_REF] since they aim at performing abstraction guided by a specific specification formula (equivalently a set of specification formulae). Indeed, slicing is a technique to syntactically reduce a model in such a way that at best the reduced model contains only those parts that may influence the property the model is analysed for [Rakow, 2008], which is the intent of the proposed reduction methods.

The remaining of this section is divided into two sub-sections presenting reduction methods preserving the (in)validity of a given extended modal specification. The first sub-section presents a reduction procedure based on the hierarchical representation of a workflow net. The second one details a reduction method based on the reduction rules presented in Section 4.1 page 68.

4.3.1/ Reduction based on hierarchical workflow nets

This section presents a reduction method preserving the (in)validity of a given extended modal specification based on the hierarchical representation of workflow nets.

We begin by defining subT ransitions, an utility function described in Algorithm 3, which takes as input a hierarchical workflow net node (i.e. a hierarchical workflow net) and returns the set of transitions of its underlying workflow net. We now define underlying r , a function described in Algorithm 4. This function takes as inputs a hierarchical workflow net and an extended modal specification formula, and returns the underlying workflow net of the input hierarchical workflow net restricted to the layers of detail relevant to the input extended modal specification formula. Differently from the function underlying, described in Algorithm 1 page 27, the function underlying r does not recursively expand every node of the input hierarchical workflow net, instead it only chooses to expand nodes for which the set produced by subT ransitions contains a transition in the domain of the input extended modal specification formula.

Data: W

= P h , T h , F h a hierarchical workflow net Result: T a set of transitions Function subTransitions(W = P h , T h , F h ) T = T h ; forall the S = P s , T s , F s ∈ P h ∪ T h do if T s ∅ then T = T ∪ T s ∪
Data: W = P h , T h , F h a hierarchical workflow net m an extended modal specification formula Result: N = P, T, F the workflow net underlying W restricted to the layers of detail relevant to n Function underlying r (W = P h , T h , F h ,m) Let W = P h , T h , F h be a hierarchical workflow net, and m a given extended modal specification formula.

N = P h , T h , F h ; forall the S = P s , T s , F s ∈ P h ∪ T h do if T s ∅ ∧ (subT ransitions(S ) ∩ Domain(m)) ∅ then N = N ⊗ S underlying
The extended modal specification formula m, interpreted as either a may-formula or a mustformula, is said to be (in)valid over the hierarchical workflow net W if and only if it is (in)valid over the underlying(W) workflow net. In order for the reduction procedure based on the function underlying r to be sound with respect to (in)validity of m, the following assumptions are required: Proof. (Sketch). We proceed by showing that the workflow nets underlying(W) = P u , T u , F u and underlying r (W, m) = P r , T r , F r are weak trace equivalent with respect to the transitions set Domain(m).

Note that, assuming W does not refine the transition of Domain(m), Domain(m) ⊆ T u and Domain(m) ⊆ T r by definitions.

Further, transition t ∈ T r \ T u is an abstract transition which always corresponds to correct executions of underlying(t) as W is generalised sound. Likewise, place p ∈ P r \ P u is an abstract place and transition t ∈ p • corresponds to correct executions composed of correct executions of underlying(p) followed by t. Theorem 29 allows us to conclude that, in order to verify a modal specification formula m interpreted as either a may-formula or a must-formula over a generalised sound hierarchical workflow net W, it is sufficient to consider the workflow net underlying r (W, m) rather than the workflow net underlying(W). As the workflow net underlying r (W, m) can be considerably smaller than the workflow net underlying(W), this reduction approach constitutes a valuable pre-processing step towards the verification of m interpreted ether as a may-formula or a must-formula.

4.3.2/ Reduction based on reduction rules

This section presents a reduction method preserving the (in)validity of a given extended modal specification based on the reduction rules presented in Section 4.1 page 68.

More precisely, it presents restrictions imposed on the reduction rules presented in Section 4.1 page 68. Given an extended modal specification formula m, these restricted reduction rules preserve the (in)validity of the extended modal specification formula m interpreted as either a mayformula or a must-formula.

In what follows, the six workflow net reduction rules presented in Section 4.1 page 68 are reviewed. The restrictions added to the conditions of application, under which it can be applied to a source workflow net N = P, T, F to produce a target workflow net Ñ = P, T , F , are specified with regard to a given extended modal specification formula m.

R 1 : Remove Place

We define φ RemoveP (m) a reduction rule strictly equivalent to the reduction φ RemoveP defined page 69. No further restriction to conditions of application of this rule is required in order to enable it to strongly preserve the (in)validity of the extended modal specification formula m. Indeed, places removed by this reduction rule are redundant places that do not change the executions set of a workflow net.

Theorem 30: Soundness of φ RemoveP (m) φ RemoveP (m) is a workflow net reduction rule which strongly preserves the (in)validity of the extended modal specification formula m interpreted as either a may-formula or a must-formula.

Proof. (Sketch). We proceed by showing that the workflow nets N and Ñ are trace equivalent.

Let f : ( P → N) → (P → N) be a bijective function such that f (M)(g) = M(g) for all g ∈ P and f (M)(p) = M(g 1 ) + .. + M(g n ).

Let l ∈ N and σ = t 1 , .., t l be a transition sequence of size l.

By conditions on N, every transition that produces (resp. consumes) a token in any of the places of G also produces (resp. consumes) a token in p.

It follows that there exists a sequence M 1 , .., M l+1 of l + 1 markings of Ñ such that M 1

t 1 -→ M 2 t 2 -→ .. t l -→ M l+1 is an execution of Ñ if and only if f (M 1 ) t 1 -→ f (M 2 ) t 2 -→ .. t l -→ f (M l+1 ) is an execution of N.
Therefore, the workflow nets N and Ñ are trace equivalent. We can then conclude that

N | = must m ⇔ Ñ | = must m, and N | = may m ⇔ Ñ | = may m.

R 2 : Remove Transition

We define φ RemoveT (m) a reduction rule which further constrains the conditions of application of the φ RemoveT reduction rule defined page 70.

In order to ensure that φ RemoveT (m) strongly preserves the (in)validity of the extended modal specification formula m, interpreted as either a may-formula or a must-formula, one has to make sure that the removed transition is not part of the domain of m (i.e. t Domain(m)). Further, one also has to ensure that {g 1 , .., g n } ∩ Domain(m) = ∅ to guarantee that alternative behaviours including transition of the domain of m are not lost by the application of such a transformation rule.

To this end, the following constraint is added to the conditions of application of the φ RemoveT reduction rule:

t Domain(m) ∧ {g 1 , ..,

g n } ∩ Domain(m) = ∅ Theorem 31: Soundness of φ RemoveT (m)
φ RemoveT (m) is a workflow net reduction rule which strongly preserves the (in)validity of the extended modal specification formula m interpreted as either a may-formula or a must-formula.

Proof. (Sketch). We proceed to show that the workflow nets N and Ñ are weak trace equivalent with respect to the transitions set Domain(m). By condition imposed on N, the firing of transition t is equivalent to the successive firings of the transitions sequence g 1 , .., g n . It follows that the occurrences of t in the executions of N can be replaced by the transitions sequence g 1 , .., g n to form executions of Ñ. R 3 : Remove Self-loop

We define φ RemoveS T (m) a reduction rule which further constrains the conditions of application of the φ RemoveS T reduction rule defined page 72.

In order to ensure that φ RemoveS T (m) strongly preserves the (in)validity of the extended modal specification formula m, interpreted as either a may-formula or a must-formula, one has to make sure that the removed transition is not part of the domain of m (i.e. t Domain(m)).

To this end, the following constraint is added to the conditions of application of the φ RemoveS T reduction rule: t Domain(m)

Theorem 32: Soundness of φ RemoveS T (m)

φ RemoveS T (m) is a workflow net reduction rule which strongly preserves the (in)validity of the extended modal specification formula m interpreted as either a may-formula or a must-formula.

Proof. (Sketch). We proceed by showing that the workflow nets N and Ñ are weak trace equivalent with respect to the transitions set Domain(m).

By condition imposed on N, firing transition t does not change the marking in which it is fired. Therefore any execution of Ñ is also an execution of N. Further, any execution of N where every occurrence of t is removed is an execution of Ñ. As t Domain(m) we can conclude that N and Ñ are weak trace equivalent with respect to the transitions set Domain(m). We define φ RemoveT P (m) a reduction rule which further constrains the conditions of application of the φ RemoveT P reduction rule defined page 73.

In order to ensure that φ RemoveT P (m) strongly preserves the (in)validity of the extended modal specification formula m, interpreted as either a may-formula or a must-formula, one has to ensure that the removed transition is not part of the domain of m (i.e. t Domain(m)).

To this end, the following constraint is added to the conditions of application of the φ RemoveT P reduction rule:

t Domain(m)

Theorem 33: Soundness of φ RemoveT P (m)

φ RemoveT P (m) is a workflow net reduction rule which strongly preserves the (in)validity of the extended modal specification formula m interpreted as either a may-formula or a must-formula.

Proof. (Sketch). As before, we show that the workflow nets N and Ñ are weak trace equivalent with respect to the transitions set Domain(m).

By construction of Ñ, ∀ i ∈ {1, .., n 3 }, the firing of ot i in Ñ is equivalent to the firing of t, ot i in N.

Therefore any execution of Ñ where, for every i ∈ {1, .., n 3 }, every occurrence of ot i is replaced by the transitions sequence t, ot i , is an execution of N. Further, any execution of N where every occurrence of t is removed is an execution of Ñ. As t Domain(m), we can conclude that N and Ñ are weak trace equivalent with respect to the transitions set Domain(m). We define φ RemovePT a reduction rule which further constrains the conditions of application of the φ RemovePT reduction rule defined page 74.

It follows that

Similarly to the constraint added to φ RemoveT P to define φ RemoveT P (m), to ensure that φ RemovePT (m) strongly preserves the (in)validity of the extended modal specification formula m, interpreted as either a may-formula or a must-formula, one has to make sure that the removed transition is not part of the domain of m (i.e. t Domain(m)).

To this end, the following constraint is added to the conditions of application of the φ RemovePT reduction rule: t Domain(m)

Theorem 34: Soundness of φ RemovePT (m)

φ RemovePT (m) is a workflow net reduction rule which strongly preserves the (in)validity of the extended modal specification formula m interpreted as either a may-formula or a must-formula.

Proof. (Sketch). Similarly to previous proofs, we show that the workflow nets N and Ñ are weak trace equivalent with respect to the transitions set Domain(m).

By construction of Ñ, ∀ i ∈ {1, .., n 3 }, the firing of it i in Ñ is equivalent to the firing of it i , t in N.

Therefore any execution of Ñ where, for every i ∈ {1, .., n 3 }, every occurrence of it i is replaced by the transitions sequence it i , t, is an execution of N. Further, any execution of N where every occurrence of t is removed is an execution of Ñ. As t Domain(m), we can conclude that N and Ñ are weak trace equivalent with respect to the transitions set Domain(m). In order to ensure that φ RemoveR (m) strongly preserves the (in)validity of the extended modal specification formula m, interpreted as either a may-formula or a must-formula, one has to make sure that none of the removed transitions (i.e. the transitions of the ring) is part of the domain of m (i.e. {t 1 , .., t m } ∩ Domain(m) = ∅).

It follows that

To this end, the following constraint is added to the conditions of application of the φ RemovePT reduction rule:

{t 1 , .., t m } ∩ Domain(m) = ∅ Theorem 35: Soundness of φ RemoveR (m)
φ RemoveR (m) is a workflow net reduction rule which strongly preserves the (in)validity of the extended modal specification formula m interpreted as either a may-formula or a must-formula.

Proof. (Sketch). As previously, we proceed by showing that the workflow nets N and Ñ are weak trace equivalent with respect to the transitions set Domain(m).

By condition imposed on N, every execution of N where occurrences of the transitions t 1 , .., t m are removed is also an execution of Ñ. Further, every execution of Ñ where occurrences of a transition t ∈ outT are replaced by the transition sequence seq, t, where seq is a sequence of transitions involving transitions of the ring such that it enables t, is an execution of N. As We can conclude that, given an extended modal specification formula m, the reduction kit Φ * (m) defined in this section can be used as a pre-processing step toward the verification of the extended modal specification formula m interpreted as either a may-formula or a must-formula. Indeed, beside reducing the size of the workflow net to be analysed, this pre-processing step provides useful diagnostic information in the form of an irreducible graph.

Furthermore, note that the reduction rules of Φ * (m) preserve weak trace equivalence with respect to the transitions set Domain(m). They are therefore also candidate to a pre-processing step toward the verification of other behavioural properties (e.g., LTL on traces [Westergaard, 2011], CTL on traces) expressed over Domain(m).

4.4/ Synthesis

This chapter presented reduction methods -abstraction methods -that have the ability to reduce the size of workflow nets while strongly preserving properties of interest.

It first presented six reduction rules generalising existing reduction rules defined by previous work [Berthelot, 1987, Murata, 1989, Sloan et al., 1996, Voorhoeve et al., 1997, Sadiq et al., 2000, Lin et al., 2002, Desel et al., 2005, Hichami et al., 2014]. It is proven that these reduction rules strongly preserve generalised soundness over workflows nets, an essential and necessary correctness property that must be satisfied by workflow nets.

Based on the definition of these reduction rules, a generalised soundness semi-decision is then described. It notably showed that, despite not being complete, this procedure, whenever unable to conclude, can be used as a pre-processing step toward verification of generalised soundness. Indeed, by reducing the size of the analysed workflow nets, this procedure can enhance conventional generalised soundness verification methods.

Finally, two reduction methods preserving the (in)validity of a given extended modal specification formula interpreted as either a may-formula or a must-formula are described. The first of these method -based on the hierarchical representation of workflow nets -aims at abstracting unnecessary layers of detail. The second method is based on the six reduction rules previously presented. Both reduction methods were proved to be sound. Thanks to the potential size reduction they provide, these reduction methods constitute pre-processing steps for extended modal specifications verification approaches (e.g., the one presented in Section 3.1.3 page 53).

Now that the theoretical contributions of this thesis have been described, the following chapter presents the tools that have been implemented as well as experimentations that have been carried out over industrial workflow nets in order to validate the approaches introduced in this chapter and the previous one. This chapter describes experimental results obtained in order to assess the value of the contributions presented previously as well as the tools developed to support the proposed approach. The first section introduces study cases (i.e. real-life examples) which highlight and motivate the use of workflow nets and extended modal specifications. The second section describes the dedicated tool chain implemented to carry out the verification of extended modal specifications according to the approach presented in Section 3.1.3 page 53 as well as the reduction procedures of workflow nets presented in Sections 4.2 page 77 and 4.3 page 79. The third section exposes and discusses experimental results obtained over the study cases presented in the first section. The fourth section has for objective to demonstrate the scalability of the proposed approaches over workflow nets of growing size and complexity. It first describes a workflow nets benchmarks generation tool able to produce large benchmarks of workflow nets of growing size and complexity together with their (in)valid extended modal specifications. It then proceeds to expose and discuss experimental results obtained over such benchmarks before providing an experimental evaluation of the effectiveness and scalability of the reduction methods proposed in Sections 4.2 page 77 and 4.3 page 79. Finally, as a conclusion, major results are summarised.

5.1/ Study Cases

This section presents the three study cases considered during this thesis to validate and evaluate the extended modal specification verification approach described in Chapter 3 page 43. These three study cases are real-life examples of industrial workflows obtained through collaboration with industrial actors.

5.1.1/ Issue Tracking System

The first study case concerns a proprietary issue tracking system used to manage bugs and issues requested by the customers of a tool provider company 1 .

General Description

This issue tracking system enables the provider to create, update and drop tickets reporting on customer's issues, and thus provides knowledge base containing problem definition, information about customer's environment, improvements and solutions to common problems, request status, request priority, and other relevant data needed to efficiently manage all the company projects. It must also be compliant with respect to several rules ensuring that business processes are suitable as well as streamlined, and implement best practices to increase management effectiveness.

Modelling

Figure 5.1 depicts an excerpt of the corresponding business process-specified from textual requirements by a business analyst team of the company-modelled using a Petri net workflow.

Note that this workflow was first designed using the BPMN Standard [White, 2004] and has been transformed into a hierarchical workflow net following [START_REF] Raedts | Transformation of bpmn models for behaviour analysis[END_REF]'s approach.

Figure 5.1: Excerpt of issue tracking system workflow net 1 For confidentiality reasons, some details about this case-study are not given.

The main process, in the top left model, is defined by two possible distinct scenarii (SubA and SubB), which are described by two other workflow nets. In the figure, big rectangles (as for SubA and SubB) define other workflow nets. Some of them are not presented here: this example is indeed deliberately simplified and abstracted to allow its small and easily understandable presentation; its complete and fully detailed workflow net is composed of 165 places and 204 transitions.

Requirements

This industrial business workflow is directly driven by the need to verify some behavioural properties possibly at the early stage of development life cycle, before going to implementation.

For this business process, the goal is to verify, at the specification or design stage of the development, some required behavioural properties, derived from textual requirements and business analyst expertise. Such properties are presented in Table 5.1 and denoted p i for later references.

# Property p 1 During a session, either the scenario SubA or the scenario SubB (and not both of them) must be executed p 2 When the scenario SubB is considered then the user must login p 3 Once a critical situation request is pending, it can either be updated, validated and dispatched, or closed p 4 Once a critical situation is created, it can be updated and closed p 5 At any time, a service request can be upgraded to a critical situation request p 6 A logged user must logout to exit the current session Table 5.1: Issue tracking system requirements To ensure the specified business process model verifies this kind of business rules, there is a need to express and assess them using modal specifications. It should be noted that usual modal specification are relevant to express properties on single transition by specifying that a transition shall be a (necessary) must-transition or a (admissible) may-transition. However, they do not allow to express requirements on several transitions. For instance, expressing the property p 1 using usual modal specification allows us to specify that transitions of SubA and SubB shall be may-transitions. Nevertheless, such formula does not ensure that SubA or SubB has to occur in an exclusive manner, and specifying some transitions as must-transition cannot tackle this imprecision. This kind of properties highlights the expressive limitation of usual modal specifications and has motivated the definition of extended modal specifications as introduced in Section 3.1.1 page 44. Indeed, by expressing behavioural properties over several transitions and their causalities, extended modal specifications are able to effectively describe such properties.

5.1.2/ Question and Answer Portal

The second study case concerns a business process workflow of a Question and Answer portal, which is a part of a proprietary issue tracking system considered in Section 5.1.1.

General Description

This Question and Answer portal allows company's customers to ask questions that are then answered by the company's sellers. To use the system, new users (e.g., new employee, new client) have to be registered. Three types of users can log-in: clients, sellers and administrators. The clients can ask questions. These questions are then answered by sellers. Once the answer to a question has been validated by the client who asked it, the administrator archives the question. An execution of the workflow is complete once all users have been logged-out and unregistered.

Modelling

We present one of the several refinements of the workflow modelled by a coloured workflow net. For clarity, this coloured workflow net is described by several coloured sub-workflow nets (Figures 5.2,5.3(a),5.3(b),5.3(c),and 5.3(d)). In these figures, places with the same name denote the same entities: for instance, place HomeQA in Figure 5. In this refinement, the following three colours are considered:

-U = {u 1 , .., u t }, a set of t user names representing the different users of the system; -R = {client, seller, admin}, a set of roles, which are assigned to users; -Q = {unanswered, answered, validated}, a set of question statuses. 5.2 shows the colours associated with places of the Question and Answer coloured workflow net, and Tab. 5.3 shows the colours, inputs, outputs and guards (u, u 1 , u 2 ∈ U, r ∈ R, q ∈ Q).

Colours

Places

U i, o U × R P 0 , Home, HomeQA, HomeS R U × R × Q × U DisplayQ, DisplayA, P 1 , P 3 Q × U Questions
Register U × R u (u, r) T rue UnRegister U × R (u, r) u T rue Login, Logout U × R (u, r) (u, r) T rue HomeT oQA U × R (u, r) (u, r) T rue QAtoHome U × R (u, r) (u, r) T rue HomeT oS R U × R (u, r) (u, r) T rue S RtoHome U × R (u, r) (u, r) T rue CreateQ U × R (u, r) (u, r, unanswered , u) r = client EditQ U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r, q, u 2 ) T rue CommitQ U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r) and (q, u 2 ) T rue S electQ U × R × Q × U (u 1 , r) and (q, u 2 ) (u, r, q, u) T rue CreateA U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r, answered , u 2 ) r = seller ∧ q = unanswered EditA U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r, q, u 2 ) T rue CommitA U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r) and (q, u 2 ) T rue ViewA U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r, q, u 2 ) u 1 = u 2 ∧ q = answered AcceptA U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r) and ( validated , u 2 ) T rue Re f useA U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r) and ( unanswered , u 2 ) T rue ArchiveQA U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r) r = admin ∧ q = validated BackT oHome U × R × Q × U (u 1 , r, q, u 2 ) (u 1 , r) and (q, u 2 ) T rue
Table 5.3: Colours, inputs, outputs, and guards of Question and Answer coloured workflow net's transitions

An execution of the Question and Answer coloured workflow net begins with at least three users (one client, one seller, and one administrator) and is complete once all users have been logged-out and unregistered. To illustrate how this coloured workflow net works, let us consider the following execution with u 1 , u 2 and u 3 as initial marking: each user is registered, then he/she logs in and navigates to the QA's Home (Figure 5.2):

-

Register(u 1 , client), Login(u 1 , client), HomeT oQA(u 1 , client)
-Register(u 2 , seller), Login(u 2 , seller), HomeT oQA(u 2 , seller)

-Register(u 3 , admin), Login(u 3 , admin), HomeT oQA(u 3 , admin)

The client creates a new question (Figure 5.3(a)):

-

CreateQ(u 1 , client), CommitQ(u 1 , client, unanswered, u 1 )
The seller selects the question and the answer (Figure 5.3(b)):

-S electQ(u 2 , seller, unanswered, u 1 ), CreateA(u 2 , seller, unanswered, u 1 )

-CommitA(u 2 , seller, answered, u 1 )

The client selects the question, reads the answer and validates (Figure 5.3(c)):

-S electQ(u 1 , client, answered, u 1 ), ViewA(u 1 , client, answered, u 1 ) -AcceptA(u 1 , client, answered, u 1 )
The administrator selects the question and archives it (Figure 5.3(d)):

-S electQ(u 3 , admin, validated, u 1 ),ArchiveQA(u 3 , admin, validated, u 1 )

The users navigate to Home and then log-out and are unregistered (Figure 5.2):

-

QAtoHome(u 1 , client), Logout(u 1 , client) UnRegister(u 1 , client) -QAtoHome(u 3 , seller), Logout(u 3 , seller) UnRegister(u 2 , seller)
-QAtoHome(u 3 , admin), Logout(u 3 , admin) UnRegister(u 3 , admin)

Requirements

Regarding this business process, the goal is to verify, at the specification or design stage of the development, some required behavioural properties derived from textual requirements and business analyst expertise.

The considered behavioural properties, denoted p i for later references are presented in Table 5.4.

Let us, one more time, emphasize that these properties could not be expressed by usual modal specifications as they involve several transitions as well as constraint over data and the initial states. This is why they have also motivated the definition of extended modal specifications as introduced in Section 3.2.2 page 59. # Property p 7 All users must register p 8 An admin may view an answer p 9 A client may create a question and refuse the answer p 10 When a client asks a question it must be answered and archived p 11 A client must not answer a question p 12 There may be an user who asks a question while another does not p 13 If there is less than three users, no question is asked p 14 If a question is asked then the system must have registered a client, a seller and an administrator Table 5.4: Question and Answer portal requirements

5.1.3/ Tax Accounting Manager

The third study case deals with a system to manage tax accounting. It is inspired by a real-life system that provides dependable, automated, efficient and integrated services to more than 400 tax municipalities and more than 3000 users.

Description

This tax accounting manager is huge and handles a vast amount of tax processes which can be, at the early stage of development life cycle, described by workflows in order to specify and to verify some behavioural properties of the payout process before going to implementation.

The payout process handles credit claims (i.e. notes issued when the tax department owes money to a taxpayer). It is composed of three sub-processes, namely, the approval process, the payout form generation process, and the payout process.

It proceeds as follows. Firstly, a credit claim must be approved. Its approbation may need two levels of approval, which can be either manual or automatic depending on the properties of the claim. Secondly, a suggested payout form is generated. It may then be corrected by a tax processor and, if corrected, it must be verified again. Once approved the payout form is sent to the bank which responds with a receipt. The receipt is then handled by a tax processor. Although this payout process is only a small portion of the whole system, its workflow is a representative example as it illustrates a real-life process of high importance. The approval process workflow must be refined to specify the property that any credit claim must be approved before being treated. To this end, two colors are defined:

Modelling

-C 1 = {lvl0, lvl1, lvl2, lvl12, approved}, a set of levels required to approve a claim -C 2 = C 1 × C 1 , a set of 2-uple whose first element represents the level required to approve the claim, and whose second element represents the actual level of the claim approval The colour C 2 is assigned to places i, P 1 , P 2 and P 3 , as well as to transitions requestApproval 1/2 , ManualApproval 1/2 , AutomaticApproval 1/2 and suggestPayoutForm. A form is suggested if and only if the credit claim has been approved at the required level(s) as described in Tab. 5.5.

Transition Instance Pre

Post

requestApproval 1 lvl1 (lvl1, lvl0) (lvl1, lvl0) lvl12 (lvl12, lvl0) (lvl12, lvl0) requestApproval 2 lvl2 (lvl2, lvl0) (lvl2, lvl0) lvl12 (lvl12, lvl1) (lvl12, lvl1) (Manual/Automatic)Approval 1 lvl1 (lvl1, lvl0) (lvl1, approved) ManualApproval 1 lvl12 (lvl12, lvl0) (lvl12, lvl1) (Manual/Automatic)Approval 2 lvl2 (lvl2, lvl0) (lvl2, approved) lvl12 (lvl12, lvl1) (lvl12, approved) suggestPayoutForm lvl x (lvl x , approved) (lvl x , approved)
Table 5.5: Function associated with transitions of the Payout Process (Figure 5.4)

Moreover, some properties of interest for this system require performance measures of the mean cost of executions. To this end, weights representing the mean cost of the activities are associated with transitions to constitute a weighted transitions Petri net (Section 2.1.5.3 page 21). This defines a price weight function, that assigns to any transition instance an amount of units needed to perform it. It is a weight function defined in the framework where C is the set of integers, and C is the summation of elements of a set. The total weight cost of a correct execution represents the total amount of units needed to perform it. In this study case context, the units in question are unit of money which represents the cost of the considered activity. The total weight of an execution represents the amount of money needed to perform it. Table 5.6 gives the mean cost in tenth of a Euro associated with transitions of the payout process. We suppose this mean cost uniform for all instances of the same transition.

We observe that automated treatments have a low mean cost while other activities, like manual approval and correction, have a significantly higher mean cost.

Requirements

This payout process is a component of a larger process, which requires valid activities with respect to a specification. Notably, under certain conditions, some activities may be admissible, while some shall be necessary.

Regarding this business process, the goal is to verify, at the specification or design stage of the development, some required behavioural properties, derived from textual requirements and analyst expertise. Denoted p i for later references, the properties presented in Table 5.7 are considered.

#

Property p 15 credits claims must be approved p 16 a payout form may be corrected p 17 if a payout form is corrected, it must be verified p 18 a payout form may be corrected three times p 19 getting a receipt from the bank is necessary p 20 any claim that requires two levels of approval requires a manual approval level 1 p 21 the treatment of a credit claim may have a mean cost of less than 30 Euros p 22 When restricting to three the number of corrections of a payout form, the cost of a credits claims treatment must not exceed a mean cost of 200 Euros Table 5.7: Payout Process requirements

We can see that those properties all express either admissible or necessary behaviours. To ensure that the specified business process model verifies this kind of business rules, there is a need to express and assess them using modal specifications. In the context of Petri net based workflow modelling, usual modal specifications are relevant to express properties on a single transition, i.e an activity, by specifying that a transition shall be a (necessary) must-transition or a (admissible) may-transition. However, they do not allow neither expressing requirements on several transitions, nor the requirements conditioned by characteristics on the treated cases, nor the requirements containing performance indicators of the process executions. For instance, the property p 17 involves distinct activities, its definition within usual modal specification over a single transition is not possible. We can also see that the property p 20 has a condition on the credit claims characteristics, whereas the properties p 21 to p 22 have restrictions on cost performance characteristics of the process executions.

However, like the properties of the previous study case covering the Question and Answer portal, these properties can be expressed by the extended modal specifications framework presented in Section 3.2.2 page 59. Moreover, they have motivated its definition over workflows described as coloured workflow nets extended by quantitative performance specification.

5.2/ Tool Chain Implementation

This section describes the tool chain developed to experimentally validate this thesis proposals, and notably illustrates its use on the three study cases presented in the previous section.

The first part of this section presents an extended modal specification verifier implementation based on the modelling approach described in Chapter 3 page 43. The second part presents an implementation of a reduction tool preserving generalised soundness of workflow nets based on the reduction rules described in Section 4.1 page 68. This reduction tool also enables the user to preserve the (in)validity of a given modal specification interpreted as a must-formula or a mayformula following the approach described in Section 4.3 page 79.

5.2.1/ Modal Specification Verifier

The approach proposed in Chapter 3 page 43 has been fully automated, allowing practitioners, at any stage of the workflow design and validation, to verify modal properties using an integrated tool chain. First, a workflow net and an extended modal specification formula are given as inputs to the verification software (1). Both models conform to an ad-hoc standard, i.e. a dedicated meta-model, so that all information needed by the verification tool is provided. Note that this implementation also supports input workflow nets model formatted by the PNML standard [START_REF] Hillah | Pnml framework: An extendable reference implementation of the petri net markup language[END_REF]]a generic Petri nets XML format -allowing the use of workflow nets exported from a third party software (e.g., Yasper [van Hee et al., 2006a], PIPE [START_REF] Bonet | PIPE v2.5: A Petri net tool for performance modelling[END_REF]).

We have also developed a graphical coloured workflow nets editor created within the Sirius framework 2 , which is an EMF-based open source project to create customized graphical modelling workbench by leveraging Eclipse Modelling technologies. Basically, it provides a generic workbench for model-based architecture engineering that could be easily tailored to fit the specific needs of a given Domain Specific Language, e.g., coloured workflow nets in our context. Hence the developed coloured workflow nets editor allows producing an XML file, corresponding to the designed coloured workflow net models, that can be used as input file of the tool chain.

Afterwards, the two code generators use the information provided by the input workflow and the input modal specification (1) to generate the code corresponding to the constraint system defined in Section 3.1.3 page 53. Such codes are expressed in the input format of the targeted constraint solver (2): SMT-Lib for Z3 [De Moura et al., 2008] version 4.4.0, an SMT solver, and SICStus Prolog [Carlsson et al., 2012] version 4.3.2, a CLP solver (that includes a CLP(FD) library).

Both solvers were selected for their proven efficiency: Z3 finished first during the 2014 SMT-COMP challenge [START_REF] Barrett | Smt-comp: Satisfiability modulo theories competition[END_REF] for solving non-linear arithmetic problems and SICStus obtained the third place during the 2014 MiniZinc challenge [START_REF] Stuckey | The minizinc challenge 2008-2013[END_REF].

Next, to verify a may-formula (resp. a must-formula) m, the tool first checks if there exists a solution of the over-approximation, given by the constraint system Q(N, M i , M o ) (Definition 37 page 49), such that the modelled execution satisfies (resp. does not satisfy) m. If such an execution exists, it then tries to find an execution of the under-approximation, given by the constraint system V(N, k, m) (resp. V(N, K, m)) of the Definition 40 page 53.

The function checking the validity of a must-formula is given by Algorithm 5. In this algorithm, S AT (CS ) is defined as the boolean function returning the satisfiability of the constraint system CS and GET MODEL(CS ) is a function returning a valuation function satisfying the constraint system CS . This algorithm returns the K-bounded validity of a given modal formula m. To cope with the complexity raised by K max , K can be fixed to a manageable value. Nevertheless, when fixing K to K max (or greater than K max ), the algorithm enables to decide the unbounded validity of the must-formula m. The results introduced in Chapter 3 ensure its soundness and completeness.

Finally, once the verification algorithm has been applied through queries to the related solver with the generated code to determine the validity of the modal specification (3), a report is produced (4). This report states the verdict about the validity of the modal specifications as well as the verification time.

Let us point out that, using SICStus, no particular labelling heuristic was found to significantly improve results. Therefore all the experiments have been conducted with the default ones ([leftmost, step, up]). However, using Z3, since the SMT tactic improved all results, this strategy has been systematically used.

The two following subsections respectively illustrate the code generation process (2) and discuss the issue of representing infinite domains.

On Code Generation

To illustrate the code generation process within this tool chain, let us consider the ordinary workflow net N = (P, T, F) depicted in Figure 5.6. Let n ∈ P ∪ T , we use the following conventions: An stands for M a (n), Bn for M b (n), Pn for ν(n) when n is a place, Tn stands for ν(n) when n is a transition, and Xn stands for ξ(n), M1n, M2n and M3n stand for M 1 (n), M 2 (n) and M 3 (n). For example, Tt2 and M2p1 respectively denote ν(t2) and M 2 (p1).

The initialMarking and finalMarking predicates are used to respectively constrain the initial and

Data: N -a WF-net, m -a must-formula, K a positive integer Result: T RUE -PN | = must m, FALS E -PN must m if S AT (Q(N, M i , M o ) ∧ C(N, ¬m)) then v = GET MODEL(Q(N, M i , M o ) ∧ C(N, ¬m)); k = max({v(n)|n ∈ T }); if k == 1 then return FALS E; else while k ≤ K do if S AT (V(N, k, ¬m)) then return FALS E; else k = k + 1; end end end else
return T RUE; end Algorithm 5: Algorithm checking the validity of a must-formula 48) is constructed through the use of the predicate subnetInit. The predicate siphon models the constraint system of Definition 12 page 49 and is used to determine the presence of a siphon in a workflow net. Based on a solution of the sta-teEquationpredicate, the noShiphon predicate ensures the absence of siphon within the subnet of the considered state equation valuation. It follows that together the stateEquation and noShiphon predicates define a predicate segment corresponding to the constraint system modelling segment of executions of the considered workflow net as defined by Definition 37 page 49.

Both solvers give the following interpretation for the three segments: M1i = 1 , M1o = 0 , M1p1 = 0 , M2i = 0 , M2o = 0 , M2p1 = 1 , M3i = 0 , M3o = 0 , M3p1 = 1 , M4i = 0 , M4o = 1 , M4p1 = 0 , P1i = 1 , P1o = 0 , P1p1 = 1 , P2i = 0 , P2o = 0 , P2p1 = 2 , P3i = 0 , P3o = 1 , P3p1 = 1 , T1t1 = 1 , T1t2 = 0 , T1t3 = 0 , T2t1 = 0 , T2t2 = 1 , T2t3 = 0 , 3 t 1 = 0 , T3t2 = 0 , T3t3 = 1

These segments are given in Figure 5.10, starting (resp. ending) in the initial (resp. final) marking where only the input place i (resp. output place o) is marked. Let us note that modellers often use, in the context of coloured workflow nets development, infinite colours (e.g., strings, integers) to represent data (e.g., usernames of a system, identifiers of files), even if these data are usually not directly manipulated by the control flow. However, coloured workflow nets with infinite colours cannot be directly handled due to the nature of the constraint solvers over finite domains.

Fortunately, abstraction techniques help to tackle the problem entailed by this restriction and can therefore cope with infinite colours. Among well-known abstraction techniques, [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF] proposes an algorithm to construct a finite state abstract program from a given, possibly infinite, state program (e.g., a coloured workflow net) by means of a syntactic program transformation starting with an initial set of predicates from a specification (e.g., modal specification). This method is shown to be sound (the abstract program is always guaranteed to simulate the original one) and complete (the algorithm can produce a finite simulation-equivalent, resp. bisimulation-equivalent, abstract program if the concrete program has a finite abstraction with respect to simulation, resp. bisimulation, equivalence). On the one hand, in the case of a bisimulation-equivalent abstract program, the abstracted modal specification can be verified using our method, and the (in)validity of the modal specification can be directly inferred. On the other hand, for simulation-equivalent abstract program, only the validity of a may-formula and the invalidity of a must-formula can be inferred.

To handle infinite colours, another approach is to consider only a finite number of data of an infinite colour according to control-flow selection criteria (e.g., decision or condition coverage) [START_REF] Vilkomir | Formalization of software testing criteria using the Z notation[END_REF]. However, this approach is not complete, it only provides a certain level of confidence in the validity or the invalidity of modal specifications depending on the applied selection criterion.

5.2.2/ Reduction Tool

This section presents an implementation of a reduction tool preserving generalised soundness of workflow nets based on the reduction rules described in Section 4.1 page 68 . It notably implements the procedure described by Algorithm 2 of Section 4.2 and has also the ability to reduce workflow nets while preserving the (in)validity of a given modal specification interpreted as a must-formula or a may-formula by following the approach described in Section 4. This tool takes as input a workflow net (2), saved as an XML file and conform to an ad-hoc and proprietary standard -a dedicated meta-model -or to the PNML standard [START_REF] Hillah | Pnml framework: An extendable reference implementation of the petri net markup language[END_REF]] -a generic Petri nets XML format -so that third party editor can be used (e.g., Yasper [van Hee et al., 2006a], PIPE [START_REF] Bonet | PIPE v2.5: A Petri net tool for performance modelling[END_REF]). It also, possibly, takes as input a modal specification formula (1) conform to an ad-hoc and proprietary XML standard.

The workflow net reducer (3) then tries to apply any of the six reduction rules presented in Section 4.1 page 68 to the input workflow net until a fix-point (i.e. none of the reduction rules can be applied) is reached. If an input modal specification formula has been provided, it instead applies the six restricted reduction rules given in Section 4.3 page 79.

Once the computation is completed, whenever the generalised soundness verification is inconclusive (i.e. the input workflow net could not be completely reduced) or when an input modal specification formula has been provided, this tool produces a reduced workflow net ( 4) which can then be further analysed. Finally, this tool provides a result report containing the status of the verification of the generalised soundness and metrics about the execution time and the number of times the rules have been applied.

In order to ease and foster its use, this tool features a web interface available online4 .

Figure 5.12 shows, as an example, the web interface output of the execution of Hadara-AdSimul-Red when applied to an industrial workflow net in order to determine its generalised soundness.

Information and graphic representations of the original and reduced workflow nets can respectively be seen at the left and right of a central frame displaying the required reduction time, the status of the generalised soundness verification as well as the reduction factor obtained. The following two sections present experimental results obtained by using the tools introduced in this section and the previous. The first one exposes and discusses results obtained over the study cases presented in Section 5.1. The second section presents and discusses, in a first step, an experimental evaluation of the scalability of the proposed extended modal specifications and supporting tool chain over generated benchmarks. In a second step, it introduces an experimental evaluation of the effectiveness and scalability of the reduction approaches implemented by the tool described in this section.

5.3/ Study cases results

For each study case the modal specifications of interest presented in Section 5.1 have been verified using the dedicated modal specification verification tool presented in Section 5.2. The obtained results are presented in this section. Additionally, this section is concluded by a synthesis of the lessons learnt from these results.

Issue Tracking System

We consider the issue tracking system used to manage bugs and issues requested by the customers of a tool provider company. In Section 5.1.1, this study case is presented and six required behavioural properties, denoted p 1 , .., p 6 , are introduced in Table 5.1 page 91. These behavioural properties have been expressed using extended modal specifications (Section 3.1.1 page 44).

Table 5.8 shows the modal specification formulae associated with each behavioural property as well as the experimental results obtained on this industrial example. The modal may-formula (resp. must-formula) m associated with each property is specified, and the result of the computation is given by its final result as well as the internal evaluation of the over-approximation

ϕ = Q(N, M i , M o ) ∧ C(N, m) (resp. ϕ = Q(N, M i , M o ) ∧ C(N, ¬m
)), the constraint system defined in Definition 37 page 49. The input K and the corresponding computed value of φ(K) = V(N, K, m) (resp. φ(K) = V(N, K, ¬m)), the constraint system defined in Definition 40 page 53, are also stated when the algorithm cannot conclude without this bound. The properties p 1 to p 6 are representa- tive of the kind of properties that have to be verified by engineers when they design the business process to be implemented. Moreover, these properties are sufficiently clear without a complete description of the workflow and enable to show all possible outcomes of our approach.

# Formula ϕ K φ(K) Result p 1 IT S | = must (S ubA ∧ ¬S ubA) ∨ (S ubB ∧ ¬S ubA) TRUE - - TRUE p 2 IT S | = must S R S electData ⇒ Login TRUE - - TRUE p 3 IT S | = must S R CreateCRIT S IT ⇒ (VandD ∨ U pdate ∨ Closure) TRUE - - TRUE p 4 IT S | = may S R CreateCRIT S IT ⇒ (U pdate ∧ Closure) FALSE - - FALSE p 5 IT S | = may S R U pgradeT oCRIT S IT TRUE 1 FALSE FALSE 6 TRUE TRUE p 6 IT S | = must Login ⇒ Logout FALSE 1 FALSE FALSE
We observe that on the one hand, when verifying must-formulae that are satisfied by the considered workflow net (see p 1 , p 2 and p 3 ), or may-formulae that are not satisfied by the workflow net (see p 4 ), the over-approximation proposed in Definition 37 is usually sufficient to conclude. On the other hand, when verifying may-formulae that are satisfied by the workflow net (see p 5 ), or mustformulae that are not satisfied by the workflow net (see p 6 ), the decomposition into K segments is needed. We empirically demonstrate that this decomposition is very effective since values of K max are usually moderate (K max = 6 in the case of p 5 , less than 10 with all the experimentations on this case-study). We can also notice the definitive invalidity of p 6 (a user can exit the current session without logout), which enabled to highlight an ambiguity in the textual requirements.

On the basis of the experiments performed on this study case and related results, we can conclude that the proposed method is feasible and effective. Furthermore, regarding efficiency, it should be noted that the developed tool is able to conclude about the (in)validity of the studied properties in a very short time (less than a second).

Question and Answer Portal

We now consider the business process workflow of a Question and Answer portal. In Section 5.1.2 page 91, this study case is presented and eight required behavioural properties, denoted p 7 , .., p 14 , are introduced in Table 5.4 page 95. These behavioural properties have been expressed using abstract extended modal specifications (Section 3.2.2 page 59) considering both initial states and transition instances.

Table 5.9 shows the abstract modal formula associated with each behavioural property as well as the experimental results obtained on this industrial example. The modal may-formula (resp. mustformula) m associated with each property is specified, and the result of the computation is given by its final result as well as the internal evaluation of the over-approximation

ϕ = Q a (N, M i , M o ) ∧ C(N, m) (resp. ϕ = Q a (N, M i , M o ) ∧ C(N, ¬m)).
The input K and the corresponding computed value of φ(K) = V a (N, K, m) (resp. φ(K) = V a (N, K, ¬m)) are also stated when it makes sense, i.e. when the algorithm cannot conclude without this bound. Table 5.9: Question and Answer Portal: Experimentation results Since the properties have initially been defined by the business analysts involved in the project, we assume that they are representative of properties that should be verified by engineers when they design and implement such business processes. Furthermore, the obtained verification results have been shared and discussed with them.

As for the previous study case, on the one hand, we observe that when verifying must-formulae that are satisfied by the coloured workflow net (e.g., p 7 , p 10 ), or may-formulae that are not satisfied by the coloured workflow net (e.g., p 8 ), the over-approximation is usually sufficient to conclude. On the other hand, when verifying may-formulae that are satisfied by the coloured workflow net (e.g., p 9 ), or must-formulae that are not satisfied by the coloured workflow net, the decomposition into K segments is needed. We empirically show that this decomposition is very effective since values of K max are usually moderate (K max = 12 for p 6 , less than 30 on all the experiments conducted on this case study).

Thanks to the experiments conducted on this study case, we can conclude that the proposed method is effective and efficient over coloured workflow nets, and can therefore gain benefits within business process design and verification. Notably, regarding efficiency, these experiments have highlighted once more that the approach is able to conclude about the (in)validity of the studied properties in a very short time (less than 5 seconds using SICStus Prolog).

Tax Accounting Manager

We consider the business process workflow of a Tax Accounting Manager. In Section 5.1.3 page 95, this study case is presented and eight required behavioural properties, denoted p 15 , .., p 22 , are introduced in Table 5.7. These behavioural properties have been expressed using abstract extended modal specifications (Section 3.2.2 page 59) considering both initial states and transition instances together with performance indicators, a new feature. Table 5.10 shows the abstract modal formula associated with each behavioural property as well as the experimental results obtained on this industrial example. The modal may-formula (resp. mustformula) m associated with each property is specified, and the result of the computation is given by its final result as well as the internal evaluation of the over-approximation ϕ

= Q a (N, M i , M o ) ∧ C(N, m) (resp. ϕ = Q a (N, M i , M o ) ∧ C(N, ¬m)).
The input K and the corresponding computed value of φ(K) = V a (N, K, m) (resp. φ(K) = V a (N, K, ¬m)) are also stated when it makes sense, i.e. when the algorithm cannot conclude without this bound. We note here that property p 22 , which expresses necessities, is transformed into a may-formula with the negation of the weight constraint imposed on it. It follows that the result of the validity of this property is the negation of the validity of the may-formula. In a similar way to the precedent study cases, we have experimentally demonstrated that verifying must-formulae that are satisfied by the coloured workflow net, or may-formulae that are not satisfied by the coloured workflow net, does not usually require segment decomposition. The verification is therefore very efficient as only the over-approximation is required. On the contrary, verifying may-formulae that are satisfied by the coloured workflow net (e.g., p 16 ), or must-formulae that are not satisfied by the coloured workflow net, does require the decomposition into K segments. Nevertheless, we have empirically shown that this decomposition is also effective and very efficient in the context of coloured workflow nets extended with weight functions since values of K are also moderate (less than 10), and efficiently handled by the constraint solver (solved in less than 5 seconds using SICStus Prolog).

# Formula ϕ K φ(K) Result p 15 T AM | = must true, true, AutomaticApproval 1 [d > 0] TRUE - - TRUE ∨AutomaticApproval 2 [d > 0] ∨ ManualApproval 1 [d > 0] ∨ManualApproval 1 [d > 0]

Synthesis

The results gathered over these three study cases allow us to conclude that the presented extended modal specification verification over workflows described as workflow nets possibly extended by data and performance indicators is effective and efficient.

They notably highlight the appropriate use of over-approximations for verifying must-formulae that are satisfied by the workflow net, or may-formulae that are not satisfied by the workflow net.

Using constraint systems satisfiability to check the validity of extended modal specifications enables the usage of efficient constraint solvers to support the verification of workflow nets against extended modal specifications. Moreover, we showed that this method is still valuable when extending modal specifications with data and/or weights.

Indeed, thanks to the experiments conducted using the dedicated tool chain relying on powerful solvers, we can conclude that the proposed method is suitable and helpful, and can therefore gain benefits within business process design and verification. Furthermore, these experiments permitted to demonstrate that the developed tooling is able to conclude about the (in)validity of the studied properties in a very short time.

The promising results obtained over real-life industrial case studies prompted a more broader evaluation to precisely measure the efficiency of this approach over large scale models. To reach this goal, the next section aims at providing an in-depth evaluation in order to assess the scalability of the proposed modal specification verification method over large benchmarks composed of workflow nets of growing size and complexity.

5.4/ Scalability

In a first step, this section presents and discusses an empirical evaluation of the scalability of the verification of extended modal specifications over workflow nets according to the verification approach defined in Chapter 3 page 43. To this end, a workflow nets generation tool, able to produce workflow nets of growing size and complexity together with (in)valid extended modal specifications, is first introduced. On the basis of such generated workflow nets, an experimental evaluation aiming at assessing the scalability of the verification approach based on such generated benchmarks is then defined. The obtained results are presented and discussed.

In a second step, this section introduces and discusses an experimental evaluation of the effectiveness and scalability of the workflow nets reduction approaches defined in Section 4.2 page 77 and 4.3 page 79.

5.4.1/ Benchmark's Generation Tool

In this section we introduce three tools forming a tool chain able to produce large benchmarks of workflow nets together with their (in)valid extended modal specifications.

The first tool, called Hadara-AdSimul-Formula-Gen, produces random extended modal formulae. The second tool, called Hadara-AdSimul-Formula-To-WF, produces workflow nets (in)valid with respect to given modal formulae. The third tool, called Hadara-AdSimul-Expander, produces larger and more complex workflow nets from given workflow nets while preserving the (in)validity of the modal formulae associated with them. All three tools are part of Hadara-AdSimul, a dedicated open source tool suite previously introduced in Section 5.2.2 page 103. The entry point of the tool chain is an XML file that contains the specifications of the formula to be generated (1): its intended size as well as the probability at which the operator and, or, and not will be used by the Formula Generator (2) to produce a Formula (3) verifying these given specifications. According to these specifications, the Formula Generator (2), starting from a single literal, recursively and randomly (according to the given probability) replaces an existing literal by either its negation, or its conjunction/disjunction with a newly introduced literal. Once the desired formula's size is reached, the produced formula is then saved in an XML file (3). The next step consists in producing an XML file describing a workflow net ( 5) satisfying (resp. not satisfying) the modal formula (resp. the negation of the modal formula) of the input formula interpreted as a must-formula. This computation is performed using the Formula to Workflow net tool (4) that maps each operator of the input formula to its corresponding workflow net structure (Section 2.1.6). Finally, the produced workflow net ( 5) is expanded using the Workflow Expander tool (7). This expansion is achieved by successively applying synthesis rules (inverse of the reduction rules presented in Section 4.1 page 68) which add transitions and/or places while preserving the validity of the modal specification associated. Note that this workflow nets generation approach is similar to the one proposed in [Van Hee et al., 2010]. However the synthesis rules used by our workflow nets generation approach are generalisation of the synthesis rules used in [Van Hee et al., 2010]. Therefore they are able to generate workflow nets exhibiting a broader range of behaviours. The result is an expanded workflow net saved as an XML file [START_REF]Definition: Ordinary Petri net[END_REF] satisfying or not the modal formula of the produced formula (3) interpreted as a may-formula or a mustformula. The produced formula (3) and the produced expanded workflow net [START_REF]Definition: Ordinary Petri net[END_REF] together form an instance of a benchmark.

Example 21: Example of workflow net generation

To illustrate this process we consider the following example. A must-formula of size 5 is generated using the Formula Generator (2): t 0 ∧t 1 ∧(t 2 ∨t 3 ∨t 4 ). The Formula to Workflow net tool ( 4) is then used to produce a workflow net, depicted in Figure 5.14, satisfying this must-formula. This workflow is then extended to the desired size of 50 nodes using the Expander tool (7) while preserving the validity of the considered must-formula. The obtained workflow is depicted in Figure 5.15. In this way, the presented tool chain is able to produce large benchmarks of workflow nets together with their (in)valid modal specifications. In the next section, an experimental protocol using this tool chain is designed to experimentally evaluate the scalability of the extended modal specification verification approach presented in Chapter 3 page 43.

5.4.2/ Experimental Evaluation of Modal Specification Verification

In this section, we present an experimental evaluation of the verification of extended modal specifications over workflow nets according to the approach presented in Chapter 3 page 43.

To this end, we first detail the objectives of the proposed experimental evaluation. Second, we define the experimental protocol. Finally, the experimental results obtained according to the defined experimental protocol are presented and discussed.

5.4.2.1/ Objectives

The primary objectives of this experimental evaluation are to experimentally assess the effectiveness, efficiency and scalability of the proposed extended modal specification verification method over workflow nets of growing size and complexity.

In the context of this experimentation, the proposed method is said to be effective over a given instance -a workflow net together with its extended modal specification -if and only if it is able to assign a verdict about the (in)validity of the given modal specification in an admissible time.

If the proposed method is effective over a given modal specification, its efficiency is its ability to return such a verdict in the least amount of time and memory. It follows that the proposed method is scalable if it is effective and efficient over workflow nets of growing size and complexity.

The secondary objective of this experimental evaluation is to compare the relative efficiency of the proposed method when employing two different constraint resolution approaches: Constraint Logic Programming and Satisfiability Modulo Theories (Section 2.3 page 38).

5.4.2.2/ Experimental Protocol

On the basis of the previously introduced objectives, the following experimental protocol have been designed.

Regarding effectiveness assessment, an admissible time is arbitrary fixed to a reasonable value of 10 minutes (i.e. the time-out of constraint solver queries if fixed to 10 minutes). To evaluate the effectiveness of the proposed method, this protocol thus consists in gathering, the proposed verification approach ability to assign a verdict to the instances of the considered data set in an admissible time of 10 minutes. If a verdict is assigned, the required time is also gathered in order to evaluate the proposed verification approach efficiency. Furthermore, in order to compare the relative efficiency of the proposed method when employing two different constraint resolution approaches (CLP vs SMT), each instance of the considered data set has to be evaluated once using a CLP constraint solver and once using a SMT solver.

To make conclusion and feedback relevant and credible, and to be able to evaluate the scalability of the extended modal specification verification approach, these experimental results has to be calculated from a broad range of modal specifications and workflow nets. Indeed, the type of modal specifications shall be taken into account because, to conclude about their validity, the verification method may require the computation of the over-approximation of the workflow nets executions or a full decomposition into segments. The proposed experimental protocol thus considers workflow nets of realistic size by evaluating workflow nets of size up to 500 nodes. Moreover, not only the size of the workflow nets is considered but also their complexity by evaluating workflow nets of classes with a growing expressiveness (state machines, marked graphs, free-choice workflow nets and ordinary Petri nets). Additionally, the size of the modal formula to be verified is also important since a larger formula may constrain further the system to be solved. For each combination of the listed parameters values, a corresponding modal formula and a workflow net have been randomly generated thanks to the tool chain described in Section 5.4.1. This produced 320 instances of growing size and complexity. Repeating this generation process three time led to the data set considered by this experimental protocol. A total of 960 workflow nets and modal specifications are thus considered in this protocol.

5.4.2.3/ Results and Feedback from Experiments

This section presents the experimental results obtained using the dedicated tools described in Sections 5.2.1 by applying the experimental protocol introduced in the previous section. Let us remind that this tool rely on two constraint solvers: Z3 [De Moura et al., 2008] version 4.4.0, an SMT solver, and SICStus Prolog [Carlsson et al., 2012] version 4.3.2, a CLP solver. For each instances of the data set the results have been gathered using both solvers and all the executions have been computed on a computer featuring an Intel(R) Xeon(R) CPU X5650 @ 2.67GHz.

The obtained results are discussed by distinguishing two different categories of modal specifications: one for may-valid and must-invalid specifications, and one for may-invalid and must-valid specifications. Indeed, using the verification algorithm given in Section 5.2.1, most may-valid and must-invalid modal specifications can be verified by using only an over-approximation of correct executions of the workflow. This over-approximation is less complex than the underapproximation that must very often be computed to verify may-invalid and must-valid modal specifications.

We also categorise the results according to the different classes of workflow nets considered in our experimental protocol. The average execution's times given below has been calculated without considering time-outs. Finally, for clarity, time-outs and singularities have been withdrawn from some plots. The interested reader can however study the complete data sets and results given at https://dx.doi.org/10.6084/m9.figshare.2067156.v3. Tables 5.11,5.12,5.13 and 5.14 summarize the average verification times, number of time-outs as well as the overall appreciation of the results obtained over the studied workflow net classes. The emoticons of the overall appreciation are interpreted as follows:

-→ Reasonable time, no time-out, -→ Reasonable time, # time-outs < 50%, -→ # time-outs > 50% Figures 5.17 5.18, 5.19, 5.20, 5.21, 5.22, 5.23 and 5.24 depict the plots displaying the verification times respectively spent by SICStus and Z3 for each class of workflow nets and types of modal specifications.

The next subsections comment on these obtained results and indicate the most important feedback for each class of workflow nets with regards to the intended objectives of the experimentations, as given in Section 5.4.2.1.

Observation from State-Machine Workflow Nets Verification

May-Valid and Must-Invalid specifications.

Both solvers were able to conclude in a comparable and reasonable time. On average, Z3 execution's times was 332ms whereas SICStus execution's times was 704ms. However, despite good results for both solvers, it should be noted that 49.2% (59/120) of SICStus executions did not finish within 10 minutes, while Z3 did not suffer from any time-outs.

q q q q q q q q q q q q q q q q q q q q q q q q q q q q q 250 500 750 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Valid-SM q q q q q q q q q q q q q q q q q q q q q q q q q q q 250 500 750 1000 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 Must-Invalid-SM Both solvers were able to conclude in a reasonable time. On average, Z3 execution's times was 79ms whereas SICStus execution's times was 43803ms. These results clearly show that Z3 performs better than SICStus on this type of modal specifications. Moreover, it should be noted that 85.8% (103/120) of SICStus executions did not finish within 10 minutes, whereas Z3 did not suffer from any time-outs. Indeed, SICStus was not able to conclude about workflow nets of size greater than 250. q q q q q q q 0 500 1000 1500 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 Must-Valid-SM q q q q q q 0 250 500 750 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Invalid-SM Synthesis. Over the class of State-Machines we observe that proposed verification method is effective and efficient using Z3. However, we also observe that when using SICStus the approach is less effective. Indeed, we can observe that SICStus is clearly overwhelmed due to the high number of choice points arising from the structure of state-machine workflow nets of size greater than 100 nodes.

Observation from Marked-Graph Workflow Nets Verification

May-Valid and Must-Invalid specifications.

Both solvers were able to conclude in a reasonable and comparable time. On average, Z3 execution's times was 635ms whereas SICStus execution's times was 767ms. It should also be pointed out that for large sized Marked-Graph workflow nets (greater than 400 nodes) SICStus performs slightly better than Z3.

q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q 400 800 1200 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Valid-MG q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q 0 500 1000 Both solvers were able to conclude in a reasonable and fairly comparable time. On average, Z3 execution's times was 108ms whereas SICStus execution's times was 415ms. Besides, it should be noted that, for this type of modal specifications, Z3 performs slightly better than SICStus.

q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q 0 200 400 600 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 Must-Valid-MG q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q 100 200 300 400 500 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Invalid-MG Synthesis. Over the class of Marked-Graph, we observe the proposed verification approach is effective and efficient using ether SICStus or Z3. We also point out that SICStus performs slightly better when verifying May-Valid and Must-Invalid specifications while Z3 performs slightly better when verifying Must-valid and May-Invalid specifications. A further investigation has shown that, in general, Z3 is more effective than SICStus for the computation of the over-approximation used by the verification method, while SICStus is more effective than Z3 for the computation of the segments needed to conclude whenever the over-approximation is not sufficient.

Observation from Free-Choice Workflow Nets Verification

May-Valid and Must-Invalid specifications.

Both solvers were able to conclude in a reasonable and comparable time. On average, Z3 execution's times was 396ms whereas SICStus execution's times was 842ms. Beyond these conclusive results for both solvers, it is important to underline that 25% (30/120) of SICStus executions did not finish within 10 minutes, whereas Z3 did not suffer from any time-outs. q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q 300 600 900 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Valid-FC q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q q 250 500 750 1000 1250 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 Must-Invalid-FC Over this type of modal specifications, Z3 clearly performs better than SICStus. On average, Z3 execution's times was 90ms, while SICStus execution's times was 45512ms. We also note that 62.5% (75/120) of SICStus executions did not finish within 10 minutes, whereas Z3 did not suffer from any time-outs. After investigation, these results stem from the fact that the verification of such modal specifications mostly relies on the results of an over-approximation for which Z3 performs far better off. q q q q q q q q q q q q q q q q q q q q q q q 0e+00 2e+05 4e+05 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 Must-Valid-FC q q q q q q q q q q q q q q q q q q q q q q q 0e+00 2e+05 4e+05 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Invalid-FC Synthesis. Over the class of Free-Choice workflow nets, we can observe that, using Z3, the proposed verification method is effective and efficient. We also note that the proposed approach is less effective when using SICStus. We thus conclude from these obtained results that the SMT approach seems to be more suited for the verification of modal specifications over Free-Choice workflow nets.

Observation from Ordinary Workflow Nets Verification

May-valid and Must-Invalid specifications.

Both solvers were able to conclude in a reasonable and comparable time. On average, Z3 execution's times was 985ms whereas SICStus execution's times was 10634ms. Besides these results, it should be underlined that 58.3% (70/120) of SICStus executions and that 32.5% (39/120) of Z3 executions did not finish within 10 minutes. However, for each instance, at least one resolution method was indeed able to assign a verdict within 10 minutes. q q q q q q q q q q q q q q q q q q q q q q q q q 0 2000 4000 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Valid-Ordinary q q q q q q q q q q q q q q q q q q q q q q q q q q 0 1000 2000 3000 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 Must-Invalid-Ordinary Must-valid and May-Invalid specifications.

On average, Z3 execution's times was 107ms whereas SICStus execution's times was 7717ms. Despite these good results for both solvers, it is important to note that 58.3% (70/120) of SICStus executions did not finish within 10 minutes, whereas Z3 did not suffer from any time-outs. As for the previous classes, Z3 indeed performs better than SICStus to compute the over-approximation constraints, which were often sufficient to conclude. q q q q q q q q q q q q q q q q q q q q q 0 1000 2000 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 Must-Valid-Ordinary q q q q q q q q q q q q q q q q q q q q q q q q q q 0 250 500 750 100 200 300 400 500

Size(nodes) t(ms)

q Sicstus Z3 May-Invalid-Ordinary Synthesis. Over the class of ordinary workflow nets, we can observe that the proposed verification method is effective and efficient. We also observe that Z3 performs better than SICStus, especially when verifying Must-valid and May-Invalid specifications. We can thus conclude from these results that the SMT approach seems to be more suited for the modal specifications verification over ordinary workflow nets. Moreover, further investigations have pointed out that the limits of the proposed method are reached when considering workflow nets of size greater than 500 nodes.

The next section summarizes the lessons learned and the benefits noticed from these experiments according to the initial objectives.

Lessons Learned from Experience

Effectiveness and Efficiency. The developed implementation of the method presented in section 5.2.1 and the underlying constraint solvers (i.e. Z3 and SICStus) have been shown to be effective and efficient for the intended verification computation. Indeed, the tool chain was always able to conclude about the validity of modal specification over workflow nets of growing size and complexity within the allowed time of 10 minutes (for each constraint system to solve, at least one resolution method was indeed able to assign a verdict, and furthermore within only few seconds in almost all cases). Furthermore, we have observed that memory usage does not seem to be a limiting factor over instances of the considered sizes. Indeed, for the biggest workflow net instance considered, the memory usage for SICStus and Z3 was less than 350MB. finally, we note that, as expected, this extended modal specification method performs efficiently when verifying the conformity of workflow nets with respect to necessary and inadmissible behaviours thanks to adequate use of over-approximations.

Scalability. On the basis of the results, we can confidently state that the verification method proposed in Chapter 3 is scalable over workflow nets of size up to 500 nodes. Indeed, our experimental results have shown that the proposed verification method has the ability to assign a verdict about the (in)validity of a given modal specification over such workflow nets of growing size and complexity. They also have shown that such verdict is obtained within the admissible time of 10 minutes.

SMT vs CLP. According to these experiments, we can infer that the SMT approach (computed using Z3) generally performs significantly better than the CLP one (computed using SICStus). However, they also highlight that the CLP approach is especially effective and efficient when verifying modal specifications over marked-graph workflow nets. Indeed, we observed that the CLP approach is less efficient than the SMT approach when the number of choice points increases as shown by the results over State-Machine workflow nets. It stems from the labelling done after constraints propagation by CLP solvers which means that an exponential number of backtracking steps may occur with respect to the number of pending choice points.

5.4.3/ Experimental Evaluation of Reduction Methods

In Section 4.3 page 79 two reduction methods, one based on the hierarchical representation of workflow nets and one based on reductions rules, are presented as pre-processing steps towards the verification of extended modal specifications (Section 3.1.1 page 44). These reduction methods aim at reducing the size of the analysed workflow nets in order to reduce the complexity of the intended analysis.

This section presents experimental results supporting the benefits provided by these reduction methods to the workflow net verification of behavioural properties such as generalised soundness and correctness with respect to extended modal specifications.

To this end, we first present the objectives of the proposed experimental evaluation. Second, we define the experimental protocol. Finally, the experimental results obtained according to the defined experimental protocol are presented and discussed.

5.4.3.1/ Objectives

The objectives of this experimental evaluation are to experimentally assess the effectiveness, efficiency and scalability of the proposed reduction methods.

In the context of this experimentation, the effectiveness of the proposed reduction methods is measured with respect to their ability to reduce the size (number of places and transitions) of the considered workflow nets. Indeed, given a workflow net of size OriginalS ize, the effectiveness of the proposed reduction methods is given by the ratio ReducedS ize/OriginalS ize, where ReducedS ize is the size of the workflow net obtained after reduction. Furthermore, the efficiency of the proposed methods is evaluated with respect to the time they required to reduce the considered workflow nets. It follows that the proposed methods are scalable over a considered set of workflow nets of growing size if they are able to effectively and efficiently reduce them.

5.4.3.2/ Experimental Protocol

On the basis of the previously introduced objectives, the following experimental protocol has been designed.

In a first step, this experimental protocol considers the hierarchical workflow net modelling of the issue tracking system presented in Section 5.1.1 page 90. This modelling is expressed by an underlying workflow net composed of 165 places and 204 transitions (369 nodes). For this workflow net, the experimental protocol consists in applying the proposed reduction methods in order to determine its generalised soundness. Additionally, in order to evaluate the effectiveness and efficiency of the proposed reductions methods when preserving the (in)validity of extended modal specification, it also consists in applying the proposed reduction methods as a pre-precessing step towards the verification of the extended modal specifications listed in Table 5.1 page 91.

In a second step, in order to assess more broadly the effectiveness and efficiency of the reduction procedure based on reduction rules introduced in Section 4.2, this experimental protocol consider the benchmark suite of 1976 industrial workflow nets previously studied in [START_REF] Mendling | Faulty epcs in the sap reference model[END_REF], van Dongen et al., 2007, Mendling et al., 2008, Fahland et al., 2009] and more recently [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF], Favre et al., 2016] where others reduction procedure also based on reduction rules have been applied. This benchmark suite is composed of two main benchmarks. The first one, denoted IBM-bpm, is a collection of 1386 free choice workflow nets that have been derived from industrial business process models provided by IBM R . These 1386 models are organized into five libraries (A, B1, B2, B3, and C). They have been translated into Petri nets from IBM Web-Sphere Business Modeler5 's language (i.e. a language similar to UML activity diagrams [START_REF] Dumas | Uml activity diagrams as a workflow specification language[END_REF]) according to [Fahland, 2008]. The resulting Petri nets often have multiple sink places and have therefore been completed according to [START_REF] Kiepuszewski | Fundamentals of control flow in workflows[END_REF] in order to obtain workflow nets. We notably point out that four of the largest workflow nets of this data set are included in the benchmark used by the 2016 Edition of the Model Checking Contest [START_REF] Kordon | Models of the 2016 Edition of the Model Checking Contest[END_REF]. More information about this data set can be found in the reference paper [START_REF] Fahland | Instantaneous soundness checking of industrial business process models[END_REF]. The second one, denoted SAP-ref, is a collection of 590 workflow nets that have been derived from SAP R 's ERP Software6 reference models. These 590 industrial workflows have been translated into workflow nets from their original EPCs models [START_REF] Lohmann | Petri net transformations for business processes-a survey[END_REF].More information about this data set can be found in the reference papers [START_REF] Mendling | Faulty epcs in the sap reference model[END_REF], van Dongen et al., 2007, Mendling et al., 2008].

In a third step, in order to further demonstrate the efficiency and scalability of the proposed reduction method based on reduction rules, two different and complementary sets of workflow nets generated using the tool chain presented in Section 5.4.1 are considered. The first set (gen1) is composed of 48 generalised sound workflow nets with size ranging from 371 nodes (165 transitions) to 17815 nodes (9233 transitions). The second set (gen2) is composed of 59 generalised sound workflow nets with size ranging from 1836 nodes (1000 transitions) to 147640 nodes (75782 transitions). Note that, since the synthesis rules used to build these workflow nets are the inverse of the reduction rules that are used to reduce them, these workflow nets are completely reducible. Therefore the following results are not dedicated to evaluate the effectiveness of the procedure but the efficiency with which it can be applied to workflow nets of growing size.

5.4.3.3/ Results and Feedback from Experiments

This section presents the experimental results obtained using the dedicated reduction tool described in Sections 5.2.2 by applying the experimental protocol introduced in the previous section. All experimental results have been obtained on a computer featuring an Intel(R) Xeon(R) CPU X5650 @ 2.67GHz. Note that only a single core has been used by the implemented tools.

In a first set, regarding the issue tracking system presented in Section 5.1.1 page 90, its underlying workflow net has been completely reduced to the atomic workflow net in 43 ms. This enabled analysts to conclude that this workflow net is generalised sound in such a short time. Furthermore, let us consider the set of requirements to be verified over this modelling given in Table 5.1 page 91. For these requirements, expressed by extended modal specifications in For every property (#Property), the processing time, the number of places (|P|) and the number of transitions (|T |) of the obtained workflow net as well as its graphical representation are given. This table also reports, for every property, the reduction factor (rf actor) obtained. This reduction factor expresses, in percentage, the size reduction with respect to the original workflow net accomplished by the reduction methods used.

These results show that the presented reduction methods are effective and can greatly reduce the size of workflow nets analysed with respect to a given extended modal specification. Indeed, for the considered extended modal specifications, an average reduction factor of 98.3% has been achieved. The obtained reduced nets are very simple (i.e. are composed of only a few transitions and places).

Note that these results are not surprising given the fact that the considered workflow net can be completely reduced to prove its generalised soundness. Furthermore, the needed processing time is reasonably low (i.e. about 40 ms per formula). It follows that these reduction methods are effective and efficient over this study case and can greatly enhance its analysis.

In a second step, let us consider the experimental results obtained over the 1976 industrial workflow nets of the data sets IBM-bpm and SAP-ref. We have analysed 1976 industrial workflow nets and determined that 642 of them are generalised sound (i.e. have been completely reduced). In addition, on average each workflow has been reduced by a factor of 82.2%. These experimental results highlight the effectiveness of the proposed reduction procedure. More precisely, with regards to the 1386 free choice workflow nets of IBM-bpm, 642 of them were identified as generalised sound. This results (i.e. the detected soundness) are in agreement with the results obtained during previous experiments applying different analysis techniques to the same data [van Dongen et al., 2007, Favre et al., 2016].

We note that all 642 sound workflow nets have been identified through structural reduction by our approach whereas only 464 of them have been identified through structural reduction by Woflan [START_REF] Verbeek | Woflan 2.0 a petri-net-based workflow diagnosis tool[END_REF]. We also note that the reduction method introduced in [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF] have found only 470 of these sound workflow nets. Furthermore, let us point out that workflow nets of this data set have been on average reduced to 13.9% of their original size (i.e. reduced by a factor of 86.1%). This underlines the greater effectiveness of our method compared with the reduction method of [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF] where workflow nets of the same data set have only been reduced to about 23% of their original size (i.e. reduced by a factor of about 77%).

To further emphasize the effectiveness of our reduction method let us focus on the results obtained for workflow nets of IBM-bpm that are included in the benchmark used by the 2016 Edition of the Model Checking Contest [START_REF] Kordon | Models of the 2016 Edition of the Model Checking Contest[END_REF]. For every considered workflow net, Table 5.4.3.3 gives the number of places (|P|) and the number of transitions (|T |) of the original and reduced workflow nets. It also states the obtained reduction factor (rf actor) as well as the processing time needed to compute it.

These workflow nets, which have been reduced by a factors ranging from 88% to 99.4%, clearly illustrate the benefit of our reduction procedure and its ability to significantly reduce the size of free choice workflow nets regardless of their soundness. None of those 590 workflow nets has been found to be generalised sound by our method. However, workflow nets of this data set have been on average reduced to 27% of their original size (i.e. reduced by a factor of 73%). These results further highlight the effectiveness of our reduction over arbitrary workflow nets. Indeed, once more this results show that our reduction method ability exceed the one of [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF] where workflow nets of the same data set have been reduced to about 35% of their original size (i.e. reduced by a factor of about 65%).

The results of our experiments for the IBM-bpm and SAP-ref benchmarks have also illustrated the efficiency of the proposed reduction method. Indeed, workflow nets of these benchmarks whose sizes are ranging from 9 to 548 nodes have been reduced on average in about 8 ms. Such a short analysis time means that this procedure could be automatically applied by integrated development environment to provide feedback as well as useful diagnostic information regarding the generalised soundness of in-development workflow nets.

In a third step, regarding that data-sets gen1 and gen2. These results allow us to empirically conclude that the proposed reduction procedure can efficiently be applied over large workflow nets (up to 147640 nodes) despite the fact that the application of rules R 1 (defined page 69) and R 2 (defined page 70) is exponential w.r.t. the size of the set ( • n) • of the considered place/transition n.

They have also highlighted that the implementation of the proposed method is able to conclude about the generalised soundness of workflow nets of size up to 17815 nodes within the fixed timescale of 180 seconds. In comparison, the approach proposed by Woflan in [START_REF] Verbeek | Diagnosing workflow processes using Woflan[END_REF] is not able to conclude about the 1-soundness of any of these generated workflow nets in the fixed timescale of 180 seconds. Furthermore, the SPIN model-checker is only able to conclude within 180 seconds about the 1-soundness of workflow nets, from our first set of generated workflow nets, of size up to 731 nodes, using the approach proposed in [START_REF] Yamaguchi | A model checking method of soundness for workflow nets[END_REF]. However, this is not so surprising since both compared approaches rely on state-space exploration and suffer from the state explosion of large-size workflow nets, contrary to the proposed method.

Moreover, as shown in Figure 5.28, the experiments have empirically demonstrated the huge scalability of the proposed method and its implementation within the tool Hadara-AdSimul-Red. This tool is indeed able to conclude in less than 90 minutes about the generalised soundness of workflow nets of size at least up to 147640 nodes. This size is clearly far beyond what is realistically produced and manageable by workflows modellers in real-life conditions. Needless to say that their analysis is out of reach of other state exploration approaches (e.g., [START_REF] Verbeek | Diagnosing workflow processes using Woflan[END_REF], [START_REF] Yamaguchi | A model checking method of soundness for workflow nets[END_REF]).

According to all presented experimental results, it follows that the reduction methods presented in Sections 4.2 page 77 and 4.3 page 79 constitute effective, efficient, scalable and therefore relevant pre-processing steps toward the analysis of behavioural properties such as generalised soundness and correctness with respect to extended modal specifications.

5.5/ Synthesis

This chapter presented convincing experimental results supporting the value of the contributions made to this thesis.

It first presented three study cases (i.e. real-life examples) which highlighted and motivated the use of workflow nets and extended modal specifications. It also described dedicated tool chains implemented to carry out the verification of extended modal specifications according to the approach presented in Section 3.1.3 page 53 as well as the reduction methods of workflow nets presented in Sections 4.2 page 77 and 4.3 page 79.

It then reported experimental results obtained during the analysis of the three study cases using the dedicated modal specification verification tools previously introduced. From these results we concluded that extended modal specifications are adapted to the description of modal behaviour involving several transitions as well as their causalities expressed over workflows modelled as workflow nets but also as coloured workflow nets. Furthermore, the verification of such extended modal specifications was shown to be possible and efficient (less than a few seconds per extended modal formula) over these real-life examples.

This chapter also exposed experimental results regarding the scalability of the proposed approaches over workflow nets of growing size and complexity. To this end, it presented a generation tool able to generate large benchmarks of workflow nets together with their (in)valid extended modal specifications. Based on this generation tool, an experimental protocol and the results it produced were described. These results enabled us to confidently state that the extended modal specification verification method proposed in Section 3.1.3 page 53 is scalable in terms of modal specification and workflow net complexity, as well as regarding their size (up to 500 nodes, at least). It also enabled to conclude that the developed implementation of this verification method and the underlying constraint solvers (i.e. Z3 and SICStus) are effective and efficient for the intended verification computation. More precisely, it showed that it was always able to conclude about the (in)validity of modal specification over workflow nets of growing size and complexity within the allowed time of 10 minutes, and furthermore within only few seconds in almost all cases.

Finally, this chapter also presented experimental results concerning the reduction methods described in Sections 4.2 page 77 and 4.3 page 79. Through one of the considered study cases as well as workflow nets issued from a benchmark suite of 1976 industrial workflow nets previously studied in [van Dongen et al., 2007, Fahland et al., 2009, Favre et al., 2016, Esparza et al., 2016], it demonstrated the size reductions benefits they provide. More precisely, it showed that the verification of extended modal specifications can be carried out over workflow nets whose size is significantly reduced (up to 98.9% smaller than the original workflow nets). Likewise, it also illustrated the effectiveness of such a reduction method to the verification of generalised soundness by providing, for the considered workflow nets, an average size reduction of 82.2%. At last, the efficiency of the developed reduction tool has been demonstrated. It was shown that despite the exponential complexity of some of the reduction rules used, the developed reduction tool was able to reduce workflow nets of size up to Nowadays workflow management has become a key factor in the success of companies and organizations around the world. Indeed, workflows, when properly designed, can significantly improve organizational efficiency, responsiveness and profitability by managing the tasks and steps of business processes.

Due to the central role of workflows for day to day operations and long term focus of companies and organizations, the verification of specifications, i.e. of desired properties of workflows, has become mandatory to ensure that such processes are properly designed and reach the expected level of trust and quality.

Within this context, this thesis presented contributions made to the verification of modal specifications of workflow nets based on powerful abstractions and the use of constraint solving.

More precisely, this thesis has addressed the three following research questions:

RQ 1 How to effectively express modal behaviour of workflow nets involving several transitions and their causalities?

RQ 2 How to effectively verify the validity of such modal specifications by leveraging the efficiency of existing mature constraint solvers? RQ 3 Which abstraction mechanisms are appropriate and relevant with respect to verification of such modal specifications?

The rest of this section briefly summarises the theoretical and practical contributions made to this thesis. Following the organisation of this manuscript, the presentation of these contributions is divided into three subsections.

6.1/ Verification of Modal specifications

To guide engineers in their specification and validation activities, modal specifications have been previously designed to allow specifications of modal behaviour (i.e. admissible or necessary behaviour) of complex systems.

127 Modal specifications of workflow nets are usually expressed over a single transition of the system under analysis. This is quite limiting as the expression of complex modal behaviour involving several transitions and their causalities is needed in real-life. To address this issue and RQ 1 , the research question prompted by it, we defined extended modal specifications, an extension of modal specification that enables the definition of modal behaviour involving several transitions as well as their causalities. Such extended modal specifications have then been further extended to handle workflow nets extensions (e.g., workflow nets with data). To this end, additional constraints on the initial and final states as well as on the data associated to transition firing have been designed and taken into account.

Verifying behavioural properties of workflows such as extended modal specifications is a very complex task which requires exponential computational resources with respect to the size of their modelling by workflow nets. To cope with this complexity, efficient tools are required. Existing mature and efficient constraint solvers offer an unprecedented support to such verification problem.

In order to benefit from it and address RQ 2 , a novel constraint-based framework for modelling workflow nets executions has been developed. This modelling framework is based on the definition of several constraint systems either over-approximating or under-approximating the set of correct executions of workflow nets. More precisely, each of these approximations is built by refining the previous one starting from a well-know over-approximation: the state equation. This led to the definition of a constraint system whose solution space under-approximates the set of correct executions of workflow nets. This latter constraint system is used to define segments of execution (i.e. partial execution structurally verifiable). It has been then demonstrated that the concatenation of such segments can be used to model any correct executions of workflow nets.

Furthermore, through the definition of abstract workflow nets -a suited abstract representation notably able to model ordinary, generalised and coloured Petri nets -this framework has been shown to be applicable to workflow nets with data and quantitative performance specification.

Its use for verifying the (in)validity of extended modal specifications of workflow nets (resp. abstract workflow nets) have been presented. Using such a constraint-based modelling for verifying the (in)validity of extended modal specifications of workflow nets (resp. abstract workflow nets) exhibits several advantages. The first advantage of this modelling is that the search is quite focussed from the beginning as we traverse the solution space of the state equation and its refinements rather than the underlying semantic labelled transition systems of workflow nets. Another advantage of such modelling is that only the segments ordering is computed, the transitions ordering within segments is not. It follows that this modelling is particularly well-adapted to the verification of extended modal specification as only the presence or absence of transitions is considered. Moreover, this extended modal specification verification approach requires the use of constraint systems satisfiability checks which can be handled by third party constraint solvers. This allows the proposed verification method to benefit from existing mature and efficient constraint solvers.

6.2/ Reduction methods

The development of large and intricate workflow nets can be a difficult task which requires powerful structuring mechanisms. Unfortunately, most often, the abstraction mechanisms, used by modellers of workflow nets, is not explicitly given beside the clear advantages they bring to their analysis. To cope with this issue and address RQ 3 , reduction methods -abstraction methodsthat have the ability to reduce the size of workflow nets while strongly preserving properties of interest such as generalised soundness and the (in)validity of a given extended modal specification have been presented. More precisely, six reduction rules preserving generalised soundness and generalising existing reduction rules have been defined.

Based on the definition of these reduction rules, a generalised soundness semi-decision have been described. We have notably shown that, despite not being complete, this procedure, whenever unable to conclude, can be used as a pre-processing step toward verification of generalised soundness. Indeed, by reducing the size of the analysed workflow nets, this procedure can enhance conventional generalised soundness verification methods. Furthermore, whenever inconclusive, this procedure produces diagnostic information in the form of a simplified and irreducible workflow net.

In addition, two reduction methods preserving the (in)validity of a given extended modal specification has been introduced. The first of these methods -based on the hierarchical representation of workflow nets -aims at abstracting unnecessary layers of detail. The second method is based on the six reduction rules previously presented and further refines them in order to preserve the (in)validity of a given extended modal specification. Both reduction methods were proved to be sound. Thanks to the potential size reduction they provide, these reduction methods have been proposed as pre-processing steps for extended modal specifications verification approaches such as the constraint-based approach previously described.

6.3/ Experimental Evaluation

As a practical contribution to RQ 2 and RQ 3 , the new formal approaches described in this thesis have been implemented and extensive experimentations have been carried out in order to validate them.

The results of convincing experimentations carried out over real-life industrial study cases have been introduced and discussed. These results highlight the need and relevance of extended modal specifications to express modal behaviour involving several transitions as well as their causalities.

They also illustrate the effectiveness of the proposed modal specification verification approach over workflow nets extended with data and quantitative performance specification.

Furthermore, an empirical evaluation of the effectiveness, efficiency and scalability of the proposed modal specification verification approach over workflow nets of growing size and complexity has been presented. These results show that the extended modal specification verification method proposed in this thesis is effective and scalable in terms of modal specification and workflow net complexity, as well as regarding their size (up to 500 nodes, at least). They also show that the developed implementation of this verification method and the underlying constraint solvers are very efficient for the intended verification computation. More precisely, they point out that the proposed verification approach is able to conclude about the (in)validity of modal specification over workflow nets of growing size and complexity within the allowed time of 10 minutes, and furthermore within only few seconds in almost all cases.

Finally, experimental results demonstrating the benefits provided by the presented reduction methods to the verification of workflow net behavioural properties such as generalised soundness and correctness with respect to modal specifications have been introduced. We have considered one of the study cases as well as workflow nets issued from a benchmark suite of 1976 industrial workflow nets previously studied in [van Dongen et al., 2007, Fahland et al., 2009, Favre et al., 2016, Esparza et al., 2016]. We have shown that the verification of extended modal specifications can be carried out over workflow nets whose size is significantly reduced (up to 98.9% smaller than the original workflow nets). Likewise, we have also illustrated the effectiveness of such a reduction method to the verification of generalised soundness. Indeed, experimental results for 1976 workflow nets derived from industrial business processes show that the nets are reduced to about 17.8% of their original size (i.e. reduced by a factor of 82.2%). At last, the efficiency of the developed reduction tool has been demonstrated. It was shown that despite the exponential complexity of some of the reduction rules used, the developed reduction tool was able to reduce workflow nets of size up to 17,815 nodes (resp. 147,640 nodes) in less that 180 seconds (resp. 90 minutes). Based on these observations we concluded that the presented reduction methods constitute effective, efficient, and scalable pre-processing steps toward the analysis of behavioural properties such as generalised soundness and correctness of workflow nets with respect to extended modal specifications.

Future Work This section presents three future work directions prompted by the research work and results of this thesis. We first discuss the adaptations that would enable the application of the presented approaches to benefit from parallel computing. Afterwards, we present an extension of the proposed generalised soundness semi-decision procedure which introduces the identification of errorpatterns during the reduction process in order to provide insight about the invalidity of workflow nets with respect to generalised soundness. Finally, we propose a reconfiguration framework which enables the definition of workflow net reconfigurations preserving behavioural properties such as generalised soundness and validity with respect to extended modal specifications.

7.1/ Towards Parallelism

Parallel computing is a type of computation in which many calculations are carried out simultaneously [START_REF] Almasi | Highly parallel computing[END_REF]. Large problems can often be divided into smaller ones, which can then be solved independently at the same time.

Within parallel computing, there exist two main paradigms: shared and distributed memory programming [START_REF] Kumar | Introduction to parallel computing: design and analysis of algorithms[END_REF]]. On the one hand, in shared memory programming, all tasks access the same memory and therefore the same data (e.g., POSIX Threads [Butenhof, 1997]). On the other hand, in distributed memory programming, all memory is local and data sharing is achieved by explicitly transporting data through communication (e.g., MPI [START_REF] Gropp | Using MPI: portable parallel programming with the message-passing interface[END_REF]).

With regards to the proposed extended modal specification verification approach based on constraint systems, note that the computation workload of the implemented tool is shifted to mature and efficient but sequential solvers. Due to the increasing demand for high performance constraint solving algorithms in the industry, parallel constraint solvers constitute an active research area [Singer, 2006, Hamadi et al., 2013, Hyvärinen et al., 2016]. In a future work, parallel constraint solvers could substitute the sequential solvers used in the considered implementation in order to further improve its efficiency.

With regards to the proposed reduction methods, note that, given a workflow net, several reduction rules may be simultaneously applied to distinct nodes. This means that the application of the presented reduction procedures based on reduction rules could in the future be implemented within a shared memory environment (e.g., actual multi-core computer). Such an implementation 131 would be very similar to the one we implemented with the difference that it would require synchronisation such as a mutual exclusion mechanism to avoid concurrent modification of the same nodes. Due to the large number of reduction rules applicable to distinct nodes observed over the industrial workflow nets considered in this thesis, we conjecture that such a shared memory parallel implementation of the proposed reduction procedures would significantly improve their overall efficiency. Furthermore, note that, given a hierarchical workflow net, each of its nodes can be reduced independently. It follows that each of these nodes can simultaneously be reduced in a distributed memory environment (e.g., cluster, grid). Depending on the number of hierarchical levels of detail, such a distributed implementation of the proposed reduction methods could also significantly improve their overall efficiency. Finally, note that those shared and distributed approach to the reduction of workflow nets are not mutually exclusive and could be combined in a mixed environment with both shared and distributed memory ability (e.g., accelerators: Intel R Xeon Phi cluster).

7.2/ Error-pattern

We designed and presented reduction rules of workflow nets notably preserving generalised soundness. The idea behind this concept is to study the construction of workflow nets. If a workflow net is generalised sound, chances are that it has been modelled using strict abstraction mechanisms either implicitly or explicitly in the case of refinement development. It follows that by identifying sound abstraction mechanisms used by modellers we may be able to prove the considered property.

In the context of generalised soundness this has led to the design of the presented reduction rules as well as their dual synthesis rules corresponding to sound abstraction mechanisms with respect to generalised soundness. These reduction rules, as it has been presented, when iteratively applied, form a semi-decision procedure for generalised soundness. Indeed, as these reduction rules are not complete, no negative results can be inferred.

A natural alternative to this approach consists in identifying workflow patterns contradicting the generalised soundness property. Such patterns are called error-patterns and correspond to defects. Recently, they have notably been used in order to provide diagnostic information for control-flow analysis of free-choice workflow nets [START_REF] Favre | Diagnostic information for control-flow analysis of workflow graphs (aka free-choice workflow nets)[END_REF]. We propose to apply a similar concept to the analysis of arbitrary workflow nets with respect to the generalised soundness property. Indeed, if a workflow net is not generalised sound, chances are that at some point in its construction an error-pattern has been introduced. Let us for example consider the following theorem.

Theorem 36: Example of error-pattern

Let N = P, T, F be a workflow net. If there exists a transition t ∈ T such that

• t t • ∧ ( • t \ t • = ∅ ∨ t • \ • t = ∅) then N is not generalised sound.
Proof. We proceed to demonstrate this theorem by contradiction. Assume that N is a generalised sound workflow net. Suppose there exists a transition t ∈ T such that • t t • ∧ • t \ t • = ∅. We have • t ⊆ t • and by assumption there exists a marking M ∈ M ∈ R N (M i(1) ) such that t is enabled. It follows that in marking M, the transition t can be fired infinitely many times. This would produce an infinite number of tokens in places of t • \ • t. The 1-closure of N would not be bounded and this would therefore contradict the assumption. Now, suppose there exists a transition t ∈ T such that • t t • ∧ t • \ • t = ∅. We have t • ⊆ • t and therefore the firing of t does not produce any new tokens.

By assumption, there exist σ 1 , σ 2 two executions of N, and M, M two markings of N such that M i( 1)

σ 1 --→ M t - → M σ 1
--→ M o(1) . It follows that the concatenation of executions σ 1 and σ 2 leads to a marking M f such that ∀ p ∈ • t \ t • , M f (p) = 1 and M f (o) = 1. Therefore we have M f ∈ R N (M i(1) ) and this contradicts the assumption.

This theorem defines infinitely many error-patterns. Our experimental results have pointed out that error-patterns such as the ones described by Theorem 36 often appear during the reduction process. Indeed, we have observed that while many defects are initially hidden by the complexity of the considered workflow net, the reduction process tends to reduce their expressions to identifiable error-patterns. It follows that the search of error-patterns during the reduction process could provide insight with regards to the invalidity of workflow nets with respect to generalised soundness. The synergy of these two complementary approaches would result in an algorithm semi-deciding both the validity and the invalidity of workflow nets with respect to generalised soundness and should greatly enhance reduction based analysis abilities.

7.3/ Reconfiguration

In order to succeed long into the future, a business needs to be flexible and constantly evolves with respect to its industry. Therefore the workflows supporting the business processes also have to evolve in order to be up to date.

In the context of workflow nets, such evolutions of the workflows are modelled through reconfigurations. There exist two types of reconfigurations: static and dynamic. Static reconfigurations are traditional updates. Following requests of users or technical imperatives, new versions of workflow nets are developed based on the actual versions before being deployed. Such reconfigurations often take time and might not be sufficiently responsive. To cope with this, dynamic reconfigurations can be used. Based on some pre-conditions (e.g., overload, failure of a task), predefined reconfigurations can be applied dynamically during execution.

A major aspect of reconfigurations is the fact that they must preserve behavioural properties of interest. For example, reconfigurations of workflow nets should at least preserve generalised soundness. Further, they should also preserve one or more extended modal specifications.

In Section 4.3 page 79, six reduction rules strongly preserving generalised soundness as well as the (in)validity of a given extended modal specification formula interpreted as either a may-formula or a must-formula have been introduced. Note that the inverse of these reduction rules are six synthesis rules, which also preserve generalised soundness as well as the (in)validity of a given extended modal specification formula interpreted as either a may-formula or a must-formula.

We propose to model the changes made to workflow nets by reconfigurations as a sequences of synthesis and reduction rules such as the ones defined in this thesis. Doing so would have the advantage to guarantee the validity of behavioural properties without having resort to the indepth analysis of the behavioural properties of interest. A sequence of synthesis and reduction rules would model a reconfiguration which preserves not only generalised soundness but also the (in)validity of a given extended modal specification formula interpreted as either a may-formula or a must-formula if necessary.

Note that, in the case of static reconfigurations, the execution of the workflows might be halted to perform reconfigurations. Further, dynamic reconfigurations might not be instantaneous and require a significant downtime. Another advantage of the proposed reconfiguration approach is that it models reconfigurations as sequences of atomic workflow transformations (i.e. synthesis and reduction rules) which can be sequentially applied. Therefore, modifications of the workflow nets are local and fast which should decrease the overall impact of reconfigurations and ensures quality of services.

De nos jours, les workflows sont largement utilisés par les entreprises et les organisations en vue d'améliorer l'efficacité organisationnelle, la réactivité et la rentabilité en gérant les tâches et les étapes de processus opérationnels. La vérification des spécifications est devenue obligatoire afin d'assurer que ces processus sont correctement conc ¸us et atteignent le niveau de confiance et de qualité attendu. Dans ce contexte, cette thèse porte sur la vérification de spécifications modales -comportements nécessaires ou recevables impliquant plusieurs activités et leurs causalités -de workflows nets -une classe de réseaux de Petri adaptés à la description de workflows. En particulier, cette thèse définit un cadre novateur permettant de modéliser les exécutions de workflow nets, avec ou sans données, et de vérifier des spécifications modales à l'aide de systèmes de contraintes. Elle présente également deux méthodes de réduction préservant la 'generalised soundness' et la validité d'une spécification modale donnée. Ces méthodes de réduction sont ensuite présentées comme des étapes de prétraitement réduisant la taille des workflow nets, de sorte que la vérification des propriétés conservées puisse être effectuée sur de plus petites instances. Enfin, cette thèse présente les outils qui ont été mis en oeuvre ainsi que des expérimentations qui ont été menées sur un grand nombre de workflows industriels afin de valider les approches proposées dans cette thèse. Ces résultats expérimentaux convaincants mettent en évidence l'efficacité, l'efficience et le passage à l'échelle de la méthode vérification de spécification modales ainsi que des méthodes de réduction introduites dans cette thèse.

Mots-clés : Vérification, Spécifications Modales, Réseaux Workflows, Solveurs de Contraintes, Réduction

Definition 2 :

 2 Binary Relation A binary relation R over two sets A and B is a subset of A × B. The domain of R, denoted Dom(R), is the set {a ∈ A | ∃ b ∈ B, (a, b) ∈ R}. The co-domain (also called the range) of R, denoted Ran(R), is the set {b ∈ B | ∃ a ∈ A, (a, b) ∈ R}. The notation aRb signifies that (a, b) ∈ R.

  a) Transition t 1 is enabled (b) Transition t 1 has been fired

Figure 2 . 1 :

 21 Figure 2.1: An ordinary Petri net in two states illustrating the firing of a transition

Figures 2 .

 2 Figures 2.1(a) and 2.1(b) depict an ordinary Petri net modelling two chemical reactions.The first chemical reaction, modelled by transition t 1 , is the reaction between carbon (C) and dioxygen (O 2 ) which produces carbon dioxide (CO 2 ). The second chemical reaction, modelled by transition t 2 , is the reaction between sodium hydroxide (NaOH) and carbon dioxide (CO 2 ) which produces sodium bicarbonate (NaHCO 3 ). The marking of figure2.1(a) models a situation where one atom of carbon, one molecule of dioxygen, and one molecule of sodium hydroxide are present. In this marking the transition t 1 is enabled and firing it leads to the marking depicted by figure 2.1(b) which models a situation where one molecule of carbon dioxide and one molecule of sodium hydroxide are present, in this marking transition t 2 is enabled.

  a) Transition t 1 is enabled (b) Transition t 1 has been fired

Figure 2 . 2 :

 22 Figure 2.2: An generalised Petri net in two states illustrating the firing of a transition

Example 3 :

 3 Illustration of the matricial representation of a Petri net Consider the generalised Petri net of Example 2 page 13 depicted in Figure 2.2(a) page 13. This generalised Petri net is composed of three places (H 2 O, O 2 and H 2 ) and a transition (t 1 ). It can be fully described by the tuple W -, W + where W -= [-2, 0, 0] and W + = [0, 1, 2] . Equivalently, as this generalised Petri net is pure, it can be fully described by its incidence matrix W defined as: W = [-2, 1, 2] . Let M a = [2, 0, 0] be the matricial representation of the marking of Figure 2.2(a) and M b = [0, 1, 2] be the matricial representation of the marking of Figure 2.2(b). We have M b = M a + W * t where t = [1] is the matricial representation of transition t 1 .

Figure 2 . 3 :

 23 Figure 2.3: State machine

  Figure 2.4: Marked graph

Figure 2 . 5 :

 25 Figure 2.5: Free choice net

  Figure 2.6: Asymmetric choice net

Figure 2 . 7 :

 27 Figure 2.7: Venn diagram of Petri nets subclasses

Figure 2 . 8 :

 28 Figure 2.8: An example of coloured Petri net

2 Figure 2 . 9 :

 229 Figure 2.9: Illustration of causal dependency, conflict and concurrency in workflow nets

Figure 2 . 11 :

 211 Figure 2.11: Two strong trace equivalent workflow nets

Figure 2 . 14 :

 214 Figure 2.14: Illustration of the transition refinement of transition t with a workflow net N sub

Theorem 9 :

 9 Sufficient conditions for k-soundness [Van der Aalst, 1997] Let N by a workflow net and N * k its k-closure Petri net. If the rank of the incidence matrix of N * k is equal to the number of clusters of N * k minus 1, and every proper siphon of N * k contains at least a token, then the workflow net is k-sound.

Figure 2 . 15 :

 215 Figure 2.15: Reduction rules of[Murata, 1989]

Figure 3 . 1 :

 31 Figure 3.1: Workflow net (N 1 ) used to illustrate a spurious solution of the state equation

Figure 3 . 2 :

 32 Figure 3.2: Illustration of a state equation solution subnet (sN(ν 1 ))

Example 13 :

 13 Illustration of the refutation of a spurious valuation of S This allows us to directly conclude that ν 1 , as defined in Example 11, is a spurious solutions of S(N 1 , M i , M o ) since sN(ν 1 ) contains a trap {p 1 , p 2 }. An interesting property of the subnet sN(ν) of any solution ν of S(N, M a , M b ) relates the presence of siphons to the presence of traps, and vice-versa, as stated by Theorem 11. Theorem 11: Siphon/Trap Property of Subnet Let N = P, T, F be a workflow net, M a , M b two markings of N, ν : P × T → N a valuation satisfying S(N, M a , M b ) and sN(ν) the subnet associated with ν. If sPN(ν) contains a trap (resp. siphon) G then G is also a siphon (resp. trap). Proof. (⇒) Let G ⊆ sP such that G ∅, by definition of S(N, M a , M b ) and ν we have p∈G ν

Figure 3 . 3 :

 33 Figure 3.3: Workflow net (N 2 ) used to illustrate a spurious solution of Q

Theorem 13 :

 13 Path Existence Let N = P, T, F be a workflow net and M a , M b two markings of N. If there exists a valuation ν : P ∪ T → N such that D(N, M a , M b ) | = ν then there exists a transition sequence σ such that M a σ -→ M b and ν | = σ. Proof. Suppose there exists a valuation ν : P ∪ T → N such that D(N, M a , M b ) | = ν. By definition of D(N, M a , M b ), sN(ν) is a marked graph with no siphons nor traps. It follows from Theorem 5 that sN(ν) = sP, sT, sF is a live marked graph from any marking (in particular from an initial marking

Theorem 14 :

 14 Path Existence Let N = P, T, F be a workflow net and M a , M b two markings of N. There exists a transition sequence σ such that M a σ -→ M b if and only if there exist k ∈ N a number of segments and ν : P ∪ T → N a valuation function such that U(N, M a , M b , k) | = ν and ν | = σ. Proof. (⇒) Suppose there exists a transition sequence σ = t 1 , .., t k such that M a σ -→ M b .

Figure 3 . 4 :

 34 Figure 3.4: Illustration of an execution modelled by three segments

Theorem 15 :

 15 Path Existence Let N = P, T, F be a workflow net and m ∈ S (N) a modal property. There exists a transition sequence σ such that M i σ -→ M o and σ | = m if and only if there exists k ∈ N and ν : P ∪ T → N a valuation function such that V(N, k, m) | = ν, and ν | = σ.

Theorem 16 :

 16 K-bounded validity of EMSLet N = P, T, F be a workflow net and a must , A may be an extended modal specification of N. The correct executions of N composed of at most k segments satisfy the extended modal specification a must , A may , noted N | = k a must , A may , if and only if:ν, V(N, ¬a must ) | = ν, and -∀ a may ∈ A may , ∃ ν, V(N, k, a may ) | = ν.Proof. Follows from Theorem 15.

  An abstract Petri net is defined within a framework where: (D, + D ) is a commutative monoid with its algebraic preordering ≤ D . We denote O D the minimal element of D and L(D, D) the space of linear maps from D to D. Definition 41: Abstract Petri Net An abstract Petri net AN is a tuple AN = P, T, W -, W + where: -P is a finite set of places, -T is a finite set of transitions, -W -: P × T → L(D, D) is the pre-incidence function, -W + : T × P → L(D, D) is the post-incidence function.

Definition 42 :

 42 Marking of an Abstract Petri NetLet AN = P, T, W -, W + be an abstract Petri net. A marking of AN is a total function M : P → D. Two markings M a and M b are in relation M a ≤ D M b if and only if ∀p ∈ P, M a (p) ≤ D M b (p).

  M b is said to be directly reachable from M a by the transition instance (t, d), written M a (t,d) ---→ M b . The reachability relation is the reflexive and transitive closure of the direct reachability relation. Let σ = (t 1 , d 1 ), .., (t n , d n ) be a sequence of transition instances, we denote by M a σ -→ M b the fact that the marking M b is reachable from the marking M a by the sequence of transition instances σ.

Example 19 :

 19 Illustration of a coloured Petri net as an abstract Petri net Consider the coloured Petri net of Example 4 page 20 depicted in Figure 2.8 page 20. This coloured Petri net have two colors (C 1 and C 2 ) and is composed of two places (p 1 , and p 2 ) and a transition (t 1 ) such that C(p 1 ) = C(t 1 ) = C 1 and C(p 2 ) = C 2 .

  and∀ a may ∈ A may , N | = may a may .

Theorem 18 :

 18 State equation Let AN = P, T, W -, W + be an abstract workflow net. If a marking M b is reachable from M a by the transition instances sequence σ = (t 1 , d 1 ), .., (t n , d n ) (i.e. M a σ -→ M b ) then: M b = M a + W T where σ | = T . Proof. By definition we have M b

Theorem 19 :

 19 Abstract Path Existence Let AN = P, T, W -, W + be an abstract workflow net, and M a , M b be two markings of AN. If there exists a valuation T : T → D such that D a (N, M a , M b ) | = T then there exists a transition instance sequence σ such that M a σ -→ M b and σ | = T . Proof. Suppose there exists a valuation T : T → D such that D a (N, M a , M b ) | = T . By definition of D a (N, M a , M b ) we have sN(T ) is a marked graph with no siphons nor traps. It follows from Theorem 5 page 34 that sN(T ) is a live marked graph from any marking (in particular from an initial marking M ∅ such that ∀ p ∈ sP, M ∅ (p) = 0). Therefore ∀ p ∈ sP there exists t pre ∈ • p, t post ∈ p • such that ∀ σ, M ∅ σ -→ M ∅ is an execution of sN(T ), we have O t post (σ) = 1 ⇒ O t pre (σ) = 1. By induction it follows that there exists σ such that M ∅ σ -→ M ∅ an execution of sN(ν) where ∀t ∈ T such that T (t) > O D we have O t (σ) = 1. As data consistency is ensured by the state equation, it follows that there exists σ * , a transition instance sequence obtained by replacing every occurrence of any transition t ∈ sT by its corresponding transition instance T (t), such that M a σ * --→ M b is an execution of AN where σ * | = T . It follows that the set of solutions of D a (AN, M a , M b ) defines an under approximation of the executions of AN reaching M b from M a .

Theorem 20 :

 20 Abstract Path Existence Let AN = P, T, W -, W + be an abstract workflow net, M a , M b be two markings of AN. There exists a transition instance sequence σ such that M a σ -→ M b if and only if there exist k ∈ N a number of segments and T : T → D a valuation function such that U a (N, M a , M b , k) | = T and σ | = T . Proof. (⇒) Suppose there exists a transition instance sequence σ = t 1 , .., t k such that M a σ -→ M b .

Figure 4 .

 4 Figure 4.1 illustrates the reduction rule φ RemoveP formally described as follows.

Figure 4 .

 4 Figure 4.3 illustrates φ RemoveS T that is formally described below.

Figure 4 . 4 :

 44 Figure 4.4: Reduction rule φ RemoveT P (R 4 )

Figure 4 . 5 :

 45 Figure 4.5: Reduction rule φ RemovePT (R 5 )

Figure 4 .

 4 Figure 4.6 illustrates φ RemoveR that is formally described below.

Figure 4 . 6 :

 46 Figure 4.6: Reduction rule φ RemoveR (R 6 )

2 :

 2 Data: N = P, T, F Result: Generalised soundness of N int sizeN = 0; do sizeN = size(N); forall the φ ∈ Φ do int subsizeN = 0; do subsizeN = size(N); N = T ryApplyRule(φ, N); while size(N) < subsizeN; end while size(N) < sizeN; if N = N Atomic then return true; else save(N); return unknown; end Algorithm Generalised soundness semi-decision algorithm Theorem 28: Soundness of Algorithm 2

Figure 4 . 7 :

 47 Figure 4.7: Illustration of the application of Algorithm 2

Algorithm 3 :

 3 Definition of the utility function subT ransitions

Algorithm 4 :

 4 Definition of the function underlying r

  The reduction procedure based on the function underlying r is said to be sound with respect to (in)validity of m if and only if underlying(W) | = must m ⇔ underlying r (W, m) | = must m, and underlying(W) | = may m ⇔ underlying r (W, m) | = may m.

∀

  t ∈ Domain(m), subT ransitions(t) ∩ Domain(m) = ∅, and Wis generalised sound The first assumption concerns the given modal specification formula m: it ensures that transitions in Domain(m) are not deleted by refinement during the construction of the underlying workflow net. The second assumption concerns the hierarchical workflow net W: it guarantees that the abstracted layers of detail always produce valid (sub)executions. Theorem 29: Soundness of underlying r Let W = P h , T h , F h be a generalised sound hierarchical workflow net, and m a given extended modal specification formula such that ∀t ∈ Domain(m), subT ransitions(t) ∩ Domain(m) = ∅. The reduction procedure based on the function underlying r is sound with respect to (in)validity of m: underlying(W) | = must m ⇔ underlying r (W, m) | = must m, and underlying(W) | = may m ⇔ underlying r (W, m) | = may m.

  It follows that, underlying(W) and underlying r (W, m) are weak trace equivalent with respect to the transitions set Domain(m). We can conclude that underlying(W) | = must m ⇔ underlying r (W, m) | = must m, and underlying(W) | = may m ⇔ underlying r (W, m) | = may m.

  Further, any execution of Ñ is an execution of N. As t Domain(m) and {g 1 , .., g n } ∩ Domain(m) = ∅, we can conclude that N and Ñ are weak trace equivalent with respect to the transitions set Domain(m). It follows that N | = must m ⇔ Ñ | = must m, and N | = may m ⇔ Ñ | = may m.

  It follows that N | = must m ⇔ Ñ | = must m, and N | = may m ⇔ Ñ | = may m.R 4 : Remove Transition Place

R 5 :

 5 N | = must m ⇔ Ñ | = must m, and N | = may m ⇔ Ñ | = may m. Remove Place Transition

  N | = must m ⇔ Ñ | = must m, and N | = may m ⇔ Ñ | = may m.R 6 : Remove Ring It remains to define φ RemoveR (m), a reduction rule which further constrains the conditions of application of the φ RemoveR reduction rule defined page 75.

  {t 1 , .., t m } ∩ Domain(m) = ∅, we can conclude that N and Ñ are weak trace equivalent with respect to the transitions set Domain(m). It follows that N | = must m ⇔ Ñ | = must m, and N | = may m ⇔ Ñ | = may m. For any given extended modal specification formula m, the six presented rules thus defines together a reduction kit, called Φ * (m), which strongly preserves the (in)validity of the extended modal specification formula m interpreted as either a may-formula or a must-formula. Indeed, given N and Ñ two workflow nets such that (N, Ñ) ∈ Φ * (m), we know that N | = must m ⇔ Ñ | = must m, and N | = may m ⇔ Ñ | = may m.

  2 and Figure 5.3(a) denotes the same place.

Figure 5 . 2 :

 52 Figure 5.2: Login and navigation coloured sub-workflow net

Figure 5 . 3 :

 53 Figure 5.3: sub-CWF-nets of the Question and Answer CWF-net

Example 20 :

 20 Example of an execution of the Question and Answer coloured workflow net

Figure 5 .

 5 Figure 5.4 presents one of the first refinements of this payout process modelled as a coloured workflow Petri net composed of 10 places and 16 transitions.

Figure 5 . 4 :

 54 Figure 5.4: Payout Process of the Tax Accounting Manager study case

Figure 5 .

 5 Figure 5.5 depicts the global architecture of the modal verification tool chain, which enables to verify modal specifications using either CLP or SMT resolution methods.

Figure 5 . 5 :

 55 Figure 5.5: Modal specification verification tool chain

Figures 5 .

 5 Figures 5.7 and 5.8 illustrate the encoding used to model the constraints seen in Chapter 3 respectively for the SMT-Lib and Prolog language.

Figure 5 .

 5 Figure 5.6: An example of workflow net

Figure 5 . 10 :

 510 Figure 5.10: The three execution's segments proposed by both solvers

  3 page 79. This tool, called Hadara-AdSimul-Red, is part of a dedicated open source workflow nets analysis tool suite, called Hadara-AdSimul. It has been developed during this thesis to conduct experimental work. This tool (including examples and source code) is available on Github 3 .

Figure 5 .Figure 5 . 11 :

 5511 Figure 5.11 depicts the global architecture of this tool.

Figure 5 .

 5 Figure 5.12: Example of the output of the execution of Hadara-AdSimul-Red

7

 7 QA | = must true, true, Register[u = u 1 ] ∧ .. ∧ Register[u = u t ] | = may true, true, CreateQ[r = client, u = u x ] TRUE 5 FALSE -∧Re f useA[r = client, u 1 = u x ] 7 TRUE TRUE p 10 QA | = must true, true, CommitQ[u 2 = u x ] ⇒ CommitA[u 2 = u x ] TRUE --TRUE ∧ArchiveQA[u 2 = u x ] p 11 QA | = musttrue, true, ¬CreateA[r = client] TRUE --TRUE p 12 QA | = may nbU sers > 3, true, CreateQ[u = u x ] ∧ ¬CreateQ[u = u y ] TRUE 12 TRUE TRUE p 13 QA | = must nbU sers < 3, true, ¬CreateQ[true] must true, true, CreateQ[true] ⇒ (Register[r = client] TRUE --TRUE ∧Register[r = seller] ∧ Register[r = admin]

p 16 T

 16 AM | = may true, true, correctPayoutForm[d > 0yPayoutForm[d > 0] p 18 T AM | = may true, true, correctPayoutForm[d = 3] TRUE 7 TRUE TRUE p 19 T AM | = must true, true, getBankReceipt[d > 0] TRUE --TRUE p 20 T AM | = must Mi(i) > (lvl12, lvl0), true, ManualApproval 1 [d > 0] TRUE --TRUE p 21 T AM | = may true, true, -|C < 300 TRUE 4 TRUE TRUE p 22 T AM | = may true, true, correctPayoutForm[d < 4] |C > 20000 FALSE --FALSE

Figure 5 .Figure 5 . 13 :

 5513 Figure 5.13 depicts the global architecture of the tool chain able to produce large benchmarks of workflow nets together with their (in)valid modal specifications. The elements in the middle line of the figure represent the thee tools above-mentioned, while the elements above and below represent data files.

Figure 5 .Figure 5 . 15 :

 5515 Figure 5.14: A workflow net satisfying the must-formula t 0 ∧ t 1 ∧ (t 2 ∨ t 3 ∨ t 4 )

Figure 5 .Figure 5 . 16 :

 5516 Figure 5.16: Workflow nets generation parameters and their values

  Figures 5.17, 5.18, 5.19, 5.20, 5.21, 5.22, 5.23 and 5.24 depict the plots displaying the verification times respectively spent by SICStus and Z3 for each class of workflow nets and types of modal specifications.

Figure 5 . 17 :

 517 Figure 5.17: State-machine -may-valid and must-invalid modal specifications

Figure 5 . 18 :

 518 Figure 5.18: State-machine -must-valid and may-invalid modal specifications

Figure 5 . 19 :

 519 Figure 5.19: Marked-graph -may-valid and must-invalid modal specifications

Figure 5 . 20 :

 520 Figure 5.20: Marked-graph -must-valid and may-invalid modal specifications

Figure 5 . 21 :

 521 Figure 5.21: Free-choice -may-valid and must-invalid modal specifications

Figure 5 . 22 :

 522 Figure 5.22: Free-choice -must-valid and may-invalid modal specifications

Figure 5 .

 5 Figure 5.23: Ordinary workflow nets -may-valid and must-invalid modal specifications

Figure 5 . 24 :

 524 Figure 5.24: Ordinary workflow nets -must-valid and may-invalid modal specifications

Figures 5 .Figure 5 . 25 :Figure 5 . 26 :

 5525526 Figure 5.25: Reduction factors of workflow nets of IBM-bpm

Figures 5 .Figure 5 . 27 :Figure 5 . 28 :

 5527528 Figure 5.27: Reduction time of workflow nets of the gen1

Contents 7 . 1

 71 Towards Parallelism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 7.2 Error-pattern . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 7.3 Reconfiguration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133

FiguresFigure 7 . 1 :

 71 Figure 7.1: Illustration of error-patterns

  Context and Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	Introduction
	Contents
	1.1

3 1.2 Research Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Contributions to this Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.4 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

  • p) become the input transitions of the initial place of N 2 and the output transitions of p (i.e. p • ) become the output transitions of the final place of N 2 . This operation is illustrated by Figure2.13.The second refinement operation is the transition refinement of a transition t ∈ T 1 with a workflow net N 2 which produces a new workflow net N = N 1 ⊗ t N 2 built by replacing the transition t by the workflow net N 2 : t is removed from N 1 , the initial place i 2 ∈ N 2 and the final place o 2 ∈ N 2 are removed from N 2 , the input places of p (i.e. • p) become the input places of the output transition of i 2 (i.e. i • 2 ) the initial place of N 2 , the output places of p (i.e. p • ) become the output places of the input transition of o 2 (i.e. • o 2 ) the final place of N 2 . This operation is illustrated byFigure 2.14.

	Figure 2.13: Illustration of the place refinement of place p with a workflow net N sub

3

  Verification of Modal specification "Being abstract is something profoundly different from being vague... The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise."-Edsger Dijkstra

Contents 3.1 Over Ordinary Workflow Nets . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.1.1 Extended Modal Specification . . . . . . . . . . . . . . . . . . . . . . 44 3.1.2 Modelling Executions of Workflow Nets . . . . . . . . . . . . . . . . . 46 3.1.3 Verifying Extended Modal Specifications . . . . . . . . . . . . . . . . 53 3.2 Over Abstract Workflow Nets . . . . . . . . . . . . . . . . . . . . . . . . . 55 3.2.1 Abstract Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 3.2.2 Extended Abstract Modal Specification . . . . . . . . . . . . . . . . . 59 3.2.3 Modelling Executions of Abstract Workflow Nets . . . . . . . . . . . . 61 3.2.4 Verifying Extended Abstract Modal Specifications . . . . . . . . . . . 64 3.3 Synthesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

  otherwise, -a transition instance (t, d) is seen as the transition t occurring d times. Example 18: Illustration of a generalised Petri net as an abstract Petri net Consider the generalised Petri net of Example 2 page 13 depicted in Figure 2.2(a) page 13. This generalised Petri net is composed of three places (H 2 O,O 2 and H 2) and a transition (t 1 ). Its incidence matrix is defined as:[-2, 1, 2] . The abstract Petri net corresponding and equivalent to this generalised Petri net is composed of the same three places and transition, and its incidence matrix is defined as:[x → -2 * x, x → 1 * x, x → 2 * x] .Coloured Petri Nets as Abstract Petri NetsA coloured Petri net (Section 2.1.5.2 page 19) is an abstract Petri net defined within the framework where D is the set C 1 ×..×C u over the colours C 1 , .., C u of the coloured Petri net , + D is the elementwise addition operation over u-uples, and ≤ D is the element-wise less-than-or-equal relation over u-uples. Let π C i be the projection of

Table 5 .

 5

2: Colours of Question and Answer coloured workflow net's places

Table 5 .

 5 6: Mean costs associated with transitions of the Payout Process

	Transition	Weight Transition	Weight
	requestApproval 1	10	requestApproval 2	10
	AutomaticApproval 1	10	AutomaticApproval 2	10
	ManualApproval 1	400	ManualApproval 2	500
	suggestPayoutForm	10	approvePayoutForm	120
	correctPayoutForm	100	veri f yPayoutForm	80
	sendPayoutForm	50	getBankReceipt	10
	handleRe jectedPayment 80	handleRe jectedPayment 60
	handleAcceptedPayment 30

Table 5 . 8 :

 58 Issue Tracking System: Experimentation results

Table 5 .

 5 10: Tax Accounting Manager: Experimentation results

Table 5 .

 5 8 page 105,Figure 5.4.3.3 presents data about the reduced workflow nets obtained after applications of the reduction methods while preserving the (in)validity of extended modal specification formulae interpreted as may-formula or must-formula.

	Reduced workflow net

#Property time(ms) |P| |T | rf actor

Table 5 .

 5

15: Reduction Results over the Issue Tracking System

Table 5 .

 5 The complete data-sets as well as the obtained experimental results are accessible at https://dx.doi. org/10.6084/m9.figshare.3573756.v5.Table 5.4.3.3 summarizes the results of our experiments for the IBM-bpm and SAP-ref benchmarks.

	Benchmark	Status	#workflow nets	#Nodes avg. max. avg. max. avg. max. r-factor(%) time(ms)
	IBM-bpm(libA)	Sound unknown	152 130	61.4 99.7	193 93.5 98.4 3.2 277 86.8 95.1 9.6	44 51
	IBM-bpm(libB1)	Sound unknown	107 181	38.6 98.6	228 86.7 98.7 3.8 360 82 95.8 7.1	67 54
	IBM-bpm(libB2)	Sound unknown	161 202	38.9 110.3 404 334	85 83	99.1 7.3 95.8 8.5	380 60
	IBM-bpm(libB3)	Sound unknown	207 214	47.5 125.7 454 85.2 252 87.8 98.8 3.9 96 8.7	56 72
	IBM-bpm(libC)	Sound unknown	15 17	127 135.6 480 84.7 94.9 5.1 548 94.4 99.5 7.1	46 28
	IBM-bpm(all)	Sound unknown	642 744	49 110.6 480 84.1 548 88.4 99.5 4.6 96 8.3	380 72
	SAP-ref	Sound unknown	0 590	-97.7	-512	-73	-95	-9.9	-967

[START_REF]Definition: Asymmetric Choice Net[END_REF]

: Results for the IBM-bpm and SAP-ref benchmarks

Table 5 .

 5 17: Reduction results over the workflow nets of the Model Checking Contest Regarding the 590 workflow nets of SAP-ref, only three of them are free choice workflow nets.

	Workflow name	|P|	|T | r -f actor t(ms)
	IBMB2S565S3960 (original) 274 180 IBMB2S565S3960 (reduced) 28 25	88.3%	53
	IBM5964 (original) IBM5964 (reduced)	264 140 19 17	90.0%	29
	IBM319 (original) IBM319 (reduced)	254 179 19 17	91.6%	22
	IBM703 (original) IBM703 (reduced)	263 285 2 1	99.4%	42

  17,815 nodes (resp. 147,640 nodes) in less that 180 seconds (resp. 90 minutes). These observations supported the fact that the reduction methods presented in Sections 4.2 page 77 and 4.3 page 79 constitute relevant, efficient, and scalable pre-processing steps toward the analysis of behavioural properties such as generalised soundness and correctness with respect to extended modal specifications. Verification of Modal specifications . . . . . . . . . . . . . . . . . . . . . . 127 6.2 Reduction methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 6.3 Experimental Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129

	6
	Conclusion
	Contents
	6.1
	III
	Conclusion and Future Work
	125

http://projects.eclipse.org/projects/modeling.sirius

https://github.com/LoW12/Hadara-AdSimul

http://www.adsimul.com/

www.ibm.com/software/products/en/modeler-basic

http://go.sap.com/product/enterprise-management/erp.html

; Variables declaration here ( d e f i n e -f un i n i t i a l M a r k i n g ( ( Ai I n t ) ( Ao I n t ) ( Ap1 I n t ) ) Bool ( and ( = Ai 1 ) ( = Ao 0 ) ( = Ap1 0 ) ) ) ( d e f i n e -f un f i n a l M a r k i n g ( ( Bi I n t ) ( Bo I n t ) ( Bp1 I n t ) ) Bool ( and ( = Bi 0 ) ( = Bo 1 ) ( = Bp1 0 ) ) ) ( d e f i n e -f un s t a t e E q u a t i o n ( ( Ai I n t ) ( Ao I n t ) ( Ap1 I n t ) ( Bi I n t ) ( Bo I n t ) ( Bp1 I n t ) ( Pi I n t ) ( Po I n t ) ( Pp1 I n t ) ( Tt1 I n t ) ( Tt2 I n t ) ( Tt3 I n t ) ) Bool ( and

) ) ( d e f i n e -f un f o r m u l a ( ( Tt1 I n t ) ( Tt2 I n t ) ) Bool ( and ( > Tt1 0 ) ( > Tt2 0 ) ) ) ( d e f i n e -f un noSiphon ( ( Ai I n t ) ( Ao I n t ) ( Ap1 I n t ) ( Bi I n t ) ( Bo I n t ) ( Bp1 I n t ) ( Pi I n t ) ( Po I n t ) ( Pp1 I n t ) ( Tt1 I n t ) ( Tt2 I n t ) ( Tt3 I n t ) ) Bool ( not ( e x i s t s ( ( Xi I n t ) ( Xo I n t ) ( Xp1 I n t ) ) ( and As illustration, the two input queries given in Figure 5.9 allow to determine, using respectively Z3 and SICStus, whether there exists a correct execution of the workflow given in Figure 5.6 made of three segments such that both t1 and t2 are fired. Note here that these inputs correspond to constraint systems modelling executions composed of at most three segments according to Definition 40 page 53.

Z3 input:

( a s s e r t ( i n i t i a l M a r k i n g M1i M1o M1p1 ) ) ( a s s e r t ( f i n a l M a r k i n g M3i M3o M3p1 ) ) ( a s s e r t ( f o r m u l a (+ T1t1 T2t1 T3t1 ) (+ T1t2 T2t2 T3t2 ) ) ) ( a s s e r t ( segment M1i M1o M1p1 M2i M2o M2p1 P1i P1o P1p1 T1t1 T1t2 T1t3 ) ) ( a s s e r t ( segment M2i M2o M2p1 M3i M3o M3p1 P2i P2o P2p1 T2t1 T2t2 T2t3 ) ) ( a s s e r t ( segment M3i M3o M3p1 M4i M4o M4p1 P3i P3o P3p1 T3t1 T3t2 T3t3 ) ) ( checks a tu s i n g smt ) ( get -model ) SICStus input:

Abstract:

Nowadays workflows are extensively used by companies and organisations in order to improve organizational efficiency, responsiveness and profitability by managing the tasks and steps of business processes. The verification of specifications has become mandatory to ensure that such processes are properly designed and reach the expected level of trust and quality. In this context, this thesis addresses the verification of modal specificationsnecessary or admissible behaviour involving several activities and their causalitiesof workflow nets -a Petri nets class suited for the description of workflows.

In particular, it defines an innovative constraint system based framework to model executions of ordinary as well as coloured workflow nets, and verify modal specifications. Further, it presents powerful reduction methods preserving properties of interest such as generalised soundness and correctness of a given modal specification. Such reduction methods are then portrayed as pre-processing steps reducing workflow nets size, so that the verification of preserved properties can be carried out on smaller instances. Finally, as a practical contribution, this thesis introduces the tools that have been implemented as well as experimentations that have been carried out over industrial workflow nets in order to validate the approaches proposed in this thesis. The convincing experimental results highlight the effectiveness, efficiency and scalability of the modal specification verification method and reduction methods introduced in this thesis.