IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2017 > Logics for Process Semantics
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Ignacio Fabregas

jueves 9 de marzo de 2017

11:00am Meeting room 302 (Mountain View), level 3

Ignacio Fabregas, Post-doctoral Researcher, Universidad Complutense de Madrid, Spain

Logics for Process Semantics


In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed in 1992 that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones.

This talk present the extension of that classical result from a purely logical point of view, but with an eye over the behavioural preorders in van Glabbeek’s linear-time branching-time spectrum. It will be shown general and sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones will be shown. As a first step towards the general result, the property is translated to the scenario of covariant-contravariant simulations over label transition systems. Finally, there will be a look into a promising direction that the speaker is exploring based in one recent paper of Legay and Fahrenberg also inspired by the foundational paper of Boudol and Larsen.