Some Institutional Requirements for Temporal Reasoning on Dynamic Reconfiguration of Component Based Systems

We study a logic adapted for the purpose of specifying component based systems with support for run time reconfiguration. In particular, we analyse some institutional properties of this logic, related to compositional reasoning in specifications.The logic is an adaptation of the Manna-Pnueli logic, a first-order temporal logic originally proposed to describe reactive systems. We present our variant in detail, and motivate the required extensions by showing how reconfigurable systems can be specified and how reasoning can be carried out in the presence of these properties. Some issues regarding the use of STeP for proof support are discussed.