DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2026.44

Positional Properties in Temporal Logic

Authors: Jessica Newman and Benjamin Plummer

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

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 ω-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.

Cite as

Jessica Newman and Benjamin Plummer. Positional Properties in Temporal Logic. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 44:1-44:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{newman_et_al:LIPIcs.CONCUR.2026.44,
  author =	{Newman, Jessica and Plummer, Benjamin},
  title =	{{Positional Properties in Temporal Logic}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{44:1--44:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.44},
  URN =		{urn:nbn:de:0030-drops-273755},
  doi =		{10.4230/LIPIcs.CONCUR.2026.44},
  annote =	{Keywords: Positionality, Temporal Logic, ATL, Games on graphs}
}

Search Results

Documents authored by Plummer, Benjamin

Positional Properties in Temporal Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message