Questo articolo introduce brevemente le nostre recenti attivita` di ricerca in relazione all’uso della programmazione logica per la specifica e verifica delle interazioni in vari contesti. L’articolo evidenzia alcuni risultati riportati in vari ambiti: sistemi multi-agente, servizi web e argomentazione, con particolare enfasi sugli aspetti collegati ai processi di business e alle coreografie di servizi Web. In this article we overview our recent research activity concerning the use of logic programming for interaction specification and verification in several domains. We outline relevant results in the areas of multi-agent systems, argumentation and web services, and we devote a special emphasis to issues related to business processes and Web service choreographies. 1
Over two decades ago, a significant part of the Italian and European CS research community and IT industry expressed great interest in the new Logic Programming (LP) paradigm. Such an interest was sensibly encouraged by the pioneering work of Giorgio Levi, Franco Turini, Ugo Montanari, Alberto Martelli, and others. The Artificial Intelligence group of DEIS, School of Engineering, University of Bologna, was born at the time of the LP wave of the Eighties. Our group was attracted by the unique features of LP, including its ability to marry formal and practical aspects, and to enable the correspondence of a declarative language with an underlying execution model.
The main research directions of our group back then were centered around distribution, modularity, parallelism, and language extensions such as Constraint and Abductive Logic Programming. In order to enable programming in the large in the LP paradigm, two approaches have been studied for structuring logic programs: an algebraic method based on meta-operators, and another approach based on language extensions. The first model brought to the definition of an extended LP language called StructuredProlog [16], while the second approach was based on the introduction of negation in LP, to support nonmonotonic reasoning.
StructuredProlog allows to to integrate blocks, modules, hypothetical reasoning, logical theory and object taxonomies. It has been implemented as an extension of the Warren Abstract Machine, via software emulation and then in hardware, and optimized using partial evaluation techniques. Past research also focussed on parallel logic languages with AND parallelism and no variable sharing on a MIMD architecture. Inter-process communication and synchronization was possible via multi-headed clauses and a shared blackboard, and an optimized unification mechanism specifically tailored to serve the purpose. Finally, the LP paradigm has been integrated with the OO paradigm, to define the Distributed Logic Objects language (DLO). In DLO, methods are expressed via multi-headed clauses, in a purely declarative style, while specific constructs are defined to express interaction among objects and inheritance. 2
Since 2001, the group has devoted most of its resources
to the study of computational logic-based multi-agent
systems [19], specifically agent interaction: the aim was to
develop an LP-based language and an operational model for
the specification and verification of agent interaction
protocols. Such work has been carried out in the context of
the EU-funded SOCS project 1 . The SOCS society model
1Project IST-2001-32530, 5FP. SOCS stands for “Societies Of
ComputeeS: a computational logic model for the description, analysis and
ver[
Expectations, whose intuition recalls the usual deontic
operators of permission, obligation, and prohibition [8],
are used to provide a semantics to both agent
communication languages and to interaction protocols [
The society model and the SCIFF operational model
were satisfactorily tested on a number of applications.
These include resource exchange [11], e-commerce
protocols [7], and combinatorial auctions [
The SOCS-SI tool [
Most of our current research has originated from the outcomes of SOCS. Starting form the many analogies between the agent paradigm and the Web service model, interaction protocols and choreographies has been the subject of ification of global and open societies of heterogeneous computees.” The project run for 42 months, from January 2001 until June 2005, and it involved 6 academic institutions, including the University of Bologna and the University of Ferrara. See [12, 23].
2http://lia.deis.unibo.it/research/socs_si and http://lia.deis.unibo.it/research/sciff conspicuous research carried out in the context of two recent national projects lead by Alberto Martelli 3 . Part of the research activity done within these projects has built on SCIFF to i) produce new formalisms for the specification and verification of interaction protocols and choreographies; and to ii) develop new techniques for automatic property verification and reasoning about Web Services.
The translation of graphical modeling languages into the formal languages developed in these projects has been also subject of research. Our group has studied the translation of choreographies (represented in WS-CDL or in BPMN) into its corresponding SCIFF specification, focussing on verification of compliance. Several tools, based on the SCIFF procedure, have been developed to cope with complete logs and with run-time events. Further supported types of verification regard the proof of “high level” properties, such as verifying in an e-commerce scenario, that a buyer is guaranteed to receive the good he/she paid for, and the seller is guaranteed to be paid.
Alongside our research on Web Services, we have
extended and applied SCIFF in the context of agent-oriented
requirements engineering. This has brought to the
development of B-Tropos (B standing for Business): a unified
framework for information systems engineering, with the
aim to reconcile requirements elicitation with declarative
specification, prototyping, and analysis [15]. B-Tropos,
built on the well-known Tropos methodology [14], lets
the user to express temporal and data constraints between
tasks, hence introducing also the concepts of start and
completion times, triggering events, and deadlines. The
verification capabilities supported by the SCIFF proof allow
prototyping (animation) and analysis (properties and
conformance verification) directly in B-Tropos. Early
requirements engineers will be able to test their models directly;
engineers testing model properties will not have to resort
to ad-hoc, error-prone translations of high-level models
into other languages, thanks to the automatic translation of
B-Tropos models into SCIFF programs; finally, managers
monitoring the correct behavior of a system will exploit
the SCIFF specification to check the compliance using the
SOCS-SI runtime and off-line checking facilities [
Another current research direction which builds on SCIFF concerns argumentation in the Semantic Web [24]. Our work resulted in the development of an operational argumentation framework, called ArgSCIFF, to support dialogic argument exchange between Semantic Web Services. In ArgSCIFF, an intelligent agent can interact with a Web Service and reason from the interaction result. The reasoning semantics is an argumentation semantics that views the interaction as a dialogue. The dialogue lets two parties exchange arguments and attack, challenge, and justify them 3In 2004-2005, our group has been involved as a partner in the National MIUR (ex 40%) project on ”Development and verification of logicbased multi-agent systems,” and in 2006-2007 on the National PRIN (ex 40%) project on “Specification and verification of agent interaction protocols.” For more information, see the project Web site [20]. A report on the most recent project is due to appear on this magazine [13]. on the basis of their knowledge. This format has the potential to overcome a well-known barrier to human users adoption of IT solutions because it permits interaction that includes justified answers that can be reasoned about and rebutted. 4
Actually, a great deal of our resources are devoted to the
development of LP-based techniques for modeling and
verifying business processes and choreographies. The
reference framework for this work is called CLIMB 4 .
As specification language, CLIMB adopts an extension
of DecSerFlow/Condec, a family of graphical languages
for the declarative specification of service/business flows
[
In particular, CLIMB exploits SCIFF for carrying out both run-time and a-priori verification tasks.
At run-time, SCIFF can be used as an alerting
infrastructure capable to perform compliance checking, i.e.,
verifying whether a concrete process execution (or service
interaction) complies with the prescribed model (and
detecting violations as soon as possible). Such a
verification can be seamlessly applied a-posteriori as well,
checking already completed execution traces. In this respect,
CLIMB rules are used as an intuitive classification
criterion which split analyzed traces into a compliant and non
compliant sub-sets; a plug-in which exploits such a
reasoning technique has been implemented and integrated inside
the ProM[
At static time, the “generative” variant of the SCIFF proof procedure can be exploited to check the consistency of developed models, by detecting the presence of conflicts (which undermine the possibility of executing the model) and by discovering if they contain dead activities (i.e., activities that can be never executed). Such verifications constitute the basis also for determining if different CLIMB models can be composed without introducing conflicts. This is particularly important in a service-oriented setting, where a choreography can be intended as a contract aiming 4CLIMB stands for “Computational Logic for the verIfication and Modeling of Business processes and choreographies.” For more information and up-to-date resources the interested reader can refer to the CLIMB Web site [18]. to make different partners correctly collaborate, and then a set of compatible concrete services implementation must be found to concretely implement the system.
It is worth noting that DecSerFlow/Condec models have an alternative underlying semantics in terms of Linear Temporal Logic formulas, which enable the possibility to apply model checking techniques in order to verify the designed models. In this respect, a research activity focused on more foundational aspects is being carried out, to compare expressivity, complexity and reasoning capabilities of the two frameworks.
Much of the work presented here has been done in tight cooperation with the AI group of the University of Ferrara. This paper is complementary to [12], where they focus on the learning and property verification issues in relation with the work carried out within and following SOCS. [15] V. Bryl, P. Mello, M. Montali, P. Torroni, and N. Zannone. B-tropos: Agent-oriented requirements engineering meets computational logic for declarative business process modeling and verification. In Computational Logic in Multi-Agent Systems VIII, LNAI.
Springer-Verlag, 2008. [18] CLIMB: Computational logic for the verification and modeling of business processes and choreographies, 2008. http://lia.deis.unibo.it/ research/climb. [20] MASSiVE: sviluppo e verifica di sistemi multiagente basati sulla logica. http://www.di. unito.it/massive. [22] Societies Of ComputeeS (SOCS): a computational logic model for the description, analysis and verification of global and open societies of heterogeneous computees. IST-2001-32530, 2002-2005. http:// lia.deis.unibo.it/research/socs. [23] F. Toni. Multi-agent systems in computational logic: Challenges and outcomes of the SOCS project. In Computational Logic in Multi-Agent Systems VI, volume 3900 of LNAI, pages 420–426. Springer-Verlag, 2006. [24] P. Torroni, M. Gavanelli, and F. Chesani. Argumentation in the semantic web. IEEE Intelligent Systems, 22(6):66–74, Nov/Dec 2007.