Il Milione: A Journey in the Computational Logic in Italy Logiche multimodali per ragionare sull’interazione Multimodal Logics for Reasoning about Interaction Matteo Baldoni, Cristina Baroglio and Viviana Patti 82 Il Milione: A Journey in the Computational Logic in Italy SOMMARIO/ABSTRACT putational counterpart, which is particularly suitable for representing the behavior of interacting and communica- Questo articolo presenta alcune delle attività condotte tive agents and which lead to the implementation of the nel corso degli ultimi anni dal gruppo di ricerca guidato declarative programming language Dynamics in LOGic. da Alberto Martelli. In particolare verrà presentato un The framework has been successfully applied to as diverse percorso che comprende la specifica, lo sviluppo e la application domains as web-based adaptive tutoring, web verifica di protocolli di interazione. Il filo conduttore è service selection and composition, reasoning about chore- costituito dall’uso di logiche multimodali e di formalismi ographies, semantic web. In particular, it has been adopted dichiarativi e tecniche di ragionamento basati sulla logica in various national and international research projects, e.g. computazionale. MASSiVE, SVP, and REWERSE. In this paper, we report some of the activities carried on in the last years by the research group leaded by Alberto Future directions Martelli. In particular, it presents a research line that en- Declarative languages are becoming very important in the compasses the specification, the development and the ver- context of Semantic Web, especially in the most recent ification of interaction protocols. The leading thread is years, when the focus moved from the ontology layer to given by the use of multimodal logics and of declarative the logic layer and the need of expressing rules and apply formalisms and reasoning techniques, based on computa- various forms of reasoning have emerged. This interest is tional logic. witnessed also by the creation of a W3C working group to define a Rule Interchange Format. The effort done for rep- Keywords: Interaction protocols, multimodal logics, web resenting and reasoning about interactions, in the frame- services, semantic web. work presented in this paper, finds a natural grounding in the development of negotiation or personalization policies, 1 Introduction expressed by rules. Challenging applications can be iden- tified also in the context of web services. Here, we are Modal logics are widely used in Artificial Intelligence for interested in applications aimed at fostering the re-use of representing knowledge and beliefs together with other at- software, task that requires abilities, e.g. flexibility, which titudes like, for instance, goals, intentions and obligations. are supplied by declarative languages and by the reasoning Moreover, modal logics are well suited for representing dy- techniques that they allow to apply. In particular, a very namic aspects in agent systems and, in particular, to for- promising direction of research is the study of methods and malize reasoning about actions and time [16, 22]. In this approaches to verify the interoperability of services and the context, one of the main research lines of the last years conformance of a service to a choreography role. concerns the specification of interaction and the forms of reasoning that can be applied to it, and gives particular at- tention to the verification of properties of the interaction 2 The origins: A class of Normal Multi- and of the interacting agents [22]. The work that we sum- modal Logics marize in these pages begins with the construction of a logical framework, based on a class of normal multimodal In [12, 3] a class of normal multimodal logics, called gram- logic (called grammar logics). This framework has a com- mar logics, is studied. The class is characterized by a set 83 Il Milione: A Journey in the Computational Logic in Italy of logical axioms of the form: description, which includes: a) action and precondition laws, describing the atomic world actions the agent may [p1 ] . . . [pn ]ϕ ⊃ [s1 ] . . . [sm ]ϕ (n > 0; m ≥ 0) (1) perform; b) a set of sensing axioms describing the agent’s atomic sensing actions; c) a set of procedure axioms de- called inclusion axioms, where the pi ’s and sj ’s are modal- scribing the agent’s complex behavior. Each atomic ac- ities. This class includes some well-known modal systems tion can have preconditions to its application (that decide such as K, K4, S4 and their multimodal versions. Differ- if the action is executable) and effects due to its applica- ently from other logics, such as those in [16], these systems tion. Moreover, effects can be subject to further conditions can be non-homogeneous (i.e., every modal operator is not in order to become true. For instance, the executability restricted to belong to the same system) and can contain precondition to the action “paying by credit card” is that I some interaction axioms (i.e., modal operators are not re- hold a valid credit card. A conditional effect of this action stricted to be mutually independent). could be “to be notified by SMS about payments”. This ef- This class of logics has been introduced by Fariñas del fect will become true only if I subscribed the service (pre- Cerro and Penttonen in [14] to simulate the behavior of for- condition to the effect). mal grammars. Given a formal grammar, a modality is as- sociated to each terminal and nonterminal symbol, while, Given this view of actions, we can think to the prob- for each production rule of the form p1 · · · pn → s1 · · · sm , lem of reasoning as the act of building or of traversing a an inclusion axiom [p1 ] . . . [pn ]ϕ ⊃ [s1 ] . . . [sm ]ϕ is de- sequence of transitions between states. Technically speak- fined. In [14] it is shown that testing whether a word is ing, a state is a set of fluents, i.e., properties whose truth generated by the formal grammar is equivalent to proving value can change over time. Such properties encode the a theorem in the logic, thus showing the undecidability of information that flows during the execution of a policy: for the whole class of logics. instance, if a requester communicates to pay by miles, this In [12, 3] an analytic tableau calculus for the class of information will be included in the state of the provider as grammar logics is presented. The calculus is paramet- a fluent. In general, we cannot assume that the value of ric w.r.t. the logics of this class. In particular, they deal each fluent in a state is known, so we want to have both the with non-homogeneous multimodal systems with arbitrary possibility of representing that some fluents are unknown interaction axioms of form (1). The calculus is a pre- and the ability of reasoning about the execution of actions fixed tableaux extension of those in [18, 15]. Prefixes are on incomplete states. To explicitly represent the unknown given an atomic name and the accessibility relationships value of some fluents, we introduced an epistemic opera- among them are explicitly represented in a graph. The tor B, to represent the beliefs an entity has about the world: key idea is using the characterizing axioms of the logic as Bf means that the fluent f is known to be true, B¬f means “rewrite rules” which create new paths among worlds in that the fluent f is known to be false. A fluent f is unde- the counter-model construction. The works prove the un- fined when both ¬Bf and ¬B¬f hold. Thus each fluent decidability of modal systems based on context-sensitive in a state can have one of the three values: true, false or and context-free grammars, while right regular grammars unknown. are decidable (by using an extension of the filtration meth- Complex behaviors can be specified by means of pro- ods by the Fischer-Ladner closure for modal logics). In the cedures, Prolog-like clauses built upon other actions. For- particular case when m is 1, the axiom schema reduces to mally, a complex action is a collection of inclusion axiom schemas of the modal logic, of form (2). s0 is a procedure hs0 iϕ ⊂ ht1 iht2 i . . . htn iϕ (2) name and the pi ’s are procedure names, atomic actions, or test actions (?f ). Procedure definitions may be recursive and the rewriting rules for describing accessibility relations and procedure clauses can be executed in a goal-directed become similar to a Prolog goal-directed proof procedure. way, similarly to standard logic programs. This observation has allowed the definition of the language Dynamics in LOGic. This class of logics has also been The language allows the specification of communicative used in the study of description logics [20, 17] and ex- behaviors [10]. Indeed, we define the communication kit tended to more general forms of interaction in [4]. [19] for an agent as consisting of a predefined set of primi- tive speech acts the agent can perform/recognize, modeled in terms of action and preconditions laws, a set of spe- 3 Dynamics in LOGic: An agent Program- cial sensing actions for getting new information by external ming Language communications, defined by sensing axioms, and a set of Dynamics in LOGic [13] has been developed as a language interaction protocols specified by procedure axioms. Usu- for programming agents and is based on a logical theory ally a communicative action modifies not only the beliefs for reasoning about actions and change in a modal logic of the executor about the world but also its beliefs about programming setting. An agent’s behavior is described in the interlocutor’s mental state. a non-deterministic way by giving the set of actions that it Given a domain description, we can reason about it and can perform. Specifically, it can be specified by a domain formalize the temporal projection and the planning prob- 84 Il Milione: A Journey in the Computational Logic in Italy lems by means of existential queries of form: protocols and that describes the interaction capabilities of the service. hp1 ihp2 i . . . hpm iFs (3) The work presented in [10] faces the problem of au- tomatic selection and composition of web services, dis- where each pk , k = 1, . . . , m may be an (atomic or com- cussing the advantages that derive from the inclusion, in plex) action executed by the agent. Checking if a query of a web service declarative description, of the high-level in- form (3) succeeds corresponds to answering the question teraction protocol, that is used by the service for interact- “Is there an execution trace of the sequence p1 , . . . , pm ing with its partners, allowing a rational inspection of it. that leads to a state where the conjunction of belief fluents Communication can, in fact, be considered as the behavior Fs holds for our agent?”. In case all the pk ’s are atomic resulting from the application of a special kind of actions: actions, it amounts to predict if the condition of interest communication actions. The reasoning problem that this will be true after their execution. In case complex actions proposal faces can intuitively be described as looking for are involved, the execution trace that is returned in the end an answer to the question “Is it possible to make a deal is a plan to bring about Fs. The procedure definition con- with this service respecting the user’s goals?”. Given a strains the search space. The plan can be conditional be- logic-based representation of the service policies and a rep- cause whenever a sensing action is involved, none of the resentation of the customer’s needs as abstract goals, ex- possible answers of the interlocutor can be excluded. pressed by a logic formula, logic programming reasoning A goal-directed proof procedure, based on negation as techniques are used for understanding if the constraints of failure, allows to (dis)prove queries of form (3). An in- the customer fit in with the policy of the service. terpreter for the language has been implemented in Sics- In this issue it is possible to distinguish three necessary tus Prolog [8]. This implementation allows the language components: (i) web services capabilities must be rep- to be used as an ordinary programming language for exe- resented according to some declarative formalism with a cuting procedures which specify the behavior of an agent, well-defined semantics, as also observed by van der Aalst but also for reasoning about them, by extracting linear or et al. [21]; (ii) automated tools for reasoning about such a conditional plans. The plan extraction process of the in- description and performing tasks of interest must be devel- terpreter is a straightforward implementation of the proof oped; (iii) in order to gain flexibility in fulfilling the user’s procedure contained in the theoretical specification of the request, reasoning tools should represent such requests as language. abstract goals. Our proposal is set in the Semantic Web field of research 3.1 Web-based Adaptive Tutoring and inherits from research in the field of multi-agent sys- tems. In particular, the declarative descriptions of services Dynamics in LOGic has been used to implement an adap- are based on the modal logic programming framework in- tive tutoring system [11] with a multi-agent architecture, troduced in Section 3. Web services are viewed as soft- that can produce personalized study plans and that can val- ware agents, communicating by predefined sharable inter- idate study plans built by a user. A key feature that allows action protocols, where the protocol-based interactions are the tutoring system agents to adapt to users is their ability formalized as Dynamics in LOGic procedures; reasoning to tackle mental attitudes, such as beliefs and intentions. about actions and change techniques (planning) are used The agent can adopt the user’s learning goal and find a for performing the selection and composition of web ser- way for achieving it, which fits the specific student’s in- vices in a way that is personalized w.r.t. the user’s request. terests and takes into account his/her current knowledge. Applying reasoning techniques on a declarative specifica- A natural evolution of this work opened the way to the ac- tion of the service interactions allows to gain flexibility in tivity carried on in the REWERSE network of excellence fulfilling the user preference in the context of a web service [2, 9, 7]. matchmaking process. As a quick example, consider a web service that allows buying products, alternatively paying 4 Reasoning about WS Composition and cash or by credit card: a user might have preferences on Choreographies the form of payment to enact. In order to decide whether or not buying at this shop, it is necessary to single out the In the last years distributed applications over the World- specific course of interaction that allows buying cash. This Wide Web have obtained wide popularity and uniform form of personalization requires to reason about a descrip- mechanisms have been developed for handling comput- tion of the service interaction policy. ing problems which involve a large number of heteroge- A declarative specification of the interaction is useful neous components, that are physically distributed and that also in the process of selecting the services which will play interoperate. These developments have begun to coalesce the various roles of the given choreography, in the particu- around the web service paradigm, where a service can be lar case in which a condition of interest is to be preserved seen as a component available over the web [1]. Each ser- (the goal for which the service is sought). In [6, 5] we vice has an interface that is accessible through standard show that current semantic matchmaking techniques do not 85 Il Milione: A Journey in the Computational Logic in Italy guarantee goal preservation. The approach is based on an [8] M .Baldoni, C. Baroglio, A. Chiarotto, and V. Patti. action-based representation of the operations of a service: Programming goal-driven web sites using an agent each operation is described in terms of its preconditions logic language. In PADL, LNCS 1990, pp. 60–75. and effects. Also in this work, the Dynamics in LOGic Springer, 2001. framework was used to represent service interaction poli- [9] M. Baldoni, C. Baroglio, and N. Henze. Personaliza- cies as well as roles. This representation allow to reason tion for the semantic web. In Reasoning Web, LNCS for checking if it is possible to reach a goal by adopting 3564, pp. 173–212. Springer, 2005. a certain role, and if the goal is preserved after the sub- stitution of the service capabilities to the abstract require- [10] M. Baldoni, C. Baroglio, A. Martelli, and V. Patti. ments specified in the role. We show that, by exploiting Reasoning about interaction protocols for customiz- reasoning mechanisms and the choreography definition, it ing web service selection and composition. J. Log. is possible to overcome the limits of the current semantic Algebr. Program., 70(1):53–73, 2007. matchmaking techniques and we have proposed a variant of the plugin match which guarantees goal preservation. [11] M. Baldoni, C. Baroglio, and V. Patti. Web-based adaptive tutoring: An approach based on logic agents and reasoning about actions. Artif. Intell. Rev., 5 Acknowledgements 22(1):3–39, 2004. The authors would like to thank all people who contributed [12] M. Baldoni, L. Giordano, and A. Martelli. A tableau to this line of research over the last years, in particular for multimodal logics and some (un)decidability re- Alberto Martelli, Alessandro Chiarotto, Laura Giordano, sults. In TABLEAUX, LNCS 1397, pp. 44–59. Claudio Schifanella and Laura Torasso, co-authoring most Springer, 1998. of the papers. [13] M. Baldoni, A. Martelli, V. Patti, and L. Giordano. Programming rational agents in a modal action logic. REFERENCES Ann. Math. Artif. Intell., 41(2-4):207–257, 2004. [1] G. Alonso, F. Casati, H. Kuno, and V. Machiraju. Web [14] L. Fariñas del Cerro and M. Penttonen. Grammar Services. Springer, 2004. Logics. Logique et Analyse, 121-122:123–134, 1988. [2] G. Antoniou, M. Baldoni, C. Baroglio, R. Baungart- [15] M. Fitting. Proof Methods for Modal and Intuitionis- ner, F. Bry, T. Eiter, N. Henze, M. Herzog, W. May, tic Logics, volume 169 of Synthese library. D. Reidel, V. Patti, S. Schaffert, R. Schidlauer, and H. Tom- Dordrecht, Holland, 1983. pits. Reasoning Methods for Personalization on the [16] Joseph Y. Halpern and Yoram Moses. A guide to Semantic Web. Ann. of Math., Comp. & Teleinf. completeness and complexity for modal logics of (AMCT), 2(1):1–24, 2004. knowledge and belief. Artif. Intell., 54(2):319–379, [3] M. Baldoni. Normal Multimodal Logics: Automatic 1992. Deduction and Logic Programming Extension. PhD [17] Ian Horrocks and Ulrike Sattler. Decidability of shiq thesis, Università degli Studi di Torino, Italy, 1998. with complex role inclusion axioms. Artif. Intell., [4] M. Baldoni. Normal Multimodal Logics with Interac- 160(1-2):79–104, 2004. tion Axioms. In Labelled Deduction, Applied Logic [18] A. Nerode. Some Lectures on Modal Logic. In F. L. Series 17, pp. 33–53. Kluwer Ac. Publisher, 2000. Bauer, editor, Logic, Algebra, and Computation, vol- ume 79 of NATO ASI Series. Springer-Verlag, 1989. [5] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and C. Schifanella. Reasoning on choreographies and ca- [19] V. Patti. Programming Rational Agents: a Modal Ap- pability requirements. Int. J. of Business Process In- proach in a Logic Programming Setting. PhD thesis, tegration and Management, 2(4), 2007. Università degli Studi di Torino, Italy, 2002. [6] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and [20] Ulrike Sattler. Description Logics for Ontologies. In C. Schifanella. Service selection by choreography- Proc. of ICCS 2003, LNAI 2746, pap. 96–116, 2003. driven matching. In Proc. of WEWST’07, vol. 313 of [21] Wil M. P. van der Aalst, Marlon Dumas, Arthur H. M. CEUR, Workshop Proc., pp. 1–17, 2008. ter Hofstede, Nick Russell, H. M. W. (Eric) Verbeek, [7] M. Baldoni, C. Baroglio, I. Brunkhorst, E .Marengo, and Petia Wohed. Life after bpel? In EPEW/WS-FM, and V. Patti. Reasoning-based curriculum sequenc- LNCS 3670, pp. 35–50. Springer, 2005. ing and validation: Integration in a service-oriented [22] Michael Wooldridge. An Introduction to Multiagent architecture. In EC-TEL, LNCS 4753, pp. 426–431. Systems. John Wiley & Sons, 2002. Springer, 2007. 86 Il Milione: A Journey in the Computational Logic in Italy 6 Contacts Matteo Baldoni (Corresponding Author) Dipartimento di Informatica — Università degli Studi di Torino c.so Svizzera, 185 I-10149 Torino (Italy) Tel. +39 011 6706756 baldoni@di.unito.it Cristina Baroglio Dipartimento di Informatica — Università degli Studi di Torino c.so Svizzera, 185 I-10149 Torino (Italy) Tel. +39 011 6706703 baroglio@di.unito.it Viviana Patti Dipartimento di Informatica — Università degli Studi di Torino c.so Svizzera, 185 I-10149 Torino (Italy) Tel. +39 011 6706804 patti@di.unito.it 7 Biography Matteo Baldoni (http://www.di.unito.it/ baldoni) is associate professor at the University of Torino since 2006. He received a Ph.D. in Computer Science from the same university. He has a background in computational logic, multi-modal and non-monotonic extensions of logic programming and reasoning about actions. Current research interests: communication protocol design and implementation, conformance and interoperability of services, personalization by reasoning in the semantic web. He is co-chair of the workshop AWESOME@MALLOW’007, and has been co-chair of the last four editions of the DALT@AAMAS international workshop. He chairs the working group ”Sistemi ad Agenti e Multiagente” of the Italian Association for Artificial Intelligence. Cristina Baroglio (http://www.di.unito.it/ baroglio) is associate professor of Computer Science at the University of Torino since 2005. She has a Ph.D. in Cognitive Sciences from the same university, and has a background in Machine Learning and Automated Reasoning. She is author of over 70 papers, co-chair of the workshop ”Agents, Web Services, and Ontologies: Integrated Methodologies” (AWESOME@MALLOW’007), and member of the PC of the Reasoning web Summer School 2007 and 2008. Her research interests include: semantic web and semantic web services, adaptation based on reasoning, conformance and interoperability of services to choreographies/protocols, automatic teaching to artificial agents, formal approaches to e-learning. Viviana Patti (http://www.di.unito.it/ patti) is a researcher associate in Computer Science at the University of Torino since 2005. She received her Ph.D. in Computer Science in 2002. She is author of more than 50 scientific papers. Her research interests include: computational logics for agent programming, reasoning enabling personalization in the semantic web, web service interoperability and conformance verification, web-based education courseware and curricula. She has been involved in the organization of several international events mainly in the fields ”Personalization in the Semantic Web”, ”Web Information systems and Technologies” and ”Agents”. She has been member of the European Network of Excellence REWERSE. 87