A public announcement separation logic - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2019

A public announcement separation logic

J.R. Courtault
  • Fonction : Auteur
D. Galmiche

Résumé

We define a Public Announcement Separation Logic (PASL) that allows us to consider epistemic possible worlds as resources that can be shared or separated, in the spirit of separation logics. After studying its semantics and illustrating its interest for modelling systems, we provide a sound and complete tableau calculus that deals with resource, agent and announcement constraints and give also a countermodel extraction method.
Fichier non déposé

Dates et versions

hal-02387377 , version 1 (29-11-2019)

Identifiants

Citer

J.R. Courtault, Hans van Ditmarsch, D. Galmiche. A public announcement separation logic. Mathematical Structures in Computer Science, 2019, 29 (06), pp.828-871. ⟨10.1017/S0960129518000348⟩. ⟨hal-02387377⟩
28 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More