@inproceedings(Alur97,
 author       = {Rajeev Alur and Thomas Henzinger and Orna Kupferman},
 year         = {1997},
 title        = {Alternating-time Temporal Logic},
 booktitle    = {Journal of the ACM},
 publisher    = {IEEE Computer Society Press},
 pages        = {100--109},
 doi          = {10.1007/3-540-49213-5_2},
)
@book(PrinciplesMC,
 author       = {Christel Baier and Joost-Pieter Katoen},
 year         = {2008},
 title        = {Principles of model checking},
 volume       = {26202649},
 publisher    = {MIT press Cambridge},
)
@inproceedings(DBLP:conf/stoc/CaludeJKL017,
 author       = {Cristian S. Calude and Sanjay Jain and Bakhadyr Khoussainov and Wei Li and Frank Stephan},
 year         = {2017},
 title        = {Deciding parity games in quasipolynomial time},
 editor       = {Hamed Hatami and Pierre McKenzie and Valerie King},
 booktitle    = {Proceedings of the 49th Annual {ACM} {SIGACT} Symposium on Theory of Computing, {STOC} 2017, Montreal, QC, Canada, June 19-23, 2017},
 publisher    = {{ACM}},
 pages        = {252--263},
 doi          = {10.1145/3055399.3055409},
)
@incollection(Church63,
 author       = {Alonzo Church},
 year         = {1963},
 title        = {Logic, arithmetic, and automata},
 booktitle    = {International Congress of Mathematicians (Stockholm, 1962)},
 publisher    = {Institute Mittag-Leffler},
 address      = {Djursholm},
 pages        = {23--35},
 doi          = {10.2307/2270398},
)
@inproceedings(ctl-origin,
 author       = {Edmund M Clarke and E Allen Emerson},
 year         = {1981},
 title        = {Design and synthesis of synchronization skeletons using branching time temporal logic},
 booktitle    = {Workshop on Logic of Programs},
 organization = {Springer},
 pages        = {52--71},
 doi          = {10.1007/BFb0025774},
)
@article(ctlstar-origin,
 author       = {E. Allen Emerson and Joseph Y. Halpern},
 year         = {1986},
 title        = {{`Sometimes' and `Not Never' Revisited: On Branching versus Linear Time Temporal Logic}},
 journal      = {J. ACM},
 volume       = {33},
 number       = {1},
 pages        = {151--178},
 doi          = {10.1145/4904.4999},
)
@article(ES84,
 author       = {E. Allen Emerson and A. Prasad Sistla},
 year         = {1984},
 title        = {Deciding full branching time logic},
 journal      = {Information and Control},
 volume       = {61},
 number       = {3},
 pages        = {175 -- 201},
 doi          = {10.1016/S0019-9958(84)80047-9},
)
@article(BS,
 author       = {Bernd Finkbeiner and Sven Schewe},
 year         = {2013},
 title        = {Bounded synthesis},
 journal      = {{STTT}},
 volume       = {15},
 number       = {5-6},
 pages        = {519--539},
 doi          = {10.1007/s10009-012-0228-z},
)
@inproceedings(syntcomp,
 author       = {Swen Jacobs and Roderick Bloem and Romain Brenguier and Ayrat Khalimov and Felix Klein and Robert K{\"{o}}nighofer and Jens Kreber and Alexander Legg and Nina Narodytska and Guillermo A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Leonid Ryzhyk and Ocan Sankur and Martina Seidl and Leander Tentrup and Adam Walker},
 year         = {2016},
 title        = {The 3rd Reactive Synthesis Competition {(SYNTCOMP} 2016): Benchmarks, Participants {\&} Results},
 editor       = {Ruzica Piskac and Rayna Dimitrova},
 booktitle    = {Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016.},
 series       = {{EPTCS}},
 volume       = {229},
 pages        = {149--177},
 doi          = {10.4204/EPTCS.229.12},
)
@inbook(CTLstarCAV,
 author       = {Ayrat Khalimov and Roderick Bloem},
 year         = {2017},
 title        = {Bounded Synthesis for Streett, Rabin, and CTL*},
 pages        = {333--352},
 publisher    = {Springer International Publishing},
 doi          = {10.1007/978-3-319-63390-9_18},
)
@inproceedings(party,
 author       = {Ayrat Khalimov and Swen Jacobs and Roderick Bloem},
 year         = {2013},
 title        = {PARTY parameterized synthesis of token rings},
 booktitle    = {Computer Aided Verification},
 organization = {Springer},
 pages        = {928--933},
 doi          = {10.1007/978-3-642-39799-8_66},
)
@article(informatio,
 author       = {Orna Kupferman and Moshe Y. Vardi},
 year         = {1999},
 title        = {Church's problem revisited},
 journal      = {Bulletin of Symbolic Logic},
 volume       = {5},
 number       = {2},
 pages        = {245--263},
 doi          = {10.1145/357084.357090},
)
@article(ATA,
 author       = {Orna Kupferman and Moshe Y. Vardi and Pierre Wolper},
 year         = {2000},
 title        = {An Automata-theoretic Approach to Branching-time Model Checking},
 journal      = {J. ACM},
 volume       = {47},
 number       = {2},
 pages        = {312--360},
 doi          = {10.1145/333979.333987},
)
@article(Piterman07,
 author       = {Nir Piterman},
 year         = {2007},
 title        = {{From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata}},
 journal      = {{Logical Methods in Computer Science}},
 volume       = {{Volume 3, Issue 3}},
 doi          = {10.1109/LICS.2006.28},
)
@inproceedings(pnueli1977temporal,
 author       = {Amir Pnueli},
 year         = {1977},
 title        = {The temporal logic of programs},
 booktitle    = {Foundations of Computer Science, 1977., 18th Annual Symposium on},
 organization = {IEEE},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@inproceedings(DBLP:conf/popl/PnueliR89,
 author       = {Amir Pnueli and Roni Rosner},
 year         = {1989},
 title        = {On the Synthesis of a Reactive Module},
 booktitle    = {Conference Record of the Sixteenth Annual {ACM} Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989},
 publisher    = {{ACM} Press},
 pages        = {179--190},
 doi          = {10.1145/75277.75293},
)
@phdthesis(RosnerThesis,
 author       = {Roni Rosner},
 year         = {1992},
 title        = {Modular synthesis of reactive systems},
 school       = {PhD thesis, Weizmann Institute of Science},
)
@inproceedings(Safra,
 author       = {Shmuel Safra},
 year         = {1988},
 title        = {On the Complexity of omega-Automata},
 booktitle    = {29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988},
 publisher    = {{IEEE} Computer Society},
 pages        = {319--327},
 doi          = {10.1109/SFCS.1988.21948},
)
@inproceedings(Schewe/09/determinise,
 author       = {Sven Schewe},
 year         = {2009},
 title        = {Tighter Bounds for the Determinisation of {B\"u}chi Automata},
 booktitle    = {Proceedings of the Twelfth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2009), 22--29 March, York, England, UK},
 series       = {Lecture Notes in Computer Science},
 volume       = {5504},
 publisher    = {Springer-Verlag},
 pages        = {167--181},
 doi          = {10.1007/978-3-642-00596-1_13},
)
@inproceedings(LTL-vs-CTL,
 author       = {Moshe Y Vardi},
 year         = {2001},
 title        = {Branching vs. linear time: Final showdown},
 booktitle    = {TACAS},
 volume       = {1},
 organization = {Springer},
 pages        = {1--22},
 doi          = {10.1007/3-540-45319-9_1},
)