Reasoning About Transfinite Sequences

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 and model-checking 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.

• Type: Conference
• Year: 2005
• Where: ATVA
• Authors: Stéphane Demri, David Nowak
• Keywords: ATVA 2005, Quantitative Temporal Operators, Temporal Logic, Temporal Logic Ltl