Business Processes Veri cation with Temporal Answer Set Programming ?

Abstract

The paper provides a framework for the speci cation and veri cation of business processes, based on a temporal extension of answer set programming (ASP). The framework allows to capture uent annotations as well as data awareness in a uniform way. It allows for a declarative speci cation of business process but also for a direct encoding of processes speci ed in conventional work ow languages. Veri cation of temporal properties of a business process, including veri cation of compliance to business rules, can be performed by LTL bounded model checking techniques.

Introduction

The veri cation of business process compliance to business rules and regulations has gained a lot of interest in recent years and it has led to the development to a process annotation approach [ 12, 18, 33, 23 ], where a business processes is enriched with information relevant for compliance veri cation, to capture the semantics of atomic tasks execution through preconditions and e ects. The treatment of data in business process veri cation, on the other hand, has attracted growing interest in the last decade, with the de nition of artifact-centric and data-centric process models [ 27, 5, 9 ].

In this paper we combine the two perspectives and propose a framework for the speci cation and veri cation of business processes which allows to model both annotations and data properties by specifying atomic tasks in a uniform way. The approach is well suited for a declarative speci cation of the business process, which has been advocated by many authors in the literature [ 32, 30, 25 ]. Following [ 7 ], the speci cation of annotation can be done in an action theory by de ning the e ects and preconditions of atomic tasks. The same approach allows to capture data properties, by modelling data acquisition tasks as actions which nondeterministically assign values to variables (data objects) on given domains, under the restriction that domains are nite.

The use of directional rules for modeling business rules as well as to capture the conditional structure of norms is widely used in the literature [ 18 ]. In our approach, besides the speci cation of action preconditions and direct e ects, causal rules in an action domain allow to capture dependencies among uents ? This work has been partially supported by Regione Piemonte, Project ICT4LAW. (propositions whose truth is a ected by actions) and uent changes, as well as dependencies between process data and uents. Our claim is that both static and dynamic causal laws are useful for the speci cation of business process annotations and their use allows unintended conclusions to be avoided. Observe that, once the data perspective is included, causal laws can include both conditions on data and annotations. For instance, the rule age 18 ) of Age may establish a link between the business process, whose execution assigns values to the variable age, and the compliance rules dealing with persons "of age".

The approach we propose is based on Answer Set Programming (ASP) [ 11 ] and, more precisely, on the temporal extension of ASP in [ 16 ], combining ASP with the temporal logic DLTL [ 22 ], an extension of LTL in which the temporal operators are enriched with program expressions. The action language in [ 16 ] allows general DLTL constraints to be included in action domains, which can be pro tably used for a declarative speci cation of the business process advocated in the literature [ 32, 30, 25 ]. In addition, the proposed approach also allows for a direct encoding of processes speci ed in work ow languages, and it can be used in combination with state of the art work ow management systems.

The paper considers several veri cation tasks including the veri cation of business process compliance to business rules. Veri cation is performed through Bounded Model Checking [ 6 ] techniques and exploits the approach in [ 16 ] for DLTL bounded model checking in ASP, which extends the approach for Bounded LTL Model Checking with Stable Models in [ 21 ]. 2

A Temporal Answer Set Programming language

In this section we recall the temporal ASP language introduced in [ 16 ]. The language is based on a temporal extension of Answer Set Programming (ASP) which combines ASP with the temporal logic DLTL [ 22 ], an extension of LTL in which temporal operators are enriched with program expressions. In particular, in DLTL the next state modality can be indexed by actions, and the until operator U can be indexed by a program which, as in PDL, can be any regular expression built from atomic actions using sequence (;), nondeterministic choice (+) and nite iteration ( ). Satis ability and validity for DLTL are PSPACE-complete problems [ 22 ].

Let = fa1; : : : ; ang be a nite non-empty alphabet of actions. From the until operator, the derived modalities h i, [ ], (next), U , 3 and 2 can be de ned as follows: h i >U , [ ] :h i: , Wa2 hai , U

