Strategic Abilities under Imperfect Information: Modeling, Reasoning and Verification
Project Members:
- Dr. Wojciech Jamroga
Partner:
- Dr. Thomas Agotnes, Bergen University College, Norway
Funding: DFG, 750 € (of 750 € total)
Duration: since 07/2005
Project Description:
We propose a non-standard interpretation of Alternating-time Temporal Logic with imperfect information, for which no commonly accepted semantics has been proposed yet. Rather than changing the semantic structures, we generalize the usual interpretation of formulae in single states to setsof states. We propose a new epistemic operator for ``practical'' or "constructive" knowledge, and we show that the new logic (which we call Constructive Strategic Logic) is strictly more expressive than most existing solutions, while it retains the same model checking complexity.
We also propose a new class of representations that can be used for modeling (and model checking) temporal, strategic and epistemic properties of agents and their teams. Our representations borrow the main ideas from interpreted systems of Halpern, Fagin et al.; however, they are also modular and compact. Surprisingly, our complexity results suggest that model checking strategic abilities under imperfect information can be computationally cheaper than checking the perfect information case.
