Probabilistic ATL with Incomplete Information

zum Volltext (339 kB)   ZIP
Beteiligte Person(en) / Institution(en)Autor :
DatumErschienen :
  • September 2009
Seitenbereich44 S.

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).
Statische URL
IDNummer des Berichts :
  • TR_0918