# ATLsc with partial observation

arXiv: https://arxiv.org/abs/1509.07208 · HTML: https://mlsanity.com/paper/1509.07208/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Sep 2015.

## Built on by (most cited first, 1 of 1)

- [Hyper Strategy Logic](https://mlsanity.com/paper/2403.13741/) (2024)

## Abstract (arXiv)

Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model-checking problem, even for very expressive logics such as ATLsc.