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)