Reasoning about knowledge and messages in asynchronous multi-agent systems

Sophia Knight, Bastien Maubert, François Schwarzentruber

Research output: Contribution to journalArticlepeer-review

4 Scopus citations

Abstract

We propose a variant of public announcement logic for asynchronous systems. To capture asynchrony, we introduce two different modal operators for sending and receiving messages. The natural approach to defining the semantics leads to a circular definition, but we describe two restricted cases in which we solve this problem. The first case requires the Kripke model representing the initial epistemic situation to be a finite tree, and the second one only allows announcements from the existential fragment. After establishing some validities, we study the model checking problem and the satisfiability problem in cases where the semantics is well-defined, and we provide several complexity results.

Original languageEnglish (US)
Pages (from-to)127-168
Number of pages42
JournalMathematical Structures in Computer Science
Volume29
Issue number1
DOIs
StatePublished - Jan 1 2019
Externally publishedYes

Bibliographical note

Publisher Copyright:
Copyright © Cambridge University Press 2017.

Fingerprint

Dive into the research topics of 'Reasoning about knowledge and messages in asynchronous multi-agent systems'. Together they form a unique fingerprint.

Cite this