---
abstract: 'Quantified () is a well-studied temporal logic that extends 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 for the first semantics and with with equal level for the second one. We establish that the model-checking problem is -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.'
author:
- Raphaël Berthon
- Bastien Maubert
- Aniello Murano
title: 'Quantified CTL with imperfect information[^1]'
---

at (current page.south) [![image](logo-ce-horizontal-en-quadri-lr.png){height="2.5em"}]{};

[10]{}

E. A.Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. In [*PL’85*]{}, pages 84–96. [ACM]{} Press, 1985.

T. [Å]{}gotnes, V. Goranko, and W. Jamroga. In [*TARK’07*]{}, pages 15–24, 2007.

R. Alur, T.A. Henzinger, and O. Kupferman. , 49(5):672–713, 2002.

Dietmar Berwanger, Anup Basil Mathew, and Marie van den Bogaard. Hierarchical information patterns and distributed strategy synthesis. In [*Automated Technology for Verification and Analysis - 13th International Symposium, [ATVA]{} 2015, Shanghai, China, October 12-15, 2015, Proceedings*]{}, pages 378–393, 2015. [](http://dx.doi.org/10.1007/978-3-319-24953-7_28).

T. Brihaye, A. Da Costa Lopes, F. Laroussinie, and N. Markey. In [*LFCS’09*]{}, LNCS 5407, pages 92–106. Springer, 2009.

P. [Č]{}erm[á]{}k, A. Lomuscio, F. Mogavero, and A. Murano. In [*CAV’14*]{}, LNCS 8559, pages 524–531. Springer, 2014.

K. Chatterjee, T.A. Henzinger, and N. Piterman. , 208(6):677–693, 2010.

E.M. Clarke and E.A. Emerson. In [*LP’81*]{}, LNCS 131, pages 52–71. Springer, 1981.

E.M. Clarke, O. Grumberg, and D.A. Peled. MIT Press, 2002.

A. [Da Costa]{}, F. Laroussinie, and N. Markey. In [*FSTTCS’10*]{}, LIPIcs 8, pages 120–132, 2010.

M. Dastani and W. Jamroga. Reasoning about strategies of multi-agent programs. In [*AAMAS’10*]{}, pages 997–1004. [IFAAMAS]{}, 2010.

C. Dima and F. L. Tiplea. Model-checking [ATL]{} under imperfect information and perfect recall semantics is undecidable. , abs/1102.4225, 2011.

C. Dima and F.L. Tiplea. Technical report, arXiv, 2011.

C. C. Elgot and M. O. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. , 31(2):169–181, 1966. URL: <http://dx.doi.org/10.2307/2269808>, [](http://dx.doi.org/10.2307/2269808).

E Allen Emerson and A Prasad Sistla. Deciding branching time logic. In [*Proceedings of the sixteenth annual ACM symposium on Theory of computing*]{}, pages 14–24. ACM, 1984.

E.A. Emerson and J.Y. Halpern. , 33(1):151–178, 1986.

Tim French. Decidability of quantifed propositional branching time logics. In [*Australian Joint Conference on Artificial Intelligence*]{}, pages 165–176. Springer, 2001.

Joseph Y Halpern and Moshe Y Vardi. The complexity of reasoning about knowledge and time. i. lower bounds. , 38(1):195–237, 1989.

W. Jamroga, S. Mauw, and M. Melissen. Fairness in non-repudiation protocols. In [*Proceedings of [STM’11]{}*]{}, volume 7170 of [*LNCS*]{}, pages 122–139, 2012.

W. Jamroga and A. Murano. In [*AAMAS’14*]{}, pages 701–708. IFAAMAS, 2014.

S. Kremer and J.-F. Raskin. A game-based verification of non-repudiation and fair exchange protocols. , 11(3), 2003.

O Kupermann and M.Y Vardi. Synthesizing distributed systems. In [*Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on*]{}, pages 389–398. IEEE, 2001.

O. Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. In [*CAV’95*]{}, LNCS 939, pages 325–338. Springer, 1995.

O. Kupferman, P. Madhusudan, P. S. Thiagarajan, and M. Y. Vardi. Open systems in reactive environments: Control and synthesis. In [*CONCUR’00*]{}, LNCS 1877, pages 92–107. Springer, 2000.

O. Kupferman and M. Y. Vardi. Module checking revisited. In [*CAV’97*]{}, volume 1254 of [*LNCS*]{}, pages 36–47. Springer, [1997]{}.

O. Kupferman, M.Y. Vardi, and P. Wolper. , 47(2):312–360, 2000.

O. Kupferman, M.Y. Vardi, and P. Wolper. , 164(2):322–344, 2001.

Orna Kupferman and Moshe Y Vardi. Church’s problem revisited. , pages 245–263, 1999.

Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. , 47(2):312–360, 2000.

Fran[ç]{}ois Laroussinie and Nicolas Markey. Quantified [CTL:]{} expressiveness and complexity. , 10(4), 2014. URL: <http://dx.doi.org/10.2168/LMCS-10(4:17)2014>, [](http://dx.doi.org/10.2168/LMCS-10(4:17)2014).

Hans L[ä]{}uchli and Christian Savioz. Monadic second order definable relations on the binary tree. , 52(01):219–226, 1987.

A. Lomuscio and F. Raimondi. : A model checker for multi-agent systems. In [*TACAS’06*]{}, LNCS 4314, pages 450–454, 2006.

A.D.C. Lopes, F. Laroussinie, and N. Markey. In [*FSTTCS’10*]{}, LIPIcs 8, pages 120–132. Leibniz-Zentrum fuer Informatik, 2010.

F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. , 15(4):34:1–42, 2014.

F. Mogavero, A. Murano, and M.Y. Vardi. In [*FSTTCS’10*]{}, LIPIcs 8, pages 133–144. Leibniz-Zentrum fuer Informatik, 2010.

F. Mogavero, A. Murano, and M.Y. Vardi. In [*LPAR’10*]{}, LNAI 6355, pages 371–387. Springer, 2010.

David E. Muller and Paul E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of rabin, mcnaughton and safra. , 141(1[&]{}2):69–107, 1995.

Gary Peterson, John Reif, and Salman Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. , 41(7):957–992, 2001.

Gary Peterson, John Reif, and Salman Azhar. Decision algorithms for multiplayer noncooperative games of incomplete information. , 43(1):179–206, 2002.

Sophie Pinchinat and St[é]{}phane Riedweg. A decidable class of problems for control under partial observation. , 95(4):454–460, 2005.

A. Pnueli. In [*FOCS’77*]{}, pages 46–57. IEEE Computer Society, 1977.

A. Pnueli and R. Rosner. In [*POPL’89*]{}, pages 179–190. Association for Computing Machinery, 1989.

Michael O Rabin. Decidability of second-order theories and automata on infinite trees. , 141:1–35, 1969.

John H. Reif. The complexity of two-player games of incomplete information. , 29(2):274–301, 1984.

A.P. Sistla. PhD thesis, Harvard University, Cambridge, MA, USA, 1983.

W. Thomas. Infinite trees and automaton-definable relations over omega-words. , 103(1):143–159, 1992.

W. van der Hoek and M. Wooldridge. Cooperation, knowledge and time: [A]{}lternating-time [T]{}emporal [E]{}pistemic [L]{}ogic and its applications. , 75(1):125–157, 2003.

M.Y. Vardi and L.J. Stockmeyer. Improved upper and lower bounds for modal logics of programs: Preliminary report. In [*STOC’85*]{}, pages 240–251, 1985.

Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. , 200(1-2):135–183, 1998.

[^1]: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 709188.
