Evaluating Compliance: From LTL to Abductive Logic Programming Marco Montali1 , Federico Chesani2 , Marco Gavanelli3 , Evelina Lamma3 , and Paola Mello2 1 Free University of Bozen-Bolzano Piazza Domenicani 3, 39100 – Bolzano (Italy) montali@inf.unibz.it 2 University of Bologna V.le Risorgimento 2, 40136 – Bologna (Italy) { federico.chesani | paola.mello }@unibo.it 3 University of Ferrara Via Saragat 1, 44122 – Ferrara (Italy) { marco.gavanelli | evelina.lamma }@unife.it Abstract. The compliance verification task amounts to establishing if the execution of a system, given in terms of observed events, does re- spect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to as- sess compliance. In this work we review the LTL and the Abductive Logic Programming frameworks in the light of compliance evaluation, and formally investigate the relationship between the two approaches. We define a notion of compliance within each approach, and then we show that an arbitrary LTL formula can be expressed in SCIFF, by pro- viding an automatic translation procedure from LTL to SCIFF which preserves compliance. Keywords: Linear Temporal Logic, Abductive Logic Programming, Compli- ance Verification, Business Process Management. 1 Introduction Linear Temporal Logic (LTL) [12] specifications are traditionally used for ex- pressing the properties that a reactive system should exhibit (or avoid), and are exploited by model checking tools for formal verification (e.g., [15,9]). Recently, LTL has been also used to describe the system under study itself, in fields like Business Process Management (BPM) and Service Oriented Computing (SOC): e.g., the DECLARE system [24] and the ConDec language [23,20] adopt LTL to model business processes, business rules and policies. In these domains, a relevant task is to assess compliance, usually defined as checking if an implementation faithfully meets the requirements of a specifica- tion. The LTL models correspond to linear Kripke structures representing the execution traces (i.e., sequences of events) occurred during a specific instanti- ation of the system, while entailment becomes a compliance evaluator w.r.t. a regulatory specification expressed as an LTL formula. Such approach has been used, for example, in [6] for static compliance verification of BPMN business processes, and in [1] for auditing event logs. Recently, Logic Programming (LP) based approaches have been applied for specification and verification of normative systems [5,14], web services [25,7] and business processes as well [11,20]. The LP framework nicely meets the ad- vantages of a declarative, first-order specification, grounded on a model-based semantics, and equipped with an operational proof procedure. Abductive Logic Programming (ALP, [17]), in particular, integrates abductive reasoning into LP, supporting an hypothesis-making mechanism. In [2] we have defined the abductive proof procedure named SCIFF, originally developed for specification and verification of open societies of “computees” (a sort of agents), and later applied to normative systems [4,8], web service interac- tion [3,21] and BPM [22,20]. SCIFF specifications are given in terms of integrity constraints linking occurring events to expectations about the future course of events, and the declarative semantics has been given in terms of compliance of a given trace with respect to a SCIFF specification. In this paper we investigate the relation between the LTL-based approach and the SCIFF framework, showing that if we focus on the compliance task, an LTL model can be (formally and correctly) translated into a SCIFF one. Starting from the seminal work in [13] about Separated Normal Forms (SNF) for LTL formulae, we define proper mapping functions and show how any LTL formula can be expressed within the SCIFF formalism. Then, we formally define the notion of compliance in both the approaches, we identify a tight equivalence relation, and we prove how such equivalence is indeed maintained when moving from the LTL approach to the SCIFF-based one. 2 Linear Temporal Logic In this section, we provide a brief introduction to (propositional) Linear-time Temporal Logic (LTL), in particular w.r.t. the notion of compliance; the inter- ested reader can refer to [12] for a more general introduction. LTL formulae are built up from atomic propositions, whose truth values change over time. The LTL time structure F, also called frame, models a single, linear timeline; formally, F is a totally ordered set (K , ≺) [12]. Definition 1 (LTL model). Let P be the set of all atomic propositions in the system. An LTL model M for P is a triple (K , ≺, v) where v : P → 2K is a function which maps each proposition in P to the set of time instants at which the proposition holds. We are interested in systems characterized by dynamics consisting of a stream of events. In this respect, each proposition represents a possible event that may occur in an instance of the system. More specifically, a proposition e ∈ P is true in a certain state if at that state the event denoted by e occurs. Under this interpretation, LTL models correspond to execution traces. Definition 2 (LTL execution trace). Given a set E of atomic propositions (representing possible events), an LTL execution trace TL is an LTL model hav- ing (N, <) as time structure and E as the set of atomic propositions. In particu- lar, TL = (N, <, vocc ), where vocc : E → 2N is a valuation function mapping each event e ∈ E to the set of all time instants i ∈ N at which e occurs. We will use the following abbreviations: TL (i) will denote the i-th state of TL , i.e. the subset {e ∈ E | i ∈ vocc (e)}. 2.1 Syntax of LTL LTL formulae are defined by using (i) atomic propositions, i.e., events, together with the two special constants true and f alse; (ii) classical propositional con- nectives, i.e., ¬, ∧, ∨ and ⇒; (iii) temporal operators, i.e., (next time), U (until), ♦ (eventually),  (globally) and W (weak until). An LTL formula is recursively defined as: each event e ∈ E is a formula; if ϕ and ψ are formulae, then ¬ϕ, ϕ ∧ ψ, ψ, and ϕUψ are formulae. Other LTL formulae can be defined as abbreviations: – ϕ ∨ ψ , ¬(¬ϕ ∧ ¬ψ) and ϕ ⇒ ψ , ¬ϕ ∨ ψ; – true , ¬ϕ ∨ ϕ and f alse , ¬true; – ♦ϕ , trueUϕ, ϕ , ¬♦¬ϕ and ψWϕ , ψUϕ ∨ ψ. 2.2 Semantics of LTL and Compliance The semantics of LTL is given w.r.t. an LTL execution trace, and w.r.t. a specific state. We will use |=L to denote the logical entailment in the LTL setting. M, i |=L ϕ means that ϕ is true at time i in model M. |=L is defined by induction on the structure of the formulae4 : (TL |=L ϕ) iff (TL , 0 |=L ϕ); (TL , i |=L e) iff e ∈ TL (i) (i.e., i ∈ vocc (e)); (TL , i 6|=L e) iff e 6∈ TL (i); (TL , i |=L ¬ϕ) iff (TL , i 6|=L ϕ); (TL , i |=L ϕ ∧ ψ) iff (TL , i |=L ϕ) and (TL , i |=L ψ); (TL , i |=L ϕ ∨ ψ) iff (TL , i |=L ϕ) or (TL , i |=L ψ); (TL , i |=L ϕ ⇒ ψ) iff (TL , i 6|=L ϕ) or (TL , i |=L ψ); (TL , i |=L ϕ) iff (TL , i + 1 |=L ϕ); (TL , i |=L ψUϕ) iff ∃k ≥ i s.t. (TL , k |=L ϕ) and ∀i ≤ j < k (TL , j |=L ψ); (TL , i |=L ♦ϕ) iff ∃j ≥ i s.t. (TL , j |=L ϕ); (TL , i |=L ϕ) iff ∀j ≥ i (TL , j |=L ϕ); 4 For the sake of readability, we explicitly show the semantics of ♦,  and W, even if their meaning can be obtained from the semantics of U and . (TL , i |=L ψWϕ) iff either (TL , i |=L ψUϕ) or (TL , i |=L ψ). When LTL is employed to formalize compliance rules, the declarative seman- tics selects those events that must be contained (or avoided) in certain states so as to fulfil them, separating compliant traces from non-compliant ones. In this respect, |=L plays the role of a compliance evaluator. Definition 3 (LTL Compliance). An LTL trace TL is compliant with a LTL formula ϕ if and only if TL entails ϕ: cmpLTL (TL , ϕ) , TL |=L ϕ. When LTL formulae are used to express business constraints/rules of a regu- latory model, as for example in the ConDec language [23], then the LTL formula used for compliance is the conjunction of all formulae contained in the regulatory model. From an operational viewpoint, the compliance of a formula ϕ w.r.t. a TL is verified by means of model checking algorithms. 3 The SCIFF Framework In the following we will briefly recap the main features of the SCIFF framework. The interested reader can refer to [2] for a detailed and comprehensive presenta- tion. A SCIFF specification S is an Abductive Logic Program hKB, A, ICi [17] where: (i) KB is a (static) knowledge base (a Logic Program [19]); (ii) A is a special set of predicates, called abducibles; two special abducibles, namely E/2 and EN/2, are used to represent the expectations; (iii) IC is a set of SCIFF integrity constraints, relating happened events with expectations. Roughly speaking, given a goal G, abductive reasoning looks for a set of literals ∆ built from predicates A such that the goal is entailed by the program KB ∪ ∆, and the set of integrity constraints IC is entailed too. The set ∆ is referred to as an abductive explanation (see Definition 6). Three special predicates are used to model happened events and positive/neg- ative expectations. Happened events are denoted by using the (non abducible) predicate H(Ev, T ), where Ev is a term representing the occurred event, while T explicitly represents the time at which the event occurred. In the remainder of this paper we will assume the time domain relies on natural numbers. Definition 4 (SCIFF Execution Trace). A SCIFF execution trace T (or simply a SCIFF trace) is a set of positive ground H(E, T ) atoms. A specific execution of the system under study is called an instance, and it is formally identified by the SCIFF specification modeling the system and by the execution trace produced during the instance execution. Definition 5 (SCIFF Instance). Given a SCIFF specification S = hKB, A, ICi and a trace T , hS, T i is an instance of S. Positive and negative expectations model expected and forbidden events. They are represented by E(Ev, T ) and EN(Ev, T ), where Ev is a term describing the event, and T is a term or a variable. The intended meaning is that event Ev is expected to occur/not occur at time T . SCIFF Integrity Constraints (IC) are mainly used to relate happened events with expectations. They are body → head rules, where body contains a conjunc- tion of happened events, general abducibles, and defined predicates, while head contains a disjunction of conjunctions of expectations, general abducibles, and defined predicates. When the body is matched with events and abducibles, the IC is triggered, and expectations occurring in the head are assumed (abduced). Definition 6 (Abductive explanation ∆). Given a SCIFF instance hS, T i, a set ∆ ⊆ A is an abductive explanation for hS, T i if and only if Comp (KB ∪ T ∪ ∆) ∪ CET ∪TX |= IC where Comp is the (two-valued) completion of a theory [18], CET stands for Clark Equational Theory [10] and TX is the CLP constraint theory [16], param- etrized by the domain X . We remind for completeness that CET is provided by the following axioms: – c 6= c0 c, c0 any pair of distinct constants – f (x1 , . . . , xn ) 6= g(y1 , . . . , ym ) f, g any pair of distinct functors – f (x1 , . . . , xn ) = f (y1 , . . . , yn ) → x1 = y1 ∧ . . . xn = yn – f (x1 , . . . , xn ) 6= c f any functor, c any constant – τ (x) 6= x τ (x) any term structure in which x is free. – x = y → [W (x) ↔ W (y)] W any formula together with the usual rules of reflexivity, symmetry and transitivity for equal- ity. Fixing a CLP theory corresponds to instantiate the parameter X and the set of allowed constraints. Therefore, different structures can be chosen without affecting the notion of SCIFF’s abductive explanation. We will instantiate such a parameter to N, with linear equations and dis-equations. The theory of con- straints TN defines the symbols +, −, ∗, /, =, >, <, ≥, . . . with the usual meanings (e.g., 1 < 2 + 2 is evaluated to true). Remark 1 (Abductive explanations and sub-specifications). If ∆ is an abduc- tive explanation for hS, T i, then ∆ is an abductive explanation also for hS 0 = hKB, A, IC 0 i, T i, where IC 0 ⊆ IC. Being able to generate hypotheses might not be enough: in specific domains like, e.g., legal reasoning, a further step of verification of the hypotheses against the observed events (available data) is mandatory. Hence, the SCIFF framework provides also an hypotheses-confirmation mechanism, based on the formal no- tions of fulfillment and violation. First of all, expectations must be E-consistent: the same event cannot be expected and prohibited at the same time. Definition 7 (E-consistency). An abducible set ∆ is E-consistent iff for each event e and for each time t it holds that {E(e, t), EN(e, t)} * ∆ The relationship between expectations and happened events is instead captured by the notions of fulfillment and violation. Definition 8 (T -Fulfillment). Given a SCIFF trace T and an abducible set ∆, ∆ is T -fulfilled iff for each event e and for each time t: E(e, t) ∈ ∆ → H(e, t) ∈ T and EN(e, t) ∈ ∆ → H(e, t) ∈ /T Definition 9 (T -Violation). Given a SCIFF trace T and an abducible set ∆, ∆ is T -violated iff it exists at least one event e and time t such that: E(e, t) ∈ ∆ ∧ H(e, t) ∈ / T , or EN(e, t) ∈ ∆ ∧ H(e, t) ∈ T Given an abductive explanation ∆, fulfillment acts as a classifier that separates the legal/correct execution traces with respect to ∆ from the wrong ones. Definition 10 (Compliance in SCIFF). A trace T is compliant with a SCIFF specification S if and only if there exists an abducible set ∆ such that: 1. ∆ is an abductive explanation for hS, T i; 2. ∆ is E-consistent; 3. ∆ is T -fulfilled. If this is the case, we write cmpSCIFF ∆ (T , S) or simply cmpSCIFF (T , S). 4 Relating LTL and SCIFF LTL and SCIFF rely on different logics, but when capturing regulatory models they both act as compliance evaluators, capturing the same idea of compliance. To capture some similarity w.r.t. compliance, we propose a mapping between LTL and SCIFF. First of all, we need to provide a mapping between an LTL trace TL and the corresponding SCIFF trace T (and vice versa). Definition 11 (Trace mapping). Given an LTL trace TL = (N, <, vocc ) and the set of atomic propositions E, we map any possible pair (e, i) into a corre- sponding SCIFF event H(e, i), where e ∈ E and i ∈ N. A trace mapping tm is a transformation which maps an arbitrary LTL trace TL onto a corresponding SCIFF one, by applying the event mapping to each proposition belonging to TL , i.e. to each e ∈ E and for each i ∈ vocc (e):  tm(TL ) = H(e, i)|e ∈ E, i ∈ vocc (e) Example 1. Let us consider an LTL execution trace TL = (N, <, vocc ), where E = {a, b, c, d } is the set of propositional events and vocc is defined as follows: vocc (a) = {0, 1} vocc (b) = {2} vocc (c) = {3} vocc (d) = ∅  Then tm (TL ) = H(a, 0), H(a, 1), H(b, 2), H(c, 3) The inverse translation, which starts from a SCIFF execution trace and produces a corresponding LTL trace, will be denoted by tm−1 . Thanks to the trace mapping function tm, it is possible to evaluate whether the “same” execution trace complies with an LTL and a SCIFF specification: if the two models agree, then they express in some sense “equivalent” prescriptions w.r.t. the trace. Generalizing, if such an agreement is valid for all the possible execution traces, then the two specifications are behaviorally equivalent. Definition 12 (Behavioural equivalence w.r.t. compliance). A SCIFF specification S and an LTL formula ϕ are behaviorally equivalent w.r.t. compli- c ance (ϕ ! S) if and only if for each LTL trace TL it holds that: cmpLTL (TL , ϕ) ⇐⇒ cmpSCIFF (tm (TL ) , S) . We might notice that Definition 12 does not pose any constraint on the SCIFF specification S: indeed, only the trace TL is somehow constrained by the appli- cation of the mapping function tm. 5 On the Expressiveness of SCIFF We show now that an arbitrary LTL formula can be expressed in SCIFF by pro- viding an automatic translation procedure from LTL to SCIFF which preserves the compliance equivalence. To this end, we exploit the Separated Normal Form (SNF) for LTL formulae. 5.1 A Separated Normal Form for LTL Formulae Fisher and colleagues [13] introduced SNF to express an arbitrary LTL formula by adopting a conjunction of three-basic forms, while preserving satisfiability. Definition 13 (SNF Formula [13]). An LTL formula ϕ is in SNF iff ϕ is a conjunction of formulas of the following forms: _ start =⇒ lc (an initial LTL-clause) c ^ _   ka =⇒ ld (a step LTL-clause) a d ^   kb =⇒ ♦l (a sometime LTL-clause) b where ki and lj are literals (i.e., atomic propositions or negation of atomic propo- sitions) and start is a special symbol true only at the initial time (i.e., whose valuation function is the set {0}). In this case, we say that ϕ is an SNF formula. Definition 14 (LTL to SNF translation [13]). snf is a function which translates an arbitrary LTL formula to a corresponding SNF formula. During the transformation, new proposition symbols are introduced to rename complex sub-formulae. Hence, we distinguish between propositions used to rep- resent activities/events, and those used for renaming. Definition 15 (Proposition symbols, renaming and event sets). Given an LTL formula ϕ, P (ϕ) is the set of proposition symbols contained in ϕ. Given an SNF formula σ s.t. σ = snf(ϕ), it holds that P (σ) = E(σ) ∪ R (σ), where: 1. event set E(σ) is the set of atomic propositions contained in the original LTL formula ϕ, which denote events (E(σ) = P (ϕ)) 2. renaming set R (σ) is the set of atomic propositions used for renaming during the transformation. Example 2. Let us consider LTL “precedence” formula stating that the send receipt activity can be executed only after having executed the pay activity: ϕ = ¬send receipt W pay Hence, P (ϕ) = {pay, send receipt}. The SNF translation of ϕ is: σ = snf [¬send receipt  W pay] =   start ⇒ (¬x ∨ ¬send receipt ∨ pay) ∧ true ⇒ (¬x ∨ ¬send receipt ∨ pay) ∧     start ⇒ (¬x ∨ y ∨ pay) ∧  = start ⇒ x ∧   true ⇒ (¬x ∨ y ∨ pay) ∧ y ⇒ (¬send receipt ∨ pay) ∧     y ⇒ (y ∨ pay)  Therefore, R (σ) = {start, x, y, true}. 5.2 Translation from SNF Formulae to SCIFF We now provide a syntactic procedure which translates an arbitrary SNF formula to SCIFF, and prove that such a translation preserves compliance. Definition 16 (IC-mapping). An IC-mapping icm is a function which trans- lates an SNF formula to a set of SCIFF integrity constraints, defined as5 : 5 Abducible predicates will be represented as bold terms. " # ^ [ icm ϕi , icm [ϕi ] i i " # _ _ icm start =⇒ lc , icm [start, 0] → icm [lc , 0] . c c " !# ^ _ ^ _ icm  ka =⇒ ld , icm [ka , T ] → (icm [ld , T2 ] ∧ T2 = T + 1) . a d a d " !# ^ ^ icm  ka =⇒ ♦l , icm [ka , T ] → icm [l, T2 ] ∧ T2 ≥ T. a a icm [start, 0] , occ(start, 0) icm [true, T ] , true(T ) icm [a, T ] , occ(a, T ) icm [¬a, T ] , not occ(a, T ) Where a stands for a generic propositional symbol. The IC-mapping maps the presence of a certain proposition in a given state onto an abducible occ/2, stating that the proposition occurs in that state. Conversely, the absence of the proposition is mapped onto an abducible not occ/2. Definition 17 (S-mapping sm). Given an SNF formula ϕ and a set V ⊆ P (ϕ) of proposition symbols, the S-mapping sm translates ϕ to a SCIFF specification depending on V . sm is defined as: sm : ϕ, V 7−→ h∅, {E/2, EN/2, true/1, occ/2, not occ/2}, IC)i where IC = icm(ϕ) ∪ { true → occ(start, 0). (S) true → true(0). (T1 ) true(T ) → true(T2 ) ∧ T2 = T + 1. (T2 ) ∀p ∈ P (ϕ), p 6= start, true(T ) → occ(p, T ) ∨ not occ(p, T ). (2V ) occ(X, T ) ∧ not occ(X, T ) → ⊥. (C) H(X, T ) ∧ X ∈ V → occ(X, T ). (O) occ(X, T ) ∧ X ∈ V → E(X, T ). (E1 ) not occ(X, T ) ∧ X ∈ V → EN(X, T ). } (E2 ) S-mapping applies IC-mapping and then augments the obtained constraints with further general rules. Such rules capture specific aspects of the LTL semantics: – (S) translates the special start symbol, which is introduced by SNF and is true only at the initial state (i.e., at time point 0). – (T1 ) and (T2 ) formalize the LTL true atom, which is implicitly subject to the formula (true). To this aim, the true abducible is introduced, using an initial rule (T1 ) and a recursive rule. – (2V ) and (C) are used to model the two-valued semantics of LTL, i.e., that in each state either a proposition is either true or false. We exclude the symbol “start”, which is introduced by Fisher et al. as a special symbol holding only in the initial state. – (O), (E1 ) and (E2 ) relate the (not) occurrence of each proposition in each state with the SCIFF concepts of happened events and expectations. The next theorem states that sm preserves compliance: an arbitrary SNF formula can be translated to a behaviourally equivalent SCIFF specification. Theorem 1 (SCIFF can express SNF formulae ). Given an SNF formula c σ and the SCIFF specification S = sm [σ, P (σ)], it holds that σ ! S. Proof. Since LTL and SCIFF share the same semantics for logical symbols AND(∧), OR (∨), and implication(⇒ in LTL and → in SCIFF), we will fo- cus only on the simplest SNF-forms, consisting of single proposition symbols (instead of conjunctions/disjunctions). σ = (start ⇒ l) If l is a positive literal, say, l = a, each compliant LTL execution trace TL must satisfy the property that a ∈ TL (0), because start always holds in state 0. The obtained S contains the corresponding IC icm[start ⇒ a] = occ(start, 0) → occ(a, 0). By taking into account also the two general ICs (S) and (E1 ), all abductive explanations of S must expect a at time point 0, i.e., they must contain E(a, 0). Therefore, each compliant trace T must contain H(a, 0). By con- sidering the trace mapping function tm, this is exactly the same property required for compliant LTL traces, and therefore compliance is preserved by switching from σ to S or vice-versa. The case in which l is a negative literal, say, l = ¬a, can be proven in a similar way. σ = (k ⇒ l) Let us consider a first case where both k and l are positive literals, and focus on one side of the equivalence ( c ); the other side can be proven in a very similar way. To disprove c , one must find an execution trace TL which is compliant with σ, but whose corresponding trace T is not compliant with S = sm [σ, P (σ)]. Notice that, by Definition 17 (applying (O) and (E1 )), S explicitly foresees that in case k happens at a time t, then l is expected to happen at time t2 , t2 = t + 1. Hence, to violate S, T must contain, for a certain time t the event H(k, t), while H(l, t2 ) 6∈ T . By applying the tm−1 function on this trace, one obtains a TL which obeys the following properties: (1) k ∈ TL (t), and (2) l 6∈ TL (t + 1). The second property in particular implies that TL is not compliant with σ, hence the initial hypothesis does not hold. The other side of the implication ( c ) can be proved in the same way, exploiting again the characteristics of the tm function. This same proving schema can be applied also to the case where k is a positive literal, and l is a negative literal: the only difference is that S will contain a negative expectation EN, rather than a positive one as before. Let us now consider the case in which k is a negative literal, say k = ¬a, and l is a positive literal, say l = b; again, the case in which l is a negative literal can be proven in the same way. Each compliant TL trace must obey the following property: ∀ t, a ∈ TL (t)∨b ∈ TL (t+1). The IC obtained by the application of icm is not occ(a, T ) → occ(b, T2 ) ∧ T2 = T + 1. For each time t, if a happens at time t then rule (O) states that occ(a, t) is abduced, rule (C) prevents not occ(a, t) to be abduced and thus the IC does not trigger. If, conversely, a does not happen at time t, by rule (2V ) we can have two options. In the first, occ(a, t) is abduced, which imposes that also E(a, t) is abduced (rule E1 ); since a does not happen at time t, this assumption is not fulfilled. In the second, not occ(a, t) is abduced, the IC triggers, abducing occ(b, t + 1), which in turn triggers (E1 ), imposing that b is expected to happen at time t + 1. Therefore, each SCIFF compliant execution trace T must satisfy that ∀ t, H(a, t) ∈ T ∨ H(b, t + 1) ∈ T , which is equivalent, under tm, to the property on LTL traces. σ = (k ⇒ ♦l) This case of a simple sometime LTL-clause trivially follows from the dis- cussion made for the previous LTL-clause. The only difference is that the constraint T2 = T + 1 is substituted by T2 ≥ T in this more general case. Having proven that sm preserves compliance for each SNF basic form, we must prove that the translation preserves compliance when applied to a conjunction of these forms. This is straightforward, because a trace complies with a SCIFF specification if all the integrity constraints are respected. 5.3 Translation of Arbitrary LTL Formulae to SCIFF We now demonstrate that also an arbitrary LTL formula can be encoded in SCIFF preserving compliance. The main technical problem is that the SNF trans- lation introduces new symbols (used for renaming complex sub-formulae) which do not represent events. At the SNF level, the distinction between concrete events and renaming symbols gets lost, and therefore the SCIFF specification produced by applying in cascade the SNF and the sm translation does not preserve com- pliance w.r.t. the original LTL formula: positive expectations are imposed also on renaming symbols, which however do not appear in the original LTL formula. To overcome this issue, the intuitive idea is to restrict the translation sm function only to events. The first step is therefore to define, in both settings, a suitable trace projection, which filters an execution trace by maintaining only certain symbols (in particular, the ones which correspond to events). Definition 18 (SCIFF trace projection). Given a SCIFF execution trace T and a set V of predicate symbols, the trace projection of T on V (T |V ) is the subset of T containing only events taken from V : T |V , {H(e, t) | H(e, t) ∈ T ∧ e ∈ V } Definition 19 (LTL trace projection). Given an LTL execution trace TL = (N, <, vocc ) and a set V of proposition symbols, the trace projection of TL on V (TL |V ) is the projection of TL containing only events taken from V :  0 0 vocc (e) if e ∈ V ; TL |V = (N, <, vocc ) s.t. vocc (e) , ∅ otherwise. Lemma 1 (Commutativity between trace projection and trace map- ping). For each LTL execution trace TL and for each set of proposition symbols V tm [TL |V ] = tm [TL ] |V Proof. From the definitions of trace mapping (Def. 11) and of trace projection (Def. 18 and 19). We now briefly recall one of the main results presented in [13], which proves that SNF preserves satisfiability, i.e., in our setting, that it preserves compli- ance. Lemma 2 reviews the satisfiability result by explicitly taking into account execution traces. In particular, it states that execution traces compliant respec- tively with an LTL formula and its corresponding SNF are exactly the same if we restrict the comparison only to concrete events. Theorem 2 (SNF preserves satisfiability [13]). An LTL formula ϕ is sat- isfiable iff snf(ϕ) is satisfiable. Lemma 2 (Compliance preservation via extended traces, adapted from [13]). For each LTL formula ϕ, it holds that  ∀ TL cmpLTL (TL , snf [ϕ]) =⇒ cmpLTL TL |E(snf[ϕ]) , ϕ ∀ TL cmpLTL (TL , ϕ) =⇒ ∃TL0 s.t. TL = TL0 |E(snf[ϕ]) ∧ cmpLTL (TL0 , snf [ϕ]) where we remember that (by Definition 15) E (snf [ϕ]) = P (ϕ). With such pre- liminaries, it is possible to prove that each LTL formula is translatable to a SCIFF specification, preserving compliance. Theorem 3 (SCIFF can express LTL). Given an arbitrary LTL formula ϕ c and the SCIFF specification S = sm [snf [ϕ] , P (ϕ)], it holds that S ! ϕ. Proof. Let us denote σ = snf [ϕ]. From Def. 12, and by remembering that the event set of σ contains all the proposition symbols of ϕ (P (ϕ) = E(σ)), one has to prove that ∀TL , cmpLTL (TL , ϕ) ⇐⇒ cmpSCIFF (tm [TL ], sm [σ, E(σ)]) We will prove firstly one way of the implication (=⇒), and then the opposite direction (⇐=). Both the proofs are organized in the same way: by applying the results obtained in Lemma 1, Lemma 2, and Theorem 1, the problem of proving a formula is reduced to prove another, simpler formula. Hence, each proof starts with a diagram that shows how each previous result is applied to a formula, and then the simpler formula is proved. (=⇒) Let us consider the following schema: (∗) ∀ TL , cmpLTL (TL , ϕ) ========⇒ cmpSCIFF (tm [TL ], sm [σ, E(σ)]) w w ~ w w w w w wLemma 2 w w w w (†)  w w ∃TL0 , TL = TL0 |E(σ) Theorem 1 =========⇒ cmpSCIFF (tm [TL0 ], sm [σ, P (σ)]) ∧cmpLTL (TL0 , σ) The schema shows that proving (∗) reduces to prove (†), i.e., we prove that cmpSCIFF (tm [TL0 ], sm [σ, P (σ)]) =⇒ cmpSCIFF tm TL0 |E(σ) , sm [σ, E(σ)]    (†) By taking into account abducible sets, Def. 15 and Lemma 1, (†) becomes: 0 cmpSCIFF ∆ T , S ER =⇒ cmpSCIFF ∆ T |E(σ) , S E   (‡) where S ER = sm [σ, E(σ) ∪ R (σ)], S E = sm [σ, E(σ)] and T = tm [TL0 ]. To prove (‡), we demonstrate that ∆0 = ∆ \ {E(e, t)|e ∈ R (σ)} \ {EN(e, t)|e ∈ R (σ)} obeys the three properties required by the Definition 10 of SCIFF compliance: 1. ∆0 is an abductive explanation for STE |E(σ) . The only difference between S E and S ER is that, for the first specification, rules (O), (E1 ) and (E2 ) of Def. 17 do not trigger for events outside E(σ) (in particular, they do not trigger for events inside R (σ)). From Remark 1, ∆ is therefore a suitable abductive ex- planation for S E too. Furthermore, being (E1 ) and (E2 ) the only constraints involving positive and negative expectations concerning elements in R (σ), it is not required for an abductive explanation to contain them anymore. 2. ∆0 is E-consistent, because ∆0 ⊆ ∆ and ∆ is E-consistent. 3. ∆0 is T |E(σ) -fulfilled. Since T |E(σ) is a projection of T , ∆0 ⊆ ∆ and ∆ is T -fulfilled, no negative expectation in ∆0 can be violated by T |E(σ) . Positive expectations concerning elements in E(σ) are maintained in ∆0 , and so are the corresponding happened events after the trace projection. Positive ex- pectations concerning elements in R (σ) are removed from ∆ when obtaining ∆0 , and therefore the application of the trace projection, which rules out happened events concerning elements in R (σ), does not affect fulfillment. (⇐=) We move then to prove the other way of the double implication stated in this theorem. Again, let us consider the following schema: (∗∗) cmpLTL tm−1 [T ] , ϕ ⇐========== ∀ T , cmpSCIFF (T , sm [σ, E(σ)])  ~ w w w w w w w w wLemma 2, then Lemma 1 w(§) w w  w  Theorem 1 ∃ T 0 , T = T 0 |E(σ) cmpLTL tm−1 [T 0 ] , σ ⇐=========== ∧cmpSCIFF (T 0 , sm [σ, P (σ)]) The schema shows that proving (∗∗) reduces to prove (§), i.e. we prove that 0 ∀ T , cmpSCIFF ∆ T , S E =⇒ ∃ T 0 , T = T 0 |E(σ) ∧ cmpSCIFF ∆ T 0 , S ER   (§) where S ER = sm [σ, E(σ) ∪ R (σ)] and S E = sm [σ, E(σ)]. First of all, it is worth noting that S ER extends S E by imposing that rules (O), (E1 ) and (E2 ) can be also triggered by occ/not occ abducibles involving symbols in R (σ), generating a larger set of expectations. Since T 0 ⊇ T , an abductive explanation ∆0 can be therefore found for S ER by extending ∆ with the new generated expectations: ∆0 = ∆ ∪ ∆E EN E R ∪ ∆R , where ∆R and ∆R EN respectively represent the inserted positive and negative expectations. ∆0 is E-consistent. Indeed, since ∆E R and ∆R EN contain only expectations generated by rules (E1 ) and (E2 ), by construction we have: 0 ∀ E(a, t), E(a, t) ∈ ∆E R ⇒ occ(a, t) ∈ ∆ (§§) ∀ EN(a, t), EN(a, t) ∈ ∆EN R ⇒ not occ(a, t) ∈ ∆0 Let us suppose by absurdum that there exist a, t (with a ∈ R (σ)) s.t. E(a, t) ∈ 0 ∆E EN R and EN(a, t) ∈ ∆R . In this case, (§§) would state that occ(a, t) ∈ ∆ and not occ(a, t) ∈ ∆ . This would violate rule (C), making impossible that ∆0 is 0 an abductive explanation. An execution trace T ∗ compliant with S ER can be therefore built as follows: T ∗ = T ∪ T R , where H(a, t) ∈ T R ⇔ E(a, t) ∈ ∆E R Under this choice: 1. ∆0 is left untouched by T ∗ . Indeed, the only impact of T R on the ICs of S ER is to trigger rule (O), generating corresponding occ abducibles. However, from (§§) we know that all these abducibles are already contained in ∆0 . 2. ∆0 is T ∗ -fulfilled by construction. 3. T ∗ |E(σ) = T , because all the happened events contained in T R involve sym- bols belonging to R (σ), and are therefore ruled out by applying the projec- tion. 6 Discussion and Conclusion In this work we compare the framework SCIFF with the widely adopted LTL, from the viewpoint of the compliance verification task. To this end, we have proposed a formal notion of compliance for each one of the approaches, and defined the equivalence of the two notions. Then we provide an automatic trans- lation between LTL-based and SCIFF-based specifications. We prove that such translation preserves the notion of compliance, w.r.t. the defined equivalence. LTL-based techniques for verification have a number of strengths and weak- nesses, as well as the SCIFF framework that inherits advantages and limits of LP approaches. An important result of this work is to better clarify the links between the two techniques: this opens up to the possibility of an integrated approach based on Computational Logic, where the best of both worlds (LTL and SCIFF) can be coherently exploited. E.g., LP-based approaches support the use of variables and constraints over them, allowing to model systems where also data and data relations/constraints are taken into account. A limit of the presented approach stems from the semi-decidability issues of (refutation-based) logic programming. SCIFF inherits such characteristics: as a consequence, not any possible LTL specification could be directly reasoned about in SCIFF. From an operational viewpoint the problem can be avoided by restricting to a significant fragment of LTL, and provide ad-hoc translations for which termination is guaranteed. Alternatively, it is possible to notice that a number of applications inherently require finite traces, like e.g. business processes [23], that are developed to reach a business goal (such as delivery a product) in a finite number of steps. Automatic translation of any LTL formula within a finite trace semantics into a SCIFF corresponding model is matter of ongoing work. References 1. van der Aalst, W., de Beer, H., van Dongen, B.: Process Mining and Verification of Properties: An Approach based on Temporal Logic. In: Meersman, R., Tari, Z. (eds.) Proceedings of the OTM 2005 Confederated International Conferences CoopIS, DOA, and ODBASE. LNCS, vol. 3760, pp. 130–147. Springer (2005) 2. Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Ver- ifiable agent interaction in abductive logic programming: the SCIFF framework. ACM Transactions on Computational Logic 9(4), 29:1–29:43 (Aug 2008) 3. Alberti, M., Gavanelli, M., Lamma, E., Chesani, F., Mello, P., Montali, M.: An abductive framework for a-priori verification of web services. In: Bossi, A., Maher, M.J. (eds.) Procs. of PPDP 2006, July 10-12, 2006, Venice, Italy. pp. 39–50. ACM, New York, USA (2006) 4. Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P., Sartor, G.: Map- ping deontic operators to abductive expectations. Computational & Mathematical Organization Theory 12(2-3), 205–225 (2006) 5. Artikis, A., Sergot, M., Pitt, J.: Specifying Norm-Governed Computational Soci- eties. ACM Transactions on Computational Logic 10(1), 1–42 (2009) 6. Awad, A., Decker, G., Weske, M.: Efficient Compliance Checking Using BPMN- Q and Temporal Logic. In: Dumas, M., Reichert, M., Shan, M.C. (eds.) 6th Intl. Conf. BPM 2008. LNCS, vol. 5240, pp. 326–341. Springer (2008) 7. Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: Reasoning about interaction protocols for customizing web service selection and composition. Journal of Logic and Algebraic Programming 70(1), 53–73 (2007) 8. Chesani, F., Mello, P., Montali, M., Torroni, P.: Commitment Tracking via the Re- active Event Calculus. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009). pp. 91–96 (2009) 9. Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV. Lecture Notes in Computer Science, vol. 2404, pp. 359–364. Springer (2002) 10. Clark, K.L.: Negation as Failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press (1978) 11. De Nicola, A., Missikoff, M., Proietti, M., Smith, F.: A logic-based method for busi- ness process knowledge base management. In: Bergamaschi, S., Lodi, S., Martoglia, R., Sartori, C. (eds.) 8th Italian Symposium on Advanced Database Systems. pp. 170–181. Rimini, Italy (2010) 12. Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics. Elsevier and MIT Press (1990) 13. Fisher, M., Dixon, C., Peim, M.: Clausal Temporal Resolution. ACM Transactions on Computational Logic 2(1), 12–56 (2001) 14. Fornara, N., Colombetti, M.: Specifying artificial institutions in the event calculus. In: Dignum, V. (ed.) Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models. pp. 335–366. IGI Global (2009) 15. Holzmann, G.: The model checker spin. Software Engineering, IEEE Transactions on 23(5), 279–295 (1997) 16. Jaffar, J., Maher, M.J., Marriott, K., Stuckey, P.J.: The semantics of constraint logic programs. J. Log. Program. 37(1-3), 1–46 (1998) 17. Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive Logic Programming. Journal of Logic and Computation 2(6), 719–770 (1993) 18. Kunen, K.: Negation in logic programming. J. Log. Program. 4(4), 289–308 (1987) 19. Lloyd, J.W.: Foundations of Logic Programming. Springer, 2nd edn. (1987) 20. Montali, M.: Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach, LNBIP, vol. 56. Springer (2010) 21. Montali, M., Pesic, M., van der Aalst, W.M.P., Chesani, F., Mello, P., Storari, S.: Declarative Specification and Verification of Service Choreographies. ACM Trans- actions on the Web 4(1) (2010) 22. Montali, M., Torroni, P., Chesani, F., Mello, P., Alberti, M., Lamma, E.: Ab- ductive logic programming as an effective technology for the static verification of declarative business processes. Fundamenta Informaticae 102(3-4), 325–361 (2010) 23. Pesic, M., van der Aalst, W.M.P.: A Declarative Approach for Flexible Business Processes Management. In: Eder, J., Dustdar, S. (eds.) Procs. of the BPM 2006 Workshops. LNCS, vol. 4103, pp. 169–180. Springer (2006) 24. Pesic, M., Schonenberg, H., van der Aalst, W.M.P.: DECLARE: Full Support for Loosely-Structured Processes. In: Procs. IEEE EDOC 2007. pp. 287–300. IEEE Computer Society (2007) 25. Roman, D., Kifer, M.: Semantic Web Service Choreography: Contracting and En- actment. In: Sheth, A.P., Staab, S., Dean, M., Paolucci, M., Maynard, D., Finin, T.W., Thirunarayan, K. (eds.) Procs. ISWC 2008. LNCS, vol. 5318, pp. 550–566. Springer (2008)