判定特征公式：分支时间谱中的探索

特征公式给出了进程在某种选定的行为语义概念下行为的完整逻辑描述。它们允许将等价或预序检查归约为模型检测，并且恰好是刻画经典行为等价和预序的模态逻辑中的公式，对这些公式模型检测可以归约为等价或预序检查。本文研究了在 van Glabbeek 分支时间谱中为基于模拟的语义提供模态刻画的每种逻辑中，判定一个公式是否为某个进程的特征公式的复杂度。由于这些逻辑中的特征公式恰好是可满足且素公式，本文给出了可满足性和素性问题的复杂度结果，并探讨了可在多项式时间内求解这些问题与变为（co）NP 完全或 PSPACE 完全的模态逻辑之间的边界。