Preference relations are at the heart of many fundamental concepts in artificial intelligence, ranging from utility comparisons, to defeat among strategies and relative plausibility among states, just to mention a few. Reasoning about such relations has been the object of extensive research and a wealth of formalisms exist to express and reason about them. One such formalism is conditional logic, which focuses on reasoning about the “best” alternatives according to a given preference relation. A “best” alternative is normally interpreted as an alternative that is either maximal (no other alternative is preferred to it) or optimal (it is at least as preferred as all other alternatives). And the preference relation is normally assumed to satisfy strong requirements (typically transitivity and some kind of well-foundedness assumption). Here, we generalize this existing literature in two ways. Firstly, in addition to maximality and optimality, we consider two other interpretations of “best”, which we call unmatchedness and acceptability. Secondly, we do not inherently require the preference relation to satisfy any constraints. Instead, we allow the relation to satisfy any combination of transitivity, totality and anti-symmetry. This allows us to model a wide range of situations, including cases where the lack of constraints stems from a modeled agent being irrational (for example, an agent might have preferences that are neither transitive nor total nor anti-symmetric) or from the interaction of perfectly rational agents (for example, a defeat relation among strategies in a game might be anti-symmetric but not total or transitive). For each interpretation of “best” (maximal, optimal, unmatched or acceptable) and each combination of constraints (transitivity, totality and/or anti-symmetry), we study the sets of valid inferences. Specifically, in all but one case we introduce a sound and strongly complete axiomatization, and in the one remaining case we show that no such axiomatization exists.

We combine social balance theory with temporal logic to obtain a Logic of Allies and Enemies (LAE), which formally describes the likely changes to a social network due to social pressure. We demonstrate how the rich language of LAE can be used to describe various interesting concepts, and show that both model checking and validity checking are PSPACE-complete.

Well-behaved preferences (e.g., total pre-orders) are a cornerstone of several areas in artificial intelligence, from knowledge representation, where preferences typically encode likelihood comparisons, to both game and decision theories, where preferences typically encode utility comparisons. Yet weaker (e.g., cyclical) structures of comparison have proven important in a number of areas, from argumentation theory to tournaments and social choice theory. In this paper we provide logical foundations for reasoning about this type of preference structures where no obvious best elements may exist. Concretely, we compare and axiomatize a number of ways in which the concepts of maximality and optimality can be generalized in this general class of preferences. We thereby expand the scope of the long-standing tradition of the logical analysis of preference.

International audience

In this contribution we present arbitrary arrow update model logic (AAUML). This is a dynamic epistemic logic or update logic. In update logics, static/basic modalities are interpreted on a given relational model whereas dynamic/update modalities induce transformations (updates) of relational models. In AAUML the update modalities formalize the execution of arrow update models, and there is also a modality for quantification over arrow update models. Arrow update models are an alternative to the well-known action models. We provide an axiomatization of AAUML. The axiomatization is a rewrite system allowing to eliminate arrow update modalities from any given formula, while preserving truth. Thus, AAUML is decidable and equally expressive as the base multi-agent modal logic. Our main result is to establish arrow update synthesis: if there is an arrow update model after which φ, we can construct (synthesize) that model from φ. We also point out some pregnant differences in update expressivity between arrow update logics, action model logics, and refinement modal logic.

This special issue of the Journal of Logic and Computation contains a selection of papers presented at the 11th Conference on Logic and the Foundations of the Theory of Games and Decisions (LOFT11), which took place in Bergen (Norway), July 27–30, 2014. 1 LOFT11 marked 20 years of LOFT conferences: the first conference took place in 1994 in Marseille (France) and, since then, LOFT has become a regular bi-annual event. 2 The LOFT conferences are interdisciplinary events that bring together researchers from a variety of fields: cognitive psychology, computer science and artificial intelligence, economics, game theory, linguistics, logic, mind sciences, philosophy and social choice. In its original conception, LOFT had as its central theme the application of logic, in particular modal epistemic logic, to foundational issues in the theory of games and individual decision-making. Epistemic considerations have been central to game theory for a long time. The expression ‘interactive epistemology’ has been used in the game-theory literature to refer to the analysis of strategic interaction based on an explicit modelling of the players' beliefs about each other's beliefs and rationality. The LOFT conferences arose from the realization that the tools and methodology that were used in game theory were closely related to those used in other fields, notably computer science, logic and philosophy. Modal logic turned out to be the common language that made it possible to bring together different professional communities.

