事后诸葛亮易：通信有限状态机刻画带“先于发生”的一阶逻辑
计算机科学中的逻辑
2018-10-22 v2 形式语言与自动机理论
摘要
消息序列图（MSCs）自然作为通信有限状态机（CFMs）的执行而产生，其中有限状态进程通过无界FIFO通道交换消息。我们研究MSCs的一阶逻辑，其具有Lamport的“先于发生”关系。我们引入一种带循环和逆的命题动态逻辑（PDL）的无星版本。我们的主要结果表明：(i) 每个一阶语句可转化为等价的无星PDL语句（反之亦然），且(ii) 每个无星PDL语句可翻译为等价的CFM。这回答了一个开放问题，并确立了CFMs与一元二阶逻辑片段之间的确切关系。作为副产品，我们证明MSCs上的一阶逻辑具有三变量性质。
引用
@article{arxiv.1804.10076,
title = {It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"},
author = {Benedikt Bollig and Marie Fortin and Paul Gastin},
journal= {arXiv preprint arXiv:1804.10076},
year = {2018}
}
备注
Full version of CONCUR'18 paper: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2018.7