Deciding characteristic formulae: A journey in the branching-time spectrum

TL;DR

This paper explores the complexity of identifying characteristic formulae in modal logics that describe process behaviors within the branching-time spectrum, focusing on satisfiability and primality problems.

Contribution

It provides complexity classifications for satisfiability and primality problems across various modal logics in the branching-time spectrum, highlighting computational boundaries.

Findings

Satisfiability and primality problems vary in complexity across different logics.

Polynomial-time solutions exist for some logics, while others are coNP- or PSPACE-complete.

The paper delineates the boundary between tractable and intractable modal logics.

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.