弱语义的有限基：失败与不可能的未来

不可能期货的公理化

On the Axiomatizability of Impossible Futures

在进程代数BCCS的背景下，建立了从弱语义的公理化导出弱语义的基完备公理化的一般方法。这种变换还保持了Ω-完备性。它适用于至少像不可能的未来语义一样粗糙的语义。作为应用，针对弱故障、完整踪迹和踪迹语义推导了基完全和omega完全公理化。然后，我们提出了一个有限的，健全的，地面完全公理化的具体不可能的期货前序，这意味着一个有限的，健全的，地面完全公理化的弱不可能的期货前序。相反，我们证明了没有有限的，健全的公理化BCCS模具体和弱不可能期货等价是地面完全的。如果作用的字母表是无限的，那么上述的地面完全公理化被证明是ω-完全的。如果字母表是有限的，我们证明了BCCS模具体和弱不可能期货预序的不等式理论缺乏这样一个有限的基础。