Safely Freezing LTL
Safely Freezing LTL
复制标题
安全冷冻零担
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
R. Lazic
中科院分区：
文献类型：
--
作者：
R. Lazic
我们考虑了带有冻结量词的线性时序逻辑的安全片段。冻结量词用于将来自无限域的值存储在寄存器中，以便稍后与其他此类值进行比较。我们表明，对于一个寄存器，可满足性，细化和模型检测问题是可判定的。本文的主要结果是可满足性是ExpSPACE完全的。EXPSPACE成员的证明涉及到一个新的错误计数器自动机类的翻译。我们还表明，细化和模型检查是不是原始递归的，和下降的安全限制，增加过去的时间操作，或增加一个以上的寄存器，每一个原因的不可判定性的所有三个决策问题。
We consider the safety fragment of linear temporal logic with the freeze quantifier. The freeze quantifier is used to store a value from an infinite domain in a register for later comparison with other such values. We show that, for one register, satisfiability, refinement and model checking problems are decidable. The main result in the paper is that satisfiability is ExpSPACE-complete. The proof of EXPSPACE-membership involves a translation to a new class of faulty counter automata. We also show that refinement and model checking are not primitive recursive, and that dropping the safety restriction, adding past-time temporal operators, or adding one more register, each cause undecidability of all three decision problems.