@article(AH98,
 author       = {R.\nobreakspace Alur and T.A. Henzinger},
 year         = {1998},
 title        = {{Finitary Fairness.}},
 journal      = {TOPLAS},
 volume       = {20},
 number       = {6},
 pages        = {1171--1194},
 doi          = {{10.1145/295656.295659}},
)
@article(AHK02,
 author       = {R.\nobreakspace Alur and T.A. Henzinger and O.\nobreakspace Kupferman},
 year         = {2002},
 title        = {{Alternating-Time Temporal Logic.}},
 journal      = {JACM},
 volume       = {49},
 number       = {5},
 pages        = {672--713},
 doi          = {{10.1145/585265.585270}},
)
@article(alur2004deterministic,
 author       = {R.\nobreakspace Alur and {La T}orre, S.\nobreakspace},
 year         = {2004},
 title        = {Deterministic generators and games for LTL fragments},
 journal      = {ACM Transactions on Computational Logic (TOCL)},
 volume       = {5},
 number       = {1},
 pages        = {1--25},
 doi          = {10.1145/963927.963928},
)
@inproceedings(AMRZ16,
 author       = {B.\nobreakspace Aminof and A.\nobreakspace Murano and S.\nobreakspace Rubin and F.\nobreakspace Zuleger},
 year         = {2016},
 title        = {{Prompt Alternating-Time Epistemic Logics}},
 booktitle    = {KR'16},
 publisher    = {AAAI Press},
 pages        = {258--267},
)
@article(BLMV08,
 author       = {P.A. Bonatti and C.\nobreakspace Lutz and A.\nobreakspace Murano and M.Y. Vardi},
 year         = {2008},
 title        = {{The Complexity of Enriched muCalculi.}},
 journal      = {LMCS},
 volume       = {4},
 number       = {3},
 pages        = {1--27},
 doi          = {{10.2168/LMCS-4(3:11)2008}},
)
@article(BMP10,
 author       = {L.\nobreakspace Bozzelli and A.\nobreakspace Murano and A.\nobreakspace Peron},
 year         = {2010},
 title        = {{Pushdown Module Checking.}},
 journal      = {FMSD},
 volume       = {36},
 number       = {1},
 pages        = {65--95},
 doi          = {{10.1007/s10703-010-0093-x}},
)
@article(CHH09,
 author       = {K.\nobreakspace Chatterjee and T.A. Henzinger and F.\nobreakspace Horn},
 year         = {2010},
 title        = {{Finitary Winning in omega-Regular Games.}},
 journal      = {TOCL},
 volume       = {11},
 number       = {1},
 pages        = {1:1--26},
 doi          = {{10.1145/1614431.1614432}},
)
@inproceedings(CE81,
 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},
 publisher    = {Springer},
 pages        = {52--71},
 doi          = {{10.1007/BFb0025774}},
)
@article(CES86,
 author       = {E.M. Clarke and E.A. Emerson and A.P. Sistla},
 year         = {1986},
 title        = {{Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications.}},
 journal      = {TOPLAS},
 volume       = {8},
 number       = {2},
 pages        = {244--263},
 doi          = {{10.1145/5397.5399}},
)
@book(CGP02,
 author       = {E.M. Clarke and O.\nobreakspace Grumberg and D.A. Peled},
 year         = {2002},
 title        = {{Model Checking.}},
 publisher    = {MIT Press},
)
@article(EH85,
 author       = {E.A. Emerson and J.Y. Halpern},
 year         = {1985},
 title        = {{Decision Procedures and Expressiveness in the Temporal Logic of Branching Time.}},
 journal      = {JCSS},
 volume       = {30},
 number       = {1},
 pages        = {1--24},
 doi          = {{10.1016/0022-0000(85)90001-7}},
)
@article(EH86,
 author       = {E.A. Emerson and J.Y. Halpern},
 year         = {1986},
 title        = {{``Sometimes'' and ``Not Never'' Revisited: On Branching Versus Linear Time.}},
 journal      = {JACM},
 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 (Extended Abstract).}},
 booktitle    = {FOCS'88},
 publisher    = {IEEE Computer Society},
 pages        = {328--337},
 doi          = {10.1109/SFCS.1988.21949},
)
@article(FMP08,
 author       = {A.\nobreakspace Ferrante and A.\nobreakspace Murano and M.\nobreakspace Parente},
 year         = {2008},
 title        = {{Enriched Mu-Calculi Module Checking.}},
 journal      = {LMCS},
 volume       = {4},
 number       = {3},
 pages        = {1--21},
 doi          = {{10.2168/LMCS-4(3:1)2008}},
)
@book(GTW02,
 author       = {E.\nobreakspace Gr{\"a}del and W.\nobreakspace Thomas and T.\nobreakspace Wilke},
 year         = {2002},
 title        = {{Automata, Logics, and Infinite Games: A Guide to Current Research.}},
 series       = {LNCS 2500},
 publisher    = {Springer},
 doi          = {{10.1007/3-540-36387-4}},
)
@article(Kri63,
 author       = {S.A. Kripke},
 year         = {1963},
 title        = {{Semantical Considerations on Modal Logic.}},
 journal      = {APF},
 volume       = {16},
 pages        = {83--94},
 doi          = {{10.1002/malq.19630090502}},
)
@article(KMM06,
 author       = {O.\nobreakspace Kupferman and G.\nobreakspace Morgenstern and A.\nobreakspace Murano},
 year         = {2006},
 title        = {{Typeness for omega-Regular Automata.}},
 journal      = {IJFCS},
 volume       = {17},
 number       = {4},
 pages        = {869--884},
 doi          = {{10.1142/S0129054106004157}},
)
@inproceedings(KPV02,
 author       = {O.\nobreakspace Kupferman and N.\nobreakspace Piterman and M.Y. Vardi},
 year         = {2002},
 title        = {{Pushdown Specifications.}},
 booktitle    = {LPAR'02},
 series       = {LNCS 2514},
 publisher    = {Springer},
 pages        = {262--277},
 doi          = {{10.1007/3-540-36078-6\_18}},
)
@article(KPV09,
 author       = {O.\nobreakspace Kupferman and N.\nobreakspace Piterman and M.Y. Vardi},
 year         = {2009},
 title        = {{From Liveness to Promptness.}},
 journal      = {FMSD},
 volume       = {34},
 number       = {2},
 pages        = {83--103},
 doi          = {{10.1007/s10703-009-0067-z}},
)
@article(KPV12,
 author       = {O.\nobreakspace Kupferman and A.\nobreakspace Pnueli and M.Y. Vardi},
 year         = {2012},
 title        = {{Once and For All.}},
 journal      = {JCSS},
 volume       = {78},
 number       = {3},
 pages        = {981--996},
 doi          = {{10.1016/j.jcss.2011.08.006}},
)
@article(KVW00,
 author       = {O.\nobreakspace Kupferman and M.Y. Vardi and P.\nobreakspace Wolper},
 year         = {2000},
 title        = {{An Automata Theoretic Approach to Branching-Time Model Checking.}},
 journal      = {JACM},
 volume       = {47},
 number       = {2},
 pages        = {312--360},
 doi          = {{10.1145/333979.333987}},
)
@article(KVW01,
 author       = {O.\nobreakspace Kupferman and M.Y. Vardi and P.\nobreakspace Wolper},
 year         = {2001},
 title        = {{Module Checking.}},
 journal      = {IC},
 volume       = {164},
 number       = {2},
 pages        = {322--344},
 doi          = {{10.1006/inco.2000.2893}},
)
@article(MMPV14,
 author       = {F.\nobreakspace Mogavero and A.\nobreakspace Murano and G.\nobreakspace Perelli and M.Y. Vardi},
 year         = {2014},
 title        = {{Reasoning About Strategies: On the Model-Checking Problem.}},
 journal      = {TOCL},
 volume       = {15},
 number       = {4},
 pages        = {34:1--42},
 doi          = {{10.1145/2631917}},
)
@article(MMS15prompt,
 author       = {F.\nobreakspace Mogavero and A.\nobreakspace Murano and L.\nobreakspace Sorrentino},
 year         = {2015},
 title        = {On Promptness in Parity Games},
 journal      = {Fundamenta Informaticae},
 volume       = {139},
 number       = {3},
 pages        = {277--305},
 doi          = {{10.3233/FI-2015-1235}},
)
@inproceedings(Pnu77,
 author       = {A.\nobreakspace Pnueli},
 year         = {1977},
 title        = {{The Temporal Logic of Programs.}},
 booktitle    = {FOCS'77},
 publisher    = {IEEE Computer Society},
 pages        = {46--57},
 doi          = {{10.1109/SFCS.1977.32}},
)
@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}},
)
@inproceedings(VW86b,
 author       = {M.Y. Vardi and P.\nobreakspace Wolper},
 year         = {1986},
 title        = {{An Automata-Theoretic Approach to Automatic Program Verification.}},
 booktitle    = {LICS'86},
 publisher    = {IEEE Computer Society},
 pages        = {332--344},
)
@article(Wol83,
 author       = {P.\nobreakspace Wolper},
 year         = {1983},
 title        = {{Temporal Logic Can Be More Expressive.}},
 journal      = {IC},
 volume       = {56},
 number       = {1-2},
 pages        = {72--99},
 doi          = {{10.1016/S0019-9958(83)80051-5}},
)
@article(Zie98,
 author       = {W.\nobreakspace Zielonka},
 year         = {1998},
 title        = {{Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees.}},
 journal      = {TCS},
 volume       = {200},
 number       = {1-2},
 pages        = {135--183},
 doi          = {{10.1016/S0304-3975(98)00009-7}},
)