ATLsc with partial observation

TL;DR

This paper proves that model-checking ATLsc with uniform incomplete observation remains decidable, enabling verification of multi-agent systems under realistic observation constraints.

Contribution

It establishes decidability results for ATLsc under uniform incomplete observation, extending the applicability of ATLsc in multi-agent system verification.

Findings

Decidability is preserved under uniform incomplete observation.

Model-checking ATLsc remains feasible with expressive logics.

Supports verification in more realistic multi-agent scenarios.

Abstract

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.