U , 3 >U , 2 :3: , where, in U , is taken to be a shorthand for the program a1 + : : : + an. Informally, a formula [ ] is true in a world w of a linear temporal model if holds in all the worlds of the model which are reachable from w through any execution of the program . A formula h i is true in a world w of a linear temporal model if there exists a world of the model reachable from w through an execution of the program , in which holds.

A domain description D is a pair ( ; C), where is a set of laws describing the e ects and executability preconditions of actions (as described below), and C is a set of temporal constraints, i.e., general DLTL formulas. Atomic propositions describing the state of the domain are called uents. Actions may have direct e ects, described by action laws, and indirect e ects, described by causal laws capturing the causal dependencies among uents.

Let L be a rst-order language which includes a nite number of constants and variables, but no function symbol. Let P be the set of predicate symbols, V ar the set of variables and C the set of constant symbols. We call uents atomic literals of the form p(t1; : : : ; tn), where, for each i, ti 2 V ar [ C. A simple uent literal l is an atomic literal p(t1; : : : ; tn) or its negation :p(t1; : : : ; tn). We denote by LitS the set of all simple uent literals, and we assume that the uent ? representing the inconsistency is included in LitS . A temporal uent literal has the form [a]l or l, where l 2 LitS and a is an action name (an atomic proposition, possibly containing variables). Given a (simple or temporal) uent literal l, not l represents the default negation of l. A (simple or temporal) uent literal possibly preceded by a default negation, will be called an extended uent literal. The laws are formulated as rules of a temporally extended logic programming language having the form l0 l1; : : : ; lm; not lm+1; : : : ; not ln (1) where the li's are simple or temporal uent literals. As usual in ASP, rules with variables are a shorthand for the set of their ground instances; and we let be the set of ground instances of atomic actions in the domain description.

In the following we call a state a set of ground uent literals. A state is said to be consistent if it is not the case that both f and :f belong to the state, or that ? belongs to the state. The execution of an action in a state may possibly change the values of uents in the state through its direct and indirect e ects, thus giving rise to a new state. We assume that a law as (1) can be applied in all states while, when pre xed with the Init, it only applies to the initial state.

Action laws, causal laws, precondition laws, persistency laws, initial state laws, etc., which are normally used in action theories, can all be de ned as instances of (1). Action laws describe the e ects of atomic tasks. The meaning of an action law [a]l0 l1; : : : ; lm; not lm+1; : : : ; not ln, (where l0 2 LitS and l1; : : : ; ln are either simple uent literals of temporal uent literals of the form [a]l) is that executing action a in a state in which l1; : : : ; lm hold and lm+1; : : : ; ln do not hold makes the e ect l0 to hold (in the state after the action).

Precondition laws allow the speci cation of executability conditions for atomic tasks; they are a special case of action laws with ? as e ect, i.e., they have the form: [a]? l1; : : : ; lm; not lm+1; : : : ; not ln meaning that a cannot be executed (has an inconsistent e ect) in case l1; : : : ; lm hold and lm+1; : : : ; ln do not hold.

Causal laws de ne causal dependencies among propositions, which are used to derive indirect e ect of actions, called rami cations in the literature of reasoning about actions where it is well known that causal dependencies among propositions are not suitably represented by material implication in classical logic. Static causal laws have the form: l0 l1; : : : ; lm; not lm+1; : : : ; not ln where the li's are uent literals. Their meaning is: if l1; : : : ; lm hold and lm+1; : : : ; ln do not hold in a state, then l0 is caused to hold in that state. Dynamic causal laws have the form: l0 t1; : : : ; tm; not tm+1; : : : ; not tn where l0 is a uent literal and the ti's are either uent literals or temporal uent literals of the form li (meaning that the uent literal li holds in the next state). Their meaning is: if t1; : : : ; tm hold and lm+1; : : : ; ln do not hold, then l0 is caused to hold in the next state. In particular, in the premise, a combination of the form :f; f (or f; :f ) may be used to mean that uent f becomes true (resp., false). The language also includes constraints of the form ? l1; : : : ; lm; not lm+1; : : : ; not ln where the li's are simple or temporal uent literals.

In this language, default negation in clause bodies allows for the speci cation of nondeterministic action laws, of the form [a](l0 _ : : : _ lk) lk+1; : : : ; lm; not lm+1; : : : ; not ln, stating that the execution of action a in a state in which lk+1; : : : ; lm hold and lm+1; : : : ; ln do not hold, makes nondeterministically one of l0; : : : ; lk true. In fact, [a](l0 _ : : : _ lk) Body can be seen as a shorthand for the rules [a]li Body; not [a]l1; : : : not [a]li 1; not [a]li+1; : : : not [a]lk (i = 1; : : : ; k).

The laws above can be used to de ne persistency laws to deal with frame uents as well as to complete the initial state in all the possible ways compatible with the initial state speci cation. The semantics of a domain description, is de ned by extending the notion of answer set [ 11 ] to temporal answer sets, so to capture the linear structure of temporal models. We refer to [ 16 ] for details. 3

Declarative speci cation of business processes: merging annotations with data

A declarative speci cation of a business process can be given by exploiting the action theory above to de ne the e ects of atomic tasks as well as their executability preconditions. This approach has been followed in di erent contexts such as in the declarative speci cation of web services in [ 26, 5 ] and in the declarative speci cation of agent communication protocols in [ 35, 14 ]. We show that causal laws have a relevant role in the speci cation of background knowledge, which is common both to the business process and to the business rules, and that the proposed approach allows for an easy integration of the data perspective.

The declarative speci cation of business processes has been advocated by many authors [ 32, 30, 25 ], as opposed to the more rigid transition based approach. A declarative speci cation of a process is, generally, more concise than transition based speci cation as it abstracts away form rigid control- ow details and does not require the order among the actions in the process to be rigidly de ned.

The Temporal ASP language in Section 2 is well suited for de ning immediate and indirect e ects of atomic tasks and their preconditions. Consider, for instance, the business process of an investment rm in [ 7 ], where the rm o ers nancial instruments to an investor. The atomic task investor identi cation has as e ect that the investor has been identi ed, while investor pro ling has the nondeterministic e ect that the investor is recognized as being either risk averse or risk seeking. This can be modeled by the action laws: [investor ident(I)]investor identif ied(I) [prof iling(I)](risk averse(I)_risk seeking(I)) investor identif ied(I)

The rst action law has empty precondition. The fact that prof iling can be executed only when the atomic task investor identi cation has been executed, can be modeled by introducing the precondition law: [prof iling(I)]?

not investor identif ied(I)) which, literally, states that executing action prof iling in a state in which the investor I has not been identi ed gives an inconsistency. Observe that, in this language, an action is executable unless there is a precondition law for it whose antecedent is not satis ed. Hence, once the investor has been identi ed, the action prof iling(I) becomes executable. However, to guarantee that it will be eventually executed, we can add in C the DLTL constraint

