动作模型等价性的判定与动作模型的化简

本文研究两个问题：判定动作模型等价性，以及在特定结构关系下最小化动作模型的事件空间。Kripke模型等价性被称为互模拟的结构关系完美刻画。本文提出广义动作模拟，完美刻画动作模型等价性。先前对动作模型等价性充分的结构关系，即互模拟、命题动作模拟、动作模拟以及典范动作模型的动作模拟，均可由广义动作模拟的若干受限版本描述。我们总结了前件原子集的四个关键性质，并证明满足这些性质的任意公式集均可用于限制广义动作模拟，从而通过迭代算法判定动作模型等价性。我们还构造了一组具有这四个性质的新公式集，其通常比原子集更高效。划分精化技术已被用于在与互模拟下最小化Kripke模型的世界空间。将划分精化应用于动作模型，可使其在互模拟下最小化事件空间。命题动作模拟弱于互模拟但仍对动作模型等价性充分。我们证明在命题动作模拟下最小化动作模型事件空间是PSPACE完全的，并给出了一个PSPACE算法。最后，我们证明在动作模型等价性下最小化事件空间是PSPACE难的，并提出了一种基于模态逻辑典范公式的可计算方法来解决该问题。