Page 190 -

6 Declarative Workflow 181
Table 6.1 Formal specification of constraints with LTL
LTL formula for Automaton representing Semantics
constraint c T
c
!bill –
♦ bill Task bill must be executed at
bill
s0 s1 least once

!bill –

Š.bill/U pickup Task bill cannot be executed
pickup
s0 s1 until task pickup is exe-
cuted

The set of possible execution traces satisfying an LTL constraint is defined as
follows.
Definition 4 (Constraint satisfying traces T ). Let constraint c be an LTL

c
formula. Then the set of traces satisfying c is defined as T Df 2 T j cg.

c
In the field of model checking, LTL is extensively used to check whether a system
satisfies properties specified by LTL formulae. Using the results from this field, it is
possible to generate a nondeterministic finite state automaton that represents exactly
all traces that satisfy the LTL formula. For a constraint c, specifiedbyanLTL for-
mula, the set of all traces satisfying c (T ) is exactly the language produced by

c
the automaton generated for this formula using the algorithm of D. Giannakopoulou
and K. Havelund. Table 6.1 shows two examples illustrating the general idea. It is
not important to understand how the automata are generated; however, to under-
stand our approach it is important to understand that for any LTL constraint a
corresponding automaton can be generated. This automaton will be used to enforce
constraints, detect violations, and to check the consistency of a specification. Sec-
tion 6.3 describes how the LTL-based automata can be used for declarative workflow
execution.
The next example gives the LTL constraints for a process involving tasks such
as shipment (i.e., Create Shipment Information Document), bill (i.e., Create Bill of
Lading), and pickup (i.e., Arrange Pickup Appointment). In this example, the num-
ber of constraints is small and it is not difficult to determine whether a trace satisfies
the given constraints, or not. For larger models this is less intuitive. Therefore, the
next subsection proposes constraint templates as a graphical way to represent LTL
formulas.
Example 1 (Constraint satisfying traces). Consider the two constraints described in
Table 6.1 for the execution of tasks bill and pickup;(c 1 ) ♦bill and (c 2 ) Š.bill/U
pickup. Examples of traces satisfying constraints c 1 and c 2 are hpickup; billi c 1 ^
c 2 and hpickup; pickup; billi c 1 ^ c 2 . Traces not satisfying constraints c 1 and c 2
are " c 1 ^ c 2 , hpickupi c 1 ^ c 2 ,and hbill; pickupi c 1 ^ c 2 . Note that " c 2 .