Positional Properties in Temporal Logic
This work provides theoretical foundations for usable specification logics in reactive synthesis, but the results are incremental and primarily of interest to researchers in temporal logic and synthesis.
The paper shows that every ω-regular positional property is expressible in linear-time temporal logic, and identifies necessary and sufficient conditions for ω-regular properties to be positional. It also proves that no class of ω-regular positional properties can simultaneously contain a prefix-independent property and be closed under Boolean operations.
We study positional properties in the context of game-based reactive synthesis. Our motivation stems from having a usable specification logic, for which tractable synthesis is guaranteed. We demonstrate that every $ω$-regular positional property (with respect to state- or edge-labelled game graphs), is expressible in linear-time temporal logic. Additionally, we provide some necessary and sufficient conditions for when an $ω$-regular property is positional, and identify well-behaved subclasses of $ω$-regular positional properties. Using varieties of languages, we prove that no class of $ω$-regular positional properties can simultaneously contain a prefix-independent property and be closed under Boolean operations. We conclude by discussing the implications on alternating-time temporal logic, where we isolate a few different fragments with tractable model checking, and compare the associated expressivity of such fragments.