@inproceedings(AGJ07,
 author       = {{\r A}gotnes, T. and V. Goranko and W. Jamroga},
 year         = {2007},
 title        = {Alternating-time temporal logics with irrevocable strategies},
 booktitle    = {TARK'07},
 pages        = {15--24},
 doi          = {10.1145/1324249.1324256},
)
@inproceedings(Alfaro04three,
 author       = {L. de Alfaro and P. Godefroid and R. Jagadeesan},
 year         = {2004},
 title        = {Three-Valued Abstractions of Games: Uncertainty, but with Precision},
 booktitle    = {LICS'04},
 publisher    = {IEEE},
 pages        = {170--179},
 doi          = {10.1109/LICS.2004.1319611},
)
@article(AlurHK02,
 author       = {R. Alur and T. A. Henzinger and O. Kupferman},
 year         = {2002},
 title        = {Alternating-time temporal logic},
 journal      = {Journal of the {ACM}},
 volume       = {49},
 number       = {5},
 pages        = {672--713},
 doi          = {10.1145/585265.585270},
)
@article(Aminof13pushdown-jc,
 author       = {B. Aminof and A. Legay and A. Murano and O. Serre and M. Y. Vardi},
 year         = {2013},
 title        = {Pushdown module checking with imperfect information},
 journal      = {Inf. Comput.},
 volume       = {223},
 number       = {1},
 pages        = {1--17},
 doi          = {10.1016/j.ic.2012.11.005},
)
@article(Basu07local,
 author       = {S. Basu and P. S. Roop and R. Sinha},
 year         = {2007},
 title        = {Local Module Checking for {CTL} Specifications},
 journal      = {ENTCS 176},
 number       = {2},
 pages        = {125--141},
 doi          = {10.1016/j.entcs.2006.02.035},
)
@inproceedings(Bozzelli11newpushown,
 author       = {L. Bozzelli},
 year         = {2011},
 title        = {New results on pushdown module checking with imperfect information},
 booktitle    = {{GandALF}'11},
 series       = {EPTCS 54},
 pages        = {162--177},
 doi          = {10.4204/EPTCS.54.12},
)
@article(Bozzelli10pushdown,
 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(1)},
 pages        = {114--133},
 doi          = {10.1145/322234.322243},
)
@article(CHP10,
 author       = {K. Chatterjee and T. A. Henzinger and N. Piterman},
 year         = {2010},
 title        = {Strategy logic},
 journal      = {Inf. Comput.},
 volume       = {208},
 number       = {6},
 pages        = {677--693},
 doi          = {10.1016/j.ic.2009.07.004},
)
@inproceedings(Clarke81ctl,
 author       = {E.M. Clarke and E.A. Emerson},
 year         = {1981},
 title        = {Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic},
 booktitle    = {LP'81},
 series       = {LNCS 131},
 pages        = {52--71},
 doi          = {10.1007/BFb0025774},
)
@article(EmersonH86,
 author       = {E.A. Emerson and J.Y. Halpern},
 year         = {1986},
 title        = {"{S}ometimes" and "{N}ot {N}ever" revisited: on branching versus linear time temporal logic},
 journal      = {Journal of the ACM},
 volume       = {33},
 number       = {1},
 pages        = {151--178},
 doi          = {10.1145/4904.4999},
)
@inproceedings(EJ88,
 author       = {E.A. Emerson and C.S. Jutla},
 year         = {1988},
 title        = {The Complexity of Tree Automata and Logics of Programs},
 booktitle    = {FOCS'88},
 pages        = {328--337},
 doi          = {10.1109/SFCS.1988.21949},
)
@article(Ferrante08enriched,
 author       = {A. Ferrante and A. Murano and M. Parente},
 year         = {2008},
 title        = {Enriched $\mu$-Calculi Module Checking},
 journal      = {Logical Methods in Computer Science},
 volume       = {4},
 number       = {3:1},
 pages        = {1--21},
 doi          = {10.2168/LMCS-4(3:1)2008},
)
@inproceedings(Godefroid03open,
 author       = {P. Godefroid},
 year         = {2003},
 title        = {Reasoning about Abstract Open Systems with Generalized Module Checking},
 booktitle    = {EMSOFT'03},
 series       = {LNCS 2855},
 publisher    = {Springer},
 pages        = {223--240},
 doi          = {10.1007/978-3-540-45212-6_15},
)
@inproceedings(JamrogaM14,
 author       = {W. Jamroga and A. Murano},
 year         = {2014},
 title        = {On module checking and strategies},
 booktitle    = {AAMAS'14},
 publisher    = {{IFAAMAS/ACM}},
 pages        = {701--708},
)
@inproceedings(JamrogaM15,
 author       = {W. Jamroga and A. Murano},
 year         = {2015},
 title        = {Module Checking of Strategic Ability},
 booktitle    = {AAMAS'15},
 publisher    = {{ACM}},
 pages        = {227--235},
)
@inproceedings(KupfermanV98,
 author       = {O. Kupferman and M. Y. Vardi},
 year         = {1998},
 title        = {Weak Alternating Automata and Tree Automata Emptiness},
 booktitle    = {{STOC}'98},
 publisher    = {{ACM}},
 pages        = {224--233},
 doi          = {10.1145/276698.276748},
)
@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(Kupferman97revisited,
 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 {A}utomata-{T}heoretic {A}pproach to {B}ranching-{T}ime {M}odel {C}hecking},
 journal      = {Journal of the ACM},
 volume       = {47},
 number       = {2},
 pages        = {312--360},
 doi          = {10.1145/333979.333987},
)
@article(LaroussinieM14,
 author       = {F. Laroussinie and N. Markey},
 year         = {2014},
 title        = {Quantified {CTL:} Expressiveness and Complexity},
 journal      = {Logical Methods in Computer Science},
 volume       = {10},
 number       = {4},
 doi          = {10.2168/LMCS-10(4:17)2014},
)
@article(LaroussinieM15,
 author       = {F. Laroussinie and N. Markey},
 year         = {2015},
 title        = {Augmenting {ATL} with strategy contexts},
 journal      = {Inf. Comput.},
 volume       = {245},
 pages        = {98--123},
 doi          = {10.1016/j.ic.2014.12.020},
)
@article(Martinelli07specification,
 author       = {F. Martinelli and I. Matteucci},
 year         = {2007},
 title        = {An Approach for the Specification, Verification and Synthesis of Secure Systems},
 journal      = {ENTCS 168},
 pages        = {29--43},
 doi          = {10.1016/j.entcs.2006.12.003},
)
@article(MMPV14,
 author       = {F. Mogavero and A. Murano and G. Perelli and M. Y. Vardi},
 year         = {2014},
 title        = {Reasoning About Strategies: On the Model-Checking Problem},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {15},
 number       = {4},
 pages        = {34:1--34:47},
 doi          = {10.1145/2631917},
)
@inproceedings(Murano08hierarchical,
 author       = {A. Murano and M. Napoli and M. Parente},
 year         = {2008},
 title        = {Program Complexity in Hierarchical Module Checking},
 booktitle    = {LPAR'08},
 series       = {LNCS 5330},
 publisher    = {Springer},
 pages        = {318--332},
 doi          = {10.1007/978-3-540-89439-1_23},
)
@inproceedings(Pnueli77,
 author       = {A. Pnueli},
 year         = {1977},
 title        = {The Temporal Logic of Programs},
 booktitle    = {FOCS'77},
 publisher    = {IEEE},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@inproceedings(Queille81verification,
 author       = {J.P. Queille and J. Sifakis},
 year         = {1982},
 title        = {Specification and verification of concurrent programs in {C}esar},
 booktitle    = {SP'82},
 series       = {LNCS 137},
 publisher    = {Springer},
 pages        = {337--351},
 doi          = {10.1007/3-540-11494-7_22},
)
@inproceedings(Safra88,
 author       = {S. Safra},
 year         = {1988},
 title        = {On the Complexity of $\omega$-Automata},
 booktitle    = {FOCS'88},
 publisher    = {{IEEE}},
 pages        = {319--327},
 doi          = {10.1109/SFCS.1988.21948},
)
@inproceedings(Schewe08,
 author       = {S. Schewe},
 year         = {2008},
 title        = {{ATL*} {S}atisfiability Is {2EXPTIME}-Complete},
 booktitle    = {ICALP'08},
 series       = {LNCS 5126},
 publisher    = {Springer},
 pages        = {373--385},
 doi          = {10.1007/978-3-540-70583-3_31},
)
@inproceedings(ScheweF06,
 author       = {S. Schewe and B. Finkbeiner},
 year         = {2006},
 title        = {Satisfiability and Finite Model Property for the Alternating-Time \emph{mu}-Calculus},
 booktitle    = {CSL'06},
 series       = {LNCS 4207},
 publisher    = {Springer},
 pages        = {591--605},
 doi          = {10.1007/11874683_39},
)
@article(VardiW94,
 author       = {M. Y. Vardi and P. Wolper},
 year         = {1994},
 title        = {Reasoning About Infinite Computations},
 journal      = {Inf. Comput.},
 volume       = {115},
 number       = {1},
 pages        = {1--37},
 doi          = {10.1006/inco.1994.1092},
)
@inproceedings(Var98,
 author       = {M.Y. Vardi},
 year         = {1998},
 title        = {Reasoning about the past with two-way automata},
 booktitle    = {ICALP'98},
 series       = {LNCS 1443},
 publisher    = {Springer},
 pages        = {628--641},
 doi          = {10.1007/BFb0055090},
)