In this paper we provide a framework for the speci cation and the veri cation of business processes, which is based on a temporal extension of answer set programming (ASP) and we address the problem of verifying the compliance of business processes to norms. The logical formalism we use, is a combination of Answer Set Programming and Dynamic Linear Time Temporal Logic (DLTL), and allows for a declarative speci cation of a business process, as well as the speci cation of norms, by means of a set of temporal rules and a set of temporal constraints. A notion of commitment, borrowed from the social approach to agent communication, is used to capture obligations within norms. Besides allowing for a declarative speci cation of business processes, the proposed framework can be used for encoding business processes speci ed in conventional work ow languages. The veri cation of temporal properties of a business process, expressed by temporal formulas, can be done by encoding bounded model checking techniques in ASP. Verifying compliance of a business process to norms consists, in particular, in verifying that there are no executions of the business process which leave commitments unful lled.
The problem of verifying the compliance of business processes has attracted a lot of interest in recent years. Many organizations (banks, hospitals, public administrations, etc.), whose activities are subject to regulations, are required to justify their behaviors with respect to the norms and to show that the business procedures they adopt conform to such norms. For instance, in the nancial domain, the Sarbanes-Oxley Act (commonly named SOX), enacted in 2002 in the USA, describes mandates and requirements for nancial reporting, and was proposed in order to restore investors' con dence in capital markets after major accounting scandals. MiFID (Markets in Financial Instruments Directive) is a EU law, e ective from 2007, with similar goals, including transparency.
In this paper, we address the problem of automatic veri cation of business
process compliance and, to this purpose, we propose a framework for the
specication and the veri cation of business processes, which is based on a temporal
extension of answer set programming (ASP [
The framework for the speci cation and the veri cation of business processes
proposed in this paper, is based on a temporal extension of Answer Set
Programming (ASP [
As concerns compliance veri cation, to represent the obligations which can
be enforced by the application of norms, we make use of the notion of
commitment, which is borrowed from the area of multi-agent communication [
For the veri cation of the business process properties and, in particular, for
compliance veri cation, we exploit Bounded Model Checking [
We shortly recall the temporal action language introduced in [17], which is based on a temporal extension of Answer Set Programming (ASP). 2.1
The action language is based on the Dynamic Linear Time Temporal Logic (DLTL) [22]. DLTL extends LTL by allowing the until operator U to be indexed by a program , an expression of Propositional Dynamic Logic: can be any regular expression built from atomic actions using sequence (;), non-deterministic choice (+) and nite iteration ( ). The usual LTL modalities 2 (always), 3 (eventually), (next), and U (until) can be de ned from U as well as the new temporal modalities [ ] and h i.
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 formula U is true at a world w if \ until " is true at w on a nite stretch of behavior which is in the linear time behavior of the program .
A domain description is de ned as a set of laws describing the e ects of actions as well as their executability preconditions. Atomic propositions describing the state of the domain are called uents. Actions may have direct e ects, that are described by action laws, and indirect e ects, that capture the causal dependencies among uents and are described by causal laws. The execution of an action a in a state s leads to a new state s0 in which the e ect of the action holds. The uents which hold in s and are not a ected by the action a, still hold in s0.
Let P be a set of atomic propositions, the uents, including the inconsistency, ?. A simple uent literal l is a uent name f or its negation :f . We will denote by LitS the set of all simple uent literals. In the language, we also make use of temporal literals, that is, literals that are pre xed by the temporal modalities [a], with a 2 , and . Their intended meaning is: [a]l holds in a state s if l holds in the state obtained after the execution of action a in s; l holds in a state s if l holds in the state next to s. LitT is the set of temporal uent literals: if l 2 LitS , then [a]l; l 2 LitT , where a is an action name (an atomic proposition, possibly containing variables), and [a] and are the temporal operators introduced in the previous section. Let Lit = LitS [ LitT [ f?g. 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. Rules have the form or the form 2(t00 or : : : or t0h
t1; : : : ; tm; not tm+1; : : : ; not tn) t00 or : : : or t0h t1; : : : ; tm; not tm+1; : : : ; not tn (1) (2) where the t0i's and the ti's are either simple uent literals or temporal uent literals. While laws of the form (1) can be applied in all states, laws of the form (2) can only be applied in 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) and (2).
A domain description D is de ned as a tuple ( ; C), where is a set of laws of the form 1 and 2 and C is a set of temporal constraints, i.e. general DLTL formulas. 2.2
To de ne the the semantics of a domain description, we extend the notion of
answer set [
We de ne a (partial) temporal interpretation as a pair ( ; S), where 2 ! is a sequence of actions and S is a consistent set of literals of the form [a1; : : : ; ak]l, where a1 : : : ak is a pre x of , meaning that l holds in the state obtained by executing a1 : : : ak. S is consistent i it is not the case that both [a1; : : : ; ak]l 2 S and [a1; : : : ; ak]:l 2 S, for some l, or [a1; : : : ; ak]? 2 S. A temporal interpretation ( ; S) is said to be total if either [a1; : : : ; ak]p 2 S or [a1; : : : ; ak]:p 2 S, for each a1 : : : ak pre x of and for each uent name p.
We de ne the satis ability of a simple, temporal or extended literal t in a partial temporal interpretation ( ; S) in the state a1 : : : ak, (written S; a1 : : : ak j= t) as follows: ( ; S); a1 : : : ak j= >, ( ; S); a1 : : : ak 6j= ? ( ; S); a1 : : : ak j= l i [a1; : : : ; ak]l 2 S, for a literal l ( ; S); a1 : : : ak j= [a]l i [a1; : : : ; ak; a]l 2 S or
a1 : : : ak; a is not a pre x of ( ; S); a1 : : : ak j= l i [a1; : : : ; ak; b]l 2 S,
where a1 : : : akb is a pre x of ( ; S); a1 : : : ak j= not l i ( ; S); a1 : : : ak 6j= l Observe that [a]l is true in any state of a linear model in which a is not the next action to be executed. The satis ability of rule bodies and rule heads in a temporal interpretation are de ned as usual. A rule 2(H Body) is satis ed in a temporal interpretation ( ; S) if, for all action sequences a1 : : : ak (including the empty one), ( ; S); a1 : : : ak j= Body implies ( ; S); a1 : : : ak j= H.
A rule H Body is satis ed in a partial temporal interpretation ( ; S) if, ( ; S); " j= Body implies ( ; S); " j= H, where " is the empty action sequence.
To de ne the answer sets of , we introduce the notion of reduct of , containing rules of the form: [a1; : : : ; ah](H Body). Such rules are evaluated in the state a1 : : : ah.
Let be a set of rules over an action alphabet , not containing default negation, and let !.
2 De nition 1. A temporal interpretation ( ; S) is a temporal answer set of if S is minimal (in the sense of set inclusion) among the S0 such that ( ; S0) is a partial interpretation satisfying the rules in .
To de ne answer sets of a program containing negation, given a temporal interpretation ( ; S) over 2 !, we de ne the reduct, ( ;S), of relative to ( ; S) extending Gelfond and Lifschitz' transform [13] to compute a di erent reduct of for each pre x a1; : : : ; ah of .
De nition 2. The reduct, a(1;;:S::);ah , of a1; : : : ; ah of , is the set of all the rules relative to ( ; S) and to the pre x [a1; : : : ; ah](H l1; : : : ; lm) such that H l1; : : : ; lm; not lm+1; : : : ; not ln is in for all i = m + 1; : : : ; n.
The reduct ( ;S) of relative to ( ; S) is the union of all reducts for all pre xes a1; : : : ; ah of . and ( ; S); a1; : : : ; ah 6j= li, De nition 3. A temporal interpretation ( ; S) is an answer set of is an answer set of the reduct ( ;S). ( ;S) a1;:::;ah if ( ; S)
Although the answer sets of a domain description are partial interpretations, in some cases, e.g., when the initial state is complete and all uents are inertial, it is possible to guarantee that the temporal answer sets of are total.
In case the initial state is not complete,we consider all the possible ways to complete the initial state by introducing in , for each uent name f , the rules: f not :f and :f not f . The case of total temporal answer sets is of special interest as a total temporal answer set ( ; S) can be regarded as temporal model ( ; V ), where, for each nite pre x a1 : : : ak of , V (a1; : : : ; ak) = fp : [a1; : : : ; ak]p 2 Sg. In the following, we restrict our consideration to domain descriptions , such that all the answer sets of are total.
The notion of extension of a domain description D = ( ; C) over is de ned in two steps: rst, the answer sets of are computed; second, all the answer sets which do not satisfy the temporal constraints in C are ltered out. For the second step, we need to de ne when a temporal formula is satis ed in a total temporal interpretation S. Observe that a total answer set S over can be regarded as a linear temporal (DLTL) model [22]. Given a total answer set S over we de ne the corresponding temporal model as MS = ( ; VS ), where p 2 VS (a1; : : : ; ah) if and only if [a1; : : : ; ah]p 2 S, for all atomic propositions p. We say that a total answer set S over satis es a DLTL formula if MS ; " j= .
De nition 4. An extension of a domain description D = ( ; C) over , is any (total) answer set S of satisfying the constraints in C. 3
Let us consider a business process of an investment rm, where the rm o ers nancial instruments to an investor. The description of the business processes given in Figure 1 in the language YAWL (Yet AnotherWork ow Language) [28].
Also, let us consider a regulation containing the following norms: (1) the rm shall provide to the investor adequate information on its services and policies before any contract is signed; (2) if the investor signs an order, the rm is obliged to provide him a copy of the contract.
The execution of each task in the process has some preconditions and e ects. Due to the presence of norms, the execution of a task in the process above should generate obligations to be ful lled. For instance, according to the second norm, signing an order generates for the rm the obligation to provide a copy of the contract to the investor. Verifying the compliance of a business process to a regulation requires to check that, in all the executions of the business process, the obligations triggered by the norms are ful lled.
In the following, we provide the speci cation of the business process and of the related norms in an action theory. The problem of verifying compliance of the business process to the norms is then de ned as a reasoning problem in the action theory. Concerning the speci cation of a business process, we distinguish two parts in this speci cation: the speci cation of the work ow itself, for which we will exploit the capability of the action language to represent complex actions, and the speci cation of the atomic tasks occurring in it. The description of the atomic actions occurring in the business process provides the background knowledge, which is common both to the business process and to the norms. The e ects and, possibly, the preconditions of the atomic tasks are de ned by introducing propositions representing the properties of the world that are a ected by the execution of the tasks and that are subject to the norms. They are the properties whose value is to be checked, for verifying the compliance of the process to the norms themselves. Such properties are sometimes used in the literature [14, 19, 30] as annotations that decorate the business process. Here, we exploit the action language to provide a more expressive formalism for formulating properties annotations. In the next subsections, we address the problems of specifying the atomic tasks, specifying the business process control and specifying the norms.
The atomic tasks occurring in the business process are those represented by boxes in the YAWL speci cation. In the action theory, they are modeled as atomic actions with the same name as the atomic tasks.
To introduce the propositions needed to describe the e ects and, possibly, the preconditions of atomic tasks, we introduce the following uent names in P: investor(C): C has been identi ed as a client (an investor); investor classif ied(C): the investor C has been classi ed; risk averse(C), risk seeking(C) represent the pro le of the client; inf ormed(C): the client has been informed about the bank services and policies; selected(T; C): client C has selected nancial instrument T ; accepted(T; C): client C has accepted nancial instrument T ; order signed(T; C): client C has signed the order of nancial instrument T ; order conf irmed(T; C): the order has been con rmed by the bank; sent contract(T; C): the contract of the order has been sent to the client; order deleted(T; C): the order has been canceled.
In the following, pro ling stands for investor pro ling, inform stands for inform investor, selection stands for nancial instrument selection, p eval stands for proposal evaluation and, nally, order verif stands for order veri cation.
The following action and causal laws describe the e ect of the actions in the business process. Although the action language is propositional, in the following, we use variables in uent names and in atomic action, so that each action/causal law stands for a nite number of ground action/causal laws: 2([investor identif ication(C)]investor identif ied(C)) client(C)) 2([prof iling(C)]investor classif ied(C) client(C)) 2([prof iling(C)]risk averse(C) or [prof iling(C)]risk seeking(C) client(C)) 2([inf orm(C)]inf ormed(C) client(C)) 2([f i selection(C)]selected(t1; C) or : : : or [f i selection(C)]selected(tn; C) f inancial instr(t1)^: : :^f inancial instr(tn)^risk averse(C)) 2([p eval(T; C)]accepted(T; C) or [p eval(T; C)]:accepted(T; C)) 2([sign order(T; C)]order signed(T; C) order(T ); client(C))
order(T ); client(C)) 2([send contract(T; C)]sent contract(T; C) order(T ); client(C)) 2([withdraw(T; C)]order deleted(T; C)) order(T ); client(C))
2([end procedure]end)
Laws de ning executability conditions for atomic tasks can also be given. For instance, 2([send contract(T; C)]?
not conf irmed(T; C)) states that it is possible to send a contract to the investor only if the contract has been con rmed. Such temporal formulae can be seen as \good properties", that the modeler would like to verify on the business process and they can be veri ed to hold in all possible executions of the business process with the same technique that will be introduced for verifying norm compliance. Indeed, some of the norms will be formalized as precondition laws. 3.2
When we are faced with the problem of specifying a business process, even in a given language as the one introduced in section 2.2, many options are available.
In [
Although this is a very simple solution, in the general case, the work ow of a business process may be non-structured or, even, we may want to provide a declarative speci cation of the business process, as done, for instance, in the declarative ow language ConDec [25]. It must be observed that the logical nature of our action language makes it well suited for a declarative speci cation. Indeed, the presence of general DLTL constraints in action domains allows for a simple way to constrain activities in a business process. As DLTL is an extension of LTL, it is possible to provide an encoding of ConDec constraints our action language.
Besides allowing for a declarative speci cation of business processes, the language introduced in Section 2 is well suited for encoding processes speci ed in conventional work ow languages, through the speci cation of action e ects, preconditions and constraints. Consider, for instance, the atomic task Investor prof iling. We can model the fact that this task can be executed only if the atomic task Investor identi cation has been executed, by introducing the precondition law: 2([prof iling(C)]? not investor identif ied(C)). Moreover, the fact that Investor prof iling has to be executed after Investor identi cation is executed can be modeled by the temporal constraint:
Consider, in addition, the atomic task Order veri cation. After its execution Send contract is to be executed if the order has been con rmed, otherwise, the task Modify order has to be executed. This can be modeled introducing the precondition laws 2([send contract(T; C)]?
:conf irmed(T; C)) conf irmed(T; C)) and temporal constraints
This approach can be generalized for translating YAWL processes into a domain description by action e ects and preconditions as well as constraints. The translation, in general, would require to introduce new uent names as, for instance, for each atomic task a, a uent executable(a), which is made true when the execution of task a is enabled. Some technicalities (that we do not address here) are needed to model AND/OR splits and AND/OR joins.
The approach we adopt in this paper for reasoning about actions is well suited for reasoning about systems with in nite computations (see [17]). To deal with nite computations we introduce a dummy action, which can be repeated in nitely many times after the termination of the process (thus giving rise to an in nite computation). In practice, however, as an optimization of the ASP translation, we can avoid looking for arbitrary models with loops during model checking and restrict to ad hoc computations corresponding to nite traces. 3.3
According to the normative speci cation, the execution of each task in the business process can trigger some normative positions (obligations, permissions, prohibitions). For instance, the identi cation task in the business process above, which introduces a new investor C, also generates the obligation to inform the investor. This obligation must be ful lled during the course of execution of the business process, if the process is compliant with the norm stating that the rm has the obligation to inform customers.
In the following we make use of causal laws to represent norms in the
action theory, and we introduce a notion of commitment to model obligations.
The use of commitments has long been recognized as a \key notion" to allow
coordination and communication in multi-agent systems [
A base level commitment C(i; j; A) can be naturally regarded as an obligation (namely, OA, \A is obligatory"), in which the debtor and the creditor are made explicit. The two kinds of base-level and conditional commitments we use here are essentially those introduced in [31]. Our present choice is di erent from the one in [20], where agents are committed to execute an action rather than to achieve a condition.
The idea is that commitments (or obligations) are created as e ects of the execution of some basic tasks in the business process and they are \discharged" when they have been ful lled. A commitment C(i; j; A), created at a given state of a run of the process, is regarded to be ful lled in the run if there is a later state of the run in which A holds. As soon as a commitment is ful lled in a run, it is considered to be satis ed and no longer active: it can be discharged.
Given the notion of commitment introduced above, the norms which generate obligations to be ful lled can be modeled as causal laws which trigger new commitments/obligations. Other norms which de ne preconditions on the executability of some actions or, in general, ordering constraints on the executions of atomic tasks can be encoded by general temporal formulas. For instance, we can encode the norms (1) and (2) above by the following precondition and causal laws:
2(C(f irm; C; sent contract(T; C)) order signed(T; C)) The rst one is a precondition for sign order(T; C), stating that, if the client has not been informed, he cannot sign an order. The second one, a causal law, states that when an order is signed by C, the rm is committed to C to send her the information required.
Causal laws are needed for modeling the interplay of commitments and uent changes. In particular, for each commitment C(i; j; ), we introduce the following dynamic causal laws in the domain description: (i) 2( (ii) 2( (iii) 2( :C(i; j; ) C(i; j; ); ) C(i; j; ) CC(i; j; ; ); ) :CC(i; j; ; ) CC(i; j; ; ); ) A commitment to bring about is considered ful lled and is discharged as soon as holds (i). A conditional commitment CC(i; j; ; ) becomes a base-level commitment C(i; j; ) when has been brought about (ii) and, in that case, the conditional commitment is discharged (iii).
One of the central issues in the representation of norms comes from the defeasible nature of norms. Norms may have exceptions: recent norms may cancel older ones; more speci c norms override more general norms and, in other cases, explicit priority information (not necessarily related to recency or speci city) is needed for eliminating con icts. Consider the following example from [19]: r1: C(S; M; O; discount) r2: :C(S; M; O; discount) sells(S; M; O); premium customer(M )
sells(S; M; O); special order(S; M; O) Rule r1 states that a seller has the obligation to apply a discount to premium customers. Rule r2 states that customers are not entitled for a discount in case the order (O) is a special order. Observe that, if two rules are regarded as being strict, a state in which the uents premium customer(M ), special order(S; M; O) and sells(S; M; O) hold results to be inconsistent.
To avoid con icting situations as the one above, priorities among rules can be incorporated. Suppose the two rules above are regarded as defeasible and assume that rule r2 has preference over rule r1 (we write r2 > r1). The priority between the con icting norms r1 and r2, with r2 > r1, can be modeled using default negation. For instance, we can transform the rules r1 and r2 as follows: 2(C(S; M; O; discount) sells(S; M; O); premium(M ); not bl(r1(S; M; O)))
where bl(ri(S; M; O)) means that rule ri is blocked. In this way, rule r2, when applicable, blocks the application of r1, but not vice-versa.
This treatment of priorities among con icting rules, in essence, relies on the
idea of using abnormality predicates for capturing exceptions. It is not intended
to provide a general solution to the problem of modeling priorities among rules,
as, in the general case, priorities may be also allowed between non con icting
rules. The problem of dealing with prioritized programs under the answer set
semantics has been addressed, for instance, in [
A further issue to be addressed when modeling norms is that of formalizing
violations and reparation obligations, and we refer to [
In this section we provide a characterization of the problem of compliance, as a problem of reasoning about action in the action theory de ned above. In Section 3.3, we have devised two di erent typologies of norms which we may want to verify compliance with: norms which can be encoded as a temporal formula (in the example, a precondition formula) and norms whose application generates obligations to be ful lled, which can be modeled as causal laws generating commitments. Concerning the rst kind of norms, the temporal formula encoding the norm has to be veri ed to be true in all the extensions of the domain description. Concerning the second kind of norms, verifying the compliance of the business process with such norms amounts to check that, in all the possible extensions of the domain description D, all the commitments generated will be eventually ful lled, unless they have been cancelled: 2(C(i; j; ) ! 3( _ :C(i; j; ))). Action withdraw, for instance, might have the indirect e ect of canceling the commitment to send the contract, if it has not yet been sent. Observe that canceling a commitment would not be possible if the commitment were encoded by the temporal formula 3 .
Let DB = ( B; CB) be a domain description de ned as the speci cation of a given business process B, including the speci cation of the atomic tasks involved in the process (semantic annotations). Let N be a set of norms, which have been encoded by a set of causal laws N and a set of temporal formulas PN . The domain description resulting from the encoding of the business process and the norms can then be de ned as D = ( B [ N ; CB). We can de ne the problem of verifying the compliance of a business process to a set of norms as follows: De nition 5. The business process B is compliant with the set of norms N = ( N ; PN ) if, for each extension ( ; S) of the domain description D = ( B [ N ; CB), the following conditions hold: { for each temporal formula in PN , ( ; S) satis es ; { for each commitment C(i; j; ) occurring in N , ( ; S) satis es the formula 2(C(i; j; ) ! 3( _ :C(i; j; ))).
Dually, the problem of identifying a violation to the norms can be regarded as a satis ability problem: the problem of nding an execution of the business process which violates some of the norms, that is, the problem of nding an extension ( ; S) of D such that either ( ; S) contains unful lled commitments, i.e., it satis es 3(C(i; j; ) ^ :3( _ :C(i; j; ))), or it falsi es a formula in N .
Consider the domain description D, including the speci cation DB of the business problem example and the causal law 2(C(f irm; C; sent contract(T; C)) order signed(T; C)). Each extension S of the domain description satis es the temporal formulas
Hence, the business process is compliant with the norms. In fact, in all the execution of the business process, the commitment to send the contract is eventually ful lled by the execution of the action send contract, which has to be eventually executed in the business process; and, for the second formula, the execution of sign order is always after inf orm which makes the client informed.
In [17] we exploit bounded model checking (BMC) techniques [
As an alternative to encoding the business process control ow in the logical formalisms (as done in section 3.2), a direct encoding of the work ow computations in the ASP program is also feasible, and makes the veri cation more e cient. In this case, the action language is used only for the speci cation of the semantic annotations and of the norms. Based on these ideas, we have used bounded model checking in ASP verify business process compliance. The implementation we have developed is based on the DLV system [23].
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. Both the business process, their semantic annotation and the norms are encoded using temporal ASP rules as well as temporal constraints. In particular, defeasible causal laws are used for modeling norms and commitments are introduced for representing obligations. The veri cation of compliance can be performed by using BMC techniques. In particular, we exploit an approach developed in [17] for DLTL bounded model checking in ASP, which extends the approach for bounded LTL model checking with Stable Models in [21]. We are currently testing our implementation on several work ow examples to verify the scalability of the approach, and to compare with other approaches to compliance veri cation, including the traditional Petri net approach.
Several proposals in the literature introduce annotations on business
processes for dealing with compliance veri cation [14, 19, 30]. In particular, [19]
proposes a logical approach to the problem of business process compliance based
on the idea of annotating the business process. Process annotations and
normative speci cations are provided in the same logical language, namely, the Formal
Contract Language (FCL), which combines defeasible logic [
In [30] a formal execution semantics for annotated business processes is introduced. The proposed semantics combines a Petri-net like (token passing) semantics for BPMN process execution, coming from the work ow community, with a declarative speci cation of actions preconditions and e ects in clausal form, coming from the AI literature of actions and state changes. Several veri cation tasks are de ned to check whether the business process control ow interacts correctly with the behaviour of the individual activities. However, [30] does not address the problem of verifying compliance of the business process with norms.
An approach to compliance based on a commitment semantics in the
context of multi-agent systems is proposed in [
[
In [24] the Abductive Logic Programming framework SHIFF [
In [26] 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 [15], 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.
Acknowledgments
We want to thank the anonymous referees for their helpful comments. This work has been partially supported by Regione Piemonte, Project \ICT4LAW: ICT Converging on Law: Next Generation Services for Citizens, Enterprises, Public Administration and Policymakers " 13. M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In Logic Programming, Proc. of the 5th Int. Conf. and Symposium, pages 1070{1080, 1988. 14. A. Ghose and G. Koliadis. Auditing business process compliance. ICSOC, LNCS 4749, pages 169{180, 2007. 15. C. Giblin, S. Muller, and B. P tzmann. From Regulatory Policies to Event Monitoring Rules: Towards Model-Driven Compliance Automation. IBM Reasearch Report, 2007. 16. L. Giordano, A. Martelli, and C. Schwind. Specifying and Verifying Interaction Protocols in a Temporal Action Logic. Journal of Applied Logic (Special issue on Logic Based Agent Veri cation), 5:214{234, 2007. 17. L. Giordano, A. Martelli, and D. Theseider Dupre. Reasoning about Actions with Temporal Answer Sets. Proc. CILC 2010, 25th Italian Conference on Computational Logic, 2010. 18. 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. 19. G. Governatori and S. Sadiq. The journey to business process compliance. Handbook of Research on BPM, IGI Global, pages 426{454, 2009. 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. N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, S. Perri, and F. Scarcello.
The dlv system for knowledge representation and reasoning. ACM Transactions on Computational Logic, 7(3):499{562, 2006. 24. Marco Montali, Paolo Torroni, Federico Chesani, Paola Mello, Marco Alberti, and Evelina Lamma. Abductive logic programming as an e ective technology for the static veri cation of declarative business processes. Fundam. Inform., 102(34):325{361, 2010. 25. 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. 26. Dumitru Roman and Michael Kifer. Semantic web service choreography: Contracting and enactment. In International Semantic Web Conference, LNCS 5318, pages 550{566, 2008. 27. M. P. Singh. A social semantics for Agent Communication Languages. Issues in
Agent Communication, LNCS(LNAI) 1916, pages 31{45, 2000. 28. W. van der Aalst and A. ter Hofstede. YAWL: Yet Another Work ow Language.
Information Systems, 30(4):245{275, 2005. 29. 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. 30. Ingo Weber, Jorg Ho mann, and Jan Mendling. Beyond soundness: On the veri cation of semantic business process models. Distributed and Parallel Databases (DAPD), 2010. 31. P. Yolum and M.P. Singh. Flexible Protocol Speci cation and Execution: Applying Event Calculus Planning using Commitments. AAMAS'02, pages 527{534, 2002.