判定 van Glabbeek 分支时间谱中特征公式的复杂度

特征公式给出了过程在某种行为语义下行为的完整逻辑描述。它们允许将等价或预序检查归约为模型检查，并且正是那些模态逻辑中刻画经典行为等价和预序的公式，使得模型检查可以归约为等价或预序检查。本文研究了在 van Glabbeek 分支时间谱中基于模拟语义的模态逻辑中，判定一个公式是否为某个有限无环过程的特征公式的复杂度。由于这些逻辑中的特征公式恰好是一致且素公式，本文给出了可满足性和素性问题的复杂度结果，并探讨了这些问题可在多项式时间内求解的模态逻辑与变得计算困难的模态逻辑之间的边界。此外，本文还研究了在刻画基于模拟语义的模态逻辑中构造特征公式的复杂度，包括显式公式和通过方程组表示的情况。