大家好， 我目前正在尝试执行 PetersonNP（又名 FilterLock）正确性证明（互斥）。 我在并发书籍上找到了几个证明草图，但我对 Nancy Lynch 的“分布式算法”中显示的草图感兴趣。我觉得它更有说服力，因为证明它所需的引理是公开的（其他人提供了一种直观的方法，但我需要更多细节）。

暗示互斥的引理（断言 10.5.5）和证明它的三个引理（10.5.3.1、10.5.3.2、10.5.4）在本书的第 287 页中有详细说明。

我想首先关注 10.5.3.* 和 10.5.4。只有当其他人被证明时，我才会考虑 10.5.5。

我已经能够机械地证明第一个引理 (10.5.3.1)。我使用连续演算手工进行我的证明，一旦我确信它们是正确的，我就会通过 PVS 来检查它们。我检查过，所以我确信第一个是正确的。

我报告了所有三个证明中涉及的关键概念，正如书中所解释的：

winner(p,c,j) = (c'i_p>j) \lor (c'i_p=j\land c'pc_p=CS)

comp(p,j)=
    winner(p,j) \lor (c'i_p=j\land c'pc_p\in\{cf,ct\}) =
        (c'i_p>j) \lor (c'i_p=j\land c'pc_p=CS) \lor (c'i_p=j\land c'pc_p\in\{cf,ct\})

到目前为止我尝试过的：

引理 10.5.3.1 声明：“如果进程 p 是 j 级的竞争者，如果 pc_p=check-flag，并且如果 S_p 中的任何进程 q\neq p 是 j 级的竞争者，则 turn(j)\ neq p."

我将定理形式化如下并证明它是正确的（证明不难但很长，因为需要大量的案例分析）。

Lemma10.5.3.1(c)=\forall p,q,j.
    \big(
        comp(p,j)\land c'pc_p=cf \land (comp(q,j)\land q\neq p\land q\in c'S(p) )
    \big)
        \Rightarrow c'turn(j)\neq p
% PROVED.

问题：

我在证明 10.5.3.2 和 10.5.4 时遇到了困难，因为首先，我不确定应该如何在一阶逻辑中说明它们（更多细节即将推出）。

引理 10.5.3.2 声明：“如果进程 p 在级别 k 是赢家，并且任何其他进程在级别 k 是竞争对手，则 turn(j)\neq p。”

到目前为止我尝试过：

\forall p,j.\big( winner(p,j) \land comp(q,j) \land p\neq q \big) \Rightarrow c'turn(j)\neq p

然而，归纳假设在少数情况下不成立，引理 10.5.3.1 不适用， 所以我怀疑它是不正确的。

然后我尝试将 q 上的量词移动到里面：

\forall p,j) \land \forall q.(comp(q,j) \land p\neq q) \big) \Rightarrow c'turn(j)\neq p

这个引理是可证明的。对 p 和 j 进行 skolemize 就足够了，当实例化 q=p 时，约束 p\neq q 变得不可满足，导致证明结束。 这种替代形式化让我感到困惑，因为当必须应用这个引理时，我不知道如何使用最内层的 forall。

最终引理 10.5.4 规定：“如果在 j 级有一个竞争者，那么 turn(j) 的值是 j 级某个竞争者的索引。”

我尝试了以下形式化：

\forall p,j.comp(p,\cz,j)\land comp(q,j)\Rightarrow(\cz'turn(j)=p\oo\cz'turn(j)=q)

但是当进程 p 和 q 都停止时，我得到一个无法证明的情况，所以我怀疑这种形式化是不正确的。

有人可以建议我适当的形式化吗？

提前致谢，