On infinitary equational hybrid logic

Abstract

Recon gurable software systems behave di erently in di erent modes of operation and commute between them along their lifetime. Such di erent behaviours can be modelled by a transition system, to express the overall system's dynamics, but with structured states to capture local properties. We take this path in this paper by endowing states in standard Kripke frames with algebras, each of them modelling a local con guration. An equational hybrid logic, with infinitary formulas, is proposed to express a broad range of properties of those structures, including liveness requirements. The paper develops a number of results on its semantics, including suitable notions of simulation and bisimulation.