Laboratoire d'informatique de l'École polytechnique

Talk by Ignacio Fábregas: «When Are Prime Formulae Characteristic?»

Speaker: Ignacio Fábregas
Location: Room Grace Hopper, Alan Turing building
Date: Mon, 13 Mar 2017, 15:30-16:30

Abstract: In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed 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 paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to the logics characterizing all the semantics in van Glabbeek's branching-time spectrum.