This paper gives a Concurrent Transaction Logic (CT R)based formal model for Weakly-structured Scienti c Work ows (WsSWFs) and further implements it in an open source rule language Prova. Compared with the related e orts, the formal model in this paper focuses on conversation-based reactive work ow logic representation and event-driven computation of complex event patterns.
The current focus of existing solutions for scienti c work ows is on the orchestrated and pre-structured execution of computational intensive and dataoriented tasks, instead of the goal-oriented and decision-centric tasks that need coordination of scientists or computer agents (aka. expert system agents) as a team supported by semi-automated Weakly-structured scienti c work ows (WsSWFs).
Such WsSWFs contain tasks that are goal-oriented and that need to be
executed on the basis of dynamic decisions which the agents can take in order to
adapt to unforeseen uncertainties in the execution and to dynamically changed
(scienti c) knowledge about the scienti c problems [
For the purpose of reducing ambiguity and opening possibilities for veri
cation and analysis, this paper gives a Concurrent Transaction Logic (CT R)-based
formal declarative model for the WsSWFs. Work ow formal models provide a
theoretical foundation to work ow programming languages and can be used to
support the design of work ow languages and of their interpreters, compilers
and optimizers as well as of debuggers, and to support the de nition of veri
cation procedures, similar to those used for verifying the correctness of complex
business transactions [
The remainder of this paper is organized as follows: Section 2 presents a WsSWF use case. Section 3 gives a brief overview of CT R. Section 4 explains how CT R is used as an underlying formalism to represent the WsSWFs. Section 5 demonstrates how the CT R-based work ow logic can be translated into a Web rule language Prova. Section 6 introduces the related e orts and the conclusion is given in Section 7. 2
This section gives a WsSWF use case taken from the EDIT (European
Distributed Institute of Taxonomy)1 to identify and treat newly discovered ants.
We adapt it from [
The process involves the collaboration of three participants: eldworker, taxonomist and curator. A eldworker who often works in the countryside rstly triggers the identi cation process by describing a newly discovered ant, then sends the description to a taxonomist, who has experience and expertise to perform the identi cation and know how to treat it. The eldworker may consult the requirements for ant description if necessary. The identi cation results are
usually ant scienti c names. After the identi cation, the taxonomist sends the results to a curator who is in charge of managing the identi cation results. In order to automate this process, we employ agents to simulate these participants and their interaction. The intelligent agents act on their behalf by using a local knowledge base of reaction and derivation rules.
Ants di er widely in their food requirements and behaviors, some pests even
can cause a serious impact on crops. In case of a pest, the corresponding
treatment schemes are also needed to provide to the eldworker. The identi cation
task involves complicated decision logic to distinguish an ant from its
homogeneous groups and is represented as a sub-process (with a \+" mark in the
notation). The details of the identi cation process are shown in Figure 2.
During the identi cation, there are two steps to assign the identi cation task to an
agent that has the appropriate knowledge base: (1) narrowing down the scope of
agents that can perform the identi cation based on the location of ant discovery;
(2) nding an agent that has the best performance (e.g., success rate) in that
area. Afterwards, the ant scienti c name is determined in terms of a knowledge
base consisting of domain rules and facts. Likewise, the tasks of identi cation
assignments and getting pest treatment are also encoded with domain rules
and facts. These knowledge-intensive decision-centric tasks are represented as
rounded rectangles with small table notations in them. Moreover, if a discovered
ant is extraordinary, it might involve domain experts to identify it manually.
Transaction Logic (T R) is a general logic that accounts for state changes in
database, logic programs and arbitrary logical theories in a clean and
declarative way [
For the purpose of allowing concurrent update operations, CT R further
extends T R with a new connective, j (aka. concurrent conjunction), and one modal
operator [
means both and must be executed along the same path.
means execute or non-deterministically.
means execute in any way provided that this will not be a valid execution { { {
means rst execute , then execute . j means that and execute concurrently.
, means that the execution of should not be interleaved with other transactions.
Concurrent processes in CT R execute in an interleaved fashion and can
communicate and synchronize themselves, thereby increasing exibility,
performance, and power of the language. In contrast to other related research e orts,
CT R is the only deductive database language that integrates concurrency,
communication and database updates in a completely logical framework, including
a natural model theory and a sound-and-complete proof theory [
In CT R, the elementary database operations are encapsulated as a pair of oracles. The oracles come with a set of database states, upon which they can operate. Each database state could be seen as a set of data items, which are accessed by data and transition oracles. The data oracle, Od(D), which maps from database states to sets of rst-order formulas, i.e., Od(D) presents queries related to a particular state D. The transition oracle, Ot(D1, D2), which maps pairs of states to set of ground atomic formulas, i.e., these transition oracles represented by the ground atomic formulas cause database state changes. For example, if a 2 Ot(D1, D2), then a is an elementary update that changes the state from D1 to D2. In other words, the oracles provide semantics for data items: a static semantics querying a particular state and a dynamic semantics changing states.
The semantics of CT R is based on multi-paths or m-paths, which are generalized from the notion of T R paths. Formally, an m-path is a nite sequence of paths, where each path presents a period of continuous execution. For example, if D1, D2, ..., D8 are database states, then hD1D2D3, D4D5, D6D7D8i is an m-path. CT R formulas are interpreted by an m-path structure, which speci es those atoms are true on the m-path. Intuitively, a transaction formula is true on an m-path represents an action that takes place along the m-path.
Work ow Modeling A work ow in this work generally de nes a process as a set of ow elements that comprise tasks and gateways. Each task has a speci c objective that contributes somehow to a work ow goal. The work ow describes how tasks can interact at a message level, with a de nition of the control and data ow. A gateway controls the ow of a process and it implies a mechanism that either allows or disallows passage through the gateway. In general, each gateway involves a set of condition expressions associated with the gateway's incoming or outgoing sequence ows. The data ow captures data dependencies between tasks, and some data may be shared within a task or across several di erent tasks. In this work, we consider the data passing between tasks as event messaging, which not only can act as \data carrier", but also can be used a basis for representing composite events, thereby implementing complex work ow patterns, especially state-based work ow patterns.
De nition 1 (Scienti c Work ow). A scienti c work ow is a collection of coordinated tasks composed to achieve complex goals. In CT R, it is represented as a CT R Horn goal.
A CT R Horn goal is any formula with the form:
is a CT R Horn goal. { any atomic formula is a CT R Horn goal; { if and are CT R Horn goals, then so are the expressions: _ ; { , where
In work ow management systems, the tasks can be classi ed into two groups: primitive task and composite task. A primitive task is an atomic unit in workows, and a composite task de nes the execution order of a set of tasks. De nition 2 (Primitive Task). The primitive task corresponds to an atomic activity in a work ow and it is represented in CT R as a predicate.
A primitive task represented by the predicate has the following format: p(arg1; :::; argn):
Here, the predicate p denotes the name of task and arg1, ..., argn (n>1) are simple terms. Since this work focuses on representing complex work ows using CT R, the details of task arguments are abbreviated as p(X), where X denotes all the arguments that p takes.
The states in CT R-based work ow modeling are regarded as data sets. Each state is a set of data items that represent current work ow status. More precisely, the data oracle Od(D) which corresponds to the queries to a particular state. The transition oracle is de ned as a task that consumes data to achieve certain goals. Formally, for a task has both input(s) and output(s), task(i, o) 2 Ot(D1, D2) i D2 = D1 [ fog - fig. Here, i and o represent the input(s) and output(s) of a task, respectively. For a task has only input(s), task(i) 2 Ot(D1, D2) i D2 = D1 - fig.
Similar to CT R that deals with state changes in deductive databases, a primitive task can both change the work ow state and act as a query to return an answer, which we refer to as update-tasks and query-tasks, respectively in this paper. The update task predicates are the ones which cause state transitions from one to another. The query task predicates are used to query the work ow state. They are helpful during the data passing between tasks. For example, a task needs to check if it can be started, such as its precedent tasks are completed or required data for its execution are available. This paper considers data passing as event messages, more details about event-based condition representation can be found in Section 4.3.
isP est(N ame)
treatment(N ame; Scheme)
The execution of primitive tasks may also be guarded by conditional statements, i.e., preconditions and post-conditions in work ows. For example, the above formula denotes that the treatment is only required if the ant is a pest. The atom isPest(Name) must return true in order for the treatment to succeed. Di erent with simple qualifying truth-valued conditions, this kind of condition evaluation (e.g., the pest evaluation) usually involves complex decision logic depending on the amount and quality of knowledge about a scienti c domain. De nition 3 (Composite Task). A composite task (aka. sub-work ow or subprocess) is the composition of a set of tasks, which could be primitive or composite. The composite task is de ned as a CT R Horn rule with a form p , where p is an atomic formula and is a CT R Horn goal.
Since they de ne the composition of a work ow, this work refers CT R Horn rules to work ow formation rules. The head of the work ow formation rule is a predicate, which corresponds to a composite task only. As the primitive task, the name of the predicate denotes the name of a composite task. The body of the work ow formation rules recursively gives the de nition of the composite task. For example, the process of ant identi cation is represented as: identP rocess Assign1 Assign2 (checkF ood j checkN est j checkBody). The identi cation starts with a two-step sequential task assignment. After that, there are three parallel tasks that respectively validate ant food preference, nest structure and body feature.
In this paper, the connectives: , j, and _ have the following semantics: { {
: execute task after task . Model-theoretically, is satis ed (or is true) on an m-path if only if and are true on some m-paths 1, 2 whose concatenation 1 2 reduces to , i.e., 1 2 = .
j : tasks and are executed concurrently. Model-theoretically, j is true on an m-path if only if and are true on some m-paths 1, 2 whose with an interleaving 1 k 2 reduces to . {
_ : represents a nondeterministic task, which means \execute task execute task ". Model-theoretically, _ is true on an m-path if only if either or is true over on . or and
Due to the space limitation, we do not explain operations on m-paths, such as
concatenation, interleaving, and reduction. For more details of these operations,
see [
It is worth noticing that, the body of CT R Horn rules and goals do not
include the classical connective ^, which is usually expressed as a constraint [
Here, the state is a special propositional constant, which is true on paths of length 1, i.e., on database states. That means the above formula is always evaluated to true, even if the task is not executed. For example, the rule f ieldworkerP rocess (consulation_state) antDescription rcvM sg de nes the process managed by the eldworker. It is satis ed on a path as long as antDescription and rcvMsg are true on the path , even if the task consultation is not executed. 4.2
Reactive Logic Representation
To support the WsSWF execution, we provided a declarative rule-based
workow speci cation by messaging reaction rules [
Bonner et al. [
The reaction rules concern the actions in response to events and actionable situations. They specify the conditions under which actions must be taken and describe the e ects of action executions. They are a collection of reactive rules, which allow to specify and program such reactive systems in a declarative manner. The most general form of a reaction rule consists of the following parts. de ne reaction rule r rule on [event] if [condition] then [conclusion] do [action] after [post condition] else [else conclusion] elseDo [else=alternative action]
Depending on the parts of the general syntax, the reaction rules can be specialized into di erent types: derivation rules (if-then, are often used for logical event/action calculi), production rules (if-do), trigger rules (on-do), and ECA rules (on-if-do). For example, as shown in Figure 2, after the ant identi cation is done, a curational request is sent to a curator if the identi cation is successful. The processes can be represented as ECA rules: de ne reactive rule identDone on identDone(AntDesc; Result) if isIdentSuccess(AntDesc; Result) do nothing: de ne reactive rule identDone on identDone(AntDesc; Result) if isIdentF aild(AntDesc; Result) do humanIdent(AntDesc):
CT R provides a complete formalization for the system behavior and these ECA rules can be further represented by CT R as follows: identif ication identDone identDone
(checkF ood j checkN est j checkBody) identDone isIdentSuccess(AntDesc; Result) state isIdentF aild(AntDesc; Result) humanIdent(AntDesc) 4.3
Complex Event Processing The reaction rules specify under which conditions a task can execute and these conditions determine intelligent routings at runtime. As we consider the data passing between tasks as event messaging, it is necessary to employ the CEP technology to represent composite events, thereby implementing complex workow patterns.
A composite event is the combination of several base events. Each composite
event is usually described by an event pattern, which contains event templates,
relational operators and variables. However, the logic-based approaches are
goaldriven and the check of a given event pattern is always performed at the time
when the goal is set [
Note that the states in T R-based CEP need to be seen from a di erent perspective. They are de ned as changes of base events during complex event pattern detection and what stored in the databases are ground atomic event formulas, D. More precisely, the data oracle Od(D) which corresponds to check if the occurrence of a base event, which simply returns the event formulas. Formally, e 2 Od(D) i the event e is in the database. For each base event e in D, the transition oracle de nes two new predicates: ins(e) and del(e), representing insertion of an event when it is detected and deletion of an event when corresponding complex event pattern is detected. Formally, ins(e(t)) 2 Ot(D1, D2) i D2 = D1 [ fe(t)g, and similarly del(e(t)) 2 Ot(D1, D2) i D2 = D1 - fe(t)g.
Conjunction of Events An event pattern based on the conjunction of
events requires all base events are detected. For example, e(T ) a(T 1)^b(T 2)^
c(T 3) de nes a composite event e occurs when the base events a, b and c are
detected. Following the event-driven complex event detection approach [
The rst six rules represent that the base events a, b and c are rstly inserted into the database when they are detected. The check rule checks if these base events already exist in the database. The composite event e occurs if all base events a, b and c are detected. As soon as the conjunction event pattern is detected, the base events a, b and c are removed from the database. Note the base events a, b, and c can always be successfully inserted into the database even the check rule fails (represented by a Negation As Failure inference rule not(check)). This is really important because that the occurred base events are always known during a complex event pattern detection. Suppose the base events a and b are detected before c, the check rule fails but the base event a and b are both successfully inserted into the database. When c is detected, the third rule rstly inserts the event c into the database, then triggers the composite event e.
Disjunction of Events An event pattern based on the disjunction of events is satis ed when any base event is detected. For example, e(T ) a(T 1)_b(T 2)_ c(T 3) de nes the composite event e occurs when any one of the events a, b and c is detected. In this work, the detection of a disjunction event pattern is represented as follows: a(T 1) : ins:a(T 1) check a(T 1) : ins:a(T 1) not(check) state b(T 2) : ins:b(T 2) check b(T 2) : ins:b(T 2) not(check) state c(T 3) : ins:c(T 3) check c(T 3) : ins:c(T 3) not(check) state check a(T 1) e(T 1) del:a(T 1) check b(T 2) e(T 2) del:b(T 2) check c(T 3) e(T 3) del:c(T 3)
Compared with the conjunction event pattern mentioned above, there are three check rules that detect the disjunction of events. It means that either base event a, b or c is detected, then one check rule is evaluated to true and the composite event e occurs. Note that we assume that the events a, b and c are mutually exclusive in this work to insure the composite event e that occurs only once.
The conjunction and disjunction are standard operators to describe complex event patterns. They are often used to represent the gateways acted as join connectors in work ows. With the aforementioned approach, it is also possible to represent more complex join connectors in work ows, such as a composite event e is detected when any two of the events a, b and c occur. Moreover, since we provide a declarative logic-based work ow representation, it is possible to represent complex conditional logic in the process of complex event detection to to make more sophisticated work ows. Due to the space limitation, they are not shown in this paper. 5
In this section we introduce a Prova implementation of the CT R-based logic WsSWF representation. Prova2 is both a Semantic Web rule language and a high expressive distributed rule engine. Prova rule language combines di erent rule types and provides a highly expressive, hybrid, declarative and compact rule programming language, which combines the declarative programming paradigm
and object-oriented programming and the Semantic Web approach [
The CT R-based work ow logic is set of CT R Horn rules that de ne the composition of a work ow. Before the work ow execution, all these CT R Horn rules need to be translated into Prova rules. As mentioned in Section 4, the body of a CT R Horn rule represents a CT R Horn goal with forms of: , j , _ ; .
Because Prova is built upon Prolog, a serial Horn rule p(X) (Y ) (Z) can be directly translated into a Prova rule with a form p(X) : (Y ); (Z). This is simply done by replacing serial connector with a comma \,".
Disjunction of tasks de nes a nondeterministic composite task and they can be simply implemented by a set of Prova rules imposed by di erent conditions. For example, p(X) (Y ) _ (Z) can be implemented by: (1) p(X) cond1; (Y ); (2) p(X) cond2; (Z). cond1 and cond2 denote the conditions under which to select branches. Similarly, it is easy to translate optional tasks, where the propositional constant state is translated to a condition without subsequent goals, i.e., (1) p(X) cond1; (Y ); (2) p(X) cond2. The implementation of concurrent tasks is based on reactive event messaging, and we will introduce later in this section.
The reactive event messaging can be implemented by the following Prova constructs to send and receive one or more context-dependent multiple outbound or inbound event messages:
Listing 1.1. Prova constructs of messaging reaction rules sendMsg (XID , Protocol , Agent , Performative , Payload | Context ) rcvMsg (XID , Protocol , From , Performative , Payload | Context ) rcvMult (XID , Protocol , From , Performative , Payload | Context )
Here, XID is the conversation identi er of a message. Protocol de nes the communication protocol. Agent and From denote the destination and the source of the message, respectively. Performative describes the pragmatic context in which the message is sent. A standard nomenclature of the performative is, e.g., the FIPA Agents Communication Language (ACL)3. And Payload|Context denotes the actual content of the message.
There are two types of Prova reaction rules: inline and global reaction rules. The inline reaction rules are used to accept just one message, a speci ed number of messages. They are usually in the body of a rule and act as sub-goals of the rule. For example, the logic after the ant identi cation can be translated into:
Listing 1.2. Inline reaction rule example 1 identProcess (XID , AntDesc , Result ) :2 ... , 3 rcvMsg (XID , async , Agent , answer , identDone ( AntDesc , Result )) ,
isSuccess ( Result ), !. 6 identProcess (XID , AntDesc , Result ) :7 rcvMsg (XID , async , Agent , answer , identDone ( AntDesc , Result )) , 8 not ( isSuccess ( Result )) , !, 9 sendMsg (XID , async , humanAgent , ident ( AntDesc )) , 10 rcvMsg (XID , async , humanAgent , ident ( Result )) , 11 ....
The pattern speci ed by inline reaction rule rcvMsg (Line 3 and 7) indicates an interest in an event message of pre-de ned type answer on the async protocol. This kind of inline reactions re only once. The global reaction rules look exactly like general Prova rules but their semantics are more aligned with reactive rules rather than derivation rules. In contrast to the inline reaction rules, the global reaction rule has a rule base lifetime scope, i.e., it is active while the rule base runs on a Prova engine and it is ready to receive any number of messages as they arrive to the agent. For example, the process of waiting form external identi cation request can be implemented as follows:
Listing 1.3. Global reaction rule example 1 rcvMsg (XID ,esb , Agent , request , ident ( AntDesc )) :2 identProcess ( AntDesc ), 3 ....
With the reactive messaging, it is possible to implement the concurrent tasks in Prova. Prova has three internal protocols for reactive messaging: self, task, async, and swing (not used in this paper). The inline reaction rule rcvMsg itself is executed on the main thread, but it creates an inline reaction waiting for a reply according to its protocol. The self protocol indicates that the thread waiting for a reply is the main thread and this protocol can ensure fully sequential processing of received messages. The task protocol means the thread waiting for a reply is randomly taken from a task thread pool. This pool is used for running tasks achieving maximum throughput. The async protocol makes good use of the conversation identi er and the thread waiting for a reply is chosen in terms of the conversation identi er. This means a conversation is always mapped to one thread. In Prova, we can use both task and async protocol of the reactive messaging to implement concurrent processes. For example, the following Prova code snippet implements the ant identi cation that involves three tasks in parallel.
Listing 1.4. Concurrent task example 1 identProcess (XID , AntDesc , Result ) :2 ... , 3 init_ident () , 4 sendMsg (XID , task ,0 , inform , checkFood ( AntDesc , Res1 )) , 5 sendMsg (XID , task ,0 , inform , checkNest ( AntDesc , Res2 )) , 6 sendMsg (XID , task ,0 , inform , checkBody ( AntDesc , Res3 )). 8 init_ident () :9 rcvMsg (XID , task , From , inform , checkFood ( AntDesc , Res1 )) , 10 checkFood ( AntDesc , Res1 ), 11 sendMsg (XID , async , 0, inform , checkFood ( AntDesc , Res1 )). 13 init_ident () :14 15 16 rcvMsg (XID , task , From , inform , checkNest ( AntDesc , Res2 )) , checkNest ( AntDesc , Res2 ), sendMsg (XID , async , 0, inform , checkNest ( AntDesc , Res2 )). 18 init_ident () :19 rcvMsg (XID , task , From , inform , checkBody ( AntDesc , Res3 )) , 20 checkBody ( AntDesc , Res3 ), 21 sendMsg (XID , async , 0, inform , checkBody ( AntDesc , Res3 )).
The predicate init ident() (Line 3) creates three parallel processing streams in one agent and each inline reaction rule randomly selects a thread from the task pool in order to wait for the event to trigger the task in branch, thereby executing them in parallel.
The logic-based CEP can also be implemented by the event-driven computation of event patterns. In Prolog, the updates are not undone during backtracking. For instance, the Prolog rule \p :- assert(event(a)), fail." asserts event(a) into the database even though the execution fails. Although it is a limitation to implement some T R-based applications that require to undo the updates during backtracking. But for the logic-based CEP, this is quite useful since the occurred events need to be stored in the database even the complex event pattern is not matched, i.e., the rule used to check the complex event pattern fails. Bene t from this feature, two CT R rules used to detect base event (see Section 4.3) can be reduced to one. Due to the space limitation, the following Prova code snippet only implements the detection of a conjunction event pattern:
Listing 1.5. Complex event pattern computation example 1 detect ( XID ) :2 rcvMsg (XID , async , From , inform , e(a)) , assert (e(a)) , check (e ). 3 detect ( XID ) :4 rcvMsg (XID , async , From , inform , e(b)) , assert (e(b)) , check (e ). 5 detect ( XID ) :6 rcvMsg (XID , async , From , inform , e(c)) , assert (e(c)) , check (e ). 8 check (e) :9 e(a), e(b), e(c), sendMsg (XID , async , 0, inform , e), 10 retract (e(a)) , retract (e(b)) , retract (e(c )).
Suppose e(a) is detected rst, it is immediately recorded as an event fact into the database. Since the base events e(b), and e(c) have not been detected, the rule check(e) (Line 8-10) is evaluated to false at the moment. The rule check(e) reasoning is triggered again when another base event is detected. It can only be evaluated to true when all base events are detected, then the composite event e occurs and the base events are removed from the database. Note that the base events a, b and c are simpli ed here for clarity. In concrete applications, they can be associated with arguments to to detect di erent composite events.
To sum up, Table 1 shows the mappings from the CT R-based work ow representation to Prova. For the purpose of connecting distributed Prova agents, a tool for rule-based collaboration Rule Responder4 that is built upon Enterprise Service Bus (ESB) Mule, is often used as a communication middleware.
Existing scienti c work ow management systems (WFMSs) (such as Kepler,
Triana, Taverna, Pegasus) are mainly designed for structured compute intensive
or data intensive applications, and each system has its own application areas.
They have proprietary work ow languages and provide limited expressiveness
to describe decision logic and conditional reactive logic. The WsSWFs
considered in this work not only involve complex task dependencies that cannot be
easily described by imperative procedural work ow languages, but also contain
knowledge-intensive decision centric steps, which need the coordination of
scientists or computer agents as a team. That is why logic-based CT R is employed as
a theoretical basis for the declarative description of the WsSWFs. Some e orts
are also trying to provide a logical framework for modeling exible work ows:
Roman et al. [
Currently there are many rule-based work ow languages, which support exible service composition and model weakly-structured process logic with declarative rule languages. However, many of them only provide a static syntactical process description without a precise declarative formal semantics. This paper provided a CT R-based formal model for the WsSWFs and especially considered conversation-based reactive work ow logic representation and event-driven computation of complex event patterns.