Encodings of Bounded Synthesis

DOI10.1007/978-3-662-54577-5_20zbMath1452.68118arXiv1803.09570OpenAlexW2600686309MaRDI QIDQ3303904

Peter Faymonville, Bernd Finkbeiner, Leander Tentrup, Markus N. Rabe

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1803.09570

zbMATH Keywords

Boolean functiontransition systemsynthesis problemconstraint systematomic proposition

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Linear temporal logic -- from infinite to finite horizon, Compositional synthesis of modular systems, Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis, BOCoSy: Small but Powerful Symbolic Output-Feedback Control, Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution, Unnamed Item, Unnamed Item, Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems, Unnamed Item, Distributed synthesis for parameterized temporal logics, Building strategies into QBF proofs, Reactive synthesis with maximum realizability of linear temporal logic specifications, Synthesis from hyperproperties, Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations, Unnamed Item, CAQE and QuAbS: Abstraction Based QBF Solvers, Davis and Putnam meet Henkin: solving DQBF with resolution, Certified DQBF solving by definition extraction

Uses Software

• Bloqqer
• ABC
• Acacia+
• CAQE
• Unbeast
• RAReQS

Cites Work

• Solving QBF with counterexample guided refinement
• Reducing bounded realizability analysis to reachability checking
• Incremental Determinization
• Lazy Synthesis
• LTL to Büchi Automata Translation: Fast and More Deterministic
• Towards Efficient Parameterized Synthesis
• SAT-Based Synthesis Methods for Safety Specs
• Unbeast: Symbolic Bounded Synthesis
• Bounded Synthesis for Petri Games
• Bounded Synthesis
• Synthesis of Asynchronous Systems
• Bounded Cycle Synthesis
• Blocked Clause Elimination for QBF
• To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
• Solving Sequential Conditions by Finite-State Strategies