2[investor ident(I)]3hprof iling(I)i>

To force the execution of prof iling immediately after investor identi cation, instead, we could add the constraint: 2[investor ident(I)] hprof iling(I)i>.

The presence of DLTL constraints in a domain speci cation allows for a simple way to constrain activities in a business process. Observe that, as DLTL is an extension of LTL, it is possible to provide an encoding of all ConDec [ 28 ] constraints into our action language. The additional expressivity which comes from the presence of program expressions in DLTL, allows for a very compact encoding of certain declarative properties of the domain dealing with nite iterations. For instance, the property \action b must be executed immediately after any even occurrence of action a in a run" can be expressed by the temporal constraint: 2[(a; ; a) ]hbi>), where represents any nite action sequence.

In [ 7 ] it has been shown that program expressions can be used to model the control ow of a business process in a rigid way. However, the solution in [ 7 ] does not deal with non-structured work ows.

As concerns the data perspective, an atomic task which acquires the value of a data variable (data object) x can be regarded as an action assigning nondeterministically to x one of the values in its domain. Consider, for instance, the atomic task verif y status which veri es the status of a customer. Assume it has the e ect of assigning a value (gold, silver or unknown) to a variable status. The task verif y status can be regarded as a non deterministic action assigning one of the possible values to the variable status:

