Deciding characteristic formulae: A journey in the branching-time spectrum
Abstract
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek's branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become (co)NP- or PSPACE-complete.
Keywords
Cite
@article{arxiv.2505.22277,
title = {Deciding characteristic formulae: A journey in the branching-time spectrum},
author = {Luca Aceto and Antonis Achilleos and Aggeliki Chalki and Anna Ingolfsdottir},
journal= {arXiv preprint arXiv:2505.22277},
year = {2026}
}
Comments
This paper combines and extends the results presented in two conference articles, which appeared at CSL 2025 and GandALF 2025. arXiv admin note: text overlap with arXiv:2405.13697, arXiv:2509.14089