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.

翻译：我们在基于博弈的反应式综合背景下研究位置性质。我们的动机源于拥有一种可用的规范逻辑，并保证其可处理性综合。我们证明，每一个$\omega$-正则位置性质（针对状态标注或边标注的博弈图）都可以在线性时序逻辑中表达。此外，我们给出了$\omega$-正则性质具有位置性的若干充分必要条件，并识别出$\omega$-正则位置性质中表现良好的子类。利用语言簇理论，我们证明不存在任何一类$\omega$-正则位置性质能够同时包含一个前缀独立性质并在布尔运算下封闭。最后，我们讨论了这些结果对交替时序逻辑的影响，在该逻辑中我们分离出几个具有可处理模型检验的不同片段，并比较了这些片段的相关表达能力。