An Epistemic Separation Logic with Action Models
Résumé
In this paper we generalize the dynamic aspects of Public Announcement Separation Logic (PASL), by defining Epistemic Separation Logic with Action Models (ESLAM), in which we replace public announcements with action models, motivated by their ability to model factual change, and instances of a more nuanced, private communication.