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.
ARM Ltd. (1999):
AMBAspecification (rev. 2).
Available at www.arm.com.
Giorgio Ausiello, Mariangiola Dezani-Ciancaglini & Simona Ronchi Della Rocca (1989):
Automata, Languages and Programming, 16th International Colloquium, (ICALP).
LNCS 372.
Springer.
Armin Biere, Marijn Heule, Hans van Maaren & Toby Walsh (2009):
Handbook of Satisfiability.
IOS Press.
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.
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.
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.
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.
Roderick Bloem, Barbara Jobstmann & Martin Weiglhofer (2007):
Anzu.
http://www.ist.tugraz.at/staff/jobstmann/anzu/.
Randal E. Bryant (1986):
Graph-Based Algorithms for Boolean Function Manipulation.
IEEE Trans. Computers 35(8),
pp. 677–691.
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.
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.
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/.
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.
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.
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.
Cindy Eisner & Dana Fisman (2006):
A Practical Introduction to PSL (Series on Integrated Circuits and Systems).
Springer-Verlag.
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.
Emanuel Falkenauer (1998):
On Method Overfitting.
J. Heuristics 4(3),
pp. 281–287.
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.
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.
Bernd Finkbeiner & Sven Schewe (2005):
Uniform Distributed Synthesis.
In: LICS.
IEEE Computer Society,
pp. 321–330,
doi:10.1109/LICS.2005.53.
Michael J. Fischer & Richard E. Ladner (1979):
Propositional Dynamic Logic of Regular Programs.
J. Comput. Syst. Sci. 18(2),
pp. 194–211.
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.
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.
Allen Van Gelder & Daniel Le Berre (2010):
Pragmatics of SAT,
Workshop at the Federated Logic Conference (FLoC) 2010, Edinburgh.
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.
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.
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.
Erich Grädel, Wolfgang Thomas & Thomas Wilke (2002):
Automata, Logics, and Infinite Games: A Guide to Current Research.
LNCS 2500.
Springer.
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.
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.
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.
IBM Research:
RuleBase formal verification tool tutorial.
https://www.research.ibm.com/haifa/projects/verification/RB_Homepage/.
Barbara Jobstmann & Roderick Bloem (2006):
Lily - a LInear Logic sYnthesizer.
http://www.iaik.tugraz.at/content/research/design_verification/lily/.
Barbara Jobstmann & Roderick Bloem (2006):
Optimizations for LTL Synthesis.
In: FMCAD.
IEEE Computer Society,
pp. 117–124,
doi:10.1109/FMCAD.2006.22.
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.
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.
Uri Klein & Amir Pnueli (2010):
Revisiting Synthesis of GR(1) Specifications.
In: HVC,
LNCS 6504.
Stephan Kottler (2010):
SAT Solving with Reference Points.
In: Strichman & Szeider,
pp. 143–157,
doi:10.1007/978-3-642-14186-7_13.
James H. Kukula & Thomas R. Shiple (2000):
Building Circuits from Relations.
In: Emerson & Sistla,
pp. 113–123.
Orna Kupferman & Moshe Y. Vardi (2005):
Safraless Decision Procedures.
In: FOCS.
IEEE,
pp. 531–542,
doi:10.1109/SFCS.2005.66.
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.
A. Morgenstern (2010):
Symbolic Controller Synthesis for LTL Specifications.
Department of Computer Science, University of Kaiserslautern, Germany.
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.
Silvia M. Müller & Wolfgang J. Paul (2000):
Computer architecture: complexity and correctness.
Springer.
Alexander Nadel & Vadim Ryvchin (2010):
Assignment Stack Shrinking.
In: Strichman & Szeider,
pp. 375–381,
doi:10.1007/978-3-642-14186-7_35.
Ian Parberry (1994):
A Guide for New Referees in Theoretical Computer Science.
Inf. Comput. 112(1),
pp. 96–116.
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.
Amir Pnueli (1977):
The Temporal Logic of Programs.
In: FOCS.
IEEE,
pp. 46–57.
Amir Pnueli & Roni Rosner (1989):
On the Synthesis of a Reactive Module.
In: POPL,
pp. 179–190.
Amir Pnueli & Roni Rosner (1989):
On the Synthesis of an Asynchronous Reactive Module.
In: editor = "Ausiello",,
pp. 652–671.
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.
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.
Kristin Y. Rozier & Moshe Y. Vardi (2010):
LTL satisfiability checking.
STTT 12(2),
pp. 123–137,
doi:10.1007/s10009-010-0140-3.
Shmuel Safra (1989):
Complexity of Automata on Infinite Objects.
Weizmann Institute of Science, Rehovot, Israel.
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.
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.
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.
Fabio Somenzi (2009):
CUDD: CU Decision Diagram Package Release 2.4.2.
Fabio Somenzi & Roderick Bloem (2000):
Efficient Büchi Automata from LTL Formulae.
In: Emerson & Sistla,
pp. 248–263.
Ofer Strichman & Stefan Szeider (2010):
Theory and Applications of Satisfiability Testing (SAT).
LNCS 6175.
Springer,
doi:10.1007/978-3-642-14186-7.
Walter F. Tichy (1998):
Should Computer Scientists Experiment More?.
IEEE Computer 31(5),
pp. 32–40.
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.
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.
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.