Abstract | ||
---|---|---|
We propose a variant of public announcement logic for asynchronous systems. We give a syntax where sending and receiving messages are modeled by different modal operators. 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. Finally, we provide complexity results for the model checking problem. |
Year | DOI | Venue |
---|---|---|
2015 | 10.1007/978-3-319-25150-9_17 | International Colloquium on Theoretical Aspects of Computing |
Field | DocType | Volume |
Discrete mathematics,Asynchronous communication,Model checking,Computer science,Communication channel,Modal operator,Natural approach,Theoretical computer science,Circular definition,Syntax,Semantics | Conference | 9399 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.35 |
References | Authors | |
7 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Sophia Knight | 1 | 32 | 4.49 |
Bastien Maubert | 2 | 45 | 14.64 |
François Schwarzentruber | 3 | 170 | 29.05 |