Reasoning about transfinite sequences
<|reference_start|>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 $\omega$-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability problem for the logics working on $\omega^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.<|reference_end|>
@article{demri2005reasoning,
    title={Reasoning about transfinite sequences},
    author={St'ephane Demri and David Nowak},
    journal={International Journal of Foundations of Computer Science,
  18(1):87-112, February 2007},
    year={2005},
    doi={10.1142/S0129054107004589},
    archivePrefix={arXiv},
    eprint={cs/0505073},
    primaryClass={cs.LO cs.CC}
}