=Paper=
{{Paper
|id=Vol-1459/paper8
|storemode=property
|title=Evaluating compliance: from LTL to abductive logic programming
|pdfUrl=https://ceur-ws.org/Vol-1459/paper8.pdf
|volume=Vol-1459
|dblpUrl=https://dblp.org/rec/conf/cilc/MontaliCGLM15
}}
==Evaluating compliance: from LTL to abductive logic programming==
https://ceur-ws.org/Vol-1459/paper8.pdf
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)