Quantified CTL with imperfect information

TL;DR

This paper extends Quantified CTL with imperfect information by introducing observation-based quantifiers, analyzing their expressiveness, and establishing complexity results, including decidability for a syntactic fragment.

Contribution

It introduces a new version of QCTL with imperfect information, studies its expressiveness, and identifies decidable fragments with automata-theoretic methods.

Findings

Expressiveness matches MSO for no-memory semantics.

Model-checking is PSpace-complete under no-memory semantics.

Decidability is achieved for a hierarchical fragment using automata.

Abstract

Quantified CTL (QCTL) is a well-studied temporal logic that extends CTL with quantification over atomic propositions. It has recently come to the fore as a powerful intermediary framework to study logics for strategic reasoning. We extend it to include imperfect information by parameterising quantifiers with an observation that defines how well they observe the model, thus constraining their behaviour. We consider two different semantics, one related to the notion of no memory, the other to perfect recall. We study the expressiveness of our logic, and show that it coincides with MSO for the first semantics and with MSO with equal level for the second one. We establish that the model-checking problem is Pspace-complete for the first semantics. While it is undecidable for the second one, we identify a syntactic fragment, defined by a notion of hierarchical formula, which we prove to be decidable thanks to an automata-theoretic approach.