Positional Properties in Temporal Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913069195591680 |
|---|---|
| author | Newman, Jessica Plummer, Benjamin |
| author_facet | Newman, Jessica Plummer, Benjamin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_25628 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Positional Properties in Temporal Logic Newman, Jessica Plummer, Benjamin Logic in Computer Science Formal Languages and Automata Theory 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. |
| title | Positional Properties in Temporal Logic |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2604.25628 |