Representing processes, constraints, and policies

With the logic described above one can represent standard procedures, as well as general policies and constraints in an uniform way. Let us assume the workflow described in figure 1. It is a simple procedure that uses the standard flow connectors [3,8]: and-split and and-join are represented by the empty circles, the or-split and or-joint are represented by the filled circles, activities are represented as squares and sequencing by the edges connecting activities.

  

Figure 1: A standard workflow process

That procedure can be represented as:

     

$$b\!\!\uparrow \rightarrow \stackrel{\leftarrow}{\Diamond}\!a\!\!\downarrow$$ (1)

$$d\!\!\uparrow \rightarrow \stackrel{\leftarrow}{\Diamond}\!b\!\!\downarrow$$ (2)

$$c\!\!\uparrow \rightarrow \stackrel{\leftarrow}{\Diamond}\!b\!\!\downarrow$$ (3)

$$e\!\!\uparrow \rightarrow \stackrel{\leftarrow}{\Diamond}\!d\!\!\downarrow$$ (4)

$$f\!\!\uparrow \rightarrow \stackrel{\leftarrow}{\Diamond}\!e\!\!\downarrow\land \stackrel{\leftarrow}{\Diamond}\!c\!\!\downarrow$$ (5)

Formula 1 states that if b has just started, then a must have ended sometime in the past. This formula states the precedence relation between a and b. Similarly, for formulas 2-4. Formula 5 states that if f has just started, then it must be true that both e and c ended sometime ago, but not necessarily at the same time.

But the formulas above only state the precedence relation among the activities, but not the fact that they should happen. To state that, one need the ``dual'' of the formulas above:

     

$$b\!\!\downarrow \rightarrow \stackrel{\rightarrow}{\Diamond}\!c\!\!\uparrow\land \stackrel{\rightarrow}{\Diamond}\!d\!\!\uparrow$$ (6)

$$d\!\!\downarrow \rightarrow \stackrel{\rightarrow}{\Diamond}\!e\!\!\uparrow$$ (7)

$$e\!\!\downarrow\land \stackrel{\leftarrow}{\Diamond}\!c\!\!\downarrow \rightarrow \stackrel{\rightarrow}{\Diamond}\!f\!\!\uparrow$$ (8)

$$c\!\!\downarrow\land \stackrel{\leftarrow}{\Diamond}\!e\!\!\downarrow \rightarrow \stackrel{\rightarrow}{\Diamond}\!f\!\!\uparrow$$ (9)

$$f\!\!\downarrow \rightarrow \stackrel{\rightarrow}{\Diamond}\!g\!\!\downarrow$$ (10)

The or-split is not yet represented in the formulas above. To represent it, we will need two auxiliary propositional symbols t₁and t₂. The issue with the or-split is that a) first it is not an or-split but an exclusive-or-split b) second, the choice implicit in the or-split is a choice of commitment to a particular branch, either the one that starts with b or the other one, that goes directly to g. Thus we will need the auxiliary propositional symbol to represent each branch.

    

$$a\!\!\downarrow \rightarrow \stackrel{\rightarrow}{\Diamond}\!((t_1 \lor t_2) \land \neg (t_1 \land t_2))$$ (11)

$$\rightarrow \stackrel{\rightarrow}{\Diamond}\!g\!\!\uparrow$$ t₁ (12)

$$\rightarrow \stackrel{\rightarrow}{\Diamond}\!b\!\!\uparrow$$ t₂ (13)

$$g\!\!\uparrow \rightarrow \stackrel{\leftarrow}{\Diamond}\!f\!\!\downarrow\lor \stackrel{\leftarrow}{\Diamond}\!t_1$$ (14)

Formula 11 states that after a ends, one must eventually choose between t₁ and t₂ but not both, or better, either t₁or t₂, but not both, must be true sometime in the future. Formula 12 states that if t₁ is chosen, then g will eventually follow, the other formula states that if t₂ is chosen , then b will follow. Finally, 14 states that g will start after either t₁ becomes true or f ends.

Policies can also be represented. For example, let us suppose that an organization has the policy that all meetings must be preceded by a call for that meeting with at least 3 time moments before the meeting (say, to comply with the organization's quality standards). That policy can be represented by the logic expression:

$$m_i \rightarrow\stackrel{\leftarrow}{\Diamond}\!_3 n_i$$ (15)

where m_i and n_i represent a meeting, and the call for that meeting, respectively.

Using logic it is possible to state some special properties of activities. For example, in business applications it is common to have activities that cannot be reexecuted, such as, ship merchandise to customer, or pay bill. The fact that an activity p cannot be redone, can be stated as:

$$p\!\!\downarrow\rightarrow\neg \stackrel{\rightarrow}{\Diamond}\!p\!\!\uparrow$$ (16)

That is, if p ended, then it is not true that it will start sometime in the future.

If an activity q can only be redone if a compensating activity ris executed, that can be stated as:

$$q\!\!\uparrow\land \stackrel{\leftarrow}{\Diamond}\!q\!\!\dow... ...arrow\land \stackrel{\leftarrow}{\Diamond}\! q\!\!\downarrow)$$ (17)

The formula states that if q just started, and it also started sometime in the past, then there must be a time in the past in which r started and before that q must have ended.