Abstract We develop a logic for reasoning about semi-public environments , i.e. environments in which a process is executing, and where agents in the environment have partial and potentially different views of the process. Previous work on this problem illustrated that it was problematic to obtain both an adequate semantic model and a language for reasoning about semi-public environments. We here use program models for representing the changes that occur during the execution of a program. These models serve both as syntactic objects and as semantic models, and are a modification of action models in Dynamic Epistemic Logic, in the sense that they allow for ontic change (i.e. change in the world or state). We show how program models can elegantly capture a notion of observation of the environment. The use of these models resolves several difficulties identified in earlier work, and admit a much simpler treatment than was possible in previous work on semi-public environments.

We provide an in-depth study of the knowledge-theoretic aspects of communication in so-called gossip protocols. Pairs of agents communicate by means of calls in order to spread information—so-called secrets—within the group. Depending on the nature of such calls knowledge spreads in different ways within the group. Systematizing existing literature, we identify 18 different types of communication, and model their epistemic effects through corresponding indistinguishability relations. We then provide a classification of these relations and show its usefulness for an epistemic analysis in presence of different communication types. Finally, we explain how to formalise the assumption that the agents have common knowledge of a distributed epistemic gossip protocol.

This special issue of the Journal of Logic and Computation contains revised and extended versions of selected papers from LORI-5, the 5th International Workshop on Logic, Rationality and Interaction. LORI-5 was held during 28–31 October 2015, in Taipei, Taiwan, and hosted by the Department of Philosophy of National Taiwan University and the Institute of Philosophy of Mind and Cognition of National Yang-Ming University. The hallmark of the LORI series is its broad topical coverage, putting logic into contact with disciplines as diverse as game theory and decision theory, philosophy and epistemology, linguistics, computer science and artificial intelligence. In the current special issue, the reader will find several mainstays of the LORI series: modal and epistemic logics, theories of learning and argumentation, and pure logic. Out of 62 original submissions to LORI-5, 32 full papers were selected for presentation based on reviews by at least two—and on average three—members of the LORI-5 program committee. After the workshop, the authors of 20 of the full papers were invited to submit extended versions of their papers to be considered for either the present special issue or a parallel special issue of the journal Synthese. Each of the 10 papers considered for this special issue underwent review by two or three referees, leading to at least one—and in some cases two or three—rounds of revision. The final products are the nine papers collected in this issue. As an overview of its contents, below we provide a brief summary of each paper (in alphabetical order by author’s last name).

In this paper we attempt to shed light on the concept of an agent’s knowledge after a non-deterministic action is executed. We start by making a comparison between notions of non-deterministic choice, and between notions of sequential composition, of settings with dynamic and/or epistemic character; namely Propositional Dynamic Logic (PDL), Dynamic Epistemic Logic (DEL), and the more recent logic of Semi-Public Environments (SPE). These logics represent two different approaches for defining the aforementioned actions, and in order to provide unified frameworks that encompass both, we define the logics DELVO (DEL+Vision+Ontic change) and PDLVE (PDL+Vision+Epistemic operators). DELVO is given a sound and complete axiomatisation.

Abstract We consider the problem of decomposing a group norm into a set of individual obligations for the agents comprising the group, such that if the individual obligations are fulfilled, the group obligation is fulfilled. Such an assignment of tasks to agents is often subject to additional social or organizational norms that specify permissible ways in which tasks can be assigned. An important role of social norms is that they can be used to impose ‘fairness constraints’, which seek to distribute individual responsibility for discharging the group norm in a ‘fair’ or ‘equitable’ way. We propose a simple language for this kind of fairness constraints and analyse the problem of computing a fair decomposition of a group obligation, both for non-repeating and for repeating group obligations.

