Luca de Alfaro & Pritam Roy (2010):
Solving games via three-valued abstraction refinement.
Inf. Comput. 208(6),
pp. 666–676,
doi:10.1016/j.ic.2009.05.007.
Tomás Babiak, Mojmír Kretínský, Vojtech Rehák & Jan Strejcek (2012):
LTL to Büchi Automata Translation: Fast and More Deterministic.
In: TACAS,
LNCS 7214.
Springer,
pp. 95–109,
doi:10.1007/978-3-642-28756-5_8.
Adrian Balint, Daniel Diepold, Daniel Gall, Simon Gerber, Gregor Kapler & Robert Retz (2011):
EDACC - An Advanced Platform for the Experiment Design, Administration and Analysis of Empirical Algorithms.
In: LION 5. Selected Papers,
LNCS 6683.
Springer,
pp. 586–599,
doi:10.1007/978-3-642-25566-3_46.
R. Bloem, R. Könighofer & M. Seidl (2014):
SAT-Based Synthesis Methods for Safety Specs.
In: VMCAI,
LNCS 8318.
Springer,
pp. 1–20,
doi:10.1007/978-3-642-54013-4_1.
Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2012):
Acacia+, a Tool for LTL Synthesis.
In: CAV,
LNCS 7358.
Springer,
pp. 652–657,
doi:10.1007/978-3-642-31424-7_45.
Robert K. Brayton & Alan Mishchenko (2010):
ABC: An Academic Industrial-Strength Verification Tool.
In: CAV,
LNCS 6174.
Springer,
pp. 24–40,
doi:10.1007/978-3-642-14295-6_5.
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2014):
AbsSynthe: abstract synthesis from succinct safety specifications.
In: SYNT,
EPTCS 157.
Open Publishing Association,
pp. 100–116,
doi:10.4204/EPTCS.157.11.
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2015):
Compositional Algorithms for Succinct Safety Games.
In: SYNT,
EPTCS 202.
Open Publishing Association,
pp. 98–111,
doi:10.4204/EPTCS.202.7.
Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere & Keijo Heljanko (2016):
Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks.
Journal on Satisfiability, Boolean Modeling and Computation 9,
pp. 135–172.
Available at https://www.satassociation.org/jsat/index.php/jsat/article/download/129/111.
Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li & Frank Stephan (2017):
Deciding parity games in quasipolynomial time.
In: Hamed Hatami, Pierre McKenzie & Valerie King: Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017.
ACM,
pp. 252–263,
doi:10.1145/3055399.3055409.
Alonzo Church (1962):
Logic, arithmetic and automata.
In: Proceedings of the international congress of mathematicians,
pp. 23–35.
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault & Laurent Xu (2016):
Spot 2.0 — a framework for LTL and ω-automata manipulation.
In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16),
LNCS 9938.
Springer,
pp. 122–129,
doi:10.1007/978-3-319-46520-3_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.
Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe & Leander Tentrup (2017):
Encodings of Bounded Synthesis.
In: TACAS (1),
LNCS 10205,
pp. 354–370,
doi:10.1007/978-3-662-54577-5_20.
Peter Faymonville, Bernd Finkbeiner & Leander Tentrup (2017):
BoSy: An Experimentation Framework for Bounded Synthesis.
In: CAV (2),
LNCS 10427.
Springer,
pp. 325–332,
doi:10.1007/978-3-319-63390-9_17.
Bernd Finkbeiner & Felix Klein (2016):
Bounded Cycle Synthesis.
In: CAV (1),
LNCS 9779.
Springer,
pp. 118–135,
doi:10.1007/978-3-319-41528-4_7.
Bernd Finkbeiner, Markus N. Rabe & César Sánchez (2015):
Algorithms for Model Checking HyperLTL and HyperCTL*.
In: CAV,
LNCS 9206.
Springer,
pp. 30–48,
doi:10.1007/978-3-319-21690-4_3.
Bernd Finkbeiner & Sven Schewe (2013):
Bounded synthesis.
STTT 15(5-6),
pp. 519–539,
doi:10.1007/s10009-012-0228-z.
Johann Glaser & Clifford Wolf (2014):
Methodology and Example-Driven Interconnect Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable Architectures,
pp. 201–221.
Springer International Publishing,
Cham,
doi:10.1007/978-3-319-01418-0_12.
Swen Jacobs (2014):
Extended AIGER Format for Synthesis.
CoRR abs/1405.5793.
Available at http://arxiv.org/abs/1405.5793.
Swen Jacobs & Roderick Bloem (2016):
The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond.
In: SYNT@CAV 2016,
EPTCS 229,
pp. 133–148,
doi:10.4204/EPTCS.229.11.
Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2017):
The first reactive synthesis competition (SYNTCOMP 2014).
STTT 19(3),
pp. 367–390,
doi:10.1007/s10009-016-0416-3.
Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2016):
The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results.
In: SYNT@CAV,
EPTCS 229,
pp. 149–177,
doi:10.4204/EPTCS.229.12.
Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2016):
The Second Reactive Synthesis Competition (SYNTCOMP 2015).
In: SYNT,
EPTCS 202.
Open Publishing Association,
pp. 27–57,
doi:10.4204/EPTCS.202.4.
Swen Jacobs, Felix Klein & Sebastian Schirmer (2016):
A High-Level LTL Synthesis Format: TLSF v1.1.
In: SYNT@CAV 2016,
EPTCS 229,
pp. 112–132,
doi:10.4204/EPTCS.229.10.
Mikolás Janota, William Klieber, Joao Marques-Silva & Edmund M. Clarke (2016):
Solving QBF with counterexample guided refinement.
Artif. Intell. 234,
pp. 1–25,
doi:10.1016/j.artint.2016.01.004.
Barbara Jobstmann (2007):
Applications and Optimizations for LTL Synthesis.
Graz University of Technology.
Barbara Jobstmann & Roderick Bloem (2006):
Optimizations for LTL Synthesis.
In: FMCAD.
IEEE Computer Society,
pp. 117–124,
doi:10.1109/FMCAD.2006.22.
Ayrat Khalimov (2015):
Specification Format for Reactive Synthesis Problems.
In: SYNT,
EPTCS 202.
Open Publishing Association,
pp. 112–119,
doi:10.4204/EPTCS.202.8.
Ayrat Khalimov, Swen Jacobs & Roderick Bloem (2013):
PARTY Parameterized Synthesis of Token Rings.
In: CAV,
LNCS 8044.
Springer,
pp. 928–933,
doi:10.1007/978-3-642-39799-8_66.
Ayrat Khalimov, Swen Jacobs & Roderick Bloem (2013):
Towards Efficient Parameterized Synthesis.
In: VMCAI,
LNCS 7737.
Springer,
pp. 108–127,
doi:10.1007/978-3-642-35873-9_9.
Alexander Legg, Nina Narodytska & Leonid Ryzhyk (2016):
A SAT-Based Counterexample Guided Method for Unbounded Synthesis.
In: CAV (2),
LNCS 9780.
Springer,
pp. 364–382,
doi:10.1007/978-3-319-41540-6_20.
Jia Hui Liang, Vijay Ganesh, Pascal Poupart & Krzysztof Czarnecki (2016):
Learning Rate Based Branching Heuristic for SAT Solvers.
In: Nadia Creignou & Daniel Le Berre: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings,
Lecture Notes in Computer Science 9710.
Springer,
pp. 123–140,
doi:10.1007/978-3-319-40970-2_9.
Donald A. Martin (1975):
Borel Determinacy.
Annals of Mathematics 102(2),
pp. 363–371.
Leonardo Mendonça de Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: TACAS,
LNCS 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
Roman R. Redziejowski (2012):
An Improved Construction of Deterministic Omega-automaton Using Derivatives.
Fundam. Inform. 119(3-4),
pp. 393–406,
doi:10.3233/FI-2012-744.
M. Seidl & R. Könighofer (2014):
Partial witnesses from preprocessed quantified Boolean formulas.
In: DATE'14.
IEEE,
pp. 1–6,
doi:10.7873/DATE2014.162.
Cong Tian, Jun Song, Zhenhua Duan & Zhao Duan (2015):
LtlNfBa: Making LTL Translation More Practical.
In: SOFL+MSVL,
LNCS 9559.
Springer,
pp. 179–194,
doi:10.1007/978-3-319-31220-0_13.
James C. Tiernan (1970):
An efficient search algorithm to find the elementary circuits of a graph.
Commun. ACM 13(12),
pp. 722–726,
doi:10.1145/362814.362819.
Cheng-Yin Wu, Chi-An Wu, Chien-Yu Lai & Chung-Yang R. Haung (2014):
A Counterexample-Guided Interpolant Generation Algorithm for SAT-Based Model Checking.
IEEE Trans. on CAD of Integrated Circuits and Systems 33(12),
pp. 1846–1858,
doi:10.1109/TCAD.2014.2363395.
Wieslaw Zielonka (1998):
Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees.
Theor. Comput. Sci. 200(1-2),
pp. 135–183,
doi:10.1016/S0304-3975(98)00009-7.