C. H. Broadbent, A. Carayol, M. Hague, and O. Serre, A Saturation Method for Collapsible Pushdown Systems, Proceedings of the 39th International Colloquium on Automata, Languages, and Programming, 2012.
DOI : 10.1007/978-3-642-31585-5_18
URL : https://hal.archives-ouvertes.fr/hal-00694991

C. H. Broadbent, A. Carayol, M. Hague, and O. Serre, C-SHORe: a collapsible approach to higher-order verification, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, pp.13-24, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00865155

C. H. Broadbent, A. Carayol, C. Ong, and O. Serre, Recursion Schemes and Logical Reflexion, Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, pp.120-129, 2010.
DOI : 10.1109/lics.2010.40
URL : https://hal.archives-ouvertes.fr/hal-00479818/file/main.pdf

[. Bouquet, O. Serre, and I. Walukiewicz, Pushdown Games with Unboundedness and Regular Conditions, Proceedings of the 23rd International Conference on Foundations of Software Technology and ?eoretical Computer Science, pp.88-99, 2003.
DOI : 10.1007/978-3-540-24597-1_8
URL : https://hal.archives-ouvertes.fr/hal-00012141

A. Carayol, D. Caucal, and O. Serre, Reachability Games Generated by Graph Grammars

A. Carayol, A. Haddad, and O. Serre, Qualitative Tree Languages, 2011 IEEE 26th Annual Symposium on Logic in Computer Science
DOI : 10.1109/LICS.2011.28
URL : https://hal.archives-ouvertes.fr/hal-00616304

A. Carayol, A. Haddad, and O. Serre, Counting branches in trees using games, Information and Computation, vol.252, pp.110-117
DOI : 10.1016/j.ic.2016.11.005

A. Carayol, A. Haddad, and O. Serre, Randomisation in Automata on Infinite Trees, In: ACM Transactions on Computational Logic, vol.153, issue.101, pp.24-99, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01260669

A. Carayol, C. Löding, and O. Serre, Pure strategies in Imperfect Information Stochastic Games, pp.2012-133

A. Carayol, A. Meyer, M. Hague, C. Ong, and O. Serre, Winning Regions of Higher-Order Pushdown Games, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008.
DOI : 10.1109/LICS.2008.41
URL : https://hal.archives-ouvertes.fr/hal-00345939

A. Carayol and O. Serre, Collapsible Pushdown Automata and Labeled Recursion Schemes: Equivalence, Safety and Effective Selection, 2012 27th Annual IEEE Symposium on Logic in Computer Science, 2012.
DOI : 10.1109/LICS.2012.73
URL : https://hal.archives-ouvertes.fr/hal-00733467

A. Carayol and O. Serre, Higher-order recursion schemes and their automata models''. In: Automata: from Mathematics to Applications, 2012.

S. Fijalkow, O. Pinchinat, and . Serre, Emptiness Of Alternating Tree Automata Using Games With Imperfect Information, Proceedings of the 33rd International Conference on Foundations of Software Technology and ?eoretical Computer Science LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, pp.299-311, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01260682

V. Gripon and O. Serre, Qualitative Concurrent Stochastic Games with Imperfect Information Lecture Notes in Computer Science. A revised corrected version of this work can be found at http://arxiv.org/abs/0902, Proceedings of the 36th International Colloquium on Automata, Languages, and Programming, pp.200-211, 2009.

M. Hague, A. S. Murawski, C. Ong, and O. Serre, Collapsible Pushdown Automata and Recursion Schemes, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.452-461, 2008.
DOI : 10.1109/LICS.2008.34
URL : https://hal.archives-ouvertes.fr/hal-00345945

O. Serre, Note on winning positions on pushdown games with ??-regular conditions, Information Processing Letters, vol.85, issue.6, pp.285-291, 2003.
DOI : 10.1016/S0020-0190(02)00445-3
URL : https://hal.archives-ouvertes.fr/hal-00009319

O. Serre, Contribution à l'étude des jeux sur des graphes de processus à pile, pp.72-80, 2004.

O. Serre, Games with Winning Conditions of High Borel Complexity
URL : https://hal.archives-ouvertes.fr/hal-00012134

O. Serre, Games with winning conditions of high Borel complexity, In: ?eoretical Computer Science, vol.350, pp.2-3, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00012134

O. Serre, Parity Games Played on Transition Graphs of One-Counter Processes, Proceedings of the 9th International Conference on Foundations of Software Science and Computational Structures, pp.337-351, 2006.
DOI : 10.1007/11690634_23
URL : https://hal.archives-ouvertes.fr/hal-00016665

A. Aminof, A. Legay, A. Murano, and O. Serre, ??-calculus Pushdown Module Checking with Imperfect State Information, Personal References Not Cited in ?is Document Proceedings of the 5th IFIP International Conference on ?eoretical Computer Science (IFIP TCS, pp.333-348, 2008.
DOI : 10.1007/978-0-387-09680-3_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.143.4378

. Vardi, Pushdown module checking with imperfect information, Information and Computation, vol.223, pp.1-17, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01260664

V. Bárány, C. Löding, and O. Serre, Regularity Problems for Visibly Pushdown Languages, Proceedings of the 25th Symposium on ?eoretical Aspects of Computer Science, pp.420-431, 2006.
DOI : 10.1007/11672142_34

[. Berwanger and O. Serre, Parity games on undirected graphs, Information Processing Letters, vol.112, issue.23, pp.928-932, 2012.
DOI : 10.1016/j.ipl.2012.08.021
URL : https://hal.archives-ouvertes.fr/hal-01260646

B. Genest, A. Muscholl, O. Serre, and M. Zeitoun, Tree Pattern Rewriting Systems, Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, pp.332-346, 2008.
DOI : 10.1016/S0020-0190(01)00337-4
URL : https://hal.archives-ouvertes.fr/hal-00344551

[. Löding, C. Lutz, and O. Serre, Propositional dynamic logic with recursive programs, Journal of Logic and Algebraic Programming, vol.73, pp.1-2, 2007.

[. Löding, P. Madhusudan, and O. Serre, Visibly Pushdown Games
DOI : 10.1007/978-3-540-30538-5_34

C. Löding and O. Serre, Propositional Dynamic Logic with Recursive Programs, Proceedings of the 9th International Conference on Foundations of Software Science and Computational Structures, pp.292-306, 2006.
DOI : 10.1007/11690634_20

O. Serre, Vectorial Languages and Linear Temporal Logic, Proceedings of the 2nd IFIP International Conference on ?eoretical Computer Science (IFIP TCS 2002, pp.576-587, 2002.
DOI : 10.1016/s0304-3975(03)00346-3
URL : https://hal.archives-ouvertes.fr/hal-00012656

O. Serre, Vectorial languages and linear temporal logic, Computer Science, vol.31013, pp.79-116, 2004.
DOI : 10.1016/s0304-3975(03)00346-3
URL : https://hal.archives-ouvertes.fr/hal-00012656

K. Aehlig, A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata, 15th Annual Conference of the EACSL, pp.104-118, 2006.
DOI : 10.1007/11874683_7

?. A. Luca-de-alfaro and . Henzinger, Concurrent omega-regular games, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332)
DOI : 10.1109/LICS.2000.855763

[. Alur, ?. A. Henzinger, and O. Kupferman, Alternating-time temporal logic, Journal of the Association for Computing Machinery (ACM), vol.495, pp.672-713, 2002.
DOI : 10.1109/sfcs.1997.646098
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.5461

?. A. Luca-de-alfaro, O. Henzinger, and . Kupferman, Concurrent reachability games, In: ?eoretical Computer Science, vol.3863, issue.129, pp.188-217, 2007.

. J. Robert, M. Aumann, and . Maschler, Repeated games with incomplete information . M.I, 1995.

[. Aehlig, J. De-miranda, and C. Ong, Safety Is not a Restriction at Level 2 for String Languages, Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures, 2005.
DOI : 10.1007/978-3-540-31982-5_31

A. Arnold and D. Niwi?ski, Rudiments of mu-calculus, Studies in Logic and the Foundations of Mathematics, p.80, 2001.

A. Arnold, ?e µ-calculus alternation-depth hierarchy is strict on binary trees, RAIRO ?eoretical Informatics and Applications 33, pp.329-340, 1999.

A. Atig, Global Model Checking of Ordered Multi-Pushdown Systems, Proceedings of the 30th International Conference on Foundations of Software Technology and ?eoretical Computer Science LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, pp.216-227, 2010.

P. Henk and . Barendregt, ?e Lambda Calculus Its Syntax and, Semantics. Revised, vol.103, 1984.

H. Bauer, Measure and Integration ?eory, p.144, 2001.

H. Bauer, Probability ?eory, 1996.

N. Baier, M. Bertrand, and . Größer, On Decision Problems for Probabilistic B??chi Automata, Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures, pp.287-301, 2008.
DOI : 10.1007/978-3-540-78499-9_21

L. Braud and A. Carayol, Linear Orders in the Pushdown Hierarchy, Proceedings of the 37th International Colloquium on Automata, Languages, and Programming, pp.88-99, 2010.
DOI : 10.1007/978-3-642-14162-1_8
URL : https://hal.archives-ouvertes.fr/hal-00733438

[. Berwanger, K. Chatterjee, L. Doyen, ?. A. Henzinger, and S. Raje, Strategy Construction for Parity Games with Imperfect Information, Proceedings of the 19th International Conference on Concurrency ?eory, pp.325-339, 2008.
DOI : 10.1007/978-3-540-85361-9_27

[. Berwanger, K. Chatterjee, M. De-wulf, L. Doyen, ?. A. Henzinger et al., Alpaga: A Tool for Solving Parity Games with Imperfect Information, Proceedings of 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.58-61, 2009.
DOI : 10.1016/S0304-3975(98)00009-7

[. Berwanger and L. Doyen, On the Power of Imperfect Information, Proceedings of the 28th International Conference on Foundations of Software Technology and ?eoretical Computer Science LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, pp.73-82, 2008.

A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking, Proceedings of the 8th International Conference on Concurrency ?eory, pp.135-150, 1997.
DOI : 10.1007/3-540-63141-0_10

M. Benois, Parties rationnelles du groupe libre''. In: Comptes-Rendus de l'Académie des Sciences de Paris, Série A, vol.269, pp.1188-1190, 1969.

M. Baier and . Größer, Recognizing omega-regular Languages with Probabilistic Automata, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, pp.137-146, 2005.

M. Baier, N. Größer, and . Bertrand, Probabilistic ??-automata, Journal of the ACM, vol.59, issue.1
DOI : 10.1145/2108242.2108243
URL : https://hal.archives-ouvertes.fr/hal-00743907

[. Bertrand, B. Genest, and H. Gimbert, Qualitative Determinacy and Decidability of Stochastic Games with Signals, 2009 24th Annual IEEE Symposium on Logic In Computer Science, pp.319-328, 2009.
DOI : 10.1109/LICS.2009.31
URL : https://hal.archives-ouvertes.fr/hal-00356566

V. Bárány, E. Grädel, and S. Rubin, Automata-based presentations of infinite structures''. In: Finite and Algorithmic Model ?eory Lecture Notes Series, pp.1-76, 2011.

J. Baier and . Katoen, Principles of Model Checking, p.97, 2008.

A. Brázdil, P. Kucera, and . Novotný, Determinacy in Stochastic Games with Unbounded Payoff Functions, Proceedings of the 8th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'12, pp.94-105, 2013.
DOI : 10.1007/978-3-642-36046-6_10

V. Bárány, L. Kaiser, and A. Rabinovich, Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Trees, Fundamenta Informaticae, vol.100, issue.108, pp.1-18, 2010.

A. Bouajjani and A. Meyer, Symbolic Reachability Analysis of Higher-Order Context-Free Processes, Proceedings of the 24th International Conference on Foundations of Software Technology and ?eoretical Computer Science, pp.135-147, 2004.
DOI : 10.1007/978-3-540-30538-5_12
URL : https://hal.archives-ouvertes.fr/hal-00149812

D. Beauquier and D. Niwi?ski, Automata on infinite trees with path counting constraints, Information and Computation, vol.1201, issue.114, pp.117-125, 1995.

[. Beauquier, M. Nivat, and D. Niwi?ski, About the effect of the number of successful paths in an infinite tree on the recognizability by a finite automaton with Buchi conditions, Proceedings of the 8th International Conference on Fundamentals of Computation ?eory (FCT'91, pp.136-145, 1991.
DOI : 10.1007/3-540-54458-5_58

S. K. Ball and . Rajamani, ?e SLAM Project: Debugging System Software via Static Analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.1-3, 2002.

C. Julian and . Bradfield, ?e Modal µ-Calculus Alternation Hierarchy is Strict, In: ?eoretical Computer Science, vol.1952, issue.152, pp.133-153, 1998.

H. Christopher and . Broadbent, ?e Limits of Decidability for First Order Logic on CPDA Graphs, Proceedings of the 29th Symposium on ?eoretical Aspects of Computer Science (STACS 2012 LIPIcs. Schloss Dagstuhl -Leibniz- Zentrum für Informatik, pp.589-600, 2012.

]. J. Büc77 and . Büchi, Using Determinancy of Games to Eliminate Quantifiers, Proceedings of the first International Conference on Fundamentals of Computation ?eory (FCT'77, pp.367-378, 1977.

A. Carayol, Regular Sets of Higher-Order Pushdown Stacks, Proceedings of the 30th Symposium, pp.168-179, 2005.
DOI : 10.1007/11549345_16
URL : https://hal.archives-ouvertes.fr/hal-00620141

A. Carayol, Automates infinis, logiques et langages, pp.74-80, 2006.
URL : https://hal.archives-ouvertes.fr/tel-00628513

D. Caucal, On infinite terms having a decidable monadic theory Lecture Notes in Computer Science, Proceedings of the 27th Symposium, pp.165-176, 2002.

D. Caucal, Deterministic graph grammars''. In: Logic and Automata: History and Perspectives, Text in Logics and Games 2, pp.169-250, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00867578

[. Chatterjee and L. Doyen, Partial-Observation Stochastic Games, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, pp.175-184, 2012.
DOI : 10.1145/2579821
URL : https://hal.archives-ouvertes.fr/hal-00714359

[. Chatterjee, L. Doyen, H. Gimbert, and ?. A. Henzinger, Randomness for Free, Proceedings of the 35th Symposium, pp.246-257, 2010.
DOI : 10.1007/978-3-642-15155-2_23
URL : https://hal.archives-ouvertes.fr/hal-01006409

[. Chatterjee, L. Doyen, and ?. A. Henzinger, Probabilistic Weighted Automata, Proceedings of the 20th International Conference on Concurrency ?eory, pp.244-258, 2009.
DOI : 10.1007/3-540-60915-6_6
URL : http://arxiv.org/abs/0909.1647

[. Chatterjee, L. Doyen, ?. A. Henzinger, and J. Raskin, Algorithms for Omega-Regular Games with Imperfect Information, In: Logical Methods in Computer Science, vol.33, issue.131, pp.132-137, 2007.
DOI : 10.1007/11874683_19

J. Cachat, W. Duparc, and . ?omas, Solving Pushdown Games with a ???3 Winning Condition, 16th Annual Conference of the EACSL, pp.322-336, 2002.
DOI : 10.1007/3-540-45793-3_22
URL : https://hal.archives-ouvertes.fr/hal-00019911

E. M. Clarke and E. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Proceedings of Logic of Programs, pp.52-71, 1981.
DOI : 10.1007/BFb0025774

[. Chatterjee, M. Jurdzi?ski, and ?. A. Henzinger, Quantitative stochastic parity games, Proceedings of the Fifteenth Annual ACM- SIAM Symposium on Discrete Algorithms, pp.121-130, 2004.
DOI : 10.1007/978-3-540-45220-1_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.5430

D. Colcombet, C. Kuperberg, M. V. Löding, and . Boom, Deciding the weak definability of Büchi definable tree languages, 27th Annual Conference of the EACSL LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, pp.215-230, 2013.

A. Carayol and C. Löding, MSO on the Infinite Binary Tree: Choice and Order, Lecture Notes in Computer Science, vol.4646, pp.161-176, 2007.
DOI : 10.1007/978-3-540-74915-8_15
URL : https://hal.archives-ouvertes.fr/hal-00620169

C. Colcombet and . Löding, The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata, Proceedings of the 35th International Colloquium on Automata, Languages, and Programming, pp.398-409, 2008.
DOI : 10.1007/978-3-540-70583-3_33
URL : https://hal.archives-ouvertes.fr/hal-00347194

[. Courcelle and M. Nivat, The algebraic semantics of recursive program schemes, Proceedings of the 7th Symposium, pp.16-30, 1978.
DOI : 10.1007/3-540-08921-7_53

. Colcombet, Fonctions régulières de coût''. Habilitation à diriger des recherches, 2013.

B. Courcelle, A Representation of Trees by Languages I'', In: ?eoretical Computer Science, vol.6, issue.20, pp.255-279, 1978.

B. Courcelle, A representation of trees by languages II, Theoretical Computer Science, vol.7, issue.1, pp.25-55, 1978.
DOI : 10.1016/0304-3975(78)90039-7

[. Courcelle, The monadic second-order logic of graphs, II: Infinite graphs of bounded width, Mathematical Systems ?eory, pp.187-221, 1989.
DOI : 10.1007/BF02088013

[. Courcelle, Monadic second-order definable graph transductions: a survey, Theoretical Computer Science, vol.126, issue.1, pp.53-75, 1994.
DOI : 10.1016/0304-3975(94)90268-2

B. Courcelle, The monadic second-order logic of graphs IX: Machines and their behaviours, Theoretical Computer Science, vol.151, issue.1, pp.125-162, 1995.
DOI : 10.1016/0304-3975(95)00049-3

A. Carayol and M. Slaats, Positional Strategies for Higher-Order Pushdown Parity Games, Proceedings of the 33rd Symposium, pp.217-228, 2008.
DOI : 10.1007/978-3-540-85238-4_17
URL : https://hal.archives-ouvertes.fr/hal-00620254

[. Chadha, A. P. Sistla, and M. Viswanathan, Power of Randomization in Automata on Infinite Strings, Proceedings of the 20th International Conference on Concurrency ?eory, pp.229-243, 2009.
DOI : 10.1016/S0019-9958(63)90290-0

A. Carayol and S. Wöhrle, The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-Order Pushdown Automata, Proceedings of the 23rd International Conference on Foundations of Software Technology and ?eoretical Computer Science, pp.112-123, 2003.
DOI : 10.1007/978-3-540-24597-1_10

[. Courcoubetis and M. Yannakakis, Markov decision processes and regular events, Proceedings of the 17th International Colloquium on Automata, Languages, and Programming, pp.336-349, 1990.
DOI : 10.1007/BFb0032043

W. Damm, Higher type program schemes and their tree languages, Lecture Notes in Computer Science, vol.48, pp.51-72, 1977.
DOI : 10.1007/3-540-08138-0_5

W. Damm, Languages defined by higher type program schemes, Proceedings of the 4th International Colloquium on Automata, Languages, and Programming, pp.164-179, 1977.
DOI : 10.1007/3-540-08342-1_13

W. Damm, An algebraic extension of the Chomsky ??? hierarchy, Proceedings of the 8th Symposium, 1979.
DOI : 10.1007/3-540-09526-8_23

W. Damm and A. Goerdt, An automata-theoretical characterization of the OI-hierarchy, Information and Control, vol.71, issue.1-2, pp.1-32, 1986.
DOI : 10.1016/S0019-9958(86)80016-X

L. Doyen and J. Raskin, Antichain Algorithms for Finite Automata, Proceedings of 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.2-22, 2010.
DOI : 10.1007/978-3-642-12002-2_2

[. Ebbinghaus, J. Flum, and W. ?omas, Mathematical Logic, p.11, 1996.
DOI : 10.1007/978-1-4757-2355-7

[. Emerson and J. Y. Halpern, ???Sometimes??? and ???not never??? revisited: on branching versus linear time temporal logic, Journal of the ACM, vol.33, issue.1, pp.151-178, 1986.
DOI : 10.1145/4904.4999

J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon, Efficient Algorithms for Model Checking Pushdown Systems Lecture Notes in Computer Science, Proceedings of the 12th International Conference on Computer Aided Verification, pp.232-247, 2000.

[. Emerson and C. S. Jutla, Tree automata, mu-calculus and determinacy (extended abstract, Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, pp.368-377, 1991.
DOI : 10.1109/sfcs.1991.185392

J. Engelfriet, Iterated pushdown automata and complexity classes, Proceedings of the fifteenth annual ACM symposium on Theory of computing , STOC '83, 1983.
DOI : 10.1145/800061.808767

J. Engelfriet, Iterated stack automata and complexity classes, Information and Computation, vol.95, issue.1, pp.21-75, 1991.
DOI : 10.1016/0890-5401(91)90015-T
URL : http://doi.org/10.1016/0890-5401(91)90015-t

H. Everett, Recursive games''. In: Contributions to the theory of games, Annals of Mathematics Studies, vol.3, issue.129, pp.47-78, 1957.

[. Flum, E. Grädel, and ?. Wilke, Logic and Automata: History and Perspectives, 2007.
DOI : 10.5117/9789053565766

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi, Reasoning about Knowledge, 1995.

S. Fratani, Automates à piles de piles ?de piles, p.68, 2006.

A. Finkel, B. Willems, and P. Wolper, A Direct Symbolic Approach to Model Checking Pushdown Systems (extended abstract), Electronic Notes in Theoretical Computer Science, vol.9, pp.27-37, 1997.
DOI : 10.1016/S1571-0661(05)80426-8

H. Gimbert, Parity and Exploration Games on Infinite Graphs, Lecture Notes in Computer Science, vol.3210, pp.56-70, 2004.
DOI : 10.1007/978-3-540-30124-0_8
URL : https://hal.archives-ouvertes.fr/hal-00160739

[. Garland and D. Luckham, Program schemes, recursion schemes, and formal languages, Journal of Computer and System Sciences, vol.7, issue.2, pp.119-160, 1973.
DOI : 10.1016/S0022-0000(73)80040-6

H. Gimbert and Y. Oualhadj, Probabilistic Automata on Finite Words: Decidable and Undecidable Problems, Proceedings of the 37th International Colloquium on Automata, Languages, and Programming, pp.527-538, 2010.
DOI : 10.1007/978-3-642-14162-1_44
URL : https://hal.archives-ouvertes.fr/hal-00456538

[. Grädel, Banach-Mazur Games on Graphs, Proceedings of the 28th International Conference on Foundations of Software Technology and ?eoretical Computer Science LIPIcs. Schloss Dagstuhl -Leibniz- Zentrum für Informatik, pp.364-382, 2008.

Y. Gurevich and S. Shelah, Abstract, The Journal of Symbolic Logic, vol.13, issue.04, pp.1105-1119, 1983.
DOI : 10.2307/1971037

[. Grädel, Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, Lecture Notes in Computer Science, vol.2500, issue.123, pp.98-130, 2001.
DOI : 10.1007/3-540-36387-4

H. Gimbert and W. Zielonka, Perfect Information Stochastic Priority Games Lecture Notes in Computer Science, Proceedings of the 34th International Colloquium on Automata, Languages , and Programming, pp.850-861, 2007.

A. Haddad, IO vs OI in Higher-Order Recursion Schemes, Electronic Proceedings in ?eoretical Computer Science. 2012, pp.23-30
DOI : 10.4204/EPTCS.77.4
URL : https://hal.archives-ouvertes.fr/hal-00865681

A. Haddad, Shape-Preserving Transformations of Higher-Order Recursion Schemes, pp.61-68, 2013.

[. Hague, Global Model Checking of Higher-Order Pushdown Systems, pp.71-72, 2008.

M. Hague, Saturation of Concurrent Collapsible Pushdown Systems

J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata ?eory, Languages and Computation, NJ, 2007.
DOI : 10.1145/568438.568455

E. [. Martin, C. Hyland, and . Ong, On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model, Information and Computation, vol.163, issue.54, pp.285-408, 2000.

M. Hague and C. Ong, Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems, In: Logical Methods in Computer Science, vol.44, issue.72, pp.71-80, 2008.

M. Hague and C. Ong, Analysing Mu-Calculus Properties of Pushdown Systems, Proceedings of the 17th International SPIN Workshop, pp.187-192, 2010.
DOI : 10.1007/978-3-642-16164-3_14

M. Hague and C. Ong, A saturation method for the modal µcalculus over pushdown systems, Information and Computation, vol.2095, issue.72, pp.799-821, 2011.

[. Inaba and S. Maneth, ?e Complexity of Tree Transducer Output Languages, Proceedings of the 28th International Conference on Foundations of Software Technology and ?eoretical Computer Science, 2008.

K. Indermark, Schemes with recursion on higher types, Proceedings of the 5th Symposium, 1976.
DOI : 10.1007/3-540-07854-1_198

P. Jancar, Decidability of DPDA Language Equivalence via First-Order Grammars, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.415-424, 2012.
DOI : 10.1109/LICS.2012.51

D. Janin and I. Walukiewicz, On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic, Proceedings of the 7th International Conference on Concurrency ?eory, 1996.
DOI : 10.1007/3-540-61604-7_60

A. Kartzow, Collapsible Pushdown Graphs of Level 2 are Tree-Automatic, Logical Methods in Computer Science, vol.9, issue.1
DOI : 10.2168/LMCS-9(1:12)2013
URL : https://hal.archives-ouvertes.fr/inria-00455744

[. Knapik, D. Niwi?ski, and P. Urzyczyn, Deciding Monadic Theories of Hyperalgebraic Trees, Proceedings of the 5th conference on Typed Lambda Calculi and Applications, pp.253-267, 2001.
DOI : 10.1007/3-540-45413-6_21

[. Knapik, D. Niwi?ski, and P. Urzyczyn, Higher-Order Pushdown Trees Are Easy, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, pp.205-222, 2002.
DOI : 10.1007/3-540-45931-6_15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.5773

T. Knapik, D. Niwi?ski, P. Urzyczyn, and I. Walukiewicz, Unsafe Grammars and Panic Automata, Proceedings of the 32nd International Colloquium on Automata, Languages, and Programming, pp.1450-1461, 2005.
DOI : 10.1007/11523468_117
URL : https://hal.archives-ouvertes.fr/hal-00335729

[. Kobayashi and C. Ong, A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes, 2009 24th Annual IEEE Symposium on Logic In Computer Science, 2009.
DOI : 10.1109/LICS.2009.29

N. Kobayashi, Model-checking higher-order functions, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, PPDP '09, pp.25-36, 2009.
DOI : 10.1145/1599410.1599415
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.161.3824

N. Kobayashi, Types and higher-order recursion schemes for verification of higher-order programs, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.416-428, 2009.

N. Kobayashi, A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes, Proceedings of the 14th International Conference on Foundations of Software Science and Computational Structures, pp.260-274, 2011.
DOI : 10.1007/978-3-642-19805-2_18

N. Kobayashi, Higher-Order Model Checking: From ?eory to Practice

N. Kobayashi and . Gtr??s2, A model checker for recursion schemes based on games and types. A tool available at http, pp.87-89

A. Kartzow and P. Parys, Strictness of the Collapsible Pushdown Hierarchy, Proceedings of the 37th Symposium, pp.566-577, 2012.
DOI : 10.1007/978-3-642-32589-2_50

J. Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, pp.199-207, 2007.
DOI : 10.1007/s10990-007-9018-9
URL : https://hal.archives-ouvertes.fr/hal-00154508

T. [. Kumar and . Shiau, Existence of Value and Randomized Strategies in Zero-Sum Discrete-Time Stochastic Dynamic Games, SIAM Journal on Control and Optimization, vol.19, issue.5, pp.617-634, 1981.
DOI : 10.1137/0319039

[. Kobayashi, R. Sato, and H. Unno, Predicate abstraction and CEGAR for higher-order model checking, Proceedings of the 32nd ACM SIG- PLAN Conference on Programming Language Design and Implementation, pp.222-233, 2011.

A. Kucera, Turn-Based Stochastic Games Lectures in Game ?eory for Computer Scientists, pp.146-184, 2011.

[. Kupferman, M. Y. Vardi, and P. Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM, vol.47, issue.2, pp.312-360, 2000.
DOI : 10.1145/333979.333987

G. Lenzi, A hierarchy theorem for the ??-calculus, Proceedings of the 23rd International Colloquium on Automata, Languages, and Programming, pp.87-97, 1996.
DOI : 10.1007/3-540-61440-0_119

A. Da, C. Lopes, F. Laroussinie, and N. Markey, ATL with Strategy Contexts: Expressiveness and Model Checking, Proceedings of the 30th International Conference on Foundations of Software Technology and ?eoretical Computer Science LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp.120-132, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00599764

[. Löding, Infinite Games and Automata ?eory''. In: Lectures in Game ?eory for Computer Scientists, pp.38-73, 2011.

]. A. Mas74 and . Maslov, ?e hierarchy of indexed languages of an arbitrary level, In: Soviet mathematics Doklady, vol.15, pp.1170-1174, 1974.

]. A. Mas76 and . Maslov, Multilevel Stack Automata, Problems of Information Transmission, vol.12, issue.37, pp.38-43, 1976.

[. Miyano and T. Hayashi, Alternating Finite Automata on omega, In: ?eoretical Computer Science, vol.32, pp.321-330, 1984.

J. De and M. , Structures generated by higher-order grammars and the safety constraint, p.47, 2006.

[. Mogavero, A. Murano, and M. Y. Vardi, Reasoning About Strategies, Proceedings of the 30th International Conference on Foundations of Software Technology and ?eoretical Computer Science LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, pp.133-144, 2010.

A. W. Mostowski, Regular expressions for infinite trees and a standard form of automata, In: Computation theory. Lecture Notes in Computer Science, vol.208, issue.152, pp.157-168, 1985.
DOI : 10.1007/3-540-16066-3_15

A. W. Mostowski, Games with forbidden positions, 1991.

. E. David, P. E. Muller, and . Schupp, ?e ?eory of Ends, Pushdown Automata , and Second-Order Logic, Computer Science, vol.37, issue.72, pp.51-75, 1985.

E. David, P. E. Muller, and . Schupp, Simulating Alternating Tree Automata by Nondeterministic Automata, In: ?eoretical Computer Science1&2, vol.141, issue.100, pp.69-107, 1995.

A. A. Muchnik, Games on infinite trees and automata with blind alleys. A new proof of decidability for the monadic theory of two successor functions''. In: Semiotics and information science, Moscow: Akad. Nauk SSSR Vsesoyuz. Inst. Nauchn. i Tekhn. Inform. An English version was later published in the Bulletin of EATCS, vol.24, issue.48, pp.16-40, 1985.

M. Nivat, On the interpretation of recursive program schemes, Symposia Matematica, 1972.

D. Niwi?ski, On fixed-point clones, Proceedings of the 13th International Colloquium on Automata, Languages, and Programming, pp.464-473, 1986.
DOI : 10.1007/3-540-16761-7_96

P. Nro12-]-robin, S. J. Neatherway, C. Ramsay, and . Ong, A traversalbased algorithm for higher-order model checking, Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, pp.353-364, 2012.

D. Niwinski and I. Walukiewicz, A gap property of deterministic tree languages, Theoretical Computer Science, vol.303, issue.1, pp.215-231, 2003.
DOI : 10.1016/S0304-3975(02)00452-8

D. Niwinski and I. Walukiewicz, Deciding Nondeterministic Hierarchy of Deterministic Tree Automata, Electronic Notes in Theoretical Computer Science, vol.123, pp.195-208, 2005.
DOI : 10.1016/j.entcs.2004.05.015
URL : https://hal.archives-ouvertes.fr/hal-00353557

]. Ong06 and . Ong, On Model-Checking Trees Generated by Higher-Order Recursion Schemes, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pp.81-90, 2006.
DOI : 10.1109/LICS.2006.38

[. Ong, S. J. , and R. , Verifying higher-order functional programs with pattern-matching algebraic data types, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011.

J. Martin, A. Osborne, and . Rubinstein, A course in game theory, 1994.

P. Parys, Collapse Operation Increases Expressive Power of Deterministic Higher Order Pushdown Automata, Proceedings of the 28th Symposium on ?eoretical Aspects of Computer Science LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, pp.603-614, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00573593

P. Parys, On the Significance of the Collapse Operation, 2012 27th Annual IEEE Symposium on Logic in Computer Science, 2012.
DOI : 10.1109/LICS.2012.62

]. A. Paz71 and . Paz, Introduction to probabilistic automata, 1971.

S. Pinchinat, A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies, Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis, pp.253-267, 2007.
DOI : 10.1007/978-3-540-75596-8_19
URL : https://hal.archives-ouvertes.fr/inria-00555753

B. Puchala, Synthesis of Winning Strategies for Interaction under Partial Information, 2013.

O. Michael and . Rabin, Probabilistic Automata, Information and Control, vol.63, issue.101 142, pp.230-245, 1963.

O. Michael and . Rabin, Decidability of second-order theories and automata on infinite trees, In: Transactions of the American Mathematical Society, vol.141, issue.106, pp.1-35, 1969.

O. Michael and . Rabin, Automata on infinite objects and Church's problem, Conference Board of the Mathematical Sciences Regional Conference Series in Mathematics, issue.13, p.22, 1972.

J. H. Reif, Universal games of incomplete information, Proceedings of the eleventh annual ACM symposium on Theory of computing , STOC '79, pp.288-308, 1979.
DOI : 10.1145/800135.804422

R. D. Reisz, Decomposition ?eorems for Probabilistic Automata over Infinite Objects, Informatica, Lith. Acad. Sci, vol.10, issue.4, pp.427-440, 1999.

J. Renault, The Value of Repeated Games with an Informed Controller, Mathematics of Operations Research, vol.37, issue.1
DOI : 10.1287/moor.1110.0518
URL : https://hal.archives-ouvertes.fr/hal-00266378

W. Reps, S. Schwoon, S. Jha, and D. Melski, Weighted pushdown systems and their application to interprocedural dataflow analysis, Science of Computer Programming, vol.581, issue.2, pp.206-263, 2005.
DOI : 10.1016/j.scico.2005.02.009
URL : http://doi.org/10.1016/j.scico.2005.02.009

A. Rubinstein, Equilibrium in supergames with the overtaking criterion, Journal of Economic Theory, vol.21, issue.1, pp.1-9, 1979.
DOI : 10.1016/0022-0531(79)90002-4

S. Schwoon, Model-checking Pushdown Systems, p.16, 2002.

[. Suwimonteerabuth, J. Esparza, and S. Schwoon, Symbolic Context-Bounded Analysis of Multithreaded Java Programs, Proceedings of the 15th International SPIN Workshop, pp.270-287, 2008.
DOI : 10.1007/978-3-540-85114-1_19

S. Lloyd and . Shapley, Stochastic games, Proceedings of the National Academy of Science USA, vol.39, pp.1095-1100, 1953.

M. Sharir and A. Pnueli, Two approaches to interprocedural data flow analysis''. In: Program Flow Analysis: ?eory and Applications, pp.189-234, 1981.

[. Suwimonteerabuth, S. Schwoon, and J. Esparza, Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains, Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, pp.141-153, 2006.
DOI : 10.1007/11901914_13

C. Stirling, Decidability of Bisimulation Equivalence for Pushdown Processes. Tech. rep. EDI-INF-RR-0005, pp.20-90, 2000.

C. Stirling, Schema Revisited, Proceedings of Computer Science Logic, 14th Annual Conference of the EACSL, pp.126-138, 2000.
DOI : 10.1007/3-540-44622-2_7

C. Stirling, Decidability of DPDA equivalence, Theoretical Computer Science, vol.255, issue.1-2, pp.1-31, 2001.
DOI : 10.1016/S0304-3975(00)00389-3

C. Stirling, Second-Order Simple Grammars, Proceedings of the 17th International Conference on Concurrency ?eory, pp.509-523, 2006.
DOI : 10.1007/11817949_34
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.2531

C. Stirling, Dependency Tree Automata, Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures, pp.92-106, 2009.
DOI : 10.1007/11787006_30
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.2532

[. Salvati and I. Walukiewicz, Krivine Machines and Higher-Order Schemes, Proceedings of the 38th International Colloquium on Automata, Languages , and Programming, pp.162-173, 2011.
DOI : 10.1007/s10990-007-9019-8
URL : https://hal.archives-ouvertes.fr/hal-01121744

[. Salvati and I. Walukiewicz, Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata, Proceedings of Reachability Problems -6th International Workshop, pp.6-20, 2012.
DOI : 10.1007/978-3-642-33512-9_2
URL : https://hal.archives-ouvertes.fr/hal-00717718

[. Salvati and I. Walukiewicz, Evaluation is MSOL-compatible, Proceedings of the 33rd International Conference on Foundations of Software Technology and ?eoretical Computer Science LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, pp.103-114, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00773126

[. Salvati and I. Walukiewicz, Using Models to Model-Check Recursive Schemes, Proceedings of the 11th International Conference on Typed Lambda Calculi and Applications (TLCA'13, pp.189-204, 2013.
DOI : 10.1007/978-3-642-38946-7_15
URL : https://hal.archives-ouvertes.fr/hal-00741077

[. Sénizergues, L(A)=L(B)? A simplified decidability proof, Theoretical Computer Science, vol.281, issue.1-2, pp.555-608, 2002.
DOI : 10.1016/S0304-3975(02)00027-0

[. Sénizergues, The equivalence problem for deterministic pushdown automata is decidable, Proceedings of the 24th International Colloquium on Automata, Languages, and Programming, pp.671-681, 1997.
DOI : 10.1007/3-540-63165-8_221

H. Unno, N. Tabuchi, and N. Kobayashi, Verification of Tree-Processing Programs via Higher-Order Model Checking, Proceedings of 8th Asian Symposium on Programming Languages and Systems, 2010.
DOI : 10.1007/978-3-642-17164-2_22

M. Y. Vardi, Reasoning about the past with two-way automata, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming, pp.628-641, 1998.
DOI : 10.1007/BFb0055090

H. Völzer and D. Varacca, Defining Fairness in Reactive and Concurrent Systems, Journal of the ACM, vol.59, issue.3, pp.13-118, 2012.
DOI : 10.1145/2220357.2220360

Y. Moshe, ?. Vardi, and . Wilke, Automata: from logics to algorithms''. In: Logic and Automata: History and Perspectives, pp.629-736, 2007.

K. W. Wagner, Eine topologische Charakterisierung einiger Klassen regulärer Folgenmengen, Elektronische Informationsverarbeitung und Kybernetik, vol.13, issue.152, pp.473-487, 1977.

I. Walukiewicz, Pushdown Processes: Games and Model Checking, BRICS Report Series, vol.3, issue.54, pp.234-263, 2001.
DOI : 10.7146/brics.v3i54.20057
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4162

I. Walukiewicz, A landscape with games in the background, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pp.356-366, 2004.
DOI : 10.1109/LICS.2004.1319630

I. Walukiewicz, Pushdown Processes: Games and Model Checking, Proceeding of the 8th International Conference on Computer Aided Verification, 1996.
DOI : 10.7146/brics.v3i54.20057
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4162

L. Martin-de-wulf, ?. A. Doyen, J. Henzinger, and . Raskin, Antichains: A New Algorithm for Checking Universality of Finite Automata

L. Martin-de-wulf, N. Doyen, J. Maquet, and . Raskin, Alaska, Alaska''. In: Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, pp.240-245, 2008.
DOI : 10.1006/inco.1994.1092

. Weidner, Private communication, p.2014

[. Wilke, Alternating Tree Automata, Parity Games and Modal µ-Calculus

S. Wöhrle and W. ?omas, Model checking synchronized products of infinite transition systems, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., 2007.
DOI : 10.1109/LICS.2004.1319595

S. Wöhrle, Decision problems over infinite graphs higher-order pushdown systems and synchronized products, 2005.

A. Yakhnis and V. Yakhnis, Gurevich-Harrington's games defined by finite automata, Annals of Pure and Applied Logic, pp.265-294, 1993.
DOI : 10.1016/0168-0072(93)90239-A
URL : http://doi.org/10.1016/0168-0072(93)90239-a

S. Zeitman, Unforgettable Forgetful Determinacy, Journal of Logic and Computation, vol.4, issue.3, pp.273-283, 1994.
DOI : 10.1093/logcom/4.3.273

[. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theoretical Computer Science, vol.200, issue.1-2, pp.1-2, 1998.
DOI : 10.1016/S0304-3975(98)00009-7

.. Collapsible-pushdown-automata, 17 1.3 A Collapsible Pushdown Approach to Verification

). ?e-tree-pref-1u, 32 5.2.2 Generating a Tree with Branch Language ta n b n c n d | n ? 1u with a Recursion Scheme, p.33

.. Collapsible-pushdown-automata, 37 6.1 Higher-Order Stacks and their Operations, p.37

. Safe and .. The-unsafe-hierarchies, 47 8.1 ?e Safety Constraint 47 8.2 Hierarchies of Trees, Hierarchies of Labelled Transition Systems 48 8.3 ?e Safe Hierarchies & the Caucal Hierarchies 50 8.5 Back to Safety: Damm's View of Safety, 51 8.6 ?e Safe vs Unsafe Conjecture, p.53

.. Back-to-logic, 80 11.1 Labelled Transition Systems, pp.11-81

S. Techniques, C. The, and O. Tool, 84 12.1.1 Checking Properties of Recursion Schemes in Practice: Related Work, Experimental Results, vol.86, issue.87, pp.12-13

.. Imperfect-information-games, 102 1.3.1 ?e Randomised Strategies Setting, 103 1.3.2 ?e Pure Strategies Setting . . 103 1.3.3 Related Work in Classical Game ?eory . . . . . . . . . . . . . . . . . 104

C. Automata and .. Constraints, 108 3.1 Automata with Cardinality Constraints 108 3.2 Counting Rejecting Branches, 109 3.2.1 ?e Case of Languages L Rej ?Count (A) . . . . . . . . . . . . . . . . . . . 109

S. Imperfect-information and .. Games, 125 6.1 Definitions 126 6.1.1 Concurrent Arenas Probability Space and Outcomes of Strategies, p.129

R. ?e, E. Using-imperfect-information-game, and .. , 137 7.2.1 A Half-Perfect-Information Emptiness Game, 138 7.2.2 Comparison with the Standard Approach . . . . . . . . . . . . . . . . 138

B. Non-deterministic-automata-the-probabilistic-setting and .. , 142 8.1 Definitions, p.142

U. Decidability and .. Results, 145 8.3.1 Partial Observation Markov Decision Processes, p.146

O. Problems and P. , 150 9.1 Qualitative Tree Languages vs Regular Tree Languages, 150 9.2 ?e Class of Qualitative Tree Languages vs Distribution µ p . . . . . . . . . . . 151