Il Milione: A Journey in the Computational Logic in Italy Computational Logic in Genova Logica Computazionale a Genova Viviana Mascardi, Giorgio Delzanno, Maurizio Martelli DISI, Università degli Studi di Genova, Via Dodecaneso 35, 16146, Genova, Italy E-mail: {viviana.mascardi,giorgio.delzanno, maurizio.martelli}@unige.it 38 Il Milione: A Journey in the Computational Logic in Italy SOMMARIO/ABSTRACT are often multiagent systems, for which we propose mod- elling languages as well as prototyping environments and La Logica Computazionale gioca un ruolo molto rilevante verification techniques. Also, we use temporal logic both nella ingegnerizzazione di sistemi complessi: può essere for modelling cooperative BDI agents and for verifying usata per specificare sistemi al livello di astrazione più op- infinite-state processes. portuno, la specifica può essere eseguita fornendo gratuita- In this paper, we describe the activities that we carried mente un prototipo funzionante e, grazie alla sua semantica out in the recent years in each research line. ben fondata, può essere usata per verificare formalmente proprietà di programmi e sistemi, cosa fondamentale nello Keywords: Computational Logic, Intelligent Agents, sviluppo di applicazioni critiche dal punto di vista della si- Rapid Prototyping, Verification of Protocols. curezza. Nell’ultimo decennio, il Gruppo di Programmazione Logic Languages for Modelling Rational Agents Logica del Dipartimento di Informatica e Scienze dell’Informazione (DISI) dell’Università degli Studi di Many logics for modelling beliefs, desires and inten- Genova ha applicato la Logica Computazionale per model- tions of agents, such as Rao and Georgeff’s BDI logic lare, prototipare e verificare sistemi complessi. Le tre linee [36, 34, 35] and Wooldridge’s LORA [40], are based di ricerca hanno ampie aree di sovrapposizione: i sistemi on temporal logics like CTL/CTL∗ (Computational Tree complessi che prendiamo in considerazione sono spesso Logic, [24, 17]) where the structure of time is branching sistemi multiagente per i quali proponiamo linguaggi di in the future and linear in the past. In 2005 we started to modellazione, ambienti di prototipazione e tecniche di ver- explore the advantages of substituting ATL∗ (Alternating- ifica. Inoltre usiamo la logica temporale sia per modellare Time Temporal Logic [1]) to CTL∗ in Rao and Georgeff’s agenti BDI cooperativi, sia per verificare processi a stati logic. This activity, resulted into the formalization of infiniti. BDIAT L [33], was born from our effort to find a BDI logic In questo articolo descriviamo le attività condotte suitable for modelling the behaviour of agents structured recentemente in ciascuna direzione di ricerca. according to the CooBDI architecture [2]. A CooBDI agent, whose behavioral specification was Computational Logic plays a very relevant role in engi- given using Prolog, is characterised by a built-in mech- neering complex systems: it can be used to specify systems anism for retrieving plans from cooperative agents, for at the right level of abstraction, the specifications can be example when no local plans suitable for achieving a executed, thus providing a working prototype for free, and certain desire are available. In particular, the coopera- thanks to its well-founded semantics it can be used to for- tion strategy of an agent includes the set of agents with mally verify properties of programs, which is fundamental which is expected to cooperate (its partner agents, or its when safety critical applications are developed. “friends”). BDIAT L allows us to express new commit- In the last decade, the Logic Programming Group at the ment strategies that are more realistic than those proposed Department of Computer and Information Science (DISI) by Rao and Georgeff (and that could not be defined in their of Genova University has been applying Computational logic), since they take collaboration among agents into ac- Logic for modelling, prototyping, and verifying complex count. In particular, we can express three variants of Rao systems. These three research lines are largely overlap- and Georgeff’s “open minded” commitment: “independent ping: the complex systems we take under consideration open minded”, “optimistic open minded”, and “pessimistic 39 Il Milione: A Journey in the Computational Logic in Italy open minded”. In these commitment strategies we exploit The work described in [37] deals with an electronic im- the new feature that ATL∗ adds to CTL∗ , namely coopera- plementation of different auction mechanisms. There are tion modalities, to express the way of thinking of CooBDI many different auction mechanisms that can be classified agents. according to their features [29]. We ran experiments with Other logic-based languages conceived for specifying all the implemented mechanisms under the hypotheses, BDI-style and, more in general, rational agents, are Con- that, according to the “Revenue Equivalence Theorem” goLog [27], AGENT-0 [38], Concurrent METATEM [25], (RET [39]), lead to the existence of an optimal bidder’s Ehhf [20], the IMPACT language [23], and “Dynamics in strategy. The experiments demonstrated that RET is satis- Logic” [10]. In 2004, we published a survey of these six fied (up to some error due to discretisation), giving empir- languages [32], chosen because of the availability, for each ical evidence of the correctness of the implementation. of them, of a working interpreter or an automatic mech- Many applications had also been developed using the anism for animating specifications. In our survey we de- ancestor of DCaseLP, CaseLP: a prototype of a multime- scribed the logic foundations of each language and we gave dia, multichannel, personalised news provider, [19], was an example of use. A comparison along twelve dimensions developed in collaboration with Ksolutions s.p.a. as part of (purpose of use, language support to time, sensing, concur- the ClickWorld project, a research project partially funded rency, nondeterminism, etc.) was also provided. by the Italian Ministero dell’Istruzione, dell’Università e della Ricerca (MIUR). Older industrial applications in- Computational Logic for MAS Prototyping volve freight train traffic [18] and vehicle monitoring [4]. The industrial applications of CaseLP and DCaseLP It is well known that computational logic and logic pro- show an increased industrial interest and trust in both gramming in particular are very suitable to implement so- agent-based and declarative technologies, and demonstrate phisticated, self-aware agents able to reason about them- the liveliness of computational logic outside the bound- selves and the other agents in a multiagent system (MAS). aries of academia. DCaseLP (Distributed Complex Applications Specification Environment based on Logic Programming [31]) is an en- Verifying Interaction Protocols with Logic vironment for rapid prototyping of MASs developed by the Logic Programming Group at DISI. DCaseLP was initially We have recently developed a tool aimed at supporting born as a logic-based framework, as the acronym itself verification of finite-state interaction protocols in a MAS suggests, and then evolved into a multi-language proto- setting, West2East [16], that exploits “WEb Service Tech- typing environment that integrates both imperative (object- nologies to Engineer Agent-based SofTware” starting from oriented) and declarative (rule-based and logic-based) lan- the specification of an Agent Interaction Protocol (AIP). guages, as well as graphical ones. The languages and tools West2East exploits AUML [11] for representing AIPs, that DCaseLP integrates are UML and an XML-based lan- many different languages, including standard languages guage for the analysis and design stages, Java, JESS [26] for Web Services, for sharing them, and Computational and tuProlog [22] for the implementation stage, and JADE Logic to reason about them. In particular, West2East con- [12] for the execution stage. Software libraries for integrat- sists of a set of libraries for ing JESS and tuProlog agents into the JADE platform and for translating UML class diagrams into JESS and tuProlog 1. Translating visual AUML AIPs to various formats: code are also provided1 . The methodological integration of starting from an AUML interaction diagram graphi- DCaseLP with the “Dynamics in Logic” agent program- cally drawn using any UML editor, West2East gen- ming language is described in [6]. erates the corresponding representation in many for- All the applications that we developed with DCaseLP in mats, including a Prolog term. collaboration with Italian industries, exploit tuProlog for implementing the MAS. 2. Generating code compliant to the AIP: starting from The most recent application, described in [30], is a MAS the Prolog term, a tuProlog program for each agent that monitors processes running in a railway signalling involved in the AIP is automatically generated by plant, detects functioning anomalies, provides diagnoses West2East. After a manual completion for adding the for explaining them, and early notifies problems to the information missing in the AIP’s specification, such Command and Control System Assistance. This work is as agents’ state and guards of conditions, the tuProlog part of an ongoing project that involves DISI and Ansaldo code can be run inside JADE thanks to the DCaseLP Segnalamento Ferroviario, the Italian leader in design and libraries. construction of signalling and automation systems for rail- way lines. 3. Reasoning about the AIP: a mechanism for allow- 1 The source code of DCaseLP libraries together with manuals and tu- ing tuProlog agents to reason about an AIP by ex- torials is available from http://www.disi.unige.it/person/ ploiting meta-programming techniques is provided by MascardiV/Software/DCaseLP.html. West2East. Existential and universal properties, such 40 Il Milione: A Journey in the Computational Logic in Italy as “There is one path of the protocol where I will re- research groups with the same objectives. The profitable ceive message1 ”, and “Whatever the path, I will send collaboration will be pursued in the future with the hope to message2 ”, can be verified. contribute in making research on Computational Logic an Italian excellence. In [21] we have further investigated in the relation be- tween (constraint) logic programming and infinite-state REFERENCES verification. More specifically, in [21] we show that a CLP bottom-up evaluation procedure can be applied to auto- [1] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating- matically verify safety and liveness properties for skele- time temporal logic. J. ACM, 49:672–713, 2002. tons of communication protocols (with a fixed number of [2] D. Ancona and V. Mascardi. Coo-BDI: Extending the processes) like mutual-exclusion algorithms. In the case- BDI model with cooperativity. In J. A. Leite, A. Omicini, studies described in [21] the source of infiniteness is the L. Sterling, and P. Torroni, editors, Proc. of the 1st Declar- presence of potentially unbounded integer variables in the ative Agent Languages and Technologies Int. Workshop, specification of individual processes. Constraints are used DALT’03, Revised Selected and Invited Papers, LNAI, here to symbolically represent infinite collections of sys- pages 109–134. Springer, 2004. tem configurations with a fixed number of processes. [3] J-M. Andreoli and R. Pareschi. Linear ojects: Logical pro- Another interesting research line concerns with the ap- cesses with built-in inheritance. New Generation Comput., plication of linear logic programming to verification of 9(3/4):445–474, 1991. infinite-state systems. Linear logic [28] is a suitable logi- [4] E. Appiani, M. Martelli, and V. Mascardi. A multi-agent cal framework for the specification of concurrent systems. approach to vehicle monitoring in motorway. Technical re- port, Computer Science Department of Genova University, The LO fragment [3] of full linear logic provides multi- 2000. DISI TR-00-13, Poster session of the Second Eu- headed linear implications with only multiplicative dis- ropean Workshop on Advanced Video-Based Surveillance junction and additive conjunction in the body. By exploit- Systems, AVBS 2001. ing and generalizing the connection between verification [5] M. Baldoni, C. Baroglio, G. Berio, A. Martelli, V. Patti, and logic programming described in [21], in [14] we have M. L. Sapino, C. Schifanella, M. Alberti, M. Ga- defined a bottom-up evaluation strategy for (first order) vanelli, E. Lamma, F. Riguzzi, S. Storari, F. Chesani, LO programs based on an effective fixpoint operator à-la A. Ciampolini, P. Mello, M. Montali, P. Torroni, A. Bot- TP (the immediate consequence operator for (constraint) trighi, L. Giordano, V. Gliozzi, G. L. Pozzato, D. Theseider logic programs). The LO TP operator works on first or- Dupré, P. Terenziani, G. Casella, and V. Mascardi. Mod- der multi-headed LO clauses [14]. Furthermore, it can eling, verifying and reasoning about web services. Intelli- be viewed as a symbolic predecessor operator for transi- genza Artificiale. To appear. tion systems described via multiset rewriting systems de- [6] M. Baldoni, C. Baroglio, I. Gungui, A. Martelli, fined over first-order atomic formulas. In [15] we have M. Martelli, V. Mascardi, V. Patti, and C. Schifanella. Rea- extended the bottom-up evaluation procedure to first order soning about agents’ interaction protocols inside DCaseLP. linear logic specification with universally quantified goals. In J. A. Leite, A. Omicini, P. Torroni, and P. Yolum, ed- In [13] we have applied the resulting procedure to ver- itors, Proc. of the 2nd Declarative Agent Languages and Technologies Int. Workshop, DALT’04, Revised Selected ify properties of cryptographic protocols for any possible and Invited Papers, volume 3476 of LNCS, pages 112–131. number of principals and parallel sessions. Springer, 2004. [7] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, C. Schi- Conclusions fanella, L. Torasso, and V. Mascardi. Personalization, Research on computational logic in Genova is very lively, verification and conformance for logic-based communicat- ing agents. In F. Corradini, F. De Paoli, E. Merelli, and and will be even more in the future thanks to the interest A. Omicini, editors, Proc. of the WOA 2005 National Work- on its practical applications raised outside the boundaries shop, Dagli Oggetti Agli Agenti, pages 177–183. Pitagora of academia. Part of this research has been carried out in Editrice Bologna, 2005. joint projects with the Logic Programming and Automated [8] M. Baldoni, C. Baroglio, and V. Mascardi, editors. Pro- Reasoning Group in Torino. The results of these projects ceedings of the Multi-Agent Logics, Languages, and Or- are described in [7, 5], and the active collaboration in wit- ganisations, Federated Workshops, MALLOW’007, Agent, nessed by many other joint activities [8, 9]. Web Services and Ontologies, Integrated Methodolo- The connections between the Logic Programming gies (MALLOW-AWESOME’007) workshop, Durham, GB. Groups in Torino and Genova date back to more than 30 2007. years ago. The heads of the groups, Alberto and Maurizio [9] M. Baldoni, A. Boccalatte, F. De Paoli, M. Martelli, and Martelli, besides the same family name, share many com- V. Mascardi, editors. WOA, Workshop dagli Oggetti agli mon experiences: they worked together at the National Re- Agenti, Proceedings. Seneca Edizioni (Italy), 2007. search Council in Pisa, were involved in the committees of [10] M. Baldoni, L. Giordano, A. Martelli, and V. Patti. Model- conferences and workshops on Computational Logics, and, ing agents in a logic action language. In Proc. of the Work- when moved to Torino and Genova respectively, founded shop on Practical Reasoning Agents, FAPR 2000, 2000. 41 Il Milione: A Journey in the Computational Logic in Italy [11] B. Bauer, J. P. Müller, and J. Odell. Agent UML: A formal- [27] G. De Giacomo, Y. Lespérance, and H. J. Levesque. Con- ism for specifying multiagent software systems. In P. Cian- golog, a concurrent programming language based on the sit- carini and M. Wooldridge, editors, Proc. of the 1st Agent- uation calculus. Artificial Intelligence, 121:109–169, 2000. Oriented Software Engineering Int. Workshop, AOSE’00, [28] J-Y. Girard. Linear logic. Theor. Comput. Sci., 50:1–102, Revised Papers, volume 1957 of LNCS, pages 91–104. 1987. Springer, 2000. [29] P. Klemperer. Auctions: Theory and practice. Princeton [12] F. L. Bellifemine, G. Caire, and D. Greenwood. Developing University Press, 2004. Multi-Agent Systems with JADE. Wiley, 2007. [30] V. Mascardi, D. Briola, M. Martelli, R. Caccia, and C. Mi- [13] M. Bozzano and G. Delzanno. Automatic verification of lani. Monitoring and diagnosing railway signalling with secrecy properties for linear logic specifications of cryp- rule-based distributed agents. Technical report, Diparti- tographic protocols. J. Symb. Comput., 38(5):1375–1415, mento di Informatica e Scienze dell’Informazione, Univer- 2004. sity of Genova, Italy, 2008. Technical Report DISI-TR-08- [14] M. Bozzano, G. Delzanno, and M. Martelli. An effec- 04. tive fixpoint semantics for linear logic programs. TPLP, [31] V. Mascardi, M. Martelli, and I. Gungui. DCaseLP: a pro- 2(1):85–122, 2002. totyping environment for multi-language agent systems. In [15] M. Bozzano, G. Delzanno, and M. Martelli. Model check- M. Dastani, A. El-Fallah Seghrouchni, J. Leite, and P. Tor- ing linear logic specifications. TPLP, 4(5-6):573–619, roni, editors, Proc. of the 1st Int. Workshop on Languages, 2004. Methodologies and Development Tools for Multi-Agent Sys- tems, LADS’007, LNCS. Springer, 2008. To appear. [16] G. Casella and V. Mascardi. West2East: exploiting WEb Service Technologies to Engineer Agent-based SofTware. [32] V. Mascardi, M. Martelli, and L. Sterling. Logic-based IJAOSE, 1(3/4):396–434, 2007. specification languages for intelligent software agents. TPLP, 4(4):429–494, 2004. [17] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time tempo- [33] R. Montagna, G. Delzanno, M. Martelli, and V. Mascardi. ral logic. In Logic of Programs, pages 52–71, 1981. BDI AT L : An alternating-time BDI logic for multiagent systems. In M. P. Gleizes, G. A. Kaminka, A. Nowé, S. Os- [18] A. Cuppari, P. L. Guida, M. Martelli, V. Mascardi, and sowski, K. Tuyls, and K. Verbeeck, editors, Proc. of the 3rd F. Zini. An agent-based prototype for freight trains traf- European Workshop on Multi-Agent Systems, EUMAS’05, fic management. In P. G. Larsen, editor, Proc. of the pages 214–223. Koninklijke Vlaamse Academie van Belie 5th FMERail Workshop. Held in conjunction with FM’99. voor Wetenschappen en Kunsten, 2005. Springer, 1999. [34] A. S. Rao and M. P. Georgeff. Asymmetry thesis and side- [19] M. Delato, A. Martelli, M. Martelli, V. Mascardi, and effect problems in linear-time and branching-time intention A. Verri. A multimedia, multichannel and personalized logics. In J. Myopoulos and R. Reiter, editors, Proc. of news provider. In G. Ventre and R. Canonico, editors, Proc. the 12th Int. Joint Conf. on Artificial Intelligence, IJCAI- of the 1st Int. Workshop on Multimedia Interactive Proto- 91. Morgan Kaufmann publishers, 1991. cols and Systems, MIPS 2003, volume 2899 of LNCS, pages [35] A. S. Rao and M. P. Georgeff. Deliberation and intentions. 388–399. Springer, 2003. In Proc. of 7th Conference on Uncertainity in Artificial In- [20] G. Delzanno and M. Martelli. Proofs as computations in telligence. Morgan Kaufmann publishers, 1991. linear logic. Theoretical Computer Science, 258(1–2):269– [36] A. S. Rao and M. P. Georgeff. Modelling rational agents 297, 2001. within a BDI-architecture. In Proc. of the 2nd Int. Confer- [21] G. Delzanno and A. Podelski. Constraint-based deductive ence of Principles of Knowledge Representation and Rea- model checking. STTT, 3(3):250–270, 2001. soning. Morgan Kaufmann publishers, 1991. [22] E. Denti, A. Omicini, and A. Ricci. Multi-paradigm Java- [37] D. Roggero, F. Patrone, and V. Mascardi. Designing and im- Prolog integration in tuProlog. Sci. Comput. Program., plementing electronic auctions in a multiagent system en- 57(2):217–250, 2005. vironment. In F. Corradini, F. De Paoli, E. Merelli, and A. Omicini, editors, Proc. of the WOA 2005 National Work- [23] T. Eiter, V.S. Subrahmanian, and G. Pick. Heterogeneous shop, Dagli Oggetti Agli Agenti, pages 157–163. Pitagora active agents, I: Semantics. Artificial Intelligence, 108(1- Editrice Bologna, 2005. 2):179–255, 1999. [38] Y. Shoham. Agent-oriented programming. Artificial Intel- [24] E. A. Emerson and J. Y. Halpern. “Sometimes” and “not ligence, 60:51–92, 1993. never” revisited: on branching versus linear time temporal logic. J. ACM, 33(1):151–178, 1986. [39] W. Vickrey. Auction and bidding games. In Recent ad- vances in Game Theory, pages 15–27. Princeton University [25] M. Fisher and H. Barringer. Concurrent METATEM pro- Conference, 1962. cesses – A language for distributed AI. In Proceedings of the European Simulation Multiconference. SCS Press, [40] M. Wooldridge. Reasoning about rational agents. Mit Copenhagen, Denmark, 1991. press, 2000. [26] E. Friedman-Hill. Jess in Action : Java Rule-Based Systems (In Action series). Manning Publications, 2002. 42