When Are Prime Formulae Characteristic?
Luca Aceto, Dario Della Monica, Ignacio Fábregas, Anna Ingólfsdóttir
TL;DR
The paper develops general, sufficient conditions under which characteristic formulae for processes coincide with the class of consistent and prime formulae, thereby enabling model checking to be reduced to behavioural relation checks in a wide range of logics. It introduces the notion of decomposable logic and shows that, if a logic is decomposable, every consistent and prime formula is characteristic for some process; it then identifies two practical paths to decomposability: finite characterization and representation-based decomposition. The framework is applied to logics and semantics across van Glabbeek's linear-time/branching-time spectrum, including modal refinement and covariant-contravariant simulation, and extended to finitely-represented logics, establishing characterization by primality for these settings. The paper also discusses limitations, notably for conformance simulation, and outlines future directions to broaden the applicability of primality-based characterizations.
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 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.