The compliance veri cation task amounts to establishing if the execution of a system, given in terms of observed events, does respect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to assess 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 de ne a notion of compliance within each approach, and then we show that an arbitrary LTL formula can be expressed in SCIFF, by providing an automatic translation procedure from LTL to SCIFF which preserves compliance.
Linear Temporal Logic (LTL) [
In these domains, a relevant task is to assess compliance, usually de ned as
checking if an implementation faithfully meets the requirements of a speci
cation. The LTL models correspond to linear Kripke structures representing the
execution traces (i.e., sequences of events) occurred during a speci c
instantiation of the system, while entailment becomes a compliance evaluator w.r.t. a
regulatory speci cation expressed as an LTL formula. Such approach has been
used, for example, in [
Recently, Logic Programming (LP) based approaches have been applied for
speci cation and veri cation of normative systems [
In [
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 [
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
interested reader can refer to [
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 ; ) [
De nition 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 speci cally, a proposition e 2 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.
(representing possible events), an LTL execution trace TL is an LTL model having (N; <) as time structure and E as the set of atomic propositions. In particular, TL = (N; <; vocc), where vocc : E ! 2N is a valuation function mapping each event e 2 E to the set of all time instants i 2 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 fe 2 E j i 2 vocc(e)g. 2.1
LTL formulae are de ned by using (i) atomic propositions, i.e., events, together with the two special constants true and f alse; (ii) classical propositional connectives, i.e., :, ^, _ and ); (iii) temporal operators, i.e., (next time), U (until), (eventually), (globally) and W (weak until). An LTL formula is recursively de ned as: each event e 2 E is a formula; if ' and are formulae, then :', ' ^ , , and 'U are formulae. Other LTL formulae can be de ned as abbreviations: { ' _ , :(:' ^ : ) and ' ) , :' _ ; { true , :' _ ' and f alse , :true; { ' , trueU ', ' , : :' and W' , U ' _ . 2.2
The semantics of LTL is given w.r.t. an LTL execution trace, and w.r.t. a speci c state. We will use j=L to denote the logical entailment in the LTL setting. M; i j=L ' means that ' is true at time i in model M. j=L is de ned by induction on the structure of the formulae4: (TL j=L ') i (TL; 0 j=L '); (TL; i j=L e) i e 2 TL(i) (i.e., i 2 vocc(e)); (TL; i 6j=L e) i e 62 TL(i); (TL; i j=L :') i (TL; i 6j=L '); (TL; i j=L ' ^ ) i (TL; i j=L ') and (TL; i j=L (TL; i j=L ' _ ) i (TL; i j=L ') or (TL; i j=L ); (TL; i j=L ' ) ) i (TL; i 6j=L ') or (TL; i j=L ); (TL; i j=L ') i (TL; i + 1 j=L '); (TL; i j=L U ') i 9k i s.t. (TL; k j=L ') and 8i (TL; i j=L ') i 9j i s.t. (TL; j j=L '); (TL; i j=L ') i 8j i (TL; j j=L '); ); j < k (TL; j j=L ); 4 For the sake of readability, we explicitly show the semantics of , their meaning can be obtained from the semantics of U and . and W, even if (TL; i j=L
W') i either (TL; i j=L
U ') or (TL; i j=L ).
When LTL is employed to formalize compliance rules, the declarative semantics selects those events that must be contained (or avoided) in certain states so as to ful l them, separating compliant traces from non-compliant ones. In this respect, j=L plays the role of a compliance evaluator.
formula ' if and only if TL entails ':
cmpLTL(TL; ') , TL j=L ':
When LTL formulae are used to express business constraints/rules of a
regulatory model, as for example in the ConDec language [
In the following we will brie y recap the main features of the SCIFF framework.
The interested reader can refer to [
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 De nition 6).
Three special predicates are used to model happened events and positive/negative 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.
simply a SCIFF trace) is a set of positive ground H(E; T ) atoms.
A speci c execution of the system under study is called an instance, and it is formally identi ed by the SCIFF speci cation modeling the system and by the execution trace produced during the instance execution.
De nition 5 (SCIFF Instance). Given a SCIFF speci cation 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 conjunction of happened events, general abducibles, and de ned predicates, while head contains a disjunction of conjunctions of expectations, general abducibles, and de ned predicates. When the body is matched with events and abducibles, the IC is triggered, and expectations occurring in the head are assumed (abduced).
a set A is an abductive explanation for hS; T i if and only if
Comp (KB [ T [
) [ CET [TX j= IC
where Comp is the (two-valued) completion of a theory [
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 re exivity, symmetry and transitivity for equality. Fixing a CLP theory corresponds to instantiate the parameter X and the set of allowed constraints. Therefore, di erent structures can be chosen without a ecting the notion of SCIFF's abductive explanation. We will instantiate such a parameter to N, with linear equations and dis-equations. The theory of constraints TN de nes the symbols +; ; ; =; =; >; <; ; : : : with the usual meanings (e.g., 1 < 2 + 2 is evaluated to true).
Remark 1 (Abductive explanations and sub-speci cations). If is an abductive explanation for hS; T i, then is an abductive explanation also for hS0 = hKB; A; IC0i; T i, where IC0 IC.
Being able to generate hypotheses might not be enough: in speci c domains like, e.g., legal reasoning, a further step of veri cation of the hypotheses against the observed events (available data) is mandatory. Hence, the SCIFF framework provides also an hypotheses-con rmation mechanism, based on the formal notions of ful llment and violation. First of all, expectations must be E-consistent : the same event cannot be expected and prohibited at the same time.
event e and for each time t it holds that fE(e; t); EN(e; t)g * The relationship between expectations and happened events is instead captured by the notions of ful llment and violation.
De nition 8 (T -Ful llment). Given a SCIFF trace T and an abducible set , is T -ful lled i for each event e and for each time t: E(e; t) 2 ! H(e; t) 2 T and EN(e; t) 2 ! H(e; t) 2= T De nition 9 (T -Violation). Given a SCIFF trace T and an abducible set , is T -violated i it exists at least one event e and time t such that: E(e; t) 2 ^ H(e; t) 2= T , or EN(e; t) 2 ^ H(e; t) 2 T Given an abductive explanation , ful llment acts as a classi er that separates the legal/correct execution traces with respect to from the wrong ones. De nition 10 (Compliance in SCIFF). A trace T is compliant with a SCIFF speci cation S if and only if there exists an abducible set such that: 1. 2. 3.
is an abductive explanation for hS; T i; is E-consistent; is T -ful lled.
If this is the case, we write cmpSCIFF (T ; S) or simply cmpSCIFF (T ; S). 4
LTL and SCIFF rely on di erent 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). De nition 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 corresponding SCIFF event H(e; i), where e 2 E and i 2 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 2 E and for each i 2 vocc(e): tm(TL) =
H(e; i)je 2 E ; i 2 vocc(e) Example 1. Let us consider an LTL execution trace TL = (N; <; vocc), where E = fa; b; c; d g is the set of propositional events and vocc is de ned as follows: vocc(a) = f0; 1g vocc(b) = f2g vocc(c) = f3g 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 speci cation: 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 speci cations are behaviorally equivalent.
speci cation S and an LTL formula ' are behaviorally equivalent w.r.t. complic ance (' ! S) if and only if for each LTL trace TL it holds that: cmpLTL (TL; ') () cmpSCIFF (tm (TL) ; S) : We might notice that De nition 12 does not pose any constraint on the SCIFF speci cation S: indeed, only the trace TL is somehow constrained by the application of the mapping function tm. 5
We show now that an arbitrary LTL formula can be expressed in SCIFF by providing 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
Fisher and colleagues [
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 represent activities/events, and those used for renaming.
De nition 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 (') = fpay; send receiptg. The SNF translation of ' is: = snf [:send receipt W pay] = 8 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 ( ) = fstart; x; y; trueg. 5.2
We now provide a syntactic procedure which translates an arbitrary SNF formula to SCIFF, and prove that such a translation preserves compliance. De nition 16 (IC-mapping). An IC-mapping icm is a function which translates an SNF formula to a set of SCIFF integrity constraints, de ned 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 " icm ^ ka =) a " _ ld d !# !# , ^ icm [ka; T ] ! _ (icm [ld; T2] ^ T2 = T + 1) :
a d 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.
De nition 17 (S-mapping sm). Given an SNF formula ' and a set V P (') of proposition symbols, the S-mapping sm translates ' to a SCIFF speci cation depending on V . sm is de ned as: sm :
'; V 7 ! h;; fE=2; EN=2; true=1; occ=2; not occ=2g; IC)i where
IC = icm(') [ f true ! occ(start; 0): true ! true(0): (S) (T1) true(T ) ! true(T2) ^ T2 = T + 1: (T2) 8p 2 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 2 V ! occ(X; T ): (O) occ(X; T ) ^ X 2 V ! E(X; T ): (E1) not occ(X; T ) ^ X 2 V ! EN(X; T ): g (E2) S-mapping applies IC-mapping and then augments the obtained constraints with further general rules. Such rules capture speci c 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 speci cation.
and the SCIFF speci cation S = sm [ ; P ( )], it holds that !c S. Proof. Since LTL and SCIFF share the same semantics for logical symbols AND(^), OR (_), and implication() in LTL and ! in SCIFF), we will focus 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 2 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 considering 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 rst 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 nd an execution trace TL which is compliant with , but whose corresponding trace T is not compliant with S = sm [ ; P ( )]. Notice that, by De nition 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) 62 T . By applying the tm 1 function on this trace, one obtains a TL which obeys the following properties: (1) k 2 TL(t), and (2) l 62 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 di erence 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: 8 t; a 2 TL(t) _ b 2 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 rst, 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 ful lled. 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 8 t; H(a; t) 2 T _ H(b; t + 1) 2 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 discussion made for the previous LTL-clause. The only di erence 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 speci cation if all the integrity constraints are respected. 5.3
We now demonstrate that also an arbitrary LTL formula can be encoded in SCIFF preserving compliance. The main technical problem is that the SNF translation 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 speci cation produced by applying in cascade the SNF and the sm translation does not preserve compliance 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 rst step is therefore to de ne, in both settings, a suitable trace projection, which lters an execution trace by maintaining only certain symbols (in particular, the ones which correspond to events).
and a set V of predicate symbols, the trace projection of T on V (T jV ) is the subset of T containing only events taken from V :
T jV , fH(e; t) j H(e; t) 2 T ^ e 2 V g De nition 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 (TLjV ) is the projection of TL containing only events taken from V : TLjV = (N; <; vocc0) s.t. vocc0(e) , ; vocc(e) if e 2 V ; otherwise:
ping). For each LTL execution trace TL and for each set of proposition symbols V
tm [TLjV ] = tm [TL] jV Proof. From the de nitions of trace mapping (Def. 11) and of trace projection (Def. 18 and 19).
We now brie y recall one of the main results presented in [
is able i snf(') is satis able.
[
8 TL cmpLTL (TL; snf [']) =) cmpLTL TLjE(snf[']); ' 8 TL cmpLTL (TL; ') =) 9TL0 s:t: TL = TL0 jE(snf[']) ^ cmpLTL (TL0 ; snf [']) where we remember that (by De nition 15) E (snf [']) = P ('). With such preliminaries, it is possible to prove that each LTL formula is translatable to a SCIFF speci cation, preserving compliance.
and the SCIFF speci cation S = sm [snf ['] ; P (')], it holds that S !c '. 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
8TL; cmpLTL(TL; ') () cmpSCIFF (tm [TL]; sm [ ; E( )]) We will prove rstly 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:
( ) 8 TL; cmpLTL(TL; ') ========) cmpSCIFF (tm [TL]; sm [ ; E ( )]) wwwwwwLemma 2 wwwww~(y) ww
Theorem 1 w 9TL0 ; TL = TL0 jE( ) =========) cmpSCIFF (tm [TL0 ]; sm [ ; P ( )])
^cmpLTL(TL0 ; ) The schema shows that proving ( ) reduces to prove (y), i.e., we prove that cmpSCIFF (tm [TL0 ]; sm [ ; P ( )]) =) cmpSCIFF tm TL0 jE( ) ; sm [ ; E ( )] By taking into account abducible sets, Def. 15 and Lemma 1, (y) becomes: cmpSCIFF
T ; SER =) cmpSCIFF 0
T jE( ); SE (y) (z) where SER = sm [ ; E ( ) [ R ( )], SE = sm [ ; E ( )] and T = tm [TL0 ]. To prove (z), we demonstrate that 0 =
n fE(e; t)je 2 R ( )g n fEN(e; t)je 2 R ( )g obeys the three properties required by the De nition 10 of SCIFF compliance: and SER is that, for the rst speci cation, 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 explanation for SE 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. 0 is E-consistent, because 0 and is E-consistent.
0 is T jE( )-ful lled. Since T jE( ) is a projection of T , 0 and is T -ful lled, no negative expectation in 0 can be violated by T jE( ). Positive expectations concerning elements in E ( ) are maintained in 0, and so are the corresponding happened events after the trace projection. Positive expectations 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 a ect ful llment. ((=) 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 ] ; ' ~ w w wwLemma 2, then Lemma 1 w w w cmpLTL tm 1 [T 0] ;
Theorem 1 (===========
( ) (========== 8 T ; cmpSCIFF (T ; sm [ ; E( )]) w w w www(x) 9 T 0; T = T 0jE( ) ^cmpSCIFF (T 0; sm [ ; P ( )]) The schema shows that proving ( ) reduces to prove (x), i.e. we prove that 8 T ; cmpSCIFF
T ; SE =) 9 T 0; T = T 0jE( ) ^ cmpSCIFF 0 T 0; SER (x) where SER = sm [ ; E( ) [ R ( )] and SE = sm [ ; E( )].
First of all, it is worth noting that SER extends SE 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 SER by extending with the new generated expectations: 0 = [ RE [ REN, where RE and REN respectively represent the inserted positive and negative expectations.
0 is E-consistent. Indeed, since RE and REN contain only expectations generated by rules (E1) and (E2), by construction we have:
8 E(a; t); E(a; t) 2 RE ) occ(a; t) 2 0 8 EN(a; t); EN(a; t) 2 REN ) not occ(a; t) 2 0 (xx) Let us suppose by absurdum that there exist a, t (with a 2 R ( )) s.t. E(a; t) 2
RE and EN(a; t) 2 REN. In this case, (xx) would state that occ(a; t) 2 0 and not occ(a; t) 2 0. This would violate rule (C), making impossible that 0 is an abductive explanation.
An execution trace T compliant with SER can be therefore built as follows: T
= T [ T R , where H(a; t) 2 T R , E(a; t) 2 RE Under this choice: 1. 0 is left untouched by T . Indeed, the only impact of T R on the ICs of SER is to trigger rule (O), generating corresponding occ abducibles. However, from (xx) we know that all these abducibles are already contained in 0. 2. 0 is T -ful lled by construction. 3. T jE( ) = T , because all the happened events contained in T R involve symbols belonging to R ( ), and are therefore ruled out by applying the projection.
In this work we compare the framework SCIFF with the widely adopted LTL, from the viewpoint of the compliance veri cation task. To this end, we have proposed a formal notion of compliance for each one of the approaches, and de ned the equivalence of the two notions. Then we provide an automatic translation between LTL-based and SCIFF-based speci cations. We prove that such translation preserves the notion of compliance, w.r.t. the de ned equivalence.
LTL-based techniques for veri cation have a number of strengths and weaknesses, 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 speci cation could be directly reasoned
about in SCIFF. From an operational viewpoint the problem can be avoided
by restricting to a signi cant 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 nite traces, like e.g. business processes
[