@(SyFCo,
 title        = {{S}ynthesis {F}ormat {C}onversion {T}ool},
 url          = {https://github.com/reactive-systems/syfco},
)
@article(AlurT04,
 author       = {Rajeev Alur and {La Torre}, Salvatore},
 year         = {2004},
 title        = {Deterministic generators and games for {LTL} fragments},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {5},
 number       = {1},
 pages        = {1--25},
 doi          = {10.1145/963927.963928},
)
@inproceedings(BalintDGGKR11,
 author       = {Adrian Balint and Daniel Diepold and Daniel Gall and Simon Gerber and Gregor Kapler and Robert Retz},
 year         = {2011},
 title        = {{EDACC} - An Advanced Platform for the Experiment Design, Administration and Analysis of Empirical Algorithms},
 booktitle    = {{LION} 5. Selected Papers},
 series       = {LNCS},
 volume       = {6683},
 publisher    = {Springer},
 pages        = {586--599},
 doi          = {10.1007/978-3-642-25566-3\_46},
)
@article(BarrettDMOS13,
 author       = {Clark Barrett and Morgan Deters and Leonardo Mendon{\c{c}}a de Moura and Albert Oliveras and Aaron Stump},
 year         = {2013},
 title        = {6 Years of {SMT-COMP}},
 journal      = {J. Autom. Reasoning},
 volume       = {50},
 number       = {3},
 pages        = {243--277},
 doi          = {10.1007/s10817-012-9246-5},
)
@manual(aiger,
 author       = {Armin Biere},
 title        = {{AIGER} Format and Toolbox},
 url          = {http://fmv.jku.at/aiger/},
)
@article(BloemJPPS12,
 author       = {R. Bloem and B. Jobstmann and N. Piterman and A. Pnueli and Y. Sa'ar},
 year         = {2012},
 title        = {Synthesis of Reactive(1) designs},
 journal      = {J. Comput. Syst. Sci.},
 volume       = {78},
 number       = {3},
 pages        = {911--938},
 doi          = {10.1016/j.jcss.2011.08.007},
)
@inproceedings(BloemKS14,
 author       = {R. Bloem and R. K{\"o}nighofer and M. Seidl},
 year         = {2014},
 title        = {{SAT}-Based Synthesis Methods for Safety Specs},
 booktitle    = {VMCAI},
 series       = {LNCS},
 volume       = {8318},
 publisher    = {Springer},
 pages        = {1--20},
 doi          = {10.1007/978-3-642-54013-4\_1},
)
@inproceedings(BloemCHJ09,
 author       = {Roderick Bloem and Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann},
 year         = {2009},
 title        = {Better Quality in Synthesis through Quantitative Objectives},
 booktitle    = {{CAV}},
 series       = {LNCS},
 volume       = {5643},
 publisher    = {Springer},
 pages        = {140--156},
 doi          = {10.1007/978-3-642-02658-4\_14},
)
@inproceedings(BloemCJK15,
 author       = {Roderick Bloem and Krishnendu Chatterjee and Swen Jacobs and Robert K{\"{o}}nighofer},
 year         = {2015},
 title        = {Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information},
 booktitle    = {{TACAS}},
 series       = {LNCS},
 volume       = {9035},
 publisher    = {Springer},
 pages        = {517--532},
 doi          = {10.1007/978-3-662-46681-0\_50},
)
@article(BloemEKKLS16,
 author       = {Roderick Bloem and Uwe Egly and Patrick Klampfl and Robert K{\"{o}}nighofer and Florian Lonsing and Martina Seidl},
 year         = {2016},
 title        = {Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications},
 journal      = {CoRR},
 volume       = {abs/1604.06204},
 url          = {http://arxiv.org/abs/1604.06204},
)
@inproceedings(BrenguierPRS14,
 author       = {Romain Brenguier and Guillermo A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Ocan Sankur},
 year         = {2014},
 title        = {{AbsSynthe}: abstract synthesis from succinct safety specifications},
 booktitle    = {{SYNT}},
 series       = {{EPTCS}},
 volume       = {157},
 pages        = {100--116},
 doi          = {10.4204/EPTCS.157.11},
)
@inproceedings(BrenguierPRS15,
 author       = {Romain Brenguier and Guillermo A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Ocan Sankur},
 year         = {2016},
 title        = {Compositional Algorithms for Succinct Safety Games},
 booktitle    = {{SYNT}},
 series       = {{EPTCS}},
 volume       = {202},
 pages        = {98--111},
 doi          = {10.4204/EPTCS.202.7},
)
@article(BL69,
 author       = {J.R. B\"uchi and L.H. Landweber},
 year         = {1969},
 title        = {Solving sequential conditions by finite-state strategies},
 journal      = {Trans. Amer. Math. Soc.},
 volume       = {138},
 pages        = {295--311},
 doi          = {10.2307/1994916},
)
@article(cabodi2016hwmcc,
 author       = {Gianpiero Cabodi and Carmelo Loiacono and Marco Palena and Paolo Pasini and Denis Patti and Stefano Quer and Danilo Vendraminetto and Armin Biere and Keijo Heljanko and Jason Baumgartner},
 year         = {2016},
 title        = {Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks},
 journal      = {Journal on Satisfiability, Boolean Modeling and Computation},
 volume       = {9},
 pages        = {135--172},
)
@inproceedings(CernyCHRS11,
 author       = {Pavol Cern{\'{y}} and Krishnendu Chatterjee and Thomas A. Henzinger and Arjun Radhakrishna and Rohit Singh},
 year         = {2011},
 title        = {Quantitative Synthesis for Concurrent Programs},
 booktitle    = {{CAV}},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {243--259},
 doi          = {10.1007/978-3-642-22110-1\_20},
)
@inproceedings(CernyH11,
 author       = {Pavol Cern{\'{y}} and Thomas A. Henzinger},
 year         = {2011},
 title        = {From boolean to quantitative synthesis},
 booktitle    = {{EMSOFT}},
 publisher    = {{ACM}},
 pages        = {149--154},
 doi          = {10.1145/2038642.2038666},
)
@inproceedings(ChatterjeeHJS11,
 author       = {Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann and Rohit Singh},
 year         = {2011},
 title        = {{QUASY:} Quantitative Synthesis Tool},
 booktitle    = {{TACAS}},
 series       = {Lecture Notes in Computer Science},
 volume       = {6605},
 publisher    = {Springer},
 pages        = {267--271},
 doi          = {10.1007/978-3-642-19835-9\_24},
)
@article(ChenDSB12,
 author       = {Yushan Chen and Xu Chu Ding and Alin Stefanescu and Calin Belta},
 year         = {2012},
 title        = {Formal Approach to the Deployment of Distributed Robotic Teams},
 journal      = {{IEEE} Transactions on Robotics},
 volume       = {28},
 number       = {1},
 pages        = {158--171},
 doi          = {10.1109/TRO.2011.2163434},
)
@inproceedings(ChiangJ15,
 author       = {Ting{-}Wei Chiang and Jie{-}Hong R. Jiang},
 year         = {2015},
 title        = {Property-Directed Synthesis of Reactive Systems from Safety Specifications},
 booktitle    = {{ICCAD}},
 publisher    = {{IEEE}},
 pages        = {794--801},
 doi          = {10.1109/ICCAD.2015.7372652},
)
@inproceedings(ChinchaliLTBM12,
 author       = {Sandeep Chinchali and Scott C. Livingston and Ufuk Topcu and Joel W. Burdick and Richard M. Murray},
 year         = {2012},
 title        = {Towards formal synthesis of reactive controllers for dexterous robotic manipulation},
 booktitle    = {{ICRA}},
 publisher    = {{IEEE}},
 pages        = {5183--5189},
 doi          = {10.1109/ICRA.2012.6225257},
)
@inproceedings(Church62,
 author       = {Alonzo Church},
 year         = {1962},
 title        = {Logic, arithmetic and automata},
 booktitle    = {Proceedings of the international congress of mathematicians},
 pages        = {23--35},
)
@inproceedings(EenLNR15,
 author       = {Niklas E{\'{e}}n and Alexander Legg and Nina Narodytska and Leonid Ryzhyk},
 year         = {2015},
 title        = {SAT-Based Strategy Extraction in Reachability Games},
 booktitle    = {{AAAI}},
 publisher    = {{AAAI} Press},
 pages        = {3738--3745},
 url          = {http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9683},
)
@inproceedings(Ehlers11,
 author       = {R{\"{u}}diger Ehlers},
 year         = {2011},
 title        = {Unbeast: Symbolic Bounded Synthesis},
 booktitle    = {{TACAS}},
 series       = {LNCS},
 volume       = {6605},
 publisher    = {Springer},
 pages        = {272--275},
 doi          = {10.1007/978-3-642-19835-9\_25},
)
@article(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},
)
@inproceedings(EhlersR16,
 author       = {R{\"{u}}diger Ehlers and Vasumathi Raman},
 year         = {2016},
 title        = {Slugs: Extensible {GR(1)} Synthesis},
 booktitle    = {{CAV} {(2)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9780},
 publisher    = {Springer},
 pages        = {333--339},
 doi          = {10.1007/978-3-319-41540-6\_18},
)
@manual(acacia,
 author       = {Emmanuel Filiot},
 title        = {Acacia+},
 url          = {http://lit2.ulb.ac.be/acaciaplus/},
)
@article(fjr11,
 author       = {Emmanuel Filiot and Naiyong Jin and Jean-Fran{\c{c}}ois Raskin},
 year         = {2011},
 title        = {Antichains and compositional algorithms for {LTL} synthesis},
 journal      = {Formal Methods in System Design},
 volume       = {39},
 number       = {3},
 pages        = {261--296},
 doi          = {10.1007/s10703-011-0115-3},
)
@article(FiliotJR13,
 author       = {Emmanuel Filiot and Naiyong Jin and Jean{-}Fran{\c{c}}ois Raskin},
 year         = {2013},
 title        = {Exploiting structure in {LTL} synthesis},
 journal      = {{STTT}},
 volume       = {15},
 number       = {5-6},
 pages        = {541--561},
 doi          = {10.1007/s10009-012-0222-5},
)
@incollection(Finkbeiner16,
 author       = {Bernd Finkbeiner},
 year         = {2016},
 title        = {Synthesis of Reactive Systems},
 booktitle    = {Dependable Software Systems Engineering},
 series       = {{NATO} Science for Peace and Security Series - {D:} Information and Communication Security},
 volume       = {45},
 publisher    = {{IOS} Press},
 pages        = {72--98},
 doi          = {10.3233/978-1-61499-627-9-72},
)
@inproceedings(FinkbeinerJ12,
 author       = {Bernd Finkbeiner and Swen Jacobs},
 year         = {2012},
 title        = {Lazy Synthesis},
 booktitle    = {{VMCAI}},
 series       = {LNCS},
 volume       = {7148},
 publisher    = {Springer},
 pages        = {219--234},
 doi          = {10.1007/978-3-642-27940-9\_15},
)
@article(Finkbeiner13,
 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},
)
@article(SYNTCOMP-format,
 author       = {Swen Jacobs},
 year         = {2014},
 title        = {Extended {AIGER} Format for Synthesis},
 journal      = {CoRR},
 volume       = {abs/1405.5793},
 url          = {http://arxiv.org/abs/1405.5793},
)
@article(SYNTCOMP14,
 author       = {Swen Jacobs and Roderick Bloem and Romain Brenguier and R{\"{u}}diger Ehlers and Timotheus Hell and Robert K{\"{o}}nighofer 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 First Reactive Synthesis Competition {(SYNTCOMP} 2014)},
 journal      = {STTT},
 doi          = {10.1007/s10009-016-0416-3},
 note         = {Published online first, journal issue to appear.},
)
@inproceedings(JacobsETAL16b,
 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},
 booktitle    = {{SYNT}},
 series       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
)
@inproceedings(SYNTCOMP15,
 author       = {Swen Jacobs and Roderick Bloem and Romain Brenguier and Robert K\"onighofer and Guillermo A. P\'erez 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 Second Reactive Synthesis Competition ({SYNTCOMP} 2015)},
 booktitle    = {{SYNT}},
 series       = {EPTCS},
 volume       = {202},
 publisher    = {Open Publishing Association},
 pages        = {27--57},
 doi          = {10.4204/EPTCS.202.4},
)
@inproceedings(JacobsK16,
 author       = {Swen Jacobs and Felix Klein and Sebastian Schirmer},
 year         = {2016},
 title        = {A High-Level {LTL} Synthesis Format: {TLSF} v1.1},
 booktitle    = {{SYNT}},
 series       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
)
@article(JarvisaloBRS12,
 author       = {Matti J{\"{a}}rvisalo and Daniel Le Berre and Olivier Roussel and Laurent Simon},
 year         = {2012},
 title        = {The International {SAT} Solver Competitions},
 journal      = {{AI} Magazine},
 volume       = {33},
 number       = {1},
)
@inproceedings(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(Khalimov16,
 author       = {Ayrat Khalimov},
 year         = {2016},
 title        = {Specification Format for Reactive Synthesis Problems},
 booktitle    = {{SYNT}},
 series       = {{EPTCS}},
 volume       = {202},
 pages        = {112--119},
 doi          = {10.4204/EPTCS.202.8},
)
@article(Kress-GazitFP09,
 author       = {Kress{-}Gazit, Hadas and Georgios E. Fainekos and George J. Pappas},
 year         = {2009},
 title        = {Temporal-Logic-Based Reactive Mission and Motion Planning},
 journal      = {{IEEE} Transactions on Robotics},
 volume       = {25},
 number       = {6},
 pages        = {1370--1381},
 doi          = {10.1109/TRO.2009.2030225},
)
@inproceedings(LeggNR16,
 author       = {Alexander Legg and Nina Narodytska and Leonid Ryzhyk},
 year         = {2016},
 title        = {A SAT-Based Counterexample Guided Method for Unbounded Synthesis},
 booktitle    = {{CAV} {(2)}},
 series       = {LNCS},
 volume       = {9780},
 publisher    = {Springer},
 pages        = {364--382},
 doi          = {10.1007/978-3-319-41540-6\_20},
)
@article(LiuOTM13,
 author       = {Jun Liu and Necmiye Ozay and Ufuk Topcu and Richard M. Murray},
 year         = {2013},
 title        = {Synthesis of Reactive Switching Protocols From Temporal Logic Specifications},
 journal      = {{IEEE} Trans. Automat. Contr.},
 volume       = {58},
 number       = {7},
 pages        = {1771--1785},
 doi          = {10.1109/TAC.2013.2246095},
)
@inproceedings(MadhusudanT01,
 author       = {P. Madhusudan and P. S. Thiagarajan},
 year         = {2001},
 title        = {Distributed Controller Synthesis for Local Specifications},
 booktitle    = {{ICALP}},
 series       = {LNCS},
 volume       = {2076},
 publisher    = {Springer},
 pages        = {396--407},
 doi          = {10.1007/3-540-48224-5\_33},
)
@inproceedings(MadhusudanT02,
 author       = {P. Madhusudan and P. S. Thiagarajan},
 year         = {2002},
 title        = {A Decidable Class of Asynchronous Distributed Controllers},
 booktitle    = {{CONCUR}},
 series       = {LNCS},
 volume       = {2421},
 publisher    = {Springer},
 pages        = {145--160},
 doi          = {10.1007/3-540-45694-5\_11},
)
@inproceedings(MorgensternS11,
 author       = {Andreas Morgenstern and Klaus Schneider},
 year         = {2011},
 title        = {A {LTL} Fragment for GR(1)-Synthesis},
 booktitle    = {iWIGP},
 series       = {{EPTCS}},
 volume       = {50},
 pages        = {33--45},
 doi          = {10.4204/EPTCS.50.3},
)
@inproceedings(NarodytskaLBRW14,
 author       = {Nina Narodytska and Alexander Legg and Fahiem Bacchus and Leonid Ryzhyk and Adam Walker},
 year         = {2014},
 title        = {Solving Games without Controllable Predecessor},
 booktitle    = {{CAV}},
 series       = {LNCS},
 volume       = {8559},
 publisher    = {Springer},
 pages        = {533--540},
 doi          = {10.1007/978-3-319-08867-9\_35},
)
@inproceedings(PnueliAMS98,
 author       = {A Pnueli and E Asarin and O Maler and J Sifakis},
 year         = {1998},
 title        = {Controller synthesis for timed automata},
 booktitle    = {Proc. System Structure and Control. Elsevier},
)
@inproceedings(Pnueli77,
 author       = {Amir Pnueli},
 year         = {1977},
 title        = {The Temporal Logic of Programs},
 booktitle    = {{FOCS}},
 publisher    = {{IEEE} Computer Society},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@inproceedings(PnueliR89,
 author       = {Amir Pnueli and Roni Rosner},
 year         = {1989},
 title        = {On the Synthesis of a Reactive Module},
 booktitle    = {POPL},
 publisher    = {{ACM} Press},
 pages        = {179--190},
 doi          = {10.1145/75277.75293},
)
@inproceedings(PnueliR90,
 author       = {Amir Pnueli and Roni Rosner},
 year         = {1990},
 title        = {Distributed Reactive Systems Are Hard to Synthesize},
 booktitle    = {Foundations of Computer Science (FOCS'90)},
 publisher    = {IEEE Computer Society},
 pages        = {746--757},
 doi          = {10.1109/FSCS.1990.89597},
)
@article(Rabin72,
 author       = {Michael O. Rabin},
 year         = {1972},
 title        = {Automata on Infinite Objects and Church's Problem},
 journal      = {Amer. Math. Soc.},
 volume       = {13},
)
@inproceedings(RyzhykWKLRSV14,
 author       = {Leonid Ryzhyk and Adam Walker and John Keys and Alexander Legg and Arun Raghunath and Michael Stumm and Mona Vij},
 year         = {2014},
 title        = {User-Guided Device Driver Synthesis},
 booktitle    = {{OSDI}},
 publisher    = {{USENIX} Association},
 pages        = {661--676},
 url          = {https://www.usenix.org/conference/osdi14/technical-sessions/presentation/ryzhyk},
)
@article(SohailS13,
 author       = {Saqib Sohail and Fabio Somenzi},
 year         = {2013},
 title        = {Safety first: a two-stage algorithm for the synthesis of reactive systems},
 journal      = {{STTT}},
 volume       = {15},
 number       = {5-6},
 pages        = {433--454},
 doi          = {10.1007/s10009-012-0224-3},
)
@inproceedings(StumpST14,
 author       = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli},
 year         = {2014},
 title        = {{StarExec}: {A} Cross-Community Infrastructure for Logic Solving},
 booktitle    = {{IJCAR}},
 series       = {LNCS},
 volume       = {8562},
 publisher    = {Springer},
 pages        = {367--373},
 doi          = {10.1007/978-3-319-08587-6\_28},
)
@article(SutcliffeS06,
 author       = {Geoff Sutcliffe and Christian B. Suttner},
 year         = {2006},
 title        = {The state of {CASC}},
 journal      = {{AI} Commun.},
 volume       = {19},
 number       = {1},
 pages        = {35--48},
)
@article(Tentrup16,
 author       = {Leander Tentrup},
 year         = {2016},
 title        = {Solving {QBF} by Abstraction},
 journal      = {CoRR},
 volume       = {abs/1604.06752},
 url          = {http://arxiv.org/abs/1604.06752},
)
@inproceedings(Thomas95,
 author       = {Wolfgang Thomas},
 year         = {1995},
 title        = {On the Synthesis of Strategies in Infinite Games},
 booktitle    = {{STACS}},
 pages        = {1--13},
 doi          = {10.1007/3-540-59042-0\_57},
)
@inproceedings(WalkerR14,
 author       = {Adam Walker and Leonid Ryzhyk},
 year         = {2014},
 title        = {Predicate abstraction for reactive synthesis},
 booktitle    = {{FMCAD}},
 publisher    = {{IEEE}},
 pages        = {219--226},
 doi          = {10.1109/FMCAD.2014.6987617},
)
@article(Zimmermann13,
 author       = {Martin Zimmermann},
 year         = {2013},
 title        = {Optimal bounds in parametric {LTL} games},
 journal      = {Theor. Comput. Sci.},
 volume       = {493},
 pages        = {30--45},
 doi          = {10.1016/j.tcs.2012.07.039},
)