The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum

TL;DR

This paper analyzes the computational complexity of determining and constructing characteristic formulae in modal logics that describe behavioural semantics in van Glabbeek's spectrum, highlighting boundaries between tractable and hard problems.

Contribution

It provides complexity results for satisfiability and primality of characteristic formulae, and explores the difficulty of constructing these formulae in various modal logics.

Findings

Complexity results for satisfiability and primality problems.

Identification of modal logics where these problems are polynomial-time solvable.

Analysis of the complexity of constructing characteristic formulae explicitly and via systems of equations.

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 finite, loop-free 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 consistent and prime ones, it 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 computationally hard. Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.