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