Rajeev Alur, Salar Moarref & Ufuk Topcu (2015):
Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis.
In: Christel Baier & Cesare Tinelli: Tools and Algorithms for the Construction and Analysis of Systems.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 501–516,
doi:10.1007/978-3-662-46681-0_49.
Ilan Beer, Shoham Ben-David, Cindy Eisner & Yoav Rodeh (2001):
Efficient Detection of Vacuity in Temporal Model Checking.
Formal Methods in System Design 18(2),
pp. 141–163,
doi:10.1023/A:1008779610539.
Shoham Ben-David, Fady Copty, Dana Fisman & Sitvanit Ruah (2015):
Vacuity in practice: temporal antecedent failure.
Formal Methods in System Design 46(1),
pp. 81–104,
doi:10.1007/s10703-014-0221-0.
Roderick Bloem, Hana Chockler, Masoud Ebrahimi & Ofer Strichman (2017):
Synthesizing Non-Vacuous Systems.
In: Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings,
pp. 55–72,
doi:10.1007/978-3-319-52234-0_4.
Roderick Bloem, Stefan Galler, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007):
Automatic hardware synthesis from specifications: A case study.
In: In Design, Automation and Test in Europe (DATE,
doi:10.1109/DATE.2007.364456.
Roderick Bloem, Hans-Jürgen Gamauf, Georg Hofferek, Bettina Könighofer & Robert Könighofer (2012):
Synthesizing Robust Systems with RATSY 84,
doi:10.4204/EPTCS.84.4.
Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2012):
Acacia+, a Tool for LTL Synthesis.
In: P. Madhusudan & Sanjit A. Seshia: Computer Aided Verification.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 652–657,
doi:10.1007/978-3-642-31424-7_45.
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík, Andreas Fellner & Jan Křetínský (2015):
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,
pp. 158–177.
Springer International Publishing,
Cham,
doi:10.1007/978-3-319-21690-4_10.
Tomas Brazdil, Krishnendu Chatterjee, Jan Kretinsky & Viktor Toman (2018):
Strategy Representation by Decision Trees in Reactive Synthesis.
In: TACAS.
Springer,
doi:10.1016/S0304-3975(98)00009-7.
J. Richard Buchi & Lawrence H. Landweber (1990):
Solving Sequential Conditions by Finite-State Strategies,
pp. 525–541.
Springer New York,
New York, NY,
doi:10.1007/978-1-4613-8928-6_29.
Krishnendu Chatterjee & Thomas A. Henzinger (2007):
Assume-Guarantee Synthesis.
In: Orna Grumberg & Michael Huth: Tools and Algorithms for the Construction and Analysis of Systems.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 261–275,
doi:10.1007/978-3-540-71209-1_21.
Krishnendu Chatterjee, Thomas A. Henzinger & Barbara Jobstmann (2008):
Environment Assumptions for Synthesis.
In: Franck van Breugel & Marsha Chechik: CONCUR 2008 - Concurrency Theory.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 147–161,
doi:10.1007/978-3-540-85361-9_14.
Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann & Arjun Radhakrishna (2010):
Gist: A Solver for Probabilistic Games.
In: Tayssir Touili, Byron Cook & Paul Jackson: Computer Aided Verification.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 665–669,
doi:10.1007/978-3-642-14295-6_57.
Chih-Hong Cheng, Yassine Hamza & Harald Ruess (2016):
Structural Synthesis for GXW Specifications.
In: International Conference on Computer Aided Verification.
Springer,
pp. 95–117,
doi:10.1007/978-3-319-89960-2_21.
Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess & Stefan Stattelmann (2014):
G4LTL-ST: Automatic generation of PLC programs.
In: International Conference on Computer Aided Verification.
Springer,
pp. 541–549,
doi:10.1007/978-3-319-08867-9_36.
Chih-Hong Cheng, Edward A Lee & Harald Ruess (2017):
autoCode4: Structural Controller Synthesis.
In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Springer,
pp. 398–404,
doi:10.1007/978-3-662-54577-5_23.
Hana Chockler, Joseph Y. Halpern & Orna Kupferman (2008):
What Causes a System to Satisfy a Specification?.
ACM Trans. Comput. Logic 9(3),
pp. 20:1–20:26,
doi:10.1145/1352582.1352588.
Hana Chockler, Orna Kupferman & Moshe Y. Vardi (2003):
Coverage Metrics for Formal Verification.
In: Daniel Geist & Enrico Tronci: Correct Hardware Design and Verification Methods.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 111–125,
doi:10.1007/978-3-540-39724-3_11.
A. Cimatti, M. Roveri, V. Schuppan & A. Tchaltsev (2008):
Diagnostic Information for Realizability.
In: Francesco Logozzo, Doron A. Peled & Lenore D. Zuck: Verification, Model Checking, and Abstract Interpretation.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 52–67,
doi:10.1007/978-3-540-78163-9_9.
Rüdiger Ehlers (2011):
Unbeast: Symbolic Bounded Synthesis.
In: Parosh Aziz Abdulla & K. Rustan M. Leino: Tools and Algorithms for the Construction and Analysis of Systems.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 272–275,
doi:10.1007/978-3-642-19835-9_25.
Rüdiger Ehlers & Vasumathi Raman (2016):
Slugs: Extensible GR(1) Synthesis.
In: Swarat Chaudhuri & Azadeh Farzan: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II,
Lecture Notes in Computer Science 9780.
Springer,
pp. 333–339,
doi:10.1007/978-3-319-41540-6_18.
Peter Faymonville, Bernd Finkbeiner & Leander Tentrup (2017):
BoSy: An Experimentation Framework for Bounded Synthesis.
In: Proceedings of CAV,
LNCS 10427.
Springer,
pp. 325–332,
doi:10.1007/978-3-319-63390-9_17.
Bernd Finkbeiner & Felix Klein (2016):
Bounded Cycle Synthesis.
Lecture Notes in Computer Science 9779.
Springer Berlin Heidelberg,
doi:10.1007/978-3-319-41528-4.
Bernd Finkbeiner & Felix Klein (2017):
Reactive Synthesis: Towards Output-Sensitive Algorithms.
In: Alexander Pretschner, Doron Peled & Thomas Hutzelmann: Dependable Software Systems Engineering,
NATO Science for Peace and Security Series, D: Information and Communication Security 50.
IOS Press,
pp. 25–43,
doi:10.3233/978-1-61499-810-5-25.
Bernd Finkbeiner & Sven Schewe (2013):
Bounded synthesis.
International Journal on Software Tools for Technology Transfer 15(5-6),
pp. 519–539,
doi:10.1007/s10009-012-0228-z.
Bernd Finkbeiner & Leander Tentrup (2015):
Detecting Unrealizability of Distributed Fault-tolerant Systems.
Logical Methods in Computer Science 11(3),
doi:10.2168/LMCS-11(3:12)2015.
Bernd Finkbeiner & Hazem Torfah (2016):
Synthesizing Skeletons for Reactive Systems,
pp. 271–286.
Springer International Publishing,
Cham,
doi:10.1007/978-3-319-46520-3_18.
M. Fujita, Y. Matsunaga & T. Kakuda (1991):
On variable ordering of binary decision diagrams for the application of multi-level logic synthesis.
In: Proceedings of the European Conference on Design Automation.,
pp. 50–54,
doi:10.1109/EDAC.1991.206358.
Yuichi Fukaya & Noriaki Yoshiura (2015):
Extracting Environmental Constraints in Reactive System Specifications.
In: Osvaldo Gervasi, Beniamino Murgante, Sanjay Misra, Marina L. Gavrilova, Ana Maria Alves Coutinho Rocha, Carmelo Torre, David Taniar & Bernady O. Apduhan: Computational Science and Its Applications – ICCSA 2015.
Springer International Publishing,
Cham,
pp. 671–685,
doi:10.1007/978-3-319-21410-8_51.
Yatin Hoskote, Timothy Kam, Pei-Hsin Ho & Xudong Zhao (1999):
Coverage Estimation for Symbolic Model Checking.
In: Proceedings of the 36th Annual ACM/IEEE Design Automation Conference,
DAC '99.
ACM,
New York, NY, USA,
pp. 300–305,
doi:10.1145/309847.309936.
Swen Jacobs, Nicolas Basset, Roderick Bloem, Romain Brenguier, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Thibaud Michaud, Guillermo A. Perez, Jean-Francois Raskin, Ocan Sankur & Leander Tentrup (2017):
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants and Results.
In: SYNT 2017,
EPTCS 260,
pp. 116–143,
doi:10.4204/EPTCS.260.10.
Barbara Jobstmann, Stefan Galler, Martin Weiglhofer & Roderick Bloem (2007):
Anzu: A Tool for Property Synthesis.
In: Werner Damm & Holger Hermanns: Computer Aided Verification.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 258–262,
doi:10.1007/978-3-540-73368-3_29.
Robert Könighofer, Georg Hofferek & Roderick Bloem (2011):
Debugging Unrealizable Specifications with Model-Based Diagnosis,
pp. 29–45.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
doi:10.1007/978-3-642-19583-9_8.
R. Könighofer, G. Hofferek & R. Bloem (2009):
Debugging formal specifications using simple counterstrategies.
In: 2009 Formal Methods in Computer-Aided Design,
pp. 152–159,
doi:10.1109/FMCAD.2009.5351127.
Wolfgang Lenders & Christel Baier (2005):
Genetic Algorithms for the Variable Ordering Problem of Binary Decision Diagrams.
In: Alden H. Wright, Michael D. Vose, Kenneth A. De Jong & Lothar M. Schmitt: Foundations of Genetic Algorithms.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 1–20,
doi:10.1007/11513575_1.
W. Li, L. Dworkin & S. A. Seshia (2011):
Mining assumptions for synthesis.
In: Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011),
pp. 43–50,
doi:10.1109/MEMCOD.2011.5970509.
Constantine Lignos, Vasumathi Raman, Cameron Finucane, Mitchell P. Marcus & Hadas Kress-Gazit (2015):
Provably correct reactive control from natural language.
Auton. Robots 38(1),
pp. 89–105,
doi:10.1007/s10514-014-9418-8.
P. Nilsson & N. Ozay (2014):
Incremental synthesis of switching protocols via abstraction refinement.
In: 53rd IEEE Conference on Decision and Control,
pp. 6246–6253,
doi:10.1109/CDC.2014.7040368.
Hans-Jörg Peter & Robert Mattmüller (2009):
Component-based Abstraction Refinement for Timed Controller Synthesis.
In: Theodore Baker: Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS 2009), December 1 - December 4, 2009, Washington, D.C., USA.
IEEE Computer Society,
Los Alamitos, CA, USA,
pp. 364–374,
doi:10.1109/RTSS.2009.14.
A. Pnueli & R. Rosner (1990):
Distributed Reactive Systems Are Hard to Synthesize.
In: Proceedings of the 31st Annual Symposium on Foundations of Computer Science,
SFCS '90.
IEEE Computer Society,
Washington, DC, USA,
pp. 746–757 vol.2,
doi:10.1109/FSCS.1990.89597.
V. Raman & H. Kress-Gazit (2013):
Explaining Impossible High-Level Robot Behaviors.
IEEE Transactions on Robotics 29(1),
pp. 94–104,
doi:10.1109/TRO.2012.2214558.
G. Reissig, A. Weber & M. Rungger (2017):
Feedback Refinement Relations for the Synthesis of Symbolic Controllers.
IEEE Transactions on Automatic Control 62(4),
pp. 1781–1796,
doi:10.1109/TAC.2016.2593947.
Kai Weng Wong, Rüdiger Ehlers & Hadas Kress-Gazit (2014):
Correct High-level Robot Behavior in Environments with Unexpected Events.
In: Robotics: Science and Systems X, University of California, Berkeley, USA, July 12-16, 2014,
doi:10.15607/RSS.2014.X.012.
Available at http://www.roboticsproceedings.org/rss10/p12.html.
Kai Weng Wong & H. Kress-Gazit (2015):
Let's talk: Autonomous conflict resolution for robots carrying out individual high-level tasks in a shared workspace.
In: 2015 IEEE International Conference on Robotics and Automation (ICRA),
pp. 339–345,
doi:10.1109/ICRA.2015.7139021.