# Workflow Modelling and Analysis Based on the Construction of Task Models

Authors: Glória Cravo
Journal: The Scientific World Journal
 (2015)

---

## Abstract

We describe the structure of a workflow as a graph whose vertices represent tasks and the arcs are associated to workflow transitions in this paper. To each task an input/output logic operator is associated. Furthermore, we associate a Boolean term to each transition present in the workflow. We still identify the structure of workflows and describe their dynamism through the construction of new task models. This construction is very simple and intuitive since it is based on the analysis of all tasks present on the workflow that allows us to describe the dynamism of the workflow very easily. So, our approach has the advantage of being very intuitive, which is an important highlight of our work. We also introduce the concept of logical termination of workflows and provide conditions under which this property is valid. Finally, we provide a counter-example which shows that a conjecture presented in a previous article is false.


---

## Body

## 1. Introduction

A workflow is an abstraction of a business process that consists on the execution of a set of tasks to complete a process (e.g., hiring process, loan application, and sales order processing). Tasks represent unities of work to be executed that can be processed by a combination of resources, such as a computer program, an external system, or human activity.Recall that a business process is a collection of interconnected tasks that takes one or more kinds of input and creates an output that is of value to the customers. The construction of process models is very often a difficult accomplishment for humans since their design can be logically incorrect and enclose errors. So the development of tools to support the design of business processes is indispensable and needs to be based on a solid theory. We believe that our technique is appropriate to model workflows.Workflows have been successfully deployed to various domains, such as bioinformatics, healthcare, the telecommunication industry, the military, insurance, school administration, mobile computing, systems management, multidata bases, Internet, application development, object technology, operating systems, and transaction management.In the present paper, we use Graph Theory and Propositional Logic to describe the structure of workflows. It is important to point out that a workflow describes all of the tasks needed to achieve each step in a business process. Documents, information, work orders, reports, and so forth are passed from one task to another for action, according to a set of rules defined by the workflow. Employees or automated applications are the entities that carry out the execution of tasks.In particular we model workflows as trilogic acyclic directed graphs. The use of trilogic graphs to represent workflows was selected since most business process languages support three types of connectors: AND, OR, and XOR. It is important to emphasize that the inclusion of workflows with OR vertices is a significant advantage of our approach.Furthermore, our approach is based on the execution of all tasks present on the workflow. This analysis has the advantage of being simple and very intuitive. On the other hand, we can create new models based on the existing ones.Besides our formal framework allows checking the logical termination of workflows. The logical termination is an important property for workflows because it is indispensable to know if a workflow, such as the hiring process, will eventually finish. Analyzing the termination of workflows is an important assignment since research and commercial products, such as METEOR and TIBCO, have no support for verification. Errors made at design-time are not detected and result in very costly failures at run-time.The use of Propositional Logic has the advantage of transforming a workflow into a set of Event-Action (EA) models. Specialized EA models can be easily created to represent new advanced workflow patterns. Afterwards, Propositional Logic and Inference can be carried out on the EA models to analyze properties of workflow models.It is important to point out that, in the last decade, the rapid increase of business process modelling and management through the adoption of Workflow Management Systems has originated the need for frameworks that can be used to provide a formal technique for defining and analyzing workflows [1–3]. Important advancements have been accomplished in the development of theoretical foundations to allow workflow modeling, verification, and analysis. Several formal methods have been proposed, such as State and Activity Charts [4], Event-Condition-Action rules [5, 6], Petri Nets [7–11], Temporal Logic [12], Markov chains [13], Process and Event Algebras [14, 15], and Six Sigma Techniques [16, 17]. Nevertheless more research is required and specially focused on the use of Graph Theory. Based on this need, we develop our formalism that uses a natural combination of Graph Theory and Propositional Logic to model workflows. Besides, our formalism provides a formal framework based on trilogic acyclic directed graphs that facilitate modeling and analyzing workflows. Finally, our formal framework allows checking the logical termination of workflows.An important highlight of this paper is the emphasis on the tasks present in the workflow, which allows us to identify easily the dynamism present in the workflow. Finally, we describe the logical termination in a very intuitive form and we present conditions under which this property is valid.We still provide a counter-example which shows that a conjecture presented in a previous article is false.


## 2. Workflow Modelling and Analysis