[verif y status]( status(gold) _ status(silver)) In general, we model a data acquisition task as a nondeterministic action. As an example, let us consider an atomic task get order which acquires an order of a product P and an atomic task select shipper(P ) which selects a shipper among the available shippers, which are compatible with the choice of the product P . Let us introduce the notation 1f[a]R(X) j P (X)g1 (similar to the notations used in Clingo and in S-models) as a shorthand for the two laws: [a]R(X) [a]:R(X) not [a]:R(X) ^ P (X)

[a]R(Y ) ^ P (X) ^ P (Y ) ^ X 6= Y meaning that after the execution of action a, R(X) holds for a unique value of X among those values satisfying P (X). Let available product(P ) and available shipper(S) be the predicates de ning the available products and shippers, and compatible(P; S) be a predicate saying that product P and shipper S are compatible. We can represent the e ect of action get order by the law:

1f[get order]product(P ) j available product(P )g1

and the e ect of action select shipper(P ) as

1f[select shipper(P )]shipper(S) j available shipper(S)g1.

The requirement that P and S must be compatible can be enforced introducing the constraint:

? [select shipper(P )]shipper(S) ^ not compatible(P; S) meaning that it is not the case that the selected shipper S and the product P to be shipped are not compatible.

The above speci cation of the e ects of the task select shipper(P ) has strong similarities with the speci cation of a post-condition for a service in [ 9 ]. Indeed, in [ 9 ], a post-condition of the form R(x) := (x), associated with a service , requires that after the execution of the argument x of R is instantiated with a (unique) tuple u such that (u) holds in the previous state (artifact instance). As a di erence with [ 9 ], where (x) is a rst-order temporal formula, our temporal language does not allow for explicit quanti cation: all variables occurring in action and causal laws are intended to be universally quanti ed in front of the laws. Furthermore, in our approach we cannot deal with in nite domains. As usual in ASP, a nite groundization the set of laws in the domain speci cation is required. Abstraction techniques as those in [ 24 ] can be adopted to abstract in nite or large domains to a nite, small set of abstract values. 4

Speci cation of business rules: causality and commitments

The use of directional implications for modeling business rules as well as for modeling the conditional structure of norms is widely recognized in the literature [ 18 ]. In this section we claim that static and dynamic causal laws, proposed in the AI literature about reasoning about actions and change, are also appropriate for modeling business processes.

Consider the domain in examples 2 and 3 in [ 33 ], with the rule stating that if an insurance claim is accepted by reviewer A and reviewer B, then it is accepted. Suppose this is represented as the material implication claimAccRevA ^ claimAccRevB claimAccepted i.e., the clause :claimAccRevA _ :claimAccRevB _ claimAccepted. Suppose further, as in [ 33 ], that as a result of an action with direct e ects, we accept models where such e ects hold, that satisfy a background theory including the implication above, and, according to the Possible Models Approach [ 34 ], differ minimally from the previous state. Consider a state where claimAccRevA already holds, and an action of acceptance for reviewer B occurs, with direct effect claimAccRevB. In order to satisfy the material implication, claimAccepted should become true, or claimAccRevA should become false, or both; minimal di erence with the previous state only excludes this third alternative, while providing equal status to the rst two. If the redundancy in the process means that the assessment of a reviewer has no in uence on the other's, then only the rst result, where claimAccepted becomes true, is intended. The (static) causal rule claimAccepted

claimAccRevA; claimAccRevB allows to obtain the rst solution, given that its semantics imposes that in all states, if claimAccRevA ^ claimAccRevB is true (and, in particular, it just became true), then claimAccepted holds (and it becomes true as a side e ect if the premise just became true).

