=Paper= {{Paper |id=Vol-487/paper-6 |storemode=property |title=Inducing Specification of Interaction Protocols and Business Processes and Proving their Properties |pdfUrl=https://ceur-ws.org/Vol-487/paper6.pdf |volume=Vol-487 |dblpUrl=https://dblp.org/rec/conf/birthday/AlbertiGLRS08 }} ==Inducing Specification of Interaction Protocols and Business Processes and Proving their Properties== https://ceur-ws.org/Vol-487/paper6.pdf

Il Milione: A Journey in the Computational Logic in Italy

Inducing Specification of Interaction Protocols and Business
Processes and Proving their Properties
Apprendimento di specifiche di procolli di interazione e processi di
business e verica delle loro proprietà
Marco Alberti, Marco Gavanelli, Evelina Lamma, Fabrizio Riguzzi, and Sergio Storari

32
Il Milione: A Journey in the Computational Logic in Italy

SOMMARIO/ABSTRACT sentation language and empower the reasoning with new
features, such as hypothetical and non-monotonic reason-
Questo articolo descrive le nostre recenti attività di ricerca ing, or to prove properties arising from the specification
per apprendere (con tecniche di Programmazione Logica itself. Induction techniques can be also applied, to learn
Induttiva) specifiche modellate in programmazione logica (general and formal) specification from logs and exten-
e per verificare (attraverso una procedura di dimostrazione sional databases or to further abstract specifications.
abduttiva) le proprietà di sistemi cosı̀ specificati. I sistemi In this paper, we describe the recent activity carried out
realizzati qui descritti sono stati applicati rispettivamente at ENDIF, University of Ferrara (also jointly with DEIS,
per l’apprendimento e la verifica di proprietà di protocolli University of Bologna) concerning the induction of CL-
di interazione in sistemi multi-agente, servizi Web, proto- based specifications, and the proof of their properties. To
colli di screening e processi di business. this purpose, in the former activity we exploit Inductive
Logic Programming techniques (ILP for short), and the
In this paper, we overview our recent research activity DPML algorithm [12] in particular. This algorithm learns
concerning the induction of Logic Programming specifica- a specification expressed in a CL-based language from
tions, and the proof of their properties via Abductive Logic labeled traces (a database of events recording happened
Programming. Both the inductive and abductive tool here interactions or activities). The target language, named
briefly described have been applied to respectively learn SCIFF, was originally defined for the specification of in-
and verify (properties of) interaction protocols in multi- teraction protocols in the context of the UE IST-2001-
agent systems, Web service choreographies, careflows and 32530 Project, and has been later adopted to specify web
business processes. service choreographies [1], careflows [11] and business
processes [5]. A system is specified in the SCIFF lan-
Keywords: Computational logic, Induction, Abduction, guage by a knowledge base (a logic program) and a set
Interaction protocols, Careflows, Business processes. of SCIFF forward rules, called integrity constraints. Each
integrity constraint relates occurring events (in the body)
1 Introduction with an expected behaviour (typically in the head) in terms
of expectations about events. Expectations can be posi-
Thanks to its declarative semantics and its underlying tive (for mandatory events) or negative (forbidden events).
proof theory, Logic Programming, and Computational Given a SCIFF specification, the compliance of the system
Logic (CL, for short) in a broader sense, have been proved to the specifications can be checked on-the-fly through the
high-level formal languages for specification and verifica- SCIFF proof-procedure [3], that abduces the expected be-
tion. The adoption of logic for computer programming haviour and verifies its matching with the actual one.
was promoted and improved in the late seventies also The adoption of a CL-based language in specifying a
in Italy by a clever community. Logic Programming is system paved also the way to follow a proof-theoretic ap-
grounded on a purely declarative representation language, proach for proving or disproving properties of the given
and a theorem-prover or model-generator (like in Answer SCIFF specification. To this purpose, we exploit abduc-
Set Programming) as the problem-solver. The main task tion, and in particular an extension of the SCIFF proof-
of the problem-solver is the verification that an (existen- procedure called g-SCIFF [2]. g-SCIFF is an abductive
tial) query holds in the given specification. Variants of the proof-procedure which, starting from a goal, verifies, in
problem-solver can be also exploited to enrich the repre- a generative manner by abduction, whether there exists

33
Il Milione: A Journey in the Computational Logic in Italy

a scenario (i.e., a set of generated events) supporting the An example of an IC is
goal, consistent with the given integrity constraints, and
not self-contradictory (e.g., an event does not unify with H(a(bob), T ) ∧ T < 10
any forbidden one). In this case, this scenario represents → E(b(alice), T1 ) ∧ T < T1 (2)
a witness for the goal, and also corresponds to extensions ∨ EN(c(mary), T1 ) ∧ T < T1 ∧ T1 < T + 10
identified by the declarative semantics. The meaning of the IC (2) is the following: if bob has ex-
The paper is organized as follows. In Section 2 we ecuted action a at a time T < 10, then we either expect
briefly introduce the SCIFF language. In Section 3, we alice to execute action b at some time (∃T1 ) later than T or
show how learning from interpretations can be exploited we expect that mary does not execute action c at any time
to learn a SCIFF theory, and also discuss some experimen- (∀T1 ) within 9 time units after T .
tal results. In Section 4, we present g-SCIFF and discuss The interpretation of an IC is the following: if there ex-
its application to the learned specification of the previous ists a substitution of variables such that the body is true in
section. Related work is mentioned throughout the paper. an interpretation representing a trace, then one of the dis-
Finally, we conclude in section 5. juncts in the head must be true.
This work has been carried out in strict collaboration Roughly speaking, SCIFF combines occurred events
with the DEIS group. This paper is complementary to [7] with the specified rules, to suitably generate the cor-
contained in this same issue, issue, where they focus on in- responding expectations; then, expectations are verified
teraction specification and verification in several domains. against the execution trace: a positive expectation must
have a corresponding matching event, whereas a nega-
2 The SCIFF Language tive expectation forbids the presence of a matching event
into the trace. If such conditions are not met (i.e., a pos-
The SCIFF proof-procedure is an abductive proof proce- itive/negative expectation is not/is matched by a corre-
dure, able to reason about dynamically happening events, sponding event), then the expectations are violated, and the
and to generate corresponding expectations. To represent execution trace is evaluated as non-compliant.
that an event ev happened (i.e., an atomic activity has The main and original application of the SCIFF proof-
been executed) at a certain time T , SCIFF uses the sym- procedure is to verify whether an execution of the process
bol H(ev, T ), where ev is a term and T is a number indi- concretely adheres to the specification, i.e., to perform
cating the time. Hence, an execution trace is modeled as compliance checking. SCIFF is seamlessly able to check
a set of happened events, also called scenario or history compliance both at run-time, by dynamically collecting
(HAP). For example, we could formalize that bob has and reasoning upon occurring events, or a-posteriori, by
performed activity a at time 5 as follows: H(a(bob), 5). analyzing the log of an observed execution trace.
Furthermore, SCIFF introduces the concept of expecta-
tion, which plays a key role when defining global interac- 3 Inducing SCIFF specifications
tion protocols, choreographies, and more in general event-
driven processes. It is quite natural, in fact, to think of Since ICs can be seen as an extension of logical clauses, we
a process in terms of rules of the form: “if A happened, can apply the techniques developed in the learning from in-
then B is expected to happen”. Positive (resp. negative) terpretations setting of Inductive Logic Programming [13]
expectations are denoted by E(ev, T ) (resp. EN(ev, T )), to the problem of inducing ICs. In particular, in [12] we
meaning that ev is expected (resp. expected not) to happen modified the Inductive Constraint Logic (ICL) algorithm
at time T . To satisfy a positive (resp. negative) expecta- [9] that takes as input a set of interpretations labeled as
tion an execution trace must contain (resp. not contain) a positive or negative and returns a clausal theory that is true
matching happened event. in as many positive interpretations as possible and false in
SCIFF Integrity Constraints (ICs for short) are forward as many negative interpretations as possible. We called
rules of the form Body → Head: the resulting system DPML [12], for Declarative Process
Model Learner.
Body → Disj1 ∨ . . . ∨ Disjn (1) DPML modifies ICL by replacing the procedure for test-
ing the truth of a clause in an interpretation with a SCIFF-
where Body is a conjunction of happened events and liter- like procedure, by defining a generality order among ICs
als of predicates defined in a SCIFF knowledge base, and and, on the basis of this order, by defining a refinement op-
Disjj is a conjunction of expectations (positive and nega- erator. In this way, we can perform search in the space of
tive) and literals from the knowledge base. ICs and evaluate each candidate against the training set.
Variables in common to Body and Head are universally In DPML the θ-subsumption generality order among
quantified (∀) with scope the whole IC. Variables occur- clauses is modified in order to take into account the fact
ring in positive (negative) expectations in Head(C) are ex- that the head is a disjunction of conjunctions. With the
istentially (universally) quantified with scope the disjunct new generality relation, we can obtain a generalization D
where they appear. of an IC C by adding a literal to the body, adding a disjunct

34
Il Milione: A Journey in the Computational Logic in Italy

to the head, removing a literal from a disjunct in the head number of nights can be billed before check-out, during
or adding a literal to a disjunct in the head. This general- check-out or even after check-out.
ization operator is used by DPML to search the space of The SCIFF representation of the hotel model is com-
ICs from specific to general. posed of eight ICs. One of them:
The literals to be added are defined by the language bias, H(massage service(T ype, ma id(IDls )), Tls )
an intensional definition of the search space. In DPML the → E(bill massage service(ma id(IDbls )), Tbls )
∧IDls = IDbls ∧ Tbls > Tls .
language bias is a set of assertions in the form of pairs
(BS, HS), where BS is a set that contains the literals that specifies that a massage service must be followed by the
can be added to the body and HS is a set that contains the registration of the cost into the client bill.
disjuncts that can be added to the head. Five training sets have been generated by randomly
Inducing SCIFF theories is also interesting because it building a trace and then classifying it with the ICs of the
has been shown [6] that other declarative process lan- correct model. The trace is then assigned to the set of pos-
guages such as DecSerFlow [16] or ConDec [15] can be itive or negative traces depending on the result of the test.
mapped to SCIFF. Therefore, if we can ensure that the The process is repeated until 2000 positive traces and 2000
form of the learned ICs corresponds to one of the con- negative traces have been generated.
straints of these languages, we could learn such constraints DecMiner, the α-algorithm and MPM were applied to
by first learning ICs and then translating them into Dec- each training set and the learned model was tested on a
SerFlow or ConDec. By providing DPML with a language randomly generated testing set. DecMiner achieved an
bias that suitably restricts the search space of ICs, DPML average accuracy of 99.96%, higher than those of the α-
returns a theory with ICs in the desired form, that can be algorithm and MPM.
automatically translated into one of the above declarative The sets of ICs returned by DPML/DecMiner can be
process languages (see also [11]). also used to check (intensional) properties. This can be
We implemented the whole process of induction plus done by exploiting the g-SCIFF proof-procedure described
translation in the DecMiner [11] plug-in of ProM. in the following.
DecMiner assists the user in all the phases of the learn-
ing process, from the definition of the language bias, to the
labeling of traces, to the translation of the mined ICs into
4 Proving properties by g-SCIFF
ConDec constraints. The SCIFF proof-procedure addresses the important soft-
In particular, the language bias is automatically gener- ware engineering task of checking compliance during run-
ated starting from a set of general templates, one for each time (or a-posteriori using an event log), i.e., whether the
ConDec constraint, that are then instantiated to generate agents behave in a compliant manner with respect to a
specific assertions. Since the number of all possible in- given interaction protocol or specification. However, this
stantiations can be huge, DecMiner asks the user to select does not exhaust the possible uses of abductive reasoning:
a subset of activities A and a subset of ConDec constraints the event literals composing the history can be assumed as
T , and it generates only the instantiations of these con- well, in order to foresee all the possible evolutions of the
straints with the selected activities. system under test. Knowing the specification (in terms of
DPML and DecMiner have been tested on artificial and an abductive program), one could (in principle) generate
real datasets. The artificial datasets were randomly gener- all the histories that the system can support and then study
ated from three process models, namely the NetBill pro- them for common patterns or to formally prove properties
tocol [8], an electronic auction protocol [4] and a hotel of the system.
and spa process [11]. The real dataset regards the health- Of course, explicitly generating all the histories is not
care process of cervical cancer screening in the Emilia- feasible, since the number of histories compliant to a pro-
Romagna Italian region. DPML and DecMiner results tocol are typically infinite for protocols of practical use.
were compared with those of the α-algorithm [17] and of However, we can generate compliant histories in inten-
the Multi-Phase Miner (MPM) [18] that learn procedural sional way, and then reason upon them: the hypothetical
process models. events can contain variables, possibly subject to CLP con-
We now briefly discuss the methodology followed by il- straints. In order to generate compliant histories, SCIFF
lustrating the application of DecMiner to the hotel and spa has been improved and extended to a generative version,
case: the model, inspired by the example presented in [14], called g-SCIFF. g-SCIFF considers H literals as ab-
describes a simple process of renting rooms and services ducibles, and contains a new transition, called fulfillment,
in a hotel and spa. After registering at the front desk, the that fulfils the expectations by abducing matching events:
client can request one or more rooms, laundry and massage
services. Each service, identified by a code, is followed E(X, T ) → H(X, T ).
by the registration of the service costs into the client bill.
Moreover, if the client chooses a “Shiatzu” massage, the g-SCIFF is provably sound: all generated histories fulfil
spa presents her/him a special offer. The cost related to the the given specifications.

35
Il Milione: A Journey in the Computational Logic in Italy

In the literature, properties are often classified as safety graphical languages. Finally, the abductive g-SCIFF proof
or liveness properties. A safety property is a universal procedure can be used for proving properties of specifica-
property: intuitively, it ensures that nothing bad will ever tions, either learned or provided by the user.
happen (whenever the protocol/specification is respected).
A liveness property is, instead, existential: it ensures that Acknowledgements
something good will eventually happen. A liveness prop-
erty can be passed to g-SCIFF as a goal containing positive We are in debt with the Artificial Intelligence group at
expectations: if the g-SCIFF proof-procedure succeeds in DEIS, University of Bologna who shared with us most of
proving the goal, the generated history witnesses that there the activity here reported.
exists a way to obtain the goal while being conformant to
the protocol. A safety property φ can be negated (as in REFERENCES
model checking), and then passed to g-SCIFF as a goal [1] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and
G ≡ ¬φ. If the g-SCIFF proof-procedure succeeds in M. Montali. An abductive framework for a-priori verification of
finding a history HAP (i.e., |=HAP ¬φ), we have a coun- web services. In PPDP 2006, pages 39–50. ACM Press, 2006.
terexample: the history HAP satisfies the protocol and [2] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and
does not enjoy the safety property φ. P. Torroni. Security protocols verification in abductive logic pro-
gramming: a case study. In ESAW 2005, pages 283–295, 2005.
The g-SCIFF proof-procedure is implemented in SICS-
[3] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and
tus 4, making extensive use of Constraint Handling Rules P. Torroni. Verifiable agent interaction in abductive logic program-
[10] to implement its transitions. SCIFF and g-SCIFF ming: the SCIFF framework. ACM Transactions on Computational
come in a same package, that can be freely downloaded Logics, 9(4), 2008. Accepted for publication.
from the web1 : the g-SCIFF behaviour is activated by sim- [4] A. Chavez and P. Maes. Kasbah: An agent marketplace for buying
ply setting an option. and selling goods. In PAAM 1996, pages 75–90, London, 1996.
The g-SCIFF proof-procedure has been applied to [5] F. Chesani, P. Mello, M. Montali, and S. Storari. Testing careflow
process execution conformance by translating a graphical language
the formal verification of various systems and proto-
to computational logic. In Proc. of the 11th Conference on Artificial
cols. g-SCIFF was able to derive the flawedness of the Intelligence in Medicine (AIME 07), number 4594 in LNAI, 2007.
Needham-Schroeder security protocol [2], and the good [6] F. Chesani, P. Mello, M. Montali, and S. Storari. Towards a DecSer-
atomicity property of the NetBill protocol [2]. It is also Flow declarative semantics based on computational logic. Technical
a basic component of the Al LoWS framework [1], for the Report DEIS-LIA-07-002, University of Bologna, 2007.
proof of interoperability between Web services. [7] F. Chesani, P. Mello, M. Montali, and P. Torroni. Modeling and
The g-SCIFF proof-procedure operates top-down in a verification of business processes and choreographies in ALP. In-
deductive and abductive manner, by manipulating the spec- telligenza Artificiale. In this issue.
ification driven by the goal, as usual in Logic Program- [8] B. Cox, J.C. Tygar, and M. Sirbu. NetBill security and transaction
ming, and also generating expectations as SCIFF does and, protocol. In 1st USENIX Workshop on Electronic Commerce, 1995.
by fulfillment an (intensional) set of events needed to sup- [9] L. De Raedt and W. Van Laer. Inductive constraint logic. In ALT
port the goal. This way, g-SCIFF can be used to prove 1995, volume 997 of LNAI, 1995.
properties of any SCIFF protocol. For example, one may
wonder if the protocol allows a massage service not to be [10] T. Frühwirth. Theory and practice of constraint handling rules. J.
followed by a shiatzu package offer. By expressing this of Logic Prog., 37(1-3):95–138, 1998.
combination as a g-SCIFF query, the user can ask g-SCIFF [11] E. Lamma, P. Mello, M. Montali, F. Riguzzi, and S. Storari. In-
to generate an intensional history that satisfies the query ducing declarative logic-based models from labeled traces. In BPM
while fulfilling the protocol. In fact, g-SCIFF generates 2007, volume 4714 of LNCS, 2007.
such a history, with the constraint that the massage type [12] E. Lamma, P. Mello, F. Riguzzi, and S. Storari. Applying inductive
must not be shiatzu: logic programming to process mining. In ILP 2007, volume 4894
H(register client data, B), of LNAI, 2007.
H(massage service(type(T ), ma id(A)), H), T 6= shiatzu [13] S. Muggleton and L. De Raedt. Inductive logic programming: The-
H(bill nights, Y ), ory and methods. J. Logic Prog., 19/20:629–679, 1994.
H(bill massage service(ma id(A)), E), [14] M. Pesic, H. Schonenberg, and W.M.P. van der Aalst. Declare: Full
support for loosely-structured processes. In EDOC 2007, pages
H(charge, D),
287–300. IEEE Computer Society, 2007.
H(complete check out, F ),
[15] W.M.P. van der Aalst and M. Pesic. A declarative approach for
flexible business processes management. In BPM 2006, volume
5 Conclusions 4103 of LNCS, 2006.
[16] W.M.P. van der Aalst and M. Pesic. DecSerFlow: Towards a truly
We have presented the CL-based language SCIFF for the declarative service flow language. In WS-FM 2006, volume 4184 of
specifications of complex systems with interacting entities, LNCS, 2006.
such as multi-agent systems, business processes or web [17] W.M.P. van der Aalst, T. Weijters, and L. Maruster. Workflow min-
ing: Discovering process models from event logs. IEEE Trans.
services. Moreover, we have discussed how techniques Knowl. Data Eng., 16(9):1128–1142, 2004.
from Inductive Logic Programming were applied for in- [18] B. F. van Dongen and W. M. P. van der Aalst. Multi-phase process
ducing SCIFF theories which can be then translated into mining: Building instance graphs. In ER 2004, volume 3288 of
1 http://lia.deis.unibo.it/sciff/ LNCS, pages 362–376, 2004.

36
Il Milione: A Journey in the Computational Logic in Italy

Contacts
Marco Alberti, marco.alberti@unife.it
Marco Gavanelli, marco.gavanelli@unife.it
Evelina Lamma, evelina.lamma@unife.it
Fabrizio Riguzzi, fabrizio.riguzzi@unife.it
Sergio Storari, sergio.storari@unife.it

tutti affiliati al

Dipartimento di Ingegneria,
Università di Ferrara
Via Saragat, 1
44100 Ferrara