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