However, the above implication might not actually be intended, as in case later steps in the process could make the claim not accepted. For example, the process model might specify that if the amount claimed is greater than a threshold, it should go through further approval by a supervisor (with possible e ect :claimAccepted). Unlike [ 33 ], we consider the case where this does not mean that claimAccRevA ^ claimAccRevB should become false, i.e., at least one conjunct (or exactly one, for a minimal change) should become false. Rather, we suggest that here, after reviewers acceptance, claimAccepted actually stands for \accepted unless decision is overridden" Dynamic causal laws are suitable to represent this; the side e ect of acceptance by the single reviewers becomes: claimAccepted claimAccRevA; :claimAccRevB; claimAccRevB claimAccepted :claimAccRevA; claimAccRevA; claimAccRevB where syntactic sugar can be introduced, as in [ 8 ], to succinctly state that the conjunction claimAccRevA ^ claimAccRevB is initiated i.e., it becomes true.

Such rules correctly make claimAccepted true after reviewer acceptance, but, if a further step has the e ect :claimAccepted, they do not \ re" because claimAccRevA ^ claimAccRevB is true, but it is not becoming true. Note the di erence with the static causal rule which would re (because claimAccRevA ^ claimAccRevB is true) and then contradict :claimAccepted.

A particularly signi cant case of the pattern above, where a uent becomes true as an indirect e ect of some activity, but may be canceled by further activities, is the one of obligations, which arise naturally in compliance rules: several such rules are variants of \if B happens, then A shall happen", or, \if B is (or becomes) true, then A shall become true". Compliance veri cation for such rules could be performed by verifying a straightforward representation of the rule as a temporal logic formula, e.g., in LTL, the formula 2(B 3A).

This, however, does not admit the possibility that a later activity cancels the obligation: e.g., if an order for goods is con rmed by the seller, goods have to be shipped; but if the customer cancels the order, the obligation to ship goods is canceled. An explicit representation of obligations is useful to this purpose. In this paper we limit our attention to one type of obligations in the classi cation in [ 19 ]: the case where a given condition should become true at least once, after they have been triggered; i.e., we consider achievement obligations in [ 19 ], and we only consider the case where the obligation should be ful lled after it is triggered.

We then identify obligations with the notion of commitment from the social approach to agent communication [ 30, 20, 10 ]. A (base) commitment C(i; j; A), means that agent i is committed to agent j to bring about A, while conditional commitments of the form CC(i; j; B; A), mean that agent i is committed to agent j to bring about A, if condition B is brought about [ 35, 14 ]. In this paper we do not consider agents explicitly, and we concentrate our attention to base commitments C(A) where A is a uent; C(A) is also a uent, which can be made true, due to an action law or a dynamic causal law, as a direct or indirect e ect of an activity in the process (order con rmation, in the example). The commitment (to ship goods, in the example) can be made false by an action with e ect :C(A) (the customer cancelling the order). Ful lling the commitment (shipping goods) also makes the commitment false. Compliance veri cation, as we shall see in Section 6, amounts then to verifying that commitments, if introduced, are discharged, i.e., they are either ful lled or explicitly canceled.

We refer to [ 7 ] for the treatment of defeasible business rules by means of default negation in ASP. 5

Translating business process work ows in ASP

The temporal action language introduced above provides a exible and declarative speci cation language for business processes, and in [ 16 ] we have provided its translation to standard ASP.

There are, however, cases where the business process is naturally modeled (or it has already been modeled) in a work ow language such as YAWL [ 31 ]. In principle, such process models could be translated automatically to the temporal action language, but we have provided a direct translation to ASP for a subset of YAWL including AND- and XOR- splits and joins. The translation is based on an enabling semantics of arcs and tasks: an atomic task can be executed (i.e., the action can occur) when it is enabled. It is enabled when its only incoming arc is enabled, or it is an AND-join and all incoming arcs are enabled, or it is a XOR-join an one incoming arc is enabled. The execution of a task enables the outgoing arcs, and, in case it is a XOR-split, the execution of a subsequent activity based on the enabling of one such arc disables the other arcs. 6

Business process veri cation by bounded model checking

In [ 16 ] we have developed Bounded Model Checking techniques for the veri cation of DLTL constraints. In particular, the approach extends the one developed in [ 21 ] for bounded LTL model checking with Stable Models. The approach can be used for checking satis ability of temporal formulas. To prove the validity of a formula, its negation is checked for satis ability. In case the formula is not valid, a counterexample is provided.