This paper is aimed as a contribution to the use of formal modal languages in Artificial Intelligence. We introduce a multi-modal version of Second-order Propositional Modal Logic (SOPML), an extension of modal logic with propositional quantification, and illustrate its usefulness as a specification language for knowledge representation as well as temporal and spatial reasoning. Then, we define novel notions of (bi)simulation and prove that these preserve the interpretation of SOPML formulas. Finally, we apply these results to assess the expressive power of SOPML.

A well-studied phenomenon in network theory are optimal schedules to distribute information by one-to-one communication between nodes. One can take these communicative actions to be ‘telephone calls’, and this process of spreading information is known as gossiping [4]. It is typical to assume a global scheduler who simply executes a possibly non-deterministic protocol. Such a protocol can be seen as consisting of a sequence of instructions “first, agent a calls b, then c, next, d calls b ...”. We investigate epistemic gossip protocols, where an agent a will call another agent not because it is so instructed but based on its knowledge or ignorance of the factual information that is distributed over the network. Such protocols therefore don't need a central schedular, but they come at a cost: they may take longer to terminate than non-epistemic, globally scheduled, protocols. We describe various epistemic protocols, we give their logical properties, and we model them in a number of ways.

International audience

This article investigates the conjecture that agents who make decisions in scenarios where trust is important can benefit from the use of asocial structure, representing the social relationships that exist between agents. We propose techniques that can be used by agents to initially build and then progressively update such a structure in the light of experience. We describe an implementation of our techniques in the domain of the Agent ART testbed: we take two existing agents for this domain (“Simplet” and “Connected”) and compare their performance with versions that use our social structure (“SocialSimplet” and “SocialConnected”). We show that SocialSimplet and SocialConnected outperform their counterparts with respect to the quality of the interactions, the number of rounds won in a competition, and the total utility gained.

Proving that one language is more succinct than an-other becomes harder when the underlying seman-tics is stronger. We propose to use Formula-Size Games (as put forward by Adler and Immerman, 2003), games that are played on two sets of mod-els, and that directly link the length of play with the size of the formula. Using FSGs, we prove three succinctness results form-dimensional modal logic: (1) In system Km, a notion of ‘everybody knows ’ makes the resulting language exponentially more succinct form> 1 (2) In S5m, the same lan-guage becomes more succinct for m> 3 and (3) Public Announcement Logic is exponentially more succinct than S5m, if m> 3. The latter settles an open problem raised by Lutz, 2006. 1

This paper extends probabilistic dynamic epistemic logic from a finite setting to an infinite setting, by introducing σ-algebras to the probability spaces in the models. This may extend the applicability of the logic to a real world setting with infinitely many possible measurements. It is shown that the dynamics preserves desirable properties of measurability and that completeness of the proof system holds with the extended semantics.

We develop a model of normative systems, where roughly speaking the model is a transition-based system and a norm is the result of flagging some of the transitions as undesirable. We then use a language that is close to that of Computation Tree Logic to reason about such systems. We demonstrate how our framework facilitates to reason about the following three settings:

We present DCL-PC: a logic for reasoning about how the abilities of agents and coalitions of agents are altered by transferring control from one agent to another. The logical foundation of DCL-PC is CL-PC, a logic for reasoning about cooperation in which the abilities of agents and coalitions of agents stem from a distribution of atomic Boolean variables to individual agents -- the choices available to a coalition correspond to assignments to the variables the coalition controls. The basic modal constructs of DCL-PC are of the form `coalition C can cooperate to bring about phi'. DCL-PC extends CL-PC with dynamic logic modalities in which atomic programs are of the form `agent i gives control of variable p to agent j'; as usual in dynamic logic, these atomic programs may be combined using sequence, iteration, choice, and test operators to form complex programs. By combining such dynamic transfer programs with cooperation modalities, it becomes possible to reason about how the power of agents and coalitions is affected by the transfer of control. We give two alternative semantics for the logic: a `direct' semantics, in which we capture the distributions of Boolean variables to agents; and a more conventional Kripke semantics. We prove that these semantics are equivalent, and then present an axiomatization for the logic. We investigate the computational complexity of model checking and satisfiability for DCL-PC, and show that both problems are PSPACE-complete (and hence no worse than the underlying logic CL-PC). Finally, we investigate the characterisation of control in DCL-PC. We distinguish between first-order control -- the ability of an agent or coalition to control some state of affairs through the assignment of values to the variables under the control of the agent or coalition -- and second-order control -- the ability of an agent to exert control over the control that other agents have by transferring variables to other agents. We give a logical characterisation of second-order control.

