Page 188 -

6 Declarative Workflow 179
constraint models allows for a wide range of possible execution alternatives, which
enhances flexibility.
The remainder of this chapter is organized as follows. First, our constraint-based
language for workflow specification is presented in Sect. 6.2. This section also dis-
cusses the possibility to verify constraint-based models and the ability to define
alternative languages and templates. Section 6.3 shows how declarative workflows
can be enacted, that is, how to create a runtime environment for execution. The pos-
sibility to change models while they are being executed (i.e., the so-called dynamic
change) is described in Sect. 6.4. Section 6.5 concludes the chapter, followed by
exercises and chapter notes.

6.2 Constraint-based Workflow Specification

A constraint-based workflow is defined by the specification of tasks and constraints.
In this section, we first show the formal foundation of a constraint specification
language. Then we introduce the concept of constraint templates, that is, reusable
constructs linking graphical notations to temporal logic. These templates also allow
for branching, that is, a construct can be associated to a variable number of tasks.
Then we introduce ConDec as an example language. This language is used in the
remainder of this chapter. We conclude this section by showing that such models
can be verified.

6.2.1 LTL-based Constraints

Various temporal logics have been proposed in the literature: Computational Tree
Logic (CTL), Linear Temporal Logic (LTL), etc. All these logics could be used to
specify constraints. In this chapter, we focus on Linear Temporal logic LTL.
LTL can be used to define properties of traces, for example, “after every occur-
rence of X eventually Y should occur.” In the context of workflow models, traces
correspond to sequences of tasks. Every trace represents an executed alternative
where the tasks in the trace occur exactly in the order in which they appear.
Definition 1 (Trace). Let T denote the universe of task identifiers, that is, the set
of all tasks. Trace 2 T is a sequence of tasks, where T is the set of all traces
composed of zero or more elements of T .Weuse Dht 1 ;t 2 ;::: ;t n i to denote a
trace consisting of tasks t 1 ;t 2 ;::: ;t n . i denotes the ith element of the trace, that is,
i D t i . e 2 denotes 9 1 i<j j Πi D e .We use C to concatenate two traces into a
new trace: he 1 ;e 2;::: ;e niChf 1 ;f 2 ;::: ;f m iD he 1 ;e 2 ;::: ;e n;f 1 ;f 2 ;::: ;f m i.
The concept of traces will be used to explain the semantics of LTL. However, we
first give the syntax of LTL. LTL provides the classical logic operators (:; ^; _; ),
and ,), and uses several temporal operators ( , ♦, , U ,and W ) that can be used
to specify constraints over the sequencing of workflow tasks. Definition 2 defines
the syntax of LTL.