The complexity of deciding characteristic formulae modulo nested simulation
Luca Aceto, Antonis Achilleos, Aggeliki Chalki, Anna Ingolfsdottir
TL;DR
The paper addresses the problem of deciding whether a modal formula is characteristic for some process under nested-simulation semantics by tying characteristic formulae to satisfiability and primality. It introduces two-player zero-sum tableau games, $\mathtt{charnse}$ and $\mathtt{primensp}$, to capture characteristic and primality properties and derives tight complexity bounds: $\mathsf{coNP}$-completeness for primality in the $2$-nested-simulation logic, $\mathsf{PSPACE}$-completeness for $n$-nested-simulation with $n\ge3$, and $\mathsf{DP}$ containment for the $2$-nested-simulation characteristic problem. These results extend the understanding of the complexity landscape of modal characterizations in the nested-simulation spectrum and provide concrete algorithms (via the two game families) to decide characteristic and primality questions. The findings have implications for reductions between process equivalence checks and model checking in the nested-simulation setting, especially when the action set is not fixed and logics are varied across the spectrum. Overall, the work delineates precise computational boundaries for characteristic formulae in nested-simulation semantics and offers a solid, game-theoretic method to achieve these bounds.
Abstract
This paper studies the complexity of determining whether a formula in the modal logics characterizing the nested-simulation semantics is characteristic for some process, which is equivalent to determining whether the formula is satisfiable and prime. The main results are that the problem of determining whether a formula is prime in the modal logic characterizing the 2-nested-simulation preorder is CoNP-complete and is PSPACE-complete in the case of the n-nested-simulation preorder, when n>= 3. This establishes that deciding characteristic formulae for the n-nested simulation semantics, n>= 3, is PSPACE-complete. In the case of the 2-nested simulation semantics, that problem lies in the complexity class DP, which consists of languages that can be expressed as the intersection of one language in NP and of one in CoNP.