We introduce a logic designed to support reasoning about social choice functions. The logic includes operators to capture strategic ability, and operators to capture agent preferences. We give a correspondence between formulae in the logic and properties of social choice functions, and show that the logic is expressively complete with respect to social choice functions, i.e., that every social choice function can be characterised as a formula of the logic. We show the decidability of the logic and give a complete axiomatization. To demonstrate the value of the logic, we show in particular how it can be applied to the problem of determining whether a social choice function is strategy-proof.

The Game Description Language (GDL) is a special purpose declarative language for defining games. GDL is used in the AAAI General Game Playing Competition, which tests the ability of computer programs to play games in general, rather than just the ability to play a specific game. Participants in the competition are provided with a previously unknown game specified in GDL, and are required to dynamically and autonomously determine how best to play this game. Recently, there has been much interest in the use of strategic cooperation logics for reasoning about game-like scenarios—the Alternating-time Temporal Logic (ATL) of Alur, Henzinger, and Kupferman is perhaps the best known example. Such logics are specifically intended to support reasoning about game-theoretic properties of multi-agent systems. In short, the aim of this article is to make a concrete link between ATL and GDL, with the ultimate goal of using ATL to reason about GDL-specified games. We make the following contributions. First, we demonstrate that GDL can be understood as a specification language for ATL models, and prove that the problem of interpreting ATL formulae over propositional GDL descriptions is EXPTIME-complete. Second, we use ATL to characterize a class of ‘fair playability’ conditions, which might or might not hold of various games.

We introduce ATLES - a variant of ATL with explicit names for strategies in the object language. ATLES makes it possible to refer to the same strategy in different occurrences of path quantifiers, and, as a consequence, it possible to express in ATLES some properties that cannot be expressed even in ATL*. We present a complete axiomatic system for ATLES. Moreover, we show that satisfiability problem for ATLES is no more complex than for ATL: it is ExpTime-complete. We identify two variants of the model-checking problem for ATLES and investigate their computational complexity. Finally, we show how ATLES can be used to reason about extensive games.

Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we use temporal logics of knowledge to reason about security protocols. We show how to specify part of the Needham-Schroeder protocol using temporal logics of knowledge and prove various properties using a clausal resolution calculus for this logic.

In this article we show how formal semantics can be given to reasoning processes in meta-level architectures that reason about (object level) knowledge states and effects changes may have on them. Especially, attention is focused on the upward and downward reflections in these architectures. Temporalized epistemic logic is used to specify meta-level reasoning processes and the outcomes of these. © 2003 Wiley Periodicals, Inc.

This paper proposes two methods for realising automated reasoning about agent-based systems. The framework for modelling intelligent agent behaviour that we focus on is a core of KARO logic, an expressive combination of various modal logics including propositional dynamic logic, a modal logic of knowledge, a modal logic of wishes, and additional non-standard operators. The first method we present is based on a translation of core KARO logic to first-order logic combined with first-order resolution. The second method uses an embedding of core KARO logic into a combination of branching-time temporal logic CTL and multi-modal S5 plus a clausal resolution calculus for these combined logics. We discuss the advantages and shortcomings of each approach and suggest ways to extend each variant to cover more of the KARO framework.

