The Workflow State Machine
Syntax
A workflow description is called a workflow schema . It is a guarded automaton:
W = ( S , T , E , C , A , V , s0 )
with

S is a set of states

E is a set of events

C is a set of conditions

A is a set of actions

V is a set of boolean variables

Ass is a set of assignments: Ass subseteq V x {true, false}

T is a set of transitions: T subseteq E x S > S x CS x AS

with

CS subseteq C

AS = {(A1, ..., An)} for Ai in A union Ass and n in N0


s0 in S is the initial state
Semantics
A workflow instance is defined as follows:
I = ( W , s , i )
with

a workflow schema W = ( S , T , E , C , A , V , s0 )

a current state s in S

a variable instantiation i : V > {true, false}
Be I = ( W , s , i ) a workflow instance. The successor of I for the event e is
(a) the workflow instance I ' = ( W , s ', i ') with

there is a t in T with

t = ( e , s , s ', cs , as )

all c in cs are complied


i '(v) = b for all v with (v, b) in as

i '(v) = i (v) for all other v
(b) I , if such a t does not exist.
Invoking a Transition
When an event e is invoked on a workflow instance I, the following algorithm is executed:
 The current state s_{current} is determined.
 The transition t from s_{current} to s_{next} which has the event e is determined.
 If t is not exactly defined, an exception is thrown.
 All conditions of t are validated.
 If all conditions are complied, the transition t fires:
 All assignments of t are executed.
 The workflow instance I is advanced to the state s_{next} .