A public announcement separation logic
Jean-René Courtault, Hans van Ditmarsch, Didier Galmiche · Mathematical Structures in Computer Science · 2019
Abstract 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.