Creating and sharing knowledge for telecommunications

Algebraic Kripke frames

on 25-01-2013


Manuel Martins, U Aveiro

January 25, 2013, Friday, 16h15m.

Abstract: 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.

Room: 3.10, Mathematics

Support: SQIG/Instituto de Telecomunicações with support from FCT and FEDER namely by the FCT project PEst-OE/EEI/LA0008/2011.

More Information..