Wiebe Van Der Hoek

This contribution is a gentle introduction to so-called dynamic epistemic logics, that can describe how agents change their knowledge and beliefs. We start with a concise introduction to epistemic logic, through the example of one, two and finally three players holding cards; and, mainly for the purpose of motivating the dynamics, we also very summarily introduce the concepts of general and common knowledge. We then pay ample attention to the logic of public announcements, wherein agents change their knowledge as the result of, indeed, public announcements. One crucial topic in that setting is that of unsuccessful updates: formulas that become false when announced. The Moore-sentences that were already extensively discussed at the conception of epistemic logic in [15] give rise to such unsuccessful updates. After that, we present a few examples of more complex epistemic updates. Our closing observations are on recent developments that link the ‘standard’ topic of (theory) belief revision [1] to the dynamic epistemic logics introduced here.

FoLLI-LNCS is the publication platform for the Association of Logic, Language and Information. The Association was founded in 1991 to advance research and education on the interface between logic, linguistics, computer science, and cognitive science. The FoLLI Publications on Logic, Language and Information aim to disseminate results of cutting-edge research and tutorial materials in these interdisciplinary areas. This LNCS volume is part of FoLLi book serie and contains the papers presented at the 5th International Workshop on Logic, Rationality and Interaction/, held in October 2015 in Taipei, Taiwan. The topics covered in this program well represent the span and depth that hasby now become a trademark of the LORI workshop series, where logic interfaceswith disciplines as diverse as game theory and decision theory, philosophyand epistemology, linguistics, computer science and artificial intelligence.

Understanding the flow of knowledge in multi-agent protocols is essential when proving the correctness or security of such protocols. Current logical approaches, often based on model checking, are well suited for modeling knowledge in systems where agents do not act strategically. Things become more complicated in strategic settings. In this paper we show that such situations can be understood as a special type of game – a knowledge condition game – in which a coalition “wins” if it is able to bring about some epistemic condition. This paper summarizes some results relating to these games. Two proofs are presented for the computational complexity of deciding whether a coalition can win a knowledge condition game with and without opponents (Σ2P-complete and NP-complete respectively). We also consider a variant of knowledge condition games in which agents do not know which strategies are played, and prove that under this assumption, the presence of opponents does not affect the complexity. The decision problem without opponents is still NP-complete, but requires a different proof.

We define a multi-modal version of Computation Tree Logic (ctl) by extending the language with path quantifiers E δ and A δ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a ctl axiomatisation for each dimension. Completeness is proved by employing the completeness result for ctl to obtain a model along each dimension in turn. We also show that the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional ctl logic.

We add a limited but useful form of quantification to Coalition Logic, a popular formalism for reasoning about cooperation in game-like multi-agent systems. The basic constructs of Quantified Coalition Logic (QCL) allow us to express such properties as “every coalition satisfying property P can achieve φ” and “there exists a coalition C satisfying property P such that C can achieve φ”. We give an axiomatisation of QCL, and show that while it is no more expressive than Coalition Logic, it is nevertheless exponentially more succinct. The complexity of QCL model checking for symbolic and explicit state representations is shown to be no worse than that of Coalition Logic, and satisfiability for QCL is shown to be no worse than satisfiability for Coalition Logic. We illustrate the formalism by showing how to succinctly specify such social choice mechanisms as majority voting, which in Coalition Logic require specifications that are exponentially long in the number of agents.

We demonstrate ways to incorporate nondeterminism in a system designed to formalize the reasoning of agents concerning their abilities and the results of the actions that they may perform. We distinguish between two kinds of nondeterministic choice operators: one that expresses an internal choice, in which the agent decides what action to take, and one that expresses an external choice, which cannot be influenced by the agent. The presence of abilities in our system is the reason why the usual approaches towards nondeterminism cannot be used here. The semantics that we define for nondeterministic actions is based on the idea that composite actions are unravelled in the strings of atomic actions and tests that constitute them. The main notions used in defining this semantics are finite computation sequences and finite computation runs of actions. The results that we obtain meet our intuitions regarding events and abilities in the presence of nondeterminism.

We add a limited but useful form of quantification to Coalition Logic, a popular formalism for reasoning about cooperation in game-like multi-agent systems. The basic constructs of Quantified Coalition Logic (QCL) allow us to express such properties as "every coalition satisfying property P can achieve φ" and "there exists a coalition C satisfying property P such that C can achieve φ". We give an axiomatisation of QCL, and show that while it is no more expressive than Coalition Logic, it is nevertheless exponentially more succinct. The complexity of QCL model checking for symbolic and explicit state representations is shown to be no worse than that of Coalition Logic, and satisfiability for QCL is shown to be no worse than satisfiability for Coalition Logic. We illustrate the formalism by showing how to succinctly specify such social choice mechanisms as majority voting, which in Coalition Logic require specifications that are exponentially long in the number of agents

