Reconfigurable systems behave differently in different modes of operation and commute between them along their lifetime. Such different behaviours can be modelled by imposing some sort of structure upon states in a transition system expressing the overall system's dynamics. We take this approach by endowing states in standard Kripke frames with algebras, each of them modelling a local configuration. An equational hybrid logic, admitting infinitary formulae, is proposed to express a broad range of properties of those structures, including liveness requirements. The paper also develops a number of preliminary results on its semantics, including a discussion of a suitable notion of bisimulation by generalizing standard invariance results to this broad setting.

The talk reports on ongoing joint work with Luís S. Barbosa and A. Madeira.