具有有限变量数的分支时间与交替时间时序逻辑的复杂性与表达性
计算机科学中的逻辑
2019-01-23 v2
摘要
我们证明了分支时间时序逻辑CTL和CTL*，以及交替时间时序逻辑ATL和ATL*，在仅含单个命题变量的语言中与其在完整语言（即具有无限多命题变量供应）中具有相同的语义表达性。由此可知，CTL以及ATL在单变量下的可满足性是EXPTIME完全的，而CTL*以及ATL*在单变量下的可满足性是2EXPTIME完全的——即对于这些逻辑，仅含一个变量的公式的可满足性与任意公式的可满足性一样困难。
引用
@article{arxiv.1810.09142,
title = {Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables},
author = {Mikhail Rybakov and Dmitry Shkatov},
journal= {arXiv preprint arXiv:1810.09142},
year = {2019}
}
备注
Prefinal version of the published paper