We define a multi-modal version of Computation Tree Logic (CTL) by extending the language with path quantifiers $E^\delta $ and $E^\delta $ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a CTL axiomatisation for each dimension. Completeness is proved by employing the completeness result for CTL to obtain a model along each dimension in turn. We also show that the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for CTL. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional CTL logic.

Rational agents are important objects of study in several research communities, including economics, philosophy, cognitive science, and most recently computer science and artificial intelligence. Crudely, a rational agent is an entity that is capable of acting on its environment, and which chooses to act in such a way as to further its own best interests. There has recently been much interest in the use of mathematical logic for developing formal theories of such agents. Such theories view agents as practical reasoning systems, deciding moment by moment which action to perform next, given the beliefs they have about the world and their desires with respect to how they would like the world to be. In this article, we survey the state of the art in developing logical theories of rational agency. Following a discussion on the dimensions along which such theories can vary, we briefly survey the logical tools available in order to construct such theories. We then review and critically assess three of the best known theories of rational agency: Cohen and Levesque's intention logic, Rao and Georgeff's BDI logics, and the KARO framework of Meyer et al. We then discuss the various roles that such logics can play in helping us to engineer rational agents, and conclude with a discussion of open problems

Modal logics have proven to be a very successful tool for reasoning about games. However, until now, although logics have been put forward for games in both normal form and games in extensive form, and for games with complete and incomplete information, the focus in the logic community has hitherto been on games with pure strategies. This paper is a first to widen the scope to logics for games that allow mixed strategies. We present a modal logic for games in normal form with mixed strategies, and demonstrate its soundness and strong completeness. Characteristic for our logic is a number of infinite rules

We study several modal languages in which some (sets of) generalized quantifiers can be represented; the main language we consider is suitable for defining any first order definable quantifier, but we also consider a sublanguage thereof, as well as a language for dealing with the modal counterparts of some higher order quantifiers. These languages are studied both from a modal logic perspective and from a quantifier perspective. Thus the issues addressed include normal forms, expressive power, completeness both of modal systems and of systems in the quantifier tradition, complexity as well as syntactic characterizations of special semantic constraints. Throughout the paper several techniques current in the theory of generalized quantifiers are used to obtain results in modal logic, and conversely.

We propose an epistemic logic in which knowledge is fully introspective and implies truth, although truth need not imply epistemic possibility. The logic is presented in sequential format and is interpreted in a natural class of partial models, called balloon models. We examine the notions of honesty and circumscription in this logic: What is the state of an agent that only knows and which honest enable such circumscription? Redefining stable sets enables us to provide suitable syntactic and semantic criteria for honesty. The rough syntactic definition of honesty is the existence of a minimal stable expansion, so the problem resides in the ordering relation underlying minimality. We discuss three different proposals for this ordering, together with their semantic counterparts, and show their effects on the induced notions of honesty

We present an epistemic default logic, based on the metaphore of a meta-level architecture. Upward reflection is formalized by a nonmonotonic entailment relation, based on the objective facts that are either known or unknown at the object level. Then, the meta (monotonic) reasoning process generates a number of default-beliefs of object-level formulas. We extend this framework by proposing a mechanism to reflect these defaults down. Such a reflection is seen as essentially having a temporal flavour: defaults derived at the meta-level are projected as facts in a next object level state. In this way, we obtain temporal models for default reasoning in meta-level formalisms which can be conceived as labeled branching trees. Thus, descending the tree corresponds to shifts in time that model downward reflection, whereas the branching of the tree corresponds to ways of combining possible defaults. All together, this yields an operational or procedural semantics of reasoning by default, which admits one to reason about it by means of branching-time temporal logic. Finally, we define sceptical and credulous entailment relations based on these temporal models and we characterize Reiter extensions in our semantics.

Qualitative Coalitional Games are a variant of coalitional games in which an agent's desires are represented as goals that are either satisfied or unsatisfied, and each choice available to a coalition is a set of goals, which would be jointly satisfied if the coalition made that choice. A coalition in a QCG will typically form in order to bring about a set of goals that will satisfy all members of the coalition. Our goal in this paper is to develop and study logics for reasoning about QCGs. We begin by introducing a logic for reasoning about “static” QCGs, where participants play a single game, and we then introduce and study Temporal QCGs, i.e., games in which a sequence of QCGs is played. In order to represent and reason about such games, we introduce a linear time temporal logic of QCGs, called ℒ. We give a complete axiomatisation of ℒ, use it to investigate the properties of TQCGs, identify its expressive power, establish its complexity, characterise classes of TQGCs with formulas from our logical language, and use it to formulate several solution concepts for TQCGs.