Reasoning about transfinite sequences

TL;DR

This paper introduces a family of temporal logics for systems with Zeno behaviors, extending LTL with ordinal-indexed operators, and analyzes their satisfiability complexity using new ordinal automata.

Contribution

It extends linear-time temporal logic to handle Zeno sequences with ordinal operators and develops ordinal automata for analyzing satisfiability complexity.

Findings

Satisfiability for these logics is EXPSPACE-complete with binary integers.

Satisfiability is PSPACE-complete with unary integer representation.

Introduces succinct ordinal automata to model ordinal interactions.

Abstract

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.