关于冻结具有有序属性的LTL
On Freeze LTL with Ordered Attributes
摘要：
本文讨论的是FreezeLTL，一种基于寄存器的数据字时序逻辑。在一个（多属性）数据字中，每个位置携带一个来自有限字母表的字母，并将一个数据值分配给一个固定的有限属性集。冻结LTL的可满足性问题是不可判定的，如果一个以上的寄存器是可用的，或元组的数据值可以存储和比较任意。从可判定的单寄存器片段开始，我们提出了一个扩展，允许指定属性上的依赖关系。这以灵活的方式限制了如何存储和比较属性值的集合。这个概念维度与寄存器的数量或可用的时态运算符正交。扩展是严格的。允许任意依赖关系的可满足性变得不可判定。树状关系，但是，诱导一个家庭的可判定的片段升级的顺序索引层次结构的快速增长的复杂性类，最近推出的非原始递归复杂性的框架。这导致类${\bf F}_{ε_0}$的完整性。我们采用嵌套计数器系统，并表明，它们涉及的层次结构的嵌套深度。
英文摘要：
This paper is concerned with Freeze LTL, a temporal logic on data words with registers. In a (multi-attributed) data word each position carries a letter from a finite alphabet and assigns a data value to a fixed, finite set of attributes. The satisfiability problem of Freeze LTL is undecidable if more than one register is available or tuples of data values can be stored and compared arbitrarily. Starting from the decidable one-register fragment we propose an extension that allows for specifying a dependency relation on attributes. This restricts in a flexible way how collections of attribute values can be stored and compared. This conceptual dimension is orthogonal to the number of registers or the available temporal operators. The extension is strict. Admitting arbitrary dependency relations satisfiability becomes undecidable. Tree-like relations, however, induce a family of decidable fragments escalating the ordinal-indexed hierarchy of fast-growing complexity classes, a recently introduced framework for non-primitive recursive complexities. This results in completeness for the class ${\bf F}_{ε_0}$. We employ nested counter systems and show that they relate to the hierarchy in terms of the nesting depth.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
