Difficult Configurations—On the Complexity of LTrL
Difficult Configurations—On the Complexity of LTrL
复制标题
困难的配置——论 LTrL 的复杂性
DOI：
10.1007/s10703-005-4593-z
复制
发表时间：
1998
影响因子：
0.8
通讯作者：
I. Walukiewicz
中科院分区：
文献类型：
--
作者：
I. Walukiewicz
研究了一种全局线性时间时间轨迹逻辑LTrL的复杂度。逻辑是全局的，因为公式的真值是在全局状态下计算的，也称为配置。逻辑是非初等的，造成这种复杂性的主要原因是公式中until操作符的嵌套。没有until操作符的逻辑片段显示为EXPSPACE-hard。
The complexity of LTrL, a global linear time temporal logic over traces is investigated. The logic is global because the truth of a formula is evaluated in a global state, also called configuration. The logic is shown to be non-elementary with the main reason for this complexity being the nesting of until operators in formulas. The fragment of the logic without the until operator is shown to be EXPSPACE-hard.