Several veri cation tasks can be addressed within the proposed approach. Compliance veri cation (described in some detail in [ 7 ]) amounts to check that all the business rules are satis ed in all the execution of the process. We distinguish among business rules which can be encoded as a temporal formula and business rules whose modeling involves commitments.

As an example of rule which can be encoded as a temporal formula to be veri ed, consider, in the order-production-delivery process in [ 24 ], the rule \Premium customer status shall only be o ered after a prior solvency check": it can be veri ed by checking the validity of the temporal formula

2(solvency check done _ :hof f er premium statusi>)

i.e., by verifying that in all executions of the business process if the action of f er premium status is executable, the uent solvency check done holds. As an example of rule modeled through causal laws whose e ect is adding a commitment, consider the rule \if the investor signs an order, the rm is obliged to provide him a copy of the contract". It can be encoded by the causal law: C(sent contract) order signed We require that all the commitments generated are eventually ful lled, unless they are explicitly cancelled (e.g., in the example, cancelling the order also cancels the obligation to send the contract). Observe that canceling a commitment would not be possible if the commitment to corresponded directly to the temporal formula 3 . A commitment is also discharged when it is ful lled, i.e., the following causal rule is added for all possible commitments: Then the veri cation of rules involving commitments amounts to verifying the validity, for all possible commitments C( ), of the formula: :C( )

C( ) ^ 2(C( ) ! 3(:C( )))

A veri cation task considered in [ 9 ] is that of verifying properties of a business process, under the assumption that the process satis es some given business rules. This veri cation task can also be addressed in our approach: the speci cation of the business rules is given by adding temporal constraints (and, possibly, causal laws) to the domain speci cation. The executions of the resulting domain speci cation are then veri ed against other temporal properties.

Satis ability and validity of a DLTL formula over the business process executions are decidable problems. However, given that BMC is not complete in general, an alternative approach to BMC in ASP is proposed in [ 15 ] to address the problem of completeness, by exploiting the Buchi automaton construction while searching for a counterexample. 7

Conclusions and related work

The paper presents an approach to the veri cation of the compliance of business processes with norms. The approach is based on a temporal extension of ASP. The business process, its semantic annotation and the norms are encoded using temporal ASP rules as well as temporal constraints. Causal laws are used for modeling norms, and commitments are introduced for representing obligations. Compliance veri cation can be performed using the BMC technique developed in [ 16 ] for DLTL bounded model checking in ASP, which extends the approach for bounded LTL model checking with Stable Models in [ 21 ].

This paper enhances the approach to business processes compliance veri cation in [ 7 ] by taking into consideration the data perspective and by providing a declarative speci cation of the business process, while in [ 7 ] the control ow of a structured business process is modeled in a rigid way by means of a program expression. Also, we have shown that a direct encoding of the process work ow in ASP can be given and exploited for process veri cation.

Several proposals in the literature introduce annotations on business processes for dealing with compliance veri cation [ 12, 18, 33 ]. In particular, [ 18 ] proposes a logical approach to business process compliance based on the idea of annotating the business process. Annotations and normative speci cations are provided in the same logical language, namely, the Formal Contract Language (FCL), which combines defeasible logic [ 3 ] and deontic logic of violations [ 17 ]. Compliance is veri ed by traversing the graph describing the process and identifying the e ects of tasks and the obligations triggered by task execution. Ad hoc algorithms for propagating obligations through the process graph are de ned.

The idea of describing the e ects of atomic tasks on data through preconditions and e ects is already present in [ 23 ], where e ects and preconditions are sets of atomic formulas, and the background knowledge consists of a theory in clausal form; I-Propagation [ 33 ] is exploited for computing annotations. In our approach the domain theory contains directional causal rules rather than general clauses (which allow unintended conclusions to be avoided when reasoning about side e ects), and domain annotations are combined with data properties in a uniform approach. In the related paper [ 33 ] several veri cation tasks are de ned to verify that the business process control ow interacts correctly with the behaviour of the individual activities.

