References

  1. Mart\'ın Abadi, Leslie Lamport & Pierre Wolper (1989): Realizable and Unrealizable Specifications of Reactive Systems. In: editor = "Ausiello",, pp. 1–17, doi:10.1007/BFb0035748.
  2. ARM Ltd. (1999): AMBAspecification (rev. 2). Available at www.arm.com.
  3. Giorgio Ausiello, Mariangiola Dezani-Ciancaglini & Simona Ronchi Della Rocca (1989): Automata, Languages and Programming, 16th International Colloquium, (ICALP). LNCS 372. Springer.
  4. Armin Biere, Marijn Heule, Hans van Maaren & Toby Walsh (2009): Handbook of Satisfiability. IOS Press.
  5. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger & Barbara Jobstmann (2010): Robustness in the Presence of Liveness. In: editor = "Touili",, pp. 410–424, doi:10.1007/978-3-642-14295-6_36.
  6. Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan & Richard Seeber (2010): RATSY - A New Requirements Analysis Tool with Synthesis. In: editor = "Touili",, pp. 425–429, doi:10.1007/978-3-642-14295-6_37.
  7. Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Interactive presentation: Automatic hardware synthesis from specifications: a case study. In: Rudy Lauwereins & Jan Madsen: DATE. ACM, pp. 1188–1193, doi:10.1145/1266366.1266622.
  8. Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Specify, Compile, Run: Hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), pp. 3–16, doi:10.1016/j.entcs.2007.09.004.
  9. Roderick Bloem, Barbara Jobstmann & Martin Weiglhofer (2007): Anzu. http://www.ist.tugraz.at/staff/jobstmann/anzu/.
  10. Randal E. Bryant (1986): Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), pp. 677–691.
  11. Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen & Didier Lime (2005): Efficient On-the-Fly Algorithms for the Analysis of Timed Games. In: Mart\'ın Abadi & Luca de Alfaro: CONCUR, LNCS 3653. Springer, pp. 66–80, doi:10.1007/11539452_9.
  12. Lorenzo Clemente & Richard Mayr (2010): Multipebble Simulations for Alternating Automata - (Extended Abstract). In: Paul Gastin & François Laroussinie: CONCUR, LNCS 6269. Springer, pp. 297–312, doi:10.1007/978-3-642-15375-4_21.
  13. Laurent Doyen, Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2009): Acacia - LTL Realizability Check and Winning Strategy Synthesis using Antichains. http://www.antichains.be/acacia/.
  14. Alexandre Duret-Lutz & Denis Poitrenaud (2004): SPOT: An Extensible Model Checking Library Using Transition-Based Generalized Büchi Automata. In: Doug DeGroot, Peter G. Harrison, Harry A. G. Wijshoff & Zary Segall: MASCOTS. IEEE Computer Society, pp. 76–83.
  15. Rüdiger Ehlers (2010): Minimising Deterministic Büchi Automata Precisely Using SAT Solving. In: Strichman & Szeider, pp. 326–332, doi:10.1007/978-3-642-14186-7_28.
  16. Rüdiger Ehlers (2010): Symbolic Bounded Synthesis. In: editor = "Touili",, pp. 365–379, doi:10.1007/978-3-642-14295-6_33.
  17. Rüdiger Ehlers (2010): Unbeast – Symbolic Bounded Synthesis. http://react.cs.uni-saarland.de/tools/unbeast/.
  18. Rüdiger Ehlers & Bernd Finkbeiner (2010): On the Virtue of Patience: Minimizing Büchi Automata. In: van de Pol & Weber, pp. 129–145, doi:10.1007/978-3-642-16164-3_10.
  19. Cindy Eisner & Dana Fisman (2006): A Practical Introduction to PSL (Series on Integrated Circuits and Systems). Springer-Verlag.
  20. E. Allen Emerson & A. Prasad Sistla (2000): Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. LNCS 1855. Springer.
  21. Emanuel Falkenauer (1998): On Method Overfitting. J. Heuristics 4(3), pp. 281–287.
  22. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2009): An Antichain Algorithm for LTL Realizability. In: Ahmed Bouajjani & Oded Maler: CAV, LNCS 5643. Springer, pp. 263–277, doi:10.1007/978-3-642-02658-4_22.
  23. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2010): Compositional Algorithms for LTL Synthesis. In: Ahmed Bouajjani & Wei-Ngan Chin: ATVA, LNCS 6252. Springer, pp. 112–127, doi:10.1007/978-3-642-15643-4_10.
  24. Bernd Finkbeiner & Sven Schewe (2005): Uniform Distributed Synthesis. In: LICS. IEEE Computer Society, pp. 321–330, doi:10.1109/LICS.2005.53.
  25. Michael J. Fischer & Richard E. Ladner (1979): Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci. 18(2), pp. 194–211.
  26. Riccardo Forth & Paul Molitor (2000): An efficient heuristic for state encoding minimizing the BDD representations of the transistion relations of finite state machines. In: ASP-DAC. ACM, pp. 61–66.
  27. Paul Gastin & Denis Oddoux (2001): Fast LTL to Büchi Automata Translation. In: Gérard Berry, Hubert Comon & Alain Finkel: CAV, LNCS 2102. Springer, pp. 53–65.
  28. Allen Van Gelder & Daniel Le Berre (2010): Pragmatics of SAT, Workshop at the Federated Logic Conference (FLoC) 2010, Edinburgh.
  29. Naghmeh Ghafari, Alan J. Hu & Zvonimir Rakamaric (2010): Context-Bounded Translations for Concurrent Software: An Empirical Evaluation. In: van de Pol & Weber, pp. 227–244, doi:10.1007/978-3-642-16164-3_17.
  30. Yashdeep Godhal, Krishnendu Chatterjee & Thomas A. Henzinger (2010): Synthesis of AMBA AHB from Formal Specification. CoRR abs/1001.2811. Available at http://arxiv.org/abs/1001.2811.
  31. Wilsin Gosti, Tiziano Villa, Alexander Saldanha & Alberto L. Sangiovanni-Vincentelli (2007): FSM Encoding for BDD Representations. Applied Mathematics and Computer Science 17(1), pp. 113–124, doi:10.2478/v10006-007-0011-6.
  32. Erich Grädel, Wolfgang Thomas & Thomas Wilke (2002): Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS 2500. Springer.
  33. Karin Greimel, Roderick Bloem, Barbara Jobstmann & Moshe Y. Vardi (2008): Open Implication. In: Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir & Igor Walukiewicz: ICALP (2), LNCS 5126. Springer, pp. 361–372, doi:10.1007/978-3-540-70583-3_30.
  34. Aidan Harding, Mark Ryan & Pierre-Yves Schobbens (2005): A New Algorithm for Strategy Synthesis in LTL Games. In: Nicolas Halbwachs & Lenore D. Zuck: TACAS, LNCS 3440. Springer, pp. 477–492.
  35. Thomas A. Henzinger & Nir Piterman (2006): Solving Games Without Determinization. In: Zoltán Ésik: CSL, LNCS 4207. Springer, pp. 395–410, doi:10.1007/11874683_26.
  36. IBM Research: RuleBase formal verification tool tutorial. https://www.research.ibm.com/haifa/projects/verification/RB_Homepage/.
  37. Barbara Jobstmann & Roderick Bloem (2006): Lily - a LInear Logic sYnthesizer. http://www.iaik.tugraz.at/content/research/design_verification/lily/.
  38. Barbara Jobstmann & Roderick Bloem (2006): Optimizations for LTL Synthesis. In: FMCAD. IEEE Computer Society, pp. 117–124, doi:10.1109/FMCAD.2006.22.
  39. Barbara Jobstmann, Stefan Galler, Martin Weiglhofer & Roderick Bloem (2007): Anzu: A Tool for Property Synthesis. In: Werner Damm & Holger Hermanns: CAV, LNCS 4590. Springer, pp. 258–262, doi:10.1007/978-3-540-73368-3_29.
  40. Joachim Klein & Christel Baier (2006): Experiments with deterministic ω-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), pp. 182–195, doi:10.1016/j.tcs.2006.07.022.
  41. Uri Klein & Amir Pnueli (2010): Revisiting Synthesis of GR(1) Specifications. In: HVC, LNCS 6504.
  42. Stephan Kottler (2010): SAT Solving with Reference Points. In: Strichman & Szeider, pp. 143–157, doi:10.1007/978-3-642-14186-7_13.
  43. James H. Kukula & Thomas R. Shiple (2000): Building Circuits from Relations. In: Emerson & Sistla, pp. 113–123.
  44. Orna Kupferman (2006): Avoiding Determinization. In: LICS. IEEE Computer Society, pp. 243–254, doi:10.1109/LICS.2006.15.
  45. Orna Kupferman, Nir Piterman & Moshe Y. Vardi (2006): Safraless Compositional Synthesis. In: Thomas Ball & Robert B. Jones: CAV, LNCS 4144. Springer, pp. 31–44, doi:10.1007/11817963_6.
  46. Orna Kupferman & Moshe Y. Vardi (1999): Church's problem revisited. Bulletin of Symbolic Logic 5(2), pp. 245–263. Available at http://www.math.ucla.edu/~asl/bsl/0502/0502-004.ps.
  47. Orna Kupferman & Moshe Y. Vardi (2001): Model Checking of Safety Properties. Formal Methods in System Design 19(3), pp. 291–314.
  48. Orna Kupferman & Moshe Y. Vardi (2001): Synthesizing Distributed Systems. In: LICS.
  49. Orna Kupferman & Moshe Y. Vardi (2005): Safraless Decision Procedures. In: FOCS. IEEE, pp. 531–542, doi:10.1109/SFCS.2005.66.
  50. Xinxin Liu & Scott A. Smolka (1998): Simple Linear-Time Algorithms for Minimal Fixed Points (Extended Abstract). In: Kim G. Larsen, Sven Skyum & Glynn Winskel: ICALP, LNCS 1443. Springer, pp. 53–66, doi:10.1007/978-3-540-64781-2_53.
  51. A. Morgenstern (2010): Symbolic Controller Synthesis for LTL Specifications. Department of Computer Science, University of Kaiserslautern, Germany.
  52. A. Morgenstern & K. Schneider (2010): Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis. In: A. Montanari, M. Napoli & M. Parente: GandALF, EPTCS 25, pp. 89–102, doi:10.4204/EPTCS.25.11.
  53. Silvia M. Müller & Wolfgang J. Paul (2000): Computer architecture: complexity and correctness. Springer.
  54. Alexander Nadel & Vadim Ryvchin (2010): Assignment Stack Shrinking. In: Strichman & Szeider, pp. 375–381, doi:10.1007/978-3-642-14186-7_35.
  55. Carsten Sinz (organiser): SAT-Race 2010. http://baldur.iti.uka.de/sat-race-2010/.
  56. Ian Parberry (1994): A Guide for New Referees in Theoretical Computer Science. Inf. Comput. 112(1), pp. 96–116.
  57. Nir Piterman, Amir Pnueli & Yaniv Sa'ar (2006): Synthesis of Reactive(1) Designs. In: E. Allen Emerson & Kedar S. Namjoshi: VMCAI, LNCS 3855. Springer, pp. 364–380, doi:10.1007/11609773_24.
  58. Amir Pnueli (1977): The Temporal Logic of Programs. In: FOCS. IEEE, pp. 46–57.
  59. Amir Pnueli & Roni Rosner (1989): On the Synthesis of a Reactive Module. In: POPL, pp. 179–190.
  60. Amir Pnueli & Roni Rosner (1989): On the Synthesis of an Asynchronous Reactive Module. In: editor = "Ausiello",, pp. 652–671.
  61. Amir Pnueli, Yaniv Sa'ar & Lenore D. Zuck (2010): Jtlv: A Framework for Developing Verification Algorithms. In: editor = "Touili",, pp. 171–174, doi:10.1007/978-3-642-14295-6_18.
  62. Jaco van de Pol & Michael Weber (2010): Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. LNCS 6349. Springer, doi:10.1007/978-3-642-16164-3.
  63. Kristin Y. Rozier & Moshe Y. Vardi (2010): LTL satisfiability checking. STTT 12(2), pp. 123–137, doi:10.1007/s10009-010-0140-3.
  64. Shmuel Safra (1989): Complexity of Automata on Infinite Objects. Weizmann Institute of Science, Rehovot, Israel.
  65. Sven Schewe & Bernd Finkbeiner (2007): Bounded Synthesis. In: Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino & Yoshio Okamura: ATVA, LNCS 4762. Springer, pp. 474–488, doi:10.1007/978-3-540-75596-8_33.
  66. Saqib Sohail & Fabio Somenzi (2009): Safety first: A two-stage algorithm for LTL games. In: FMCAD. IEEE, pp. 77–84, doi:10.1109/FMCAD.2009.5351138.
  67. Saqib Sohail, Fabio Somenzi & Kavita Ravi (2008): A Hybrid Algorithm for LTL Games. In: Francesco Logozzo, Doron Peled & Lenore D. Zuck: VMCAI, LNCS 4905. Springer, pp. 309–323, doi:10.1007/978-3-540-78163-9_26.
  68. Fabio Somenzi (2009): CUDD: CU Decision Diagram Package Release 2.4.2.
  69. Fabio Somenzi & Roderick Bloem (2000): Efficient Büchi Automata from LTL Formulae. In: Emerson & Sistla, pp. 248–263.
  70. Ofer Strichman & Stefan Szeider (2010): Theory and Applications of Satisfiability Testing (SAT). LNCS 6175. Springer, doi:10.1007/978-3-642-14186-7.
  71. Walter F. Tichy (1998): Should Computer Scientists Experiment More?. IEEE Computer 31(5), pp. 32–40.
  72. Tayssir Touili, Byron Cook & Paul Jackson (2010): The 22nd International Conference on Computer Aided Verification (CAV). LNCS 6174. Springer, doi:10.1007/978-3-642-14295-6.
  73. Moshe Y. Vardi (1995): An Automata-Theoretic Approach to Linear Temporal Logic. In: Faron Moller & Graham M. Birtwistle: Banff Higher Order Workshop, LNCS 1043. Springer.
  74. Moshe Y. Vardi & Larry J. Stockmeyer (1985): Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report. In: STOC. ACM, pp. 240–251.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org