A modal separation logic for resource dynamics

摘要

The logic of Bunched implications (BI), and its Boolean version (Boolean BI), are logics that allow us to express properties on resources and to provide logical frameworks for the so-called separation logics. In this article, we study a new modal separation logic that extends Boolean BI with two kinds of modalities, to deal with resources having dynamic properties (which depend on the current state of a system) and also to capture some resource evolutions or transformations. We show how we can model concurrent processes manipulating resources, and we provide a sound and complete tableau calculus, with a counter-model extraction method, for proving properties expressed in this logic.