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.

翻译：特征公式为进程行为提供了关于所选行为语义概念的完整逻辑描述。它们使得等价性或预序检查可归约为模型检测，并且恰好是那些模态逻辑中的公式——这些逻辑刻画了经典行为等价与预序——对于这些公式，模型检测可归约为等价性或预序检查。本文研究了在范格拉贝克分支时间谱中，为基于模拟的语义提供模态刻画的各个逻辑里，判定一个公式是否为某个有限无环进程的特征公式的复杂性。由于在这些逻辑中，特征公式恰好是一致且本原的公式，本文给出了可满足性与本原性问题的复杂性结果，并探讨了这些问题可在多项式时间内解决的模态逻辑与那些计算困难的模态逻辑之间的界限。除其他贡献外，本文还研究了在刻画基于模拟语义的模态逻辑中构建特征公式的复杂性，包括以显式形式和通过方程组呈现这些公式的情况。