论不可能未来的可公理化
计算机科学中的逻辑
2017-01-11 v2
摘要
在进程代数 BCCS 的背景下，建立了一个通用方法，可从具体对应语义的基完全公理化推导出弱语义的基完全公理化。该变换还保持 ω-完备性。它适用于至少与不可能未来语义一样粗的语义。作为应用，推导出了弱失败、完全迹与迹语义的基完全且 ω-完备的公理化。随后，我们给出了具体不可能未来预序的一个有限、可靠、基完全的公理化，其蕴含弱不可能未来预序的一个有限、可靠、基完全的公理化。相反，我们证明对于 BCCS 在具象与弱不可能未来等价下，不存在有限、可靠的基完全公理化。若动作字母表是无限的，则上述基完全公理化被证明是 ω-完备的。若字母表有限，我们证明 BCCS 在具象与弱不可能未来预序下的不等式理论缺乏这样的有限基。
引用
@article{arxiv.1505.04985,
title = {On the Axiomatizability of Impossible Futures},
author = {Taolue Chen and Wan Fokkink and Rob van Glabbeek},
journal= {arXiv preprint arXiv:1505.04985},
year = {2017}
}