Pure future local temporal logics are expressively complete for Mazurkiewicz traces
Pure future local temporal logics are expressively complete for Mazurkiewicz traces
复制标题
对于 Mazurkiewicz 轨迹来说，纯粹的未来局部时序逻辑是表达完整的
DOI：
10.1016/j.ic.2006.07.002
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
P. Gastin
中科院分区：
文献类型：
--
作者：
V. Diekert;P. Gastin
本文解决了Mazurkiewicz迹的一个长期存在的问题：用基本模态定义的纯未来局部时态逻辑存在-next和until是表达完备的。这意味着Mazurkiewicz迹的每一个一阶可定义语言都可以在纯未来局部时态逻辑中定义。类似的结果与一个全球的解释已经知道，但处理一个本地的解释原来是更多的参与。局部逻辑是有趣的，因为可满足性问题和模型检验问题对于这些逻辑在P空间中是可解的，而对于全局逻辑它们是非初等的。这两个，（以前已知的）全球和（新的）本地的结果推广坎普定理的话，因为序列的本地和全球的观点一致。
The paper settles a long standing problem for Mazurkiewicz traces: the pure future local temporal logic defined with the basic modalities exists-next and until is expressively complete. This means every first-order definable language of Mazurkiewicz traces can be defined in a pure future local temporal logic. The analogous result with a global interpretation has been known, but the treatment of a local interpretation turned out to be much more involved. Local logics are interesting because both the satisfiability problem and the model checking problem are solvable in Pspace for these logics whereas they are non-elementary for global logics. Both, the (previously known) global and the (new) local results generalize Kamp’s Theorem for words, because for sequences local and global viewpoints coincide.