Probabilistic ATL with Incomplete Information

Alternating-time Temporal Logic (ATL) is widely used to reason about strategic abilities of players. Aiming at strategies that can realistically be implemented in software, many variants of ATL study a setting with incomplete information, where strategies may only take available information into account. Another generalization of ATL is Probabilistic ATL, where strategies are required to achieve their goal with a certain probability. We introduce a semantics of ATL that takes into account both of these aspects. We prove that our semantics allows simulation relations similar in spirit to usual bisimulations, and has a decidable model checking problem (in the case of memoryless strategies, with memory-dependent strategies the problem is undecidable).

Logo BII

BII

Rechte

Nutzung und Vervielfältigung:

Keine Lizenz. Es gelten die Bestimmungen des deutschen Urheberrechts (UrhG).

Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.