Dynamic Reconfiguration via Typed Modalities

Modern software systems are increasingly exhibiting dynamic-reconfiguration features analogous to naturally occurring phenomena where the architecture of a complex changes dynamically, at run time, on account of interactions between its components. This has led to a renewed interest in modal logics for formal system development, building on the intuitive idea that system configurations can be regarded as local models of a Kripke structure, while reconfigurations are captured by accessibility relations. We contribute to this line of research by advancing a modal logic with varying quantification domains that employs typed modalities and dedicated modal operators to specify and reason about a new generation of Kripke structures, called dynamic networks of interactions, that account for the context of a system’s dynamics, identifying which actants have triggered a reconfiguration and what are its outcomes. To illustrate the expressiveness of the formalism, we provide a specification of the biological process of membrane budding, which we then analyse using a sound and complete proof-by-translation method that links dynamic networks of interactions with partial first-order logic.