In [ 9 ] a service over an artifact schema is de ned as a triple: a precondition, a post-condition and a set of static rules, which de ne changes on state relations, and are formulas in a rst-order temporal logic. State update rules S(x) +(x) and :S(x) (x) are essentially speci c kind of causal laws whose antecedents + and + are evaluated in the artifact instance in which the service is executed and whose consequents are added to the resulting artifact instance. [ 9 ] identi es a class of guarded artifacts for which veri cation of properties in a (guarded) rst-order extension of LTL is decidable. While our action language does not allow for explicit quanti cation, it allows for a exible formulation of action e ects and causal laws, which permits (as shown in Section 3) an encoding of post-conditions as in [ 9 ].

In [ 4 ] compliance checking for BPMN process models is based on the BPMNQ visual language. Rules are given a declarative representation as BPMN-Q queries, which are translated into temporal formulas for veri cation.

In [ 25 ] the Abductive Logic Programming framework SHIFF [ 2 ] is exploited in the declarative speci cation of business processes as well as in the veri cation of their properties. In [ 1 ] expectations are used for modelling obligations and prohibitions and norms are formalized by abductive integrity constraints.

In [ 29 ] Concurrent Transaction Logic (CTR) is used to model and reason about general service choreographies. Service choreographies and contract requirements are represented in CTR. The paper addresses the problem of deciding if there is an execution of the service choreography that complies both with the service policies and the client contract requirements.

Temporal rule patterns for regulatory policies are introduced in [ 13 ], where regulatory requirements are formalized as sets of compliance rules in a real-time temporal object logic. The approach is used essentially for event monitoring.

References

