References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. Rüdiger Ehlers (2012): Symbolic bounded synthesis. Formal Methods in System Design 40(2), pp. 232–262, doi:10.1007/s10703-011-0137-x.
  9. Rüdiger Ehlers (2013): Symmetric and Efficient Synthesis. Saarland University.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  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.
  23. Amir Pnueli (1977): The Temporal Logic of Programs. In: FOCS. IEEE, pp. 46–57.
  24. Amir Pnueli & Roni Rosner (1989): On the Synthesis of an Asynchronous Reactive Module. In: ICALP, pp. 652–671.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. 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.
  31. 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.
  32. 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.
  33. 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.
  34. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org