Publications on Modal Logic

Alberto Artosi and Guido Governatori.
Popper on Necessity and Natural Laws. In Mario Alai and Gino Tarozzi, editors, Karl Popper Philosopher of Science. pages 107-118. Rubbettino Editore, Soveria Mannelli, 2006.
Abstract: During his philosophical career Popper sought to characterize natural laws alternately as strictly universal and as `naturally' or `physically' necessary statements. In this paper we argue that neither characterization does what Popper claimed and sketch a reconstruction of his views that avoids some of their major drawbacks.
 
Jeff Blee, David Billington, Guido Governatori, and Abdul Sattar.
Levels of modalities for BDI logic. In 2008 IEEE/WIC/ACM International Conference on Web Intelligence and Intelligent Agent Technology, pages 647-650. IEEE Press, 2008, Copyright © 2008 IEEE.
Abstract: The use of rational agents for modelling real world problems has both been heavily investigated and become well accepted, with BDI Logic being a widely used architecture to represent and reason about rational agency. However, in the real world, we often have to deal with different levels of confidence in our beliefs, desires, and intentions. This paper extends our previous framework that integrated qualitative levels into BDI Logic. We describe an expanded set of axioms and properties of the extended logic and also define a detailed non-normal Kripke type semantics.
 
Guido Governatori.
Labelled modal tableaux. In Carlos Areces, Patrick Blackburn, and Rob Goldblatt, editors, Advances in Modal Logic, volume 7. College Publications, London, 2008.
Abstract: Labelled tableaux are extensions of semantic tableaux with annotations (labels, indices) whose main function is to enrich the modal object language with semantic elements. This paper consists of three parts. In the first part we consider some options for labels: simple constant labels vs labels with free variables, logic depended inference rules vs labels manipulation based on a label algebra. In the second and third part we concentrate on a particular labelled tableaux system called KEM using free variable and a specialised label algebra. Specifically in the second part we show how labelled tableaux (KEM) can account for different types of logics (e.g., non-normal modal logics and conditional logics). In the third and final part we investigate the relative complexity of labelled tableaux systems and we show that the uses of KEM's label algebra can lead to speed up on proofs.
 
Guido Governatori, Ian Hodkinson and Yde Venema (eds).
Advances in Modal Logic. Vol. 6. College Press, London, 2006.
 
Guido Governatori and Antonino Rotolo.
De re modal semantics. Bulletin of Symbolic Logic, 9 no. 2 pp. 259-260, June 2003.
 
Guido Governatori and Antonino Rotolo.
On the axiomatization of Elgesem's logic of ability and agency. Bulletin of Symbolic Logic, 10 in print, 2004.
 
Guido Governatori and Antonino Rotolo.
On the axiomatization of Elgesem's logic of agency. In Mark Reynold and Heinrich Wansing, editors, Advances in Modal Logic 5, Manchester, 8-11 September 2004.
Abstract: In this paper we show that the Hilbert system of agency and ability presented by Dag Elgesem is incomplete with respect to the intended semantics. We argue that completeness result may be easily regained. Finally, we shortly discuss some issues related to the philosophical intuition behind his approach. This is done by examining Elgesem's modal logic of agency and ability using semantics with different flavours.
 
Guido Governatori and Antonino Rotolo.
On the axiomatization of Elgesemís logic of agency and ability. Journal of Philosophical Logic 34, 4, pp. 403-431. The original publication is available at www.springerlink.com.
Abstract:In this paper we show that the Hilbert system of agency and ability presented by Dag Elgesem is incomplete with respect to the intended semantics. We argue that completeness result may be easily regained. Finally, we shortly discuss some issues related to the philosophical intuition behind his approach. This is done by examining Elgesem's modal logic of agency and ability using semantics with different flavours.
 
Vineet Padmanabhan, Guido Governatori, and Subhasis Thakur.
Knowledge assessment: A modal logic approach. In The Duy Bui, Tuong Vinh Ho, and Quang-Thuy Ha, editors, 11th Pacific Rim International Conference on Multi-Agents (PRIMA 2008), Lecture Notes in Computer Science 5357, pages 315-322. Springer, 2008, Copy rigth © 2008 Springer.
Abstract: The possible worlds semantics is a fruitful approach used in Artificial Intelligence (AI) for both modelling as well as reasoning about knowledge in agent systems via modal logics. In this work our main idea is not to model/reason about knowledge but to provide a theoretical framework for knowledge assessment (KA) with the help of Monatague-Scott (MS) semantics of modal logic. In KA questions asked and answers collected are the central elements and knowledge notions will be defined from these (i.e., possible states of knowledge of subjects in a population with respect to a field of information).
 
Kaile Su, Abdul Sattar, Guido Governatori, and Qingliang Chen.
A computationally grounded logic of knowledge, belief and certainty. In Proceedings of The Fourth International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS 2005) ACM Press, 2005, pp. 149-156. Copyright © 2005, ACM Press.
Abstract:This paper develops a logic of knowledge, belief and certainty, which allows us to explicitly mention an agent's knowledge, belief and certainty in multi-agent systems. A computationally grounded model, called interpreted KBC systems, is given for interpreting this logic. The relationship between knowledge, belief and certainty is explored. In particular, certainty entails belief; and to the agent what it is certain of appears to be knowledge. To characterize all valid formulas in our logic, we provide a sound and complete proof system. We show that the validity problem for the interpreted KBC systems is PSPACE-complete. Our proof approach is based on the well-known tableau method. To formalize those agents that are able to introspect their own belief and certainty, we identify a subclass of interpreted $KBC$ systems, called introspective KBC systems. The validity problem for introspective KBC systems turns out to be co-NP complete, and is no harder than propositional logic. We also give a sound and complete proof system with respect to the introspective KBC systems.
 
Kaile Su, Abdul Sattar, Kewen Wang, Xiangyu Luo, Guido Governatori, and Vineet Nair.
The observation-based model for BDI-agents. In Proceedings of AAAI 2005In print. AAAI Press, 2005. Copyright © 2005. AAAI Press, 2005, pp. 190-195. Copyright © 2005, AAAI, American Association for Artificial Intelligence.
Abstract:We present a new computational model of BDI-agents, called the observation-based BDI-model. The key point of this BDI-model is to express agents' beliefs, desires and intentions as a set of runs (computing paths), which is exactly a system in the interpreted system model, a well-known agent model due to Halpern and his colleagues. Our BDI-model is computationally grounded in that we are able to associate the BDI-agent model with a computer program, and formulas, involving agents' beliefs, desires (goals) and intentions, can be understood as properties of program computations. We present a sound and complete proof system with respect to our BDI-model and explore how symbolic model checking techniques can be applied to model checking BDI-agents. In order to make our BDI-model more flexible and practically realistic, we generalize it so that agents can have multiple sources of beliefs, goals and intentions.
 
Kaile Su, Abdul Sattar, Kewen Wang, and Guido Governatori.
Computationally grounded model of {BDI}-agents. Proceedings of IJCAI'05, 30 July - 3 August 2005, pp. 1581-1582. Copyright © 2005 IJCAI.
Abstract:We introduce a multimodal logic of belief, desire and intention, called OBDI logic, where the changes and computation of agents' beliefs, desires, and desires are based on agents' observations (i.e. local states), and we propose a model checking techniques for the logic based on interpreted systems.