2 ATL with Strategy Contexts : Expressiveness and Model Checking

We study the alternating-time temporal logics ATL and ATL extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL where strategy quantifiers reset previously selected strategies. We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc, equally expressive: any formula in ATL ? sc can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we prove that their model-checking problems remain decidable by designing a treeautomata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.