Positional Properties in Temporal Logic

TL;DR

This paper investigates positional properties in game-based reactive synthesis, showing all $mbda$-regular positional properties are expressible in linear-time temporal logic and exploring their structural characteristics.

Contribution

It provides necessary and sufficient conditions for $mbda$-regular properties to be positional and identifies subclasses with specific closure properties.

Findings

All $mbda$-regular positional properties are expressible in linear-time temporal logic.

No class of $mbda$-regular positional properties can be both prefix-independent and closed under Boolean operations.

Implications for fragments of alternating-time temporal logic with tractable model checking.

Abstract

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 $\omega$-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 $\omega$-regular property is positional, and identify well-behaved subclasses of $\omega$-regular positional properties. Using varieties of languages, we prove that no class of $\omega$-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.