In this paper, we consider communication between agents that employ different vocabularies to represent information. In particular, we develop a communication mechanism in which translators between the vocabularies of agents are generated. Instead of being defined in advance, these translators are dynamically constructed during execution of the system, and are based both on the information that the agents exchange and on their underpinning ontologies. Moreover, these translators are not necessarily defined for the total vocabulary of the agents, but instead, only for the parts that have been involved in communication steps. The framework can for instance be used to study and to analyze experiments as performed in the research on the origins of language, like language games, in which the purpose of communication is to come to a mutual understanding of the agents' vocabularies. © 2001 John Wiley & Sons, Inc.

In this paper, we present a logical framework that combines modality with a first‐order variable‐binding mechanism. The logic, which belongs to the family of hybrid languages, differs from standard first‐order modal logics in that quantification is not performed inside the worlds of a model, but the worlds in the model themselves constitute the domain of quantification. The locality principle of modal logic is preserved via the condition that in each world, the domain of quantification is given by a subset of the entire set of worlds in the model. In comparison with standard hybrid languages, the logic covers separate mechanisms for navigation and for variable‐binding and formalizes reasoning about the worlds of a model in terms of equational logic. We show that the logic is semantically characterized by a generalization of classical bisimulation, called history‐based bisimulation, and study the application of the logic to describe and reason about network topologies.

We present a formal system to reason about and specify the behavior of multiple intelligent artificial agents. Essentially, each agent can perform certain actions, and it may possess a variety of information in order to reason about its and other agent's actions. Thus, our KARO-framework tries to deal formally with the notion of Knowledge, possessed by the agents, and their possible execution of actions. In particular, each agent may reason about its —or, alternatively, other's— Abilities to perform certain actions, the possible Results of such an execution and the availability of the Opportunities to take a particular action. Formally, we combine dynamic and epistemic logic into one modal system, and add the notion of ability to it. We demonstrate that there are several options to define the ability to perform a sequentially composed action, and we outline several properties under two alternative choices. Also, the agents' views on the correctness and feasibility of their plans are highlighted. Finally, the complications in the completeness proof for both systems indicate that the presence of abilities in the logic makes the use of infinite proof rules useful, if not inevitable.

We add a binary operator ≥ to the logical language, with intended meaning of φ<ψ: ‘φ is at least as likely, probable, or trustworthy, as ψ’. The operator ≥ is interpreted on Kripke structures, making it possible to define the standard necessity operator □ in terms of ≥. The operator ≥ provides us with an intermediate for the K-axiom, in the sense that we have both □(p→q)→(q≥p) and (q≥p)→(□p→□q). We discuss two semantics for this binary modal operator. It turns out that, as shown by Gärdenfors and Segerberg, ≥ is not only too weak to distinguish finite models from infinite ones or to distinguish countable additivity from finite additivity, ≥ also cannot distinguish sophisticated ways of assigning exact probabilities to events (‘measuring’) from the conceptually simpler task of just counting them.

In this paper we indicate how default logic can be based on epistemic logic, and particularly how we may employ Halpern & Moses' minimal epistemic states for this purpose. In this way we obtain a simple and natural S5-based logic for default reasoning that appears to be cumulative in the sense of Kraus, Lehmann and Magidor.

We survey results on axiomatic completeness and complexity of formal languages for reasoning about finite quantities. These languages are interpreted on domains with and without structure. Expressions dealt with include ‘at least n Xs are Ys,’ in the case of unstructured domains, and ‘at least n ’related‘ Xs are Ys,’ in the structured case. The results contained in this paper are brought together from generalized quantifier theory, modal logic, and knowledge representation, while a few new results are also included. A unifying approach is offered to the wide variety of formalisms available in the literature.

We investigate modal systems for knowledge and belief, taking as a starting point a logic that was originally introduced by Kraus and Lehmann. We derive several properties and discuss (their) consequences for the epistemic operators. Kraus and Lehmann observed that adding the axiom Biϕ → B1K1ϕ to the system gives a collapse of knowledge and belief: (K1ϕ ↔ Biϕ). We investigate the cause(s) of this problem and suggest a ‘similar’ system that does allow the same axiom without the mentioned collapse. We consider as the main benefit of this paper, however, the techniques that are developed to come to this solution. It appears that applying basic correspondence theory to a multi-modal system allows a systematic examination of possible combinations of epistemic operators.