RT Journal Article
T1 When are prime formulae characteristic?
A1 Aceto, Luca
A1 Della Monica, Dario
A1 Fábregas, Ignacio
A1 Ingólfsdóttir, Anna
A1 Fábregas Alfaro, Ignacio
AB 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 various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek’s linear time-branching time spectrum.
SN 1879-2294
YR 2018
FD 2018
LK https://hdl.handle.net/20.500.14352/98254
UL https://hdl.handle.net/20.500.14352/98254
LA eng
NO L. Aceto, D. Della Monica, I. Fábregas, A. Ingólfsdóttir, When are prime formulae characteristic?, Theoretical Computer Science 777 (2019) 3–31. https://doi.org/10.1016/j.tcs.2018.12.004.
DS Docta Complutense
RD 27 mar 2026