@article(Akers:1978:BDD:1310167.1310815,
 author       = {S. B. Akers},
 year         = {1978},
 title        = {Binary Decision Diagrams},
 journal      = {IEEE Trans. Comput.},
 volume       = {27},
 number       = {6},
 pages        = {509--516},
 doi          = {10.1109/TC.1978.1675141},
)
@article(alurmoarref,
 author       = {Rajeev Alur and Salar Moarref and Ufuk Topcu},
 year         = {2013},
 title        = {Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications},
 doi          = {10.1109/FMCAD.2013.6679387},
)
@inproceedings(PatternBasedRefinement,
 author       = {Rajeev Alur and Salar Moarref and Ufuk Topcu},
 year         = {2015},
 title        = {Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis},
 editor       = {Christel Baier and Cesare Tinelli},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {501--516},
 doi          = {10.1007/978-3-662-46681-0_49},
)
@article(Beer2001,
 author       = {Ilan Beer and Ben-David, Shoham and Cindy Eisner and Yoav Rodeh},
 year         = {2001},
 title        = {Efficient Detection of Vacuity in Temporal Model Checking},
 journal      = {Formal Methods in System Design},
 volume       = {18},
 number       = {2},
 pages        = {141--163},
 doi          = {10.1023/A:1008779610539},
)
@article(Ben-David2015,
 author       = {Ben-David, Shoham and Fady Copty and Dana Fisman and Sitvanit Ruah},
 year         = {2015},
 title        = {Vacuity in practice: temporal antecedent failure},
 journal      = {Formal Methods in System Design},
 volume       = {46},
 number       = {1},
 pages        = {81--104},
 doi          = {10.1007/s10703-014-0221-0},
)
@inproceedings(DBLP:conf/vmcai/BloemCES17,
 author       = {Roderick Bloem and Hana Chockler and Masoud Ebrahimi and Ofer Strichman},
 year         = {2017},
 title        = {Synthesizing Non-Vacuous Systems},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation - 18th International Conference, {VMCAI} 2017, Paris, France, January 15-17, 2017, Proceedings},
 pages        = {55--72},
 doi          = {10.1007/978-3-319-52234-0_4},
)
@inproceedings(Bloem07automatichardware,
 author       = {Roderick Bloem and Stefan Galler and Nir Piterman and Amir Pnueli and Martin Weiglhofer},
 year         = {2007},
 title        = {Automatic hardware synthesis from specifications: A case study},
 booktitle    = {In Design, Automation and Test in Europe (DATE},
 doi          = {10.1109/DATE.2007.364456},
)
@article(RATSY,
 author       = {Roderick Bloem and Hans-Jürgen Gamauf and Georg Hofferek and Bettina Könighofer and Robert Könighofer},
 year         = {2012},
 title        = {Synthesizing Robust Systems with RATSY},
 volume       = {84},
 doi          = {10.4204/EPTCS.84.4},
)
@inproceedings(ACACIA,
 author       = {Aaron Bohy and V{\'e}ronique Bruy{\`e}re and Emmanuel Filiot and Naiyong Jin and Jean-Fran{\c{c}}ois Raskin},
 year         = {2012},
 title        = {Acacia+, a Tool for LTL Synthesis},
 editor       = {P. Madhusudan and Sanjit A. Seshia},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {652--657},
 doi          = {10.1007/978-3-642-31424-7_45},
)
@inbook(Brazdil2015,
 author       = {Tom{\'a}{\v{s}} Br{\'a}zdil and Krishnendu Chatterjee and Martin Chmel{\'i}k and Andreas Fellner and K{\v{r}}et{\'i}nsk{\'y}, Jan},
 year         = {2015},
 title        = {Counterexample Explanation by Learning Small Strategies in Markov Decision Processes},
 pages        = {158--177},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-21690-4_10},
)
@inproceedings(tacasjantomas,
 author       = {Tomas Brazdil and Krishnendu Chatterjee and Jan Kretinsky and Viktor Toman},
 year         = {2018},
 title        = {Strategy Representation by Decision Trees in Reactive Synthesis},
 booktitle    = {TACAS},
 organization = {Springer},
 doi          = {10.1016/S0304-3975(98)00009-7},
)
@inbook(Buchi1990,
 author       = {J. Richard Buchi and Lawrence H. Landweber},
 year         = {1990},
 title        = {Solving Sequential Conditions by Finite-State Strategies},
 pages        = {525--541},
 publisher    = {Springer New York},
 address      = {New York, NY},
 doi          = {10.1007/978-1-4613-8928-6_29},
)
@inproceedings(AssumeGuarantee,
 author       = {Krishnendu Chatterjee and Thomas A. Henzinger},
 year         = {2007},
 title        = {Assume-Guarantee Synthesis},
 editor       = {Orna Grumberg and Michael Huth},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {261--275},
 doi          = {10.1007/978-3-540-71209-1_21},
)
@inproceedings(chaterjee2008,
 author       = {Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann},
 year         = {2008},
 title        = {Environment Assumptions for Synthesis},
 editor       = {Franck van Breugel and Marsha Chechik},
 booktitle    = {CONCUR 2008 - Concurrency Theory},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {147--161},
 doi          = {10.1007/978-3-540-85361-9_14},
)
@inproceedings(gist,
 author       = {Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann and Arjun Radhakrishna},
 year         = {2010},
 title        = {Gist: A Solver for Probabilistic Games},
 editor       = {Tayssir Touili and Byron Cook and Paul Jackson},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {665--669},
 doi          = {10.1007/978-3-642-14295-6_57},
)
@inproceedings(cheng2016structural,
 author       = {Chih-Hong Cheng and Yassine Hamza and Harald Ruess},
 year         = {2016},
 title        = {Structural Synthesis for GXW Specifications},
 booktitle    = {International Conference on Computer Aided Verification},
 organization = {Springer},
 pages        = {95--117},
 doi          = {10.1007/978-3-319-89960-2_21},
)
@inproceedings(cheng2014g4ltl,
 author       = {Chih-Hong Cheng and Chung-Hao Huang and Harald Ruess and Stefan Stattelmann},
 year         = {2014},
 title        = {G4LTL-ST: Automatic generation of PLC programs},
 booktitle    = {International Conference on Computer Aided Verification},
 organization = {Springer},
 pages        = {541--549},
 doi          = {10.1007/978-3-319-08867-9_36},
)
@inproceedings(cheng2017autocode4,
 author       = {Chih-Hong Cheng and Edward A Lee and Harald Ruess},
 year         = {2017},
 title        = {autoCode4: Structural Controller Synthesis},
 booktitle    = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 organization = {Springer},
 pages        = {398--404},
 doi          = {10.1007/978-3-662-54577-5_23},
)
@article(Chockler:2008:CSS:1352582.1352588,
 author       = {Hana Chockler and Joseph Y. Halpern and Orna Kupferman},
 year         = {2008},
 title        = {What Causes a System to Satisfy a Specification?},
 journal      = {ACM Trans. Comput. Logic},
 volume       = {9},
 number       = {3},
 pages        = {20:1--20:26},
 doi          = {10.1145/1352582.1352588},
)
@inproceedings(coverage,
 author       = {Hana Chockler and Orna Kupferman and Moshe Y. Vardi},
 year         = {2003},
 title        = {Coverage Metrics for Formal Verification},
 editor       = {Daniel Geist and Enrico Tronci},
 booktitle    = {Correct Hardware Design and Verification Methods},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {111--125},
 doi          = {10.1007/978-3-540-39724-3_11},
)
@inproceedings(cimatti,
 author       = {A. Cimatti and M. Roveri and V. Schuppan and A. Tchaltsev},
 year         = {2008},
 title        = {Diagnostic Information for Realizability},
 editor       = {Francesco Logozzo and Doron A. Peled and Lenore D. Zuck},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {52--67},
 doi          = {10.1007/978-3-540-78163-9_9},
)
@inproceedings(Unbeast10.1007,
 author       = {R{\"u}diger Ehlers},
 year         = {2011},
 title        = {Unbeast: Symbolic Bounded Synthesis},
 editor       = {Parosh Aziz Abdulla and K. Rustan M. Leino},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {272--275},
 doi          = {10.1007/978-3-642-19835-9_25},
)
@inproceedings(DBLP:conf/cav/EhlersR16,
 author       = {R{\"{u}}diger Ehlers and Vasumathi Raman},
 year         = {2016},
 title        = {Slugs: Extensible {GR(1)} Synthesis},
 editor       = {Swarat Chaudhuri and Azadeh Farzan},
 booktitle    = {Computer Aided Verification - 28th International Conference, {CAV} 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9780},
 publisher    = {Springer},
 pages        = {333--339},
 doi          = {10.1007/978-3-319-41540-6_18},
)
@inproceedings(conf/cav/FaymonvilleFT17,
 author       = {Peter Faymonville and Bernd Finkbeiner and Leander Tentrup},
 year         = {2017},
 title        = {BoSy: An Experimentation Framework for Bounded Synthesis},
 booktitle    = {Proceedings of {CAV}},
 series       = {LNCS},
 volume       = {10427},
 publisher    = {Springer},
 pages        = {325--332},
 doi          = {10.1007/978-3-319-63390-9_17},
)
@incollection(FinkbeinerKlein16,
 author       = {Bernd Finkbeiner and Felix Klein},
 year         = {2016},
 title        = {Bounded Cycle Synthesis},
 series       = {Lecture Notes in Computer Science},
 volume       = {9779},
 publisher    = {Springer Berlin Heidelberg},
 doi          = {10.1007/978-3-319-41528-4},
)
@inproceedings(F16,
 author       = {Bernd Finkbeiner and Felix Klein},
 year         = {2017},
 title        = {Reactive Synthesis: Towards Output-Sensitive Algorithms},
 editor       = {Alexander Pretschner and Doron Peled and Thomas Hutzelmann},
 booktitle    = {Dependable Software Systems Engineering},
 series       = {{NATO} Science for Peace and Security Series, {D:} Information and Communication Security},
 volume       = {50},
 publisher    = {{IOS} Press},
 pages        = {25--43},
 doi          = {10.3233/978-1-61499-810-5-25},
)
@article(FS13,
 author       = {Bernd Finkbeiner and Sven Schewe},
 year         = {2013},
 title        = {Bounded synthesis},
 journal      = {International Journal on Software Tools for Technology Transfer},
 volume       = {15},
 number       = {5-6},
 pages        = {519--539},
 doi          = {10.1007/s10009-012-0228-z},
)
@article(FT15,
 author       = {Bernd Finkbeiner and Leander Tentrup},
 year         = {2015},
 title        = {Detecting Unrealizability of Distributed Fault-tolerant Systems},
 journal      = {Logical Methods in Computer Science},
 volume       = {11},
 number       = {3},
 doi          = {10.2168/LMCS-11(3:12)2015},
)
@inbook(Finkbeiner2016,
 author       = {Bernd Finkbeiner and Hazem Torfah},
 year         = {2016},
 title        = {Synthesizing Skeletons for Reactive Systems},
 pages        = {271--286},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-46520-3_18},
)
@inproceedings(206358,
 author       = {M. Fujita and Y. Matsunaga and T. Kakuda},
 year         = {1991},
 title        = {On variable ordering of binary decision diagrams for the application of multi-level logic synthesis},
 booktitle    = {Proceedings of the European Conference on Design Automation.},
 pages        = {50--54},
 doi          = {10.1109/EDAC.1991.206358},
)
@inproceedings(fukaya,
 author       = {Yuichi Fukaya and Noriaki Yoshiura},
 year         = {2015},
 title        = {Extracting Environmental Constraints in Reactive System Specifications},
 editor       = {Osvaldo Gervasi and Beniamino Murgante and Sanjay Misra and Marina L. Gavrilova and Ana Maria Alves Coutinho Rocha and Carmelo Torre and David Taniar and Bernady O. Apduhan},
 booktitle    = {Computational Science and Its Applications -- ICCSA 2015},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {671--685},
 doi          = {10.1007/978-3-319-21410-8_51},
)
@inproceedings(Hoskote:1999:CES:309847.309936,
 author       = {Yatin Hoskote and Timothy Kam and Pei-Hsin Ho and Xudong Zhao},
 year         = {1999},
 title        = {Coverage Estimation for Symbolic Model Checking},
 booktitle    = {Proceedings of the 36th Annual ACM/IEEE Design Automation Conference},
 series       = {DAC '99},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {300--305},
 doi          = {10.1145/309847.309936},
)
@inproceedings(SYNTCOMP2017,
 author       = {Swen Jacobs and Nicolas Basset and Roderick Bloem and Romain Brenguier and Maximilien Colange and Peter Faymonville and Bernd Finkbeiner and Ayrat Khalimov and Felix Klein and Thibaud Michaud and Guillermo A. Perez and Jean-Francois Raskin and Ocan Sankur and Leander Tentrup},
 year         = {2017},
 title        = {The 4th Reactive Synthesis Competition {(SYNTCOMP 2017)}: Benchmarks, Participants and Results},
 booktitle    = {SYNT 2017},
 series       = {EPTCS},
 volume       = {260},
 pages        = {116--143},
 doi          = {10.4204/EPTCS.260.10},
)
@inproceedings(10.1007,
 author       = {Barbara Jobstmann and Stefan Galler and Martin Weiglhofer and Roderick Bloem},
 year         = {2007},
 title        = {Anzu: A Tool for Property Synthesis},
 editor       = {Werner Damm and Holger Hermanns},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {258--262},
 doi          = {10.1007/978-3-540-73368-3_29},
)
@inbook(Koenighofer2011,
 author       = {Robert K{\"o}nighofer and Georg Hofferek and Roderick Bloem},
 year         = {2011},
 title        = {Debugging Unrealizable Specifications with Model-Based Diagnosis},
 pages        = {29--45},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-19583-9_8},
)
@inproceedings(5351127,
 author       = {R. Könighofer and G. Hofferek and R. Bloem},
 year         = {2009},
 title        = {Debugging formal specifications using simple counterstrategies},
 booktitle    = {2009 Formal Methods in Computer-Aided Design},
 pages        = {152--159},
 doi          = {10.1109/FMCAD.2009.5351127},
)
@inproceedings(GeneticAlgorithmsbdd,
 author       = {Wolfgang Lenders and Christel Baier},
 year         = {2005},
 title        = {Genetic Algorithms for the Variable Ordering Problem of Binary Decision Diagrams},
 editor       = {Alden H. Wright and Michael D. Vose and De Jong, Kenneth A. and Lothar M. Schmitt},
 booktitle    = {Foundations of Genetic Algorithms},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {1--20},
 doi          = {10.1007/11513575_1},
)
@inproceedings(5970509,
 author       = {W. Li and L. Dworkin and S. A. Seshia},
 year         = {2011},
 title        = {Mining assumptions for synthesis},
 booktitle    = {Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011)},
 pages        = {43--50},
 doi          = {10.1109/MEMCOD.2011.5970509},
)
@article(DBLP:journals/arobots/LignosRFMK15,
 author       = {Constantine Lignos and Vasumathi Raman and Cameron Finucane and Mitchell P. Marcus and Kress{-}Gazit, Hadas},
 year         = {2015},
 title        = {Provably correct reactive control from natural language},
 journal      = {Auton. Robots},
 volume       = {38},
 number       = {1},
 pages        = {89--105},
 doi          = {10.1007/s10514-014-9418-8},
)
@inproceedings(7040368,
 author       = {P. Nilsson and N. Ozay},
 year         = {2014},
 title        = {Incremental synthesis of switching protocols via abstraction refinement},
 booktitle    = {53rd IEEE Conference on Decision and Control},
 pages        = {6246--6253},
 doi          = {10.1109/CDC.2014.7040368},
)
@inproceedings(peter+mattmueller/rtss/09,
 author       = {Hans-J{\"o}rg Peter and Robert Mattm{\"u}ller},
 year         = {2009},
 title        = {Component-based Abstraction Refinement for Timed Controller Synthesis},
 editor       = {Theodore Baker},
 booktitle    = {Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS 2009), December 1 - December 4, 2009, Washington, D.C., USA},
 publisher    = {IEEE Computer Society},
 address      = {Los Alamitos, CA, USA},
 pages        = {364--374},
 doi          = {10.1109/RTSS.2009.14},
)
@inproceedings(hardtosynthesize,
 author       = {A. Pnueli and R. Rosner},
 year         = {1990},
 title        = {Distributed Reactive Systems Are Hard to Synthesize},
 booktitle    = {Proceedings of the 31st Annual Symposium on Foundations of Computer Science},
 series       = {SFCS '90},
 publisher    = {IEEE Computer Society},
 address      = {Washington, DC, USA},
 pages        = {746--757 vol.2},
 doi          = {10.1109/FSCS.1990.89597},
)
@article(6301745,
 author       = {V. Raman and Kress-Gazit, H.},
 year         = {2013},
 title        = {Explaining Impossible High-Level Robot Behaviors},
 journal      = {IEEE Transactions on Robotics},
 volume       = {29},
 number       = {1},
 pages        = {94--104},
 doi          = {10.1109/TRO.2012.2214558},
)
@article(7519063,
 author       = {G. Reissig and A. Weber and M. Rungger},
 year         = {2017},
 title        = {Feedback Refinement Relations for the Synthesis of Symbolic Controllers},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {62},
 number       = {4},
 pages        = {1781--1796},
 doi          = {10.1109/TAC.2016.2593947},
)
@article(SCHUPPAN2012908,
 author       = {Viktor Schuppan},
 year         = {2012},
 title        = {Towards a notion of unsatisfiable and unrealizable cores for LTL},
 journal      = {Science of Computer Programming},
 volume       = {77},
 number       = {7},
 pages        = {908 -- 939},
 doi          = {10.1016/j.scico.2010.11.004},
 url          = {http://www.sciencedirect.com/science/article/pii/S0167642310002030},
 note         = {(1) FOCLASA’09 (2) FSEN’09},
)
@inproceedings(DBLP:conf/rss/WongEK14,
 author       = {Kai Weng Wong and R{\"{u}}diger Ehlers and Kress{-}Gazit, Hadas},
 year         = {2014},
 title        = {Correct High-level Robot Behavior in Environments with Unexpected Events},
 booktitle    = {Robotics: Science and Systems X, University of California, Berkeley, USA, July 12-16, 2014},
 doi          = {10.15607/RSS.2014.X.012},
 url          = {http://www.roboticsproceedings.org/rss10/p12.html},
)
@inproceedings(7139021,
 author       = {Kai Weng Wong and Kress-Gazit, H.},
 year         = {2015},
 title        = {Let's talk: Autonomous conflict resolution for robots carrying out individual high-level tasks in a shared workspace},
 booktitle    = {2015 IEEE International Conference on Robotics and Automation (ICRA)},
 pages        = {339--345},
 doi          = {10.1109/ICRA.2015.7139021},
)