This section is devoted to the presentation of our main results. In particular, we start this section by providing the formal definition of a workflow. In other words, we furnish the formal structure of a business process. Notice that this workflow structure can be also found in [18–21]. It is also important to point out that this type of graphs has an input/output logic operator associated with each vertex. Further, we analyze each model present on the workflow and give special emphasis to the execution of all tasks present in a workflow. Besides, we will create new models based on the existing ones. Finally, we will describe conditions under which a workflow logical terminates. In conclusion, our approach allows us to provide a complete description of workflows.Definition 1 (see [18–21]).
A workflow is a trilogic acrylic directed graphWG=(T,A,A′,M), where T={t1,t2,…,tn} is a finite nonempty set of vertices representing workflow tasks. Each task ti (i.e., a vertex) has attributed an input logic operator (represented by ≻ti) and an output logic operator (represented by ti≺). An input/output logic operator can be the logical AND (•), the OR (⊗), or the XOR—exclusive-or—(⊕). The set A={a⊔,a⊓,a1,a2,…,am} is a finite nonempty set of arcs representing workflow transitions. The transition a⊔ is the tuple (⊔,t1) and transition a⊓ is the tuple (tn,⊓), where the symbols ⊔ and ⊓ represent abstract tasks which indicate the entry and ending point of the workflow, respectively. Every transition ai, i∈{1,…,n} corresponds to a tuple of the form (tk,tl), where tk,tl∈T.
We use the symbol′ to reference the label of a transition; that is, ai′ references transition ai,  ai∈A. The elements ai′ are called Boolean terms and form the set A′.
Giventi∈T, the incoming transitions for task ti are the tuples of the form (tl,ti),  tl∈T, and the outgoing transitions are the tuples of the form (ti,tl),  tl∈T.
The incoming/outgoing condition of taskti is the Boolean expression ak1′φ⋯φakl′, where φ∈{•,⊗,⊕},  ak1′,…,akl′∈A′ and ak1,…,akl are the incoming/outgoing transitions of task ti. The terms ak1′,…,akl′ are connected with the logic operator ≻ti,  ti≺, respectively. If task ti has only one incoming/outgoing transition we assume that the condition does not have logic operator.
An Event-Action(EA) model for task ti is an implication of the form ti:fE⇝fC, where fE and fC are the incoming and outgoing conditions of task ti, respectively. An EA model has the behavior with two distinct modes: when fE is evaluated to true, fC is also evaluated to true; when fE is evaluated to false, fC is always false. And the EA model ti:fE⇝fC is true if both fE, fC are true; otherwise it is false. We say that the EA model ti:fE⇝fC is positive if its Boolean value is true; otherwise it is said to be negative.
We denote byM the set of all EA models present in WG.
Taskti is said to be executed if the EA model ti:fE⇝fC is positive. In this case, task ti has attributed the Boolean value true.Remark 2.
Given an expression whose Boolean value is true (resp., false), we simply can represent this fact by1, (resp., 0).Remark 3.
Given anEA model ti:fE⇝fC, if fE is false, then task ti disables all its outgoing transitions. Consequently fC is also false.Notice that the workflow starts its execution by enabling transitiona⊔, that is, by asserting a⊔′ to be true. In other words, the workflow starts its execution by executing task t1.Notice thatai′ is true if transition ai is enabled; otherwise ai is false. Transitions can be enabled by a user or by an external event. If the EA model ti:fE⇝fC is negative, then both fE,  fC are false. In this case, all the transitions of fC are disabled.Example 4.
In Figure1 we present a workflow WG=(T,A,A′,M), where T={t1,t2,…,t9},  A={a⊔,a⊓,a1,a2,…,a11},  A′={a⊔′,a⊓′,a1′,a2′,…,a11′}, and  M={t1:a⊔′⇝a1′•a2′,t2:a1′⇝a3′⊕a4′, t3:a2′⇝a8′,t4:a3′⇝a5′⊕a6′,t5:a4′⇝a7′,t6:a5′⇝a9′,t7:a6′⇝a10′,t8:a7′⊕a9′⊕a10′⇝a11′, t9:a8′•a11′⇝a⊓′}.
The output logic operator of taskt2(t2≺) is XOR (⊕), while the input logic operator of task t9(≻t9) is an AND (•).
The incoming transition for taskt2 is a1=(t1,t2) and its outgoing transitions are a3=(t2,t4) and a4=(t2,t5). Hence the incoming condition for task t2 is a1′, while its outgoing condition is a3′⊕a4′.
Taskt2 is executed if the EA model t2:a1′⇝a3′⊕a4′ is positive, that is, if a1′ is true and only one of the Boolean terms a3′, a4′ is true.Figure 1
Example of a workflow.Notice that the workflow from Figure1 corresponds to the following real situation. Indeed, it can represent the tasks necessary to be executed for a person driving a new car. Let us assume that tasks ti, i∈{1,…,9} have the following meanings:t1: deciding to purchase a new car to own use;t2: payment of the car;t3: getting the drivers license;t4: deciding to pay by credit;t5: deciding to pay without credit;t6: getting rental credit;t7: getting bank credit;t8: purchasing of the car;t9: driving the new car.Clearly, the decision of purchasing a new car to own use implies to pay the car and to get the drivers license. The payment of the car implies the execution of only one of the situations to pay by credit or to pay without credit. And to get credit implies to get a rental credit or a bank credit. It is clear that the purchase of the car depends on the execution of only one of the tasks: decide to pay without credit, get rental credit, and get bank credit.Hence, the possibility to drive a new car depends on the purchase of the car and in obtaining the drivers license. In other words, the execution of taskt9 depends on the execution of both tasks t3, t8.Many other examples can be given. Indeed, too many situations in our life can be described by workflows. For example, the request for a credit card or a loan application is simple examples of workflows.Proposition 5.
LetWG=(T,A,A′,M) be a workflow. Let al=(ti,tj)∈A,  ti,tj∈T. If al′ is true, then ti is necessarily executed.Proof.
Let us assume thatal′ is true. Let ti:fEi⇝fCi be the EA model associated to task ti. If task ti is not executed, then the EA model ti:fEi⇝fCi is negative. Since the EA model is negative, all outgoing transitions of task ti are disabled; in particular al is disabled, that is, al′ is false, wich is a contradiction. Hence task ti is executed.Remark 6.
The condition of Proposition5 is not sufficient. For example in the workflow from Figure 1, if task t2 is executed, then the EA model t2:a1′⇝a3′⊕a4′ is positive. For a1′=true, a3′=true, a4′=false,  and a4=(t2,t5),  t2 is executed, but a4′ is false.Remark 7.
Let us consider the Boolean termal′ where al=(ti,tj)∈A,  ti,tj∈T. If al′ is true, task tj is not necessarily executed. For example, in the workflow from Figure 2, let us assume that a⊔′=true, a1′=true,  a2′=false, a3′=true, a4′=true, a5′=true,  a6′=true, a7′=true, a8′=true, and  a⊓′=false. Hence, for this assignment the EA model t7:a6′⊕a8′⇝a⊓′ is negative, which means that task t7 is not executed. Nevertheless, a8=(t6,t7) and a8′ is true.Figure 2
Example of a workflow.Next we introduce the concept of logical termination. This is a very important structural property, since its analysis will allow to verify if a workflow will eventually finish, according to the initial specifications.Definition 8.
LetWG=(T,A,A′,M) be a workflow. One says that WG logically terminates if task tn is executed whenever task t1 is executed.In the following result we establish a necessary and sufficient condition for the logical termination.Theorem 9.
LetWG=(T,A,A′,M) be a workflow. Then WG logically terminates if and only if a⊓′ is true whenever a⊔′ is true.Proof.
Let us assume thatWG logically terminates; that is, task tn is executed whenever task t1 is executed. This means that the EA model tn:fEn⇝a⊓′ is positive whenever the EA model t1:a⊔′⇝fC1 is positive. Bearing in mind that WG starts its execution by executing task t1, then the EA model t1:a⊔′⇝fC1 is positive. Hence the EA model tn:fEn⇝a⊓′ is also positive. Consequently, a⊔′,  fC1,  fEn,  and a⊓′ are true. Thus, a⊓′ is true whenever a⊔′ is true.
Conversely, let us assume thata⊓′ is true whenever a⊔′ is true. Let us assume that task t1 is executed. This means that the EA model t1:a⊔′⇝fC1 is positive. Bearing in mind that a⊓′ is true, according to the behavior of the EA models, necessarily fEn is true. Hence the EA model tn:fEn⇝a⊓′ is positive, which means that task tn is executed. So we can conclude that task tn is executed whenever task t1 is executed, which means that WG logically terminates.Example 10.
It is not hard to check that, in the workflow from Figure1, a⊓′ is true whenever a⊔′ is true. Thus, the workflow logically terminates.Next we address our study on the dynamism present in a workflow. Obviously the dynamism is associated with the sequential execution of its tasks. In the workflow from Figure1 the execution of task t1 implies the execution of both tasks t2, t3; the execution of task t2 implies the execution of only one of the tasks t4, t5; the execution of task t4 implies the execution of only one of the tasks t6, t7; the execution of only one of the tasks t5, t6, and t7 implies the execution of task t8. Finally, the execution of both tasks t3, t8 implies the execution of task t9. Hence, we can state the execution of task t1 implies the execution of t2•t3; the execution of task t2 implies the execution of t4⊕t5; the execution of task t4 implies the execution of t6⊕t7; the execution of t5⊕t6⊕t7 implies the execution of task t8; the execution of t3•t8 implies the execution of task t9. Notice that when we consider t2•t3, the operator • is the output logic operator of task t1, while when we consider t5⊕t6⊕t7,  ⊕ is the input logic operator of task t8.These remarks led us to introduce the following concept.Definition 11.
LetWG=(T,A,A′,M) be a workflow. The compound tasks of WG are the elements of the following form: ti1φti2φ⋯φtik,ti1,ti2,…,tik∈T,  φ∈{•,⊗,⊕}. The set of all compound tasks of WG is denoted by T′; that is,
(1)T′=ti1φti2φ⋯φtik:ti1,ti2,…,tik∈T,φ∈•,⊗,⊕.Example 12.
In the workflow from Figure1, T′={t2•t3,t4⊕t5,t6⊕t7,t5⊕t6⊕t7,t3•t8}.Remark 13.
Since every taskti has associated a Boolean value, according to its execution, it is also natural to attribute a Boolean value to the compound tasks of WG. The natural attribution is the following. Given any compound task of WG,  ti1φti2φ⋯φtik,φ∈{•,⊗,⊕}.
Ifφ=•, then the Boolean value of ti1φti2φ⋯φtik is 1 if and only if the Boolean value of all tasks ti1,ti2,…,tik is equal to 1.
Ifφ=⊗, then the Boolean value of ti1φti2φ⋯φtik is 1 if and only if there exists at least one of the tasks ti1,ti2,…,tik whose Boolean value is equal to 1.
Ifφ=⊕, then the Boolean value of ti1φti2φ⋯φtik is 1 if and only if there exists only one of the tasks ti1,ti2,…,tik with Boolean value equal to 1.
Naturally, we can state that a compound taskti1φti2φ⋯φtik is executed if and only if its Boolean value is equal to 1, which means that the compound task ti1φti2φ⋯φtik is positive. In other words, ti1φti2φ⋯φtik is executed if and only if, one of the following cases holds:
Ifφ=•, all tasks ti1,ti2,…,tik are executed.
Ifφ=⊗, at least one of the tasks ti1,ti2,…,tik is executed.
Ifφ=⊕, only one of the tasks ti1,ti2,…,tik is executed.In what follows, we introduce a new type of task models that we designate by compound task models.Definition 14.
LetWG=(T,A,A′,M) be a workflow. Let ti,tj,ti1,ti2,…,tik,tj1,tj2,…,tjl∈T, φ,ψ{•,⊗,⊕}. A compound task model is an implication with one of the following forms:(1)
ti↪tj1ψtj2ψ⋯ψtjl;(2)
ti1φti2φ⋯φtik↪tj;(3)
ti1φti2φ⋯φtik↪tj1ψtj2ψ⋯ψtjl.
Usually we represent a compound task model bytIi↪tOi, where tIi is called the incoming task and tOi is called the outgoing task. We say that a compound task model tIi↪tOi is positive if both incoming and outgoing tasks are positive, that is, if both tasks tIi, tOi are executed.
In particular, the implication of the formti↪tj is called a simple task model. Clearly, it is positive if both tasks ti, tj are executed.
The set of all simple and compound task models present inWG is called the set of task models of WG and is denoted by TM.
The task models have the behavior with two distinct modes: if its incoming task is true, necessarily its outgoing task is true; if the incoming task is false, the outgoing task is false. In other words, iftIi↪tOi is a compound task model, then tIi is executed if and only if tOi is executed.Notice that, in a compound task modeltIi↪tOi, at least one of the tasks tIi,  tOi is compound.Example 15.
In the workflow from Figure1, the set of its task models is TM={t1↪t2•t3,t2↪t4⊕t5,t4↪t6⊕t7,t5⊕t6⊕t7↪t8,t3•t8↪t9}.From now on, we use the symbol↔ with the following meaning: X↔Y means that the compound statements X and Y are logically equivalent.According to simple rules of Logic and taking into account the behavior of the task models, we can infer the following result. And the establishment of this result allows us to identify new task models present in the workflow.In what follows we establish some properties that will allow us to create new task models based on the existing ones.Proposition 16.
LetWG=(T,A,A′,M) be a workflow. Suppose that the task models tIi↪tOi and tOi↪tOj belong to TM. Then the model tIi↪tOj still hods in WG.Proof.
The proof is trivial.Theorem 17.
LetWG=(T,A,A′,M) be a workflow.(a)
If both task models(2)tIi↪tOi,(3)tIj↪tOj
belong to TM, where tOi↔tIj, then the model tIi↪tOj still holds in WG.(b)
If both task modelstIi↪tOi and tIj↪tOj belong to TM, where tOi↔tLφtIj,  φ∈{•,⊗,⊕}, then the compound task model tIi↪tLφtOj still holds in WG.(c)
If both task modelstIi↪tOi and tOj↪tIj belong to TM, where tOi↔tLφtIj,  φ∈{•,⊗,⊕}, then the compound task model tIi↪tLφtOj still holds in WG.(d)
If both task modelstIi↪tOi and tIj↪tOj belong to TM, where tIi↔tLφtIj,  φ∈{•,⊗,⊕}, then the compound task model tLφtOj↪tOi still holds in WG.(e)
If both task modelstIi↪tOi and tOj↪tIj belong to TM, where tIi↔tLφtIj,  φ∈{•,⊗,⊕}, then the compound task model tLφtOj↪tOi still holds in WG.Proof.
(a) Let us assume that both task models (2) and (3) belong to TM. Notice that if either (2) or (3) is negative, since tOi↔tIj, then necessarily both task models (2) and (3) are negative. So, we just need to verify the result when both task models (2) and (3) are positive.
Let us assume that both tasks models (2) and (3) are positive. Since (2) is positive, necessarily both tIi, tOi are true. In other words, some of the tasks from tIi, tOi are executed allowing that tIi, tOi are executed. Bearing in mind that tOi↔tIj, then tIj is true. So according to the behavior of the task models, necessarily tOj is true. Hence we can state that tOj is executed, whenever tIj is executed. Therefore the model tIi↪tOj still holds in WG.
Now, in order to prove (b) and (c), we start with the following argument. Bearing in mind thattOi↔tLφtIj, according to the behavior of the task models, we can consider that tOi↪tLφtIj still holds in WG. Since tIi↪tOi and tOi↪tLφtIj holds in WG, according to Proposition 16 we can conclude that
(4)tIi↪tLφtIj
still holds in WG.
(b) Taking into account thattIj↪tOj belong to TM, and consequently tIj,  tOj have the same Boolean value, we can replace tIj by tOj in (4), obtaining the new model tIi↪tLφtOj, which means that tIi↪tLφtOj still holds in WG.
(c) Taking into account thattOj↪tIj belong to TM, and consequently tOj, tIj have the same Boolean value, we can replace tIj by tOj in (4), obtaining the new model tIi↪tLφtOj, which means that tIi↪tLφtOj still holds in WG.
Analogously, in order to prove (d) and (e) we start by making the next statement. Taking into account thattIi↔tLφtIj, according to the behavior of the compound task models, we can consider that tLφtIj↪tIi holds in WG. Since tLφtIj↪tIi and tIi↪tOi hold in WG, according to Proposition 16 we can conclude that
(5)tLφtIj↪tOi
still holds in WG.
(d) Bearing in mind thattIj↪tOj holds in WG, and consequently tIj, tOj have the same Boolean value, we can replace tIj by tOj in (5), obtaining the new model tLφtOj↪tOi, which means that tLφtOj↪tOi still holds in WG.
(e) Bearing in mind thattOj↪tIj holds in WG, and consequently tOj, tIj have the same Boolean value, we can replace tIj by tOj in (5), obtaining the new model tLφtOj↪tOi, which means that tLφtOj↪tOi still holds in WG.The previous results allow us to identify new task models based on the existing ones, as it is described below.Definition 18.
LetWG=(T,A,A′,M) be a workflow. An extended task model is a model obtained by applying a finite sequence of some of the properties established in Proposition 16 and Theorem 17. One adopts the notation TM′ to represent the set of all extended task models of WG.Example 19.
In the workflow from Figure1, bearing in mind that t1↪t2•t3, t2↪t4⊕t5∈TM, according to Theorem 17 we can conclude that the model t1↪(t4⊕t5)•t3 still holds in WG. Therefore, we can state that t1↪(t4⊕t5)•t3 is an extended task model of WG.Notice we adopt the same notation of the task models to represent the extended task models. Furthermore, the extended task models verify the same properties of the task models. In particular, given an extended task modelB↪C, necessarily both B, C have the same Boolean value.Naturally when we consider the set of all task models and extended task models presented inWG, we obtain all possible models that can be generated by the task models of the workflow. This set of task models will be designated by the closure of TM. In certain sense, we can state that the set of all task models from WG is a set of generators of all possible models of WG.Definition 20.
LetWG=(T,A,A′,M) be a workflow. One defines the closure of TM as the set of all task models and extended task models in WG. This set is denoted by TM*. In other words, TM*=TM∪TM′.Example 21.
As we saw in Example15 in the workflow from Figure 1, TM={t1↪t2•t3,t2↪t4⊕t5,t4↪t6⊕t7,t5⊕t6⊕t7↪t8,t3•t8↪t9}. Since t1↪t2•t3,t2↪t4⊕t5∈TM, according to Theorem 17 we can deduce that t1↪(t4⊕t5)•t3∈TM*. Now bearing in mind that t4↪t6⊕t7∈TM, applying again Theorem 17 we can conclude that t1↪((t6⊕t7)⊕t5)•t3∈TM*. As (t6⊕t7)⊕t5↔t5⊕t6⊕t7 we can state that t1↪(t5⊕t6⊕t7)•t3∈TM*. Bearing in mind that t5⊕t6⊕t7↪t8, applying once more Theorem 17 we infer that t1↪t8•t3∈TM*. As t8•t3↔t3•t8, applying again Theorem 17 we conclude that t1↪t9∈TM*.Notice the workflow from Figure1 logically terminates and t1↪t9∈TM*. Furthermore, we studied many other examples of workflows that logically terminates and simultaneously t1↪tn∈TM*. The analysis of these different cases led us to formulate the following conjecture.Conjecture 22 (see [21]).
Given a workflowWG=(T,A,A′,M), then WG logically terminates if and only if t1↪tn∈TM*.After the analysis of many cases, we start believing that the conjecture was true. Nevertheless it is false, as the following example proves. Let us consider the following workflow.Example 23.
It is not hard to check that the workflow from Figure3 logically terminates; nevertheless the condition t1↪tn∈TM* is not valid.Figure 3
Example of a workflow.Indeed the condition of the Conjecture22 is not necessary. However it is sufficient, as we prove in the following result.Theorem 24.
LetWG=(T,A,A′,M) be a workflow. If t1↪tn∈TM*, then WG logically terminates.Proof.
Let us assume thatt1↪tn∈TM*.
Case 1. Suppose that t1↪tn∈TM. This means that WG has the following structure:
(6)⊔⟶a⊔t1⟶a⊓t⊓.
In this case,t1=tn. Since WG starts its execution by executing task t1 we can conclude that task tn is executed whenever task t1 is executed, which means that WG logically terminates.
Case 2. Suppose that t1↪tn∈TM*∖TM=TM′. So, t1↪tn was obtained by applying some of the results established in Proposition 16 and Theorem 17. Since t1↪tn∈TM* and the workflow starts its execution by executing task t1, that is, by asserting t1 to be true, according to the behavior of the extended models, necessarily tn is still asserted to be true. This means that task tn is executed. Hence, task tn is executed whenever task t1 is executed. Thus WG logically terminates.


## 3. Conclusions

In this paper we develop a formalism to describe and analyse the structure of workflows, based on graphs and Propositional Logic. Indeed, we describe the structure of a workflow as a graph whose vertices represent tasks and the arcs are associated to workflow transitions. To each task an input/output logic operator is associated and this logic operator can be the logical AND(•), the OR (⊗), or the XOR—exclusive-or—(⊕). Furthermore, we associate a Boolean term to each transition present in the workflow.It is important to point out that our main emphasis is the analysis of a workflow through the study of its task models which allows us to describe the dynamism of the workflow in a very simple and intuitive way.Another relevant aspect of our approach is the introduction of the concept of compound tasks. This concept allows us to identify new task models based on the existing ones. Through these new task models we are able to describe the dynamism present in a workflow in a very simple way. Clearly, the study of the dynamism of a workflow is equivalent to analyse the sequential execution of its tasks.We still analyze the concept of logical termination and we provide necessary and sufficient conditions under which this property is valid.Finally, given a workflowWG we provide a counter-example which shows that the conjecture of t1↪tn∈TM* being a necessary and sufficient condition under which WG logically terminates is false. In fact, the condition is necessary; nevertheless it is not sufficient.



---

*Source: 481767-2015-01-29.xml*