Deciding characteristic formulae: A journey in the branching-time spectrum
This work addresses complexity boundaries in modal logics for process behavior, which is incremental as it extends existing theoretical frameworks without broad practical impact.
The paper studies the computational complexity of determining whether a formula is characteristic for a process in modal logics that characterize simulation-based semantics in van Glabbeek's branching-time spectrum, finding that these problems range from polynomial-time solvable to (co)NP- or PSPACE-complete.
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.