@inproceedings(DBLP:conf/movep/AmnellBBDDFHJLMPWY00,
 author       = "Tobias Amnell and Gerd Behrmann and Johan Bengtsson and Pedro R. D'Argenio and Alexandre David and Ansgar Fehnker and Thomas Hune and Bertrand Jeannet and Kim Guldstrand Larsen and M. Oliver M{\"o}ller and Paul Pettersson and Carsten Weise and Wang Yi",
 year         = "2000",
 title        = "UPPAAL - Now, Next, and Future",
 editor       = "Franck Cassez and Claude Jard and Brigitte Rozoy and Mark Dermot Ryan",
 booktitle    = "MOVEP",
 series       = "Lecture Notes in Computer Science",
 volume       = "2067",
 publisher    = "Springer",
 pages        = "99--124",
 doi          = "10.1007/3-540-45510-8\_4",
)
@article(DBLP:journals/jcss/BloemJPPS12,
 author       = "Roderick Bloem and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Yaniv 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(Chatterjee08,
 author       = "Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann",
 year         = "{2008}",
 title        = "{Environment Assumptions for Synthesis}",
 booktitle    = "{International Conference on Concurrency Theory (CONCUR)}",
 publisher    = "{Springer-Verlag}",
 address      = "{Berlin, Heidelberg}",
 pages        = "{147--161}",
 doi          = "10.1007/978-3-540-85361-9\_14",
)
@inproceedings(DBLP:conf/cav/CimattiCGGPRST02,
 author       = "Alessandro Cimatti and Edmund M. Clarke and Enrico Giunchiglia and Fausto Giunchiglia and Marco Pistore and Marco Roveri and Roberto Sebastiani and Armando Tacchella",
 year         = "2002",
 title        = "NuSMV 2: An OpenSource Tool for Symbolic Model Checking",
 editor       = "Ed Brinksma and Kim Guldstrand Larsen",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "2404",
 publisher    = "Springer",
 pages        = "359--364",
 doi          = "10.1007/3-540-45657-0\_29",
)
@inproceedings(Cimatti08,
 author       = "Alessandro Cimatti and Marco Roveri and Viktor Schuppan and Andrei Tchaltsev",
 year         = "{2008}",
 title        = "{Diagnostic Information for Realizability}",
 booktitle    = "{Verification, Model Checking, and Abstract Interpretation (VMCAI)}",
 pages        = "{52--67}",
 doi          = "10.1007/978-3-540-78163-9\_9",
)
@inproceedings(Cimatti07,
 author       = "Alessandro Cimatti and Marco Roveri and Viktor Schuppan and Stefano Tonetta",
 year         = "{2007}",
 title        = "{Boolean Abstraction for Temporal Logic Satisfiability}",
 booktitle    = "{Computer Aided Verification (CAV)}",
 pages        = "{532--546}",
 doi          = "10.1007/978-3-540-73368-3\_53",
)
@inproceedings(DBLP:conf/dac/CoudertM92,
 author       = "Olivier Coudert and Jean Christophe Madre",
 year         = "1992",
 title        = "Implicit and Incremental Computation of Primes and Essential Primes of Boolean Functions",
 booktitle    = "DAC",
 pages        = "36--39",
 url          = "http://portal.acm.org/citation.cfm?id=113938.113929",
)
@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",
)
@phdthesis(Ehlers2013,
 author       = "R{\"u}diger Ehlers",
 year         = "2013",
 title        = "Symmetric and Efficient Synthesis",
 school       = "Saarland University",
)
@inproceedings(EhlersTopcuHSCC2014,
 author       = "R{\"u}diger Ehlers and Ufuk Topcu",
 year         = "2014",
 title        = "Resilience to Intermittent Assumption Violations in Reactive Synthesis",
 booktitle    = "17th International Conference on Hybrid Systems: Computation and Control (HSCC)",
 pages        = "203--212",
 doi          = "10.1145/2562059.2562128",
)
@inproceedings(DBLP:conf/aaai/FinucaneJK11,
 author       = "Cameron Finucane and Gangyuan Jing and Hadas Kress-Gazit",
 year         = "2011",
 title        = "Designing Reactive Robot Controllers with LTLMoP",
 booktitle    = "Automated Action Planning for Autonomous Mobile Robots",
 series       = "AAAI Workshops",
 volume       = "WS-11-09",
 publisher    = "AAAI",
 url          = "http://www.aaai.org/ocs/index.php/WS/AAAIW11/paper/view/3982",
)
@inproceedings(DBLP:conf/hvc/FismanKSV08,
 author       = "Dana Fisman and Orna Kupferman and Sarai Sheinvald-Faragy and Moshe Y. Vardi",
 year         = "2008",
 title        = "A Framework for Inherent Vacuity",
 editor       = "Hana Chockler and Alan J. Hu",
 booktitle    = "Haifa Verification Conference",
 series       = "Lecture Notes in Computer Science",
 volume       = "5394",
 publisher    = "Springer",
 pages        = "7--22",
 doi          = "10.1007/978-3-642-01702-5\_7",
)
@inproceedings(DBLP:conf/hvc/KleinP10,
 author       = "Uri Klein and Amir Pnueli",
 year         = "2010",
 title        = "Revisiting Synthesis of {GR(1)} Specifications",
 booktitle    = "Haifa Verification Conference (HVC)",
 pages        = "161--181",
 doi          = "10.1007/978-3-642-19583-9\_16",
)
@inproceedings(DBLP:conf/hvc/KonighoferHB10,
 author       = "Robert K{\"o}nighofer and Georg Hofferek and Roderick Bloem",
 year         = "2010",
 title        = "Debugging Unrealizable Specifications with Model-Based Diagnosis",
 booktitle    = "Haifa Verification Conference",
 pages        = "29--45",
 doi          = "10.1007/978-3-642-19583-9\_8",
)
@article(DBLP:journals/sttt/KonighoferHB13,
 author       = "Robert K{\"o}nighofer and Georg Hofferek and Roderick Bloem",
 year         = "2013",
 title        = "Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies",
 journal      = "STTT",
 volume       = "15",
 number       = "5-6",
 pages        = "563--583",
 doi          = "10.1007/s10009-011-0221-y",
)
@inproceedings(DBLP:conf/icra/Kress-GazitFP07,
 author       = "Hadas Kress-Gazit and Georgios E. Fainekos and George J. Pappas",
 year         = "2007",
 title        = "Where's Waldo? Sensor-Based Temporal Logic Motion Planning",
 booktitle    = "ICRA",
 publisher    = "IEEE",
 pages        = "3116--3121",
 doi          = "10.1109/ROBOT.2007.363946",
)
@article(KGF,
 author       = "Hadas Kress-Gazit 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(Li11,
 author       = "Wenchao Li and Lili Dworkin and Sanjit A. Seshia",
 year         = "{2011}",
 title        = "{Mining Assumptions for Synthesis}",
 booktitle    = "{{{ACM-IEEE}} International Conference on Formal Methods and Models for Codesign (MEMOCODE)}",
 pages        = "{43--50}",
 doi          = "10.1109/MEMCOD.2011.5970509",
)
@article(DBLP:journals/taosd/MaozS13,
 author       = "Shahar Maoz and Yaniv Sa'ar",
 year         = "2013",
 title        = "Two-Way Traceability and Conflict Debugging for AspectLTL Programs",
 journal      = "T. Aspect-Oriented Software Development",
 volume       = "10",
 pages        = "39--72",
 doi          = "10.1007/978-3-642-36964-3\_2",
)
@article(Nuzzo13,
 author       = "P. Nuzzo and H. Xu and N. Ozay and J.B. Finn and A.L. Sangiovanni-Vincentelli and R.M. Murray and A. Donze and S.A. Seshia",
 year         = "2013",
 title        = "A Contract-Based Methodology for Aircraft Electric Power System Design",
 journal      = "Access, IEEE",
 volume       = "PP",
 number       = "99",
 pages        = "1--1",
 doi          = "10.1109/ACCESS.2013.2295764",
)
@inproceedings(DBLP:conf/iccps/OzayTMW11,
 author       = "Necmiye Ozay and Ufuk Topcu and Richard M. Murray and Tichakorn Wongpiromsarn",
 year         = "2011",
 title        = "Distributed Synthesis of Control Protocols for Smart Camera Networks",
 booktitle    = "ICCPS",
 publisher    = "IEEE",
 pages        = "45--54",
 doi          = "10.1109/ICCPS.2011.22",
)
@inproceedings(DBLP:conf/cav/PeterEM11,
 author       = "Hans-J{\"o}rg Peter and R{\"u}diger Ehlers and Robert Mattm{\"u}ller",
 year         = "2011",
 title        = "Synthia: Verification and Synthesis for Timed Automata",
 editor       = "Ganesh Gopalakrishnan and Shaz Qadeer",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "6806",
 publisher    = "Springer",
 pages        = "649--655",
 doi          = "10.1007/978-3-642-22110-1\_52",
)
@inproceedings(DBLP:conf/focs/Pnueli77,
 author       = "Amir Pnueli",
 year         = "1977",
 title        = "The Temporal Logic of Programs",
 booktitle    = "FOCS",
 publisher    = "IEEE",
 pages        = "46--57",
)
@inproceedings(DBLP:conf/icalp/PnueliR89,
 author       = "Amir Pnueli and Roni Rosner",
 year         = "1989",
 title        = "On the Synthesis of an Asynchronous Reactive Module",
 booktitle    = "ICALP",
 pages        = "652--671",
)
@inproceedings(Raman_CAV11,
 author       = "Vasumathi Raman and Hadas Kress-Gazit",
 year         = "{2011}",
 title        = "{Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using {{LTLMoP}}}",
 booktitle    = "{Computer Aided Verification (CAV)}",
 pages        = "{663--668}",
 doi          = "10.1007/978-3-642-22110-1\_54",
)
@article(Raman_TRO13,
 author       = "Vasumathi Raman and Hadas Kress-Gazit",
 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",
)
@inproceedings(Raman_IROS13,
 author       = "Vasumathi Raman and Hadas Kress-Gazit",
 year         = "2013",
 title        = "Towards minimal explanations of unsynthesizability for high-level robot behaviors",
 booktitle    = "IROS",
 publisher    = "IEEE",
 pages        = "757--762",
 doi          = "10.1109/IROS.2013.6696436",
)
@inproceedings(DBLP:conf/icra/RamanPK13,
 author       = "Vasumathi Raman and Nir Piterman and Hadas Kress-Gazit",
 year         = "2013",
 title        = "Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations",
 booktitle    = "ICRA",
 publisher    = "IEEE",
 pages        = "4075--4081",
 doi          = "10.1109/ICRA.2013.6631152",
)
@inproceedings(Schuppan09,
 author       = "Viktor Schuppan",
 year         = "2009",
 title        = "Towards a Notion of Unsatisfiable Cores for {LTL}",
 booktitle    = "Fundamentals of Software Engineering ({FSEN})",
 pages        = "129--145",
 doi          = "10.1007/978-3-642-11623-0\_7",
)
@inproceedings(Shlyakhter03,
 author       = "I. Shlyakhter and R. Seater and D. Jackson and M. Sridharan and M. Taghdiri",
 year         = "{2003}",
 title        = "{Debugging Overconstrained Declarative Models Using Unsatisfiable Cores}",
 booktitle    = "{IEEE International Conference on Automated Software Engineering (ASE)}",
 pages        = "{94--105}",
 doi          = "{10.1109/ASE.2003.1240298}",
)
@inproceedings(DBLP:conf/fmcad/SohailS09,
 author       = "Saqib Sohail and Fabio Somenzi",
 year         = "2009",
 title        = "Safety first: A two-stage algorithm for {LTL} games",
 editor       = "Armin Biere and Carl Pixley",
 booktitle    = "FMCAD",
 publisher    = "IEEE",
 pages        = "77--84",
 doi          = "10.1109/FMCAD.2009.5351138",
)
@inproceedings(Wongpiromsarn2011-infotech,
 author       = "Tichakorn Wongpiromsarn and Ufuk Topcu and Richard M. Murray",
 year         = "2011",
 title        = "Formal synthesis of embedded control software for vehicle management systems",
 booktitle    = "AIAA Infotech@Aerospace",
 doi          = "10.2514/6.2011-1506",
)
@article(Nok10,
 author       = "Tichakorn Wongpiromsarn and Ufuk Topcu and Richard M. Murray",
 year         = "2012",
 title        = "Receding Horizon Temporal Logic Planning",
 journal      = "IEEE Trans. Automat. Contr.",
 volume       = "57",
 number       = "11",
 pages        = "2817--2830",
 doi          = "10.1109/TAC.2012.2195811",
)
@inproceedings(DBLP:conf/hybrid/WongpiromsarnTOXM11,
 author       = "Tichakorn Wongpiromsarn and Ufuk Topcu and Necmiye Ozay and Huan Xu and Richard M. Murray",
 year         = "2011",
 title        = "TuLiP: a software toolbox for receding horizon temporal logic planning",
 editor       = "Marco Caccamo and Emilio Frazzoli and Radu Grosu",
 booktitle    = "HSCC",
 publisher    = "ACM",
 pages        = "313--314",
 doi          = "10.1145/1967701.1967747",
)