@article(DBLP:journals/jacm/AlurHK02,
 author       = "Rajeev Alur and Thomas A. Henzinger and Orna Kupferman",
 year         = "2002",
 title        = "Alternating-time temporal logic",
 journal      = "J. ACM",
 volume       = "49",
 number       = "5",
 pages        = "672--713",
 doi          = "10.1145/585265.585270",
)
@article(DBLP:journals/entcs/BloemGJPPW07,
 author       = "Roderick Bloem and Stefan Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer",
 year         = "2007",
 title        = "Specify, Compile, Run: Hardware from {PSL}",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "190",
 number       = "4",
 pages        = "3--16",
 doi          = "10.1016/j.entcs.2007.09.004",
)
@inproceedings(DBLP:conf/dac/ClarkeGMZ95,
 author       = "Edmund M. Clarke and Orna Grumberg and Kenneth L. McMillan and Xudong Zhao",
 year         = "1995",
 title        = "Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking",
 booktitle    = "DAC",
 pages        = "427--432",
 doi          = "10.1145/217474.217565",
)
@inproceedings(DBLP:conf/lata/Ehlers10,
 author       = "R{\"u}diger Ehlers",
 year         = "2010",
 title        = "Short Witnesses and Accepting Lassos in $\omega $-Automata",
 editor       = "Adrian Horia Dediu and Henning Fernau and Carlos Mart\'{\i }n-Vide",
 booktitle    = "LATA",
 series       = "LNCS",
 volume       = "6031",
 publisher    = "Springer",
 pages        = "261--272",
 doi          = "10.1007/978-3-642-13089-2_22",
)
@techreport(atr080,
 author       = "R\"{u}diger Ehlers",
 year         = "2011",
 title        = "Small witnesses, accepting lassos and winning strategies in $\omega $-automata and games",
 type         = "Technical Report",
 number       = "80",
 institution  = "SFB/TR 14 AVACS",
 note         = "ISSN: 1860-9821, http://www.avacs.org.",
)
@article(DBLP:journals/fmsd/Ehlers12,
 author       = "R{\"u}diger Ehlers",
 year         = "2012",
 title        = "Symbolic bounded synthesis",
 journal      = "Formal Methods in System Design",
 volume       = "40",
 number       = "2",
 pages        = "232--262",
 doi          = "10.1007/s10703-011-0137-x",
)
@mastersthesis(Ellonen2010,
 author       = "Sakari Ellonen",
 year         = "2010",
 title        = "Synthesis of Moore Machines from LTL Specifications",
 school       = "Aalto University, School of Science and Technology",
)
@inproceedings(DBLP:conf/focs/EmersonJ91,
 author       = "E. Allen Emerson and Charanjit S. Jutla",
 year         = "1991",
 title        = "Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)",
 booktitle    = "FOCS",
 publisher    = "IEEE Computer Society",
 pages        = "368--377",
 doi          = "10.1109/SFCS.1991.185392",
)
@inproceedings(DBLP:conf/jelia/GiunchigliaM06,
 author       = "Enrico Giunchiglia and Marco Maratea",
 year         = "2006",
 title        = "{OPTSAT}: A Tool for Solving {SAT} Related Optimization Problems",
 editor       = "Michael Fisher and Wiebe van der Hoek and Boris Konev and Alexei Lisitsa",
 booktitle    = "JELIA",
 series       = "Lecture Notes in Computer Science",
 volume       = "4160",
 publisher    = "Springer",
 pages        = "485--489",
 doi          = "10.1007/11853886_43",
)
@proceedings(DBLP:conf/dagstuhl/2001automata,
 editor       = "Erich Gr{\"a}del and Wolfgang Thomas and Thomas Wilke",
 year         = "2002",
 title        = "Automata, Logics, and Infinite Games: A Guide to Current Research",
 series       = "Lecture Notes in Computer Science",
 volume       = "2500",
 publisher    = "Springer",
)
@inproceedings(DBLP:conf/fmcad/JobstmannB06,
 author       = "Barbara Jobstmann and Roderick Bloem",
 year         = "2006",
 title        = "Optimizations for {LTL} Synthesis",
 booktitle    = "FMCAD",
 publisher    = "IEEE Computer Society",
 pages        = "117--124",
 doi          = "10.1109/FMCAD.2006.22",
)
@inproceedings(DBLP:conf/concur/KupfermanS06,
 author       = "Orna Kupferman and Sarai Sheinvald-Faragy",
 year         = "2006",
 title        = "Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words",
 editor       = "Christel Baier and Holger Hermanns",
 booktitle    = "{CONCUR}",
 series       = "Lecture Notes in Computer Science",
 volume       = "4137",
 publisher    = "Springer",
 pages        = "492--508",
 doi          = "10.1007/11817949_33",
)
@article(DBLP:journals/bsl/KupfermanV99,
 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",
)
@inproceedings(DBLP:conf/atva/Neider11,
 author       = "Daniel Neider",
 year         = "2011",
 title        = "Small Strategies for Safety Games",
 editor       = "Tevfik Bultan and Pao-Ann Hsiung",
 booktitle    = "ATVA",
 series       = "Lecture Notes in Computer Science",
 volume       = "6996",
 publisher    = "Springer",
 pages        = "306--320",
 doi          = "10.1007/978-3-642-24372-1_22",
)
@inproceedings(DBLP:conf/atva/ScheweF07a,
 author       = "Sven Schewe and Bernd Finkbeiner",
 year         = "2007",
 title        = "Bounded Synthesis",
 editor       = "Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura",
 booktitle    = "ATVA",
 series       = "Lecture Notes in Computer Science",
 volume       = "4762",
 publisher    = "Springer",
 pages        = "474--488",
 doi          = "10.1007/978-3-540-75596-8_33",
)
@article(DBLP:journals/igpl/Stirling99,
 author       = "Colin Stirling",
 year         = "1999",
 title        = "Bisimulation, Modal Logic and Model Checking Games",
 journal      = "Logic Journal of the IGPL",
 volume       = "7",
 number       = "1",
 pages        = "103--124",
)
@incollection(Thomas1994,
 author       = "Wolfgang Thomas",
 year         = "1994",
 title        = "Automata on Infinite Objects",
 editor       = "J. van Leeuwen",
 booktitle    = "Handbook of Theoretical Computer Science -- Vol. B: Formal Models and Semantics",
 publisher    = "MIT Press",
 pages        = "133--191",
)
@inproceedings(Vardi1996,
 author       = "Moshe Y. Vardi",
 year         = "1996",
 title        = "An Automata-theoretic Approach to Linear Temporal Logic",
 booktitle    = "Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency: structure versus automata",
 publisher    = "Springer",
 pages        = "238--266",
)