R. Alur, S. Chaudhuri & P. Madhusudan (2006):
Languages of Nested Trees.
In: CAV'06,
LNCS 4144.
Springer,
pp. 329–342,
doi:10.1007/11817963_31.
B. Aminof, A. Murano & M.Y. Vardi (2007):
Pushdown Module Checking with Imperfect Information.
In: CONCUR'07,
LNCS 4703.
Springer,
pp. 460–475,
doi:10.1007/978-3-540-74407-8_31.
T. Ball & S. Rajamani (2000):
Bebop: a symbolic model checker for boolean programs.
In: 7th SPIN Workshop,
LNCS 1885.
Springer,
pp. 113–130,
doi:10.1007/3-540-46419-0_21.
A. Bouajjani, J. Esparza & O. Maler (1997):
Reachability Analysis of Pushdown Automata: Application to Model-Checking.
In: CONCUR'97,
LNCS 1243.
Springer,
pp. 135–150,
doi:10.1007/3-540-63141-0_10.
L. Bozzelli (2007):
Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages.
In: CONCUR'07,
LNCS 4703.
Springer,
pp. 476–491,
doi:10.1007/978-3-540-74407-8_32.
L. Bozzelli (2007):
Complexity results on branching-time pushdown model checking.
Theor. Comput. Sci. 379(1–2),
pp. 286–297,
doi:10.1016/j.tcs.2007.03.049.
L. Bozzelli, A. Murano & A. Peron (2010):
Pushdown module checking.
Formal Methods in System Design 36(1),
pp. 65–95,
doi:10.1007/s10703-010-0093-x.
A.K. Chandra, D.C. Kozen & L.J. Stockmeyer (1981):
Alternation.
Journal of the ACM 28(1),
pp. 114–133,
doi:10.1145/322234.322243.
K. Chatterjee & T.A. Henzinger (2005):
Semiperfect-Information Games.
In: FSTTCS'05,
LNCS 3821.
Springer,
pp. 1–18,
doi:10.1007/11590156_1.
E.M. Clarke & E.A. Emerson (1981):
Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic.
In: Proceedings of Workshop on Logic of Programs,
LNCS 131.
Springer,
pp. 52–71.
A. Ferrante, A. Murano & M. Parente (2007):
Enriched μ-Calculus Pushdown Module Checking.
In: LPAR'07,
LNCS 4790.
Springer,
pp. 438–453,
doi:10.1007/978-3-540-75560-9_32.
J.E. Hopcroft & J.D. Ullman (1979):
Introduction to Automata Theory, Languages and Computation.
Addison-Wesley.
O. Kupferman & M.Y. Vardi (1996):
Module Checking.
In: CAV'96,
LNCS 1102.
Springer,
pp. 75–86,
doi:10.1007/3-540-61474-5_59.
O. Kupferman & M.Y. Vardi (1997):
Module Checking Revisited.
In: CAV'97,
LNCS 1254.
Springer,
pp. 36–47,
doi:10.1007/3-540-63166-6_7.
O. Kupferman, M.Y. Vardi & P. Wolper (2000):
An automata-theoretic approach to branching-time model checking.
Journal of the ACM 47(2),
pp. 312–360,
doi:10.1145/333979.333987.
O. Kupferman, M.Y. Vardi & P. Wolper (2001):
Module Checking.
Inf. Comput. 164(2),
pp. 322–344,
doi:10.1006/inco.2000.2893.
J.H Reif (1984):
The Complexity of Two-Player Games of Incomplete Information.
J. Comput. Syst. Sci. 29(2),
pp. 274–301,
doi:doi:10.1016/0022-0000(84)90034-5.
I. Walukiewicz (1996):
Pushdown processes: Games and Model Checking.
In: CAV'96,
LNCS 1102.
Springer,
pp. 62–74,
doi:10.1007/3-540-61474-5_58.
I. Walukiewicz (2000):
Model Checking CTL Properties of Pushdown Systems.
In: FSTTCS'00,
LNCS 1974.
Springer,
pp. 127–138,
doi:10.1007/3-540-44450-5_10.