Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002):
Alternating-time temporal logic.
J. ACM 49(5),
pp. 672–713,
doi:10.1145/585265.585270.
Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007):
Specify, Compile, Run: Hardware from PSL.
Electr. Notes Theor. Comput. Sci. 190(4),
pp. 3–16,
doi:10.1016/j.entcs.2007.09.004.
Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan & Xudong Zhao (1995):
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.
In: DAC,
pp. 427–432,
doi:10.1145/217474.217565.
Rüdiger Ehlers (2010):
Short Witnesses and Accepting Lassos in ω-Automata.
In: Adrian Horia Dediu, Henning Fernau & Carlos Mart\'ın-Vide: LATA,
LNCS 6031.
Springer,
pp. 261–272,
doi:10.1007/978-3-642-13089-2_22.
Rüdiger Ehlers (2011):
Small witnesses, accepting lassos and winning strategies in ω-automata and games.
Technical Report 80.
SFB/TR 14 AVACS.
ISSN: 1860-9821, http://www.avacs.org..
Rüdiger Ehlers (2012):
Symbolic bounded synthesis.
Formal Methods in System Design 40(2),
pp. 232–262,
doi:10.1007/s10703-011-0137-x.
Sakari Ellonen (2010):
Synthesis of Moore Machines from LTL Specifications.
Aalto University, School of Science and Technology.
E. Allen Emerson & Charanjit S. Jutla (1991):
Tree Automata, Mu-Calculus and Determinacy (Extended Abstract).
In: FOCS.
IEEE Computer Society,
pp. 368–377,
doi:10.1109/SFCS.1991.185392.
Enrico Giunchiglia & Marco Maratea (2006):
OPTSAT: A Tool for Solving SAT Related Optimization Problems.
In: Michael Fisher, Wiebe van der Hoek, Boris Konev & Alexei Lisitsa: JELIA,
Lecture Notes in Computer Science 4160.
Springer,
pp. 485–489,
doi:10.1007/11853886_43.
Erich Grädel, Wolfgang Thomas & Thomas Wilke (2002):
Automata, Logics, and Infinite Games: A Guide to Current Research.
Lecture Notes in Computer Science 2500.
Springer.
Barbara Jobstmann & Roderick Bloem (2006):
Optimizations for LTL Synthesis.
In: FMCAD.
IEEE Computer Society,
pp. 117–124,
doi:10.1109/FMCAD.2006.22.
Orna Kupferman & Sarai Sheinvald-Faragy (2006):
Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words.
In: Christel Baier & Holger Hermanns: CONCUR,
Lecture Notes in Computer Science 4137.
Springer,
pp. 492–508,
doi:10.1007/11817949_33.
Orna Kupferman & Moshe Y. Vardi (1999):
Church's problem revisited.
Bulletin of Symbolic Logic 5(2),
pp. 245–263.
Daniel Neider (2011):
Small Strategies for Safety Games.
In: Tevfik Bultan & Pao-Ann Hsiung: ATVA,
Lecture Notes in Computer Science 6996.
Springer,
pp. 306–320,
doi:10.1007/978-3-642-24372-1_22.
Sven Schewe & Bernd Finkbeiner (2007):
Bounded Synthesis.
In: Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino & Yoshio Okamura: ATVA,
Lecture Notes in Computer Science 4762.
Springer,
pp. 474–488,
doi:10.1007/978-3-540-75596-8_33.
Colin Stirling (1999):
Bisimulation, Modal Logic and Model Checking Games.
Logic Journal of the IGPL 7(1),
pp. 103–124.
Wolfgang Thomas (1994):
Automata on Infinite Objects.
In: J. van Leeuwen: Handbook of Theoretical Computer Science – Vol. B: Formal Models and Semantics.
MIT Press,
pp. 133–191.
Moshe Y. Vardi (1996):
An Automata-theoretic Approach to Linear Temporal Logic.
In: Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency: structure versus automata.
Springer,
pp. 238–266.