关于超限序列的推理
Reasoning about transfinite sequences
摘要：
我们引入了一个时间逻辑族来描述具有Zeno行为的系统的行为。我们扩展线性时间时序逻辑LTL授权模型承认芝诺序列的行动和定量的时间运营商的序数索引取代标准的下一次，直到未来的时间运营商。我们的目标是通过设计控制器来控制这样的系统，这些控制器安全地工作在$ω$序列上，但与系统同步交互，以限制它们的行为。我们证明了当整数用二进制表示时，工作在$ω^k$ -序列上的逻辑的可满足性问题是EXPSPACE-完全的，当整数用一元表示时，工作在$ω^k$-序列上的逻辑的可满足性问题是PSPACE-完全的。要做到这一点，我们大大延长标准的结果LTL通过引入一类新的简洁的顺序自动机，可以编码不同的定量时间算子之间的相互作用。
英文摘要：
We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on $ω$-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability problem for the logics working on $ω^k$-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
