Reasoning About Connector Reconfiguration II: Basic Reconfiguration Logic

Software systems evolve over time. To facilitate this, the coordination language Reo offers operations to dynamically reconfigure the topology of component connectors. We present a semantics of Reo in the presence of reconfiguration, and a logic, and its model checking algorithm, for reasoning about connector behaviour in this setting.