We propose communication pattern logic. A communication pattern describes how processes or agents inform each other, independently of the information content. The full-information protocol in distributed computing is the special case wherein all agents inform each other. We study this protocol in distributed computing models where communication might fail: an agent is certain about the messages it receives, but it may be uncertain about the messages other agents have received. In a dynamic epistemic logic with distributed knowledge and with modalities (...) for communication patterns, the latter are interpreted by updating Kripke models. We propose an axiomatization of communication pattern logic, and we show that collective bisimilarity (comparing models on their distributed knowledge) is preserved when updating models with communication patterns. We can also interpret communication patterns by updating simplicial complexes, a well-known topological framework for distributed computing. We show that the different semantics correspond, and propose collective bisimulation between simplicial complexes. (shrink)

In this paper, we propose a dynamic epistemic framework to capture the knowledge evolution in multi-agent systems where agents are not able to observe. We formalize multi-agent conformant planning with group knowledge, and reduce planning problems to model checking problems. We prove that multi-agent conformant planning with group knowledge is Pspace -complete on the size of dynamic epistemic models. We also consider the alternative Kripke semantics, and show that for each Kripke model with perfect recall and no miracles, there is (...) an equivalent dynamic epistemic model and vice versa. (shrink)

We study classical modal logics with pooling modalities, i.e. unary modal operators that allow one to express properties of sets obtained by the pointwise intersection of neighbourhoods. We discuss salient properties of these modalities, situate the logics in the broader area of modal logics, establish key properties concerning their expressive power, discuss dynamic extensions of these logics and provide reduction axioms for the latter.

We study the logic of so-called lexicographic or priority merge for multi-agent plausibility models. We start with a systematic comparison between the logical behavior of priority merge and the more standard notion of pooling through intersection, used to define, for instance, distributed knowledge. We then provide a sound and complete axiomatization of the logic of priority merge, as well as a proof theory in labeled sequents that admits cut. We finally study Moorean phenomena and define a dynamic resolution operator for (...) priority merge for which we also provide a complete set of reduction axioms. (shrink)

Coalition announcement logic is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.

M. B. Hintikka and J. Hintikka claimed that their reconstruction of the ‘Sherlock Holmes sense of deduction’ can “serve as an explication for the link between intelligence and memory”. The claim is vindicated, first for the single-agent case, where the reconstruction captures strategies for accessing the content of a distributed and associative memory; then, for the multi-agent case, where the reconstruction captures strategies for accessing knowledge distributed in a community. Moreover, the reconstruction of the ‘Sherlock Holmes sense of deduction’ allows (...) to conceptualize those strategies as belonging to a continuum of behavioral strategies. (shrink)

There are several ways to quantify over public announcements. The most notable are reflected in arbitrary, group, and coalition announcement logics, with the latter being the least studied so far. In the present work, we consider coalition announcements through the lens of group announcements, and provide a complete axiomatisation of a logic with coalition announcements. To achieve this, we employ a generalisation of group announcements. Moreover, we study some logical properties of both coalition and group announcements that have not been (...) studied before. (shrink)

Public announcement logic is an extension of epistemic logic with dynamic operators that model the effects of all agents simultaneously and publicly acquiring the same piece of information. One of the extensions of PAL, group announcement logic, allows quantification over announcements made by agents. In GAL, it is possible to reason about what groups can achieve by making such announcements. It seems intuitive that this notion of coalitional ability should be closely related to the notion of distributed knowledge, the implicit (...) knowledge of a group. Thus, we study the extension of GAL with distributed knowledge, and in particular possible interaction properties between GAL operators and distributed knowledge. The perhaps surprising result is that, in fact, there are no interaction properties, contrary to intuition. We make this claim precise by providing a sound and complete axiomatisation of GAL with distributed knowledge. We also consider several natural variants of GAL with distributed knowledge, as well as some other related logic, and compare their expressive power. (shrink)