1. M. Alberti , M. Gavanelli , E. Lamma, P. Mello , P. Torroni , and G. Sartor . Mapping of Deontic Operators to Abductive Expectations . NORMAS, pages 126 { 136 , 2005 .

2. Marco Alberti , Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni . Veri able agent interaction in abductive logic programming: the SCIFF framework . ACM Trans. Comput. Log. , 9 ( 4 ), 2008 .

3. G. Antoniou , D. Billington , G. Governatori, and M. J. Maher . Representation results for defeasible logic . ACM Trans. on Computational Logic , 2 : 255 { 287 , 2001 .

4. Ahmed Awad , Gero Decker, and Mathias Weske . E cient compliance checking using BPMN-Q and temporal logic, LNCS 5240 . In BPM , pages 326 { 341 . Springer, 2008 .

5. K. Bhattacharya , C. Gerede , R. Hull , R. Liu, and J. Su . Towards formal analysis of artifact-centric business process models . In BPM , pages 288 { 304 , 2007 .

6. A. Biere , A. Cimatti , E. M. Clarke , O. Strichman , and Y. Zhu . Bounded model checking . Advances in Computers , 58 : 118 { 149 , 2003 .

7. D. D'Aprile , L. Giordano , V. Gliozzi , A. Martelli , G. L. Pozzato , and D. Theseider Dupre . Verifying business process compliance by reasoning about actions . In CLIMA XI , pages 99 { 116 , 2010 .

8. M. Denecker , D. Theseider Dupre , and K. Van Belleghem . An inductive de nitions approach to rami cations . Electronic Transactions on Arti cial Intelligence , 2 : 25 { 97 , 1998 .

9. A. Deutsch , R. Hull , F. Patrizi , and V. Vianu . Automatic veri cation of datacentric business processes . In ICDT , pages 252 { 267 , 2009 .

10. N. Fornara and M. Colombetti. De ning Interaction Protocols using a Commitment-based Agent Communication Language . AAMAS03 , pages 520 { 527 .

11. M. Gelfond . Answer Sets. Handbook of Knowledge Representation, chapter 7 , Elsevier , 2007 .

12. A. Ghose and G. Koliadis . Auditing business process compliance . ICSOC, LNCS 4749 , pages 169 { 180 , 2007 .

13. C. Giblin , S. Muller, and B. P tzmann. From Regulatory Policies to Event Monitoring Rules: Towards Model-Driven Compliance Automation . IBM Reasearch Report , 2007 .

14. L. Giordano , A. Martelli , and C. Schwind . Specifying and Verifying Interaction Protocols in a Temporal Action Logic . Journal of Applied Logic , 5 : 214 { 234 , 2007 .

15. L. Giordano , A. Martelli , and D. Theseider Dupre . Achieving completeness in bounded model checking of action theories in ASP . In Proc. KR 2012 .

16. L. Giordano , A. Martelli , and D. Theseider Dupre . Reasoning about actions with temporal answer sets . Theory and Practice of Logic Programming , 2012 .

17. G. Governatori and A. Rotolo . Logic of Violations: A Gentzen System for Reasoning with Contrary-To-Duty Obligations . Australasian Journal of Logic , 4 : 193 { 215 , 2006 .

18. G. Governatori and S. Sadiq . The journey to business process compliance . Handbook of Research on BPM, IGI Global , pages 426 { 454 , 2009 .

19. Guido Governatori . Law, logic and business processes . In Third International Workshop on Requirements Engineering and Law. IEEE, 2010 .

20. F. Guerin and J. Pitt . Veri cation and Compliance Testing . Communications in Multiagent Systems , Springer LNAI 2650, 2003 .

21. K. Heljanko and I. Niemela. Bounded LTL model checking with stable models . Theory and Practice of Logic Programming , 3 ( 4 -5): 519 { 550 , 2003 .

22. J.G. Henriksen and P.S. Thiagarajan . Dynamic Linear Time Temporal Logic . Annals of Pure and Applied logic , 96 ( 1-3 ): 187 { 207 , 1999 .

23. J. Ho mann, I. Weber, and G. Governatori . On compliance checking for clausal constraints in annotated process models . Information Systems Frontieres , 2009 .

24. D. Knuplesch , L. T. Ly , S. Rinderle-Ma , H. Pfeifer , and P. Dadam . On enabling data-aware compliance checking of business process models . In Proc. ER 2010 , 29th International Conference on Conceptual Modeling, pages 332 { 346 , 2010 .

25. M. Montali , P. Torroni , F. Chesani , P. Mello , M. Alberti , and E. Lamma. Abductive logic programming as an e ective technology for the static veri cation of declarative business processes . Fundam . Inform., 102 ( 3-4 ): 325 { 361 , 2010 .

26. S. Narayanan and S. McIlraith . Simulation, veri cation and automated composition of web services . In Proc. 11th Int. World Wide Web Conference, WWW2002 , pages 77 { 88 , 2002 .

27. A. Nigam and N. S. Caswell . Business artifacts: An approach to operational speci cation . IBM Systems Journal , 42 ( 3 ): 428445 , 2003 .

28. Maja Pesic and Wil M. P. van der Aalst . A declarative approach for exible business processes management . In Business Process Management Workshops, LNCS 4103 , pages 169 { 180 . Springer, 2006 .

29. D. Roman and M. Kifer . Semantic web service choreography: Contracting and enactment . In International Semantic Web Conference, LNCS 5318 , pages 550 { 566 , 2008 .

30. M. P. Singh . A social semantics for Agent Communication Languages. Issues in Agent Communication , LNCS(LNAI) 1916 , pages 31 { 45 , 2000 .

31. A. M. ter Hofstede , W. M. P. van der Aalst , M. Adamns, and N. Russell . Modern Business Process Automation: YAWL and its Support Environment . 2010 .

32. Wil M. P. van der Aalst and Maja Pesic . Decser ow: Towards a truly declarative service ow language . In The Role of Business Processes in Service Oriented Architectures , volume 06291 of Dagstuhl Seminar Proceedings, 2006 .

33. I. Weber , J. Ho mann, and J. Mendling . Beyond soundness: On the veri cation of semantic business process models . Distributed and Parallel Databases (DAPD) , 2010 .

34. M. Winslett . Reasoning about action using a possible models approach . In Proc. AAAI 88, 7th National Conference on Arti cial Intelligence , pages 89 { 93 , 1988 .

35. P. Yolum and M.P. Singh . Flexible Protocol Speci cation and Execution: Applying Event Calculus Planning using Commitments . AAMAS'02 , pages 527 { 534 , 2002 .