Positional Properties in Temporal Logic

Non-terminating systems are often modelled with the use of temporal logic: ATL∗ and Strategy Logic are two logics designed for multi-agent systems in particular. Their semantics are based on the existence of strategies that enable groups of agents to enforce specified goals. It has been noted that for certain fragments of ATL∗, the semantics are equivalent even when we restrict to positional strategies, which is beneficial as positional strategies yield favourable algorithmic properties for model-checking and strategy synthesis. However, therehasnotbeenmuchstudyofthenecessary and sufficient conditions for a fragment of temporal logic to have equivalent semantics under positional and memoryful strategies - most existing work on positional strategies in infinite games assumes observations are on edges rather than states, a distinction that can affect whether a property is positional. We investigate this problem, as well as a similar phenomenon noted in Strategy Logic; in certain fragments, existentially quantified strategies do notdependonentireuniversallyquantifiedstrategiesintheirscope, but only on moves chosen by those strategies at the current state.

Authors

• Jessica L. Newman University of Southampton

Keywords

• Temporal Logic
• ATL
• Strategic Reasoning
• Positional Strategies