Encodings of bounded synthesis
From MaRDI portal
Abstract: The reactive synthesis problem is to compute a system satisfying a given specification in temporal logic. Bounded synthesis is the approach to bound the maximum size of the system that we accept as a solution to the reactive synthesis problem. As a result, bounded synthesis is decidable whenever the corresponding verification problem is decidable, and can be applied in settings where classic synthesis fails, such as in the synthesis of distributed systems. In this paper, we study the constraint solving problem behind bounded synthesis. We consider different reductions of the bounded synthesis problem of linear-time temporal logic (LTL) to constraint systems given as boolean formulas (SAT), quantified boolean formulas (QBF), and dependency quantified boolean formulas (DQBF). The reductions represent different trade-offs between conciseness and algorithmic efficiency. In the SAT encoding, both inputs and states of the system are represented explicitly; in QBF, inputs are symbolic and states are explicit; in DQBF, both inputs and states are symbolic. We evaluate the encodings systematically using benchmarks from the reactive synthesis competition (SYNTCOMP) and state-of-the-art solvers. Our key, and perhaps surprising, empirical finding is that QBF clearly dominates both SAT and DQBF.
Recommendations
Cites work
- Blocked clause elimination for QBF
- Bounded Cycle Synthesis
- Bounded Synthesis
- Bounded synthesis for Petri games
- Incremental determinization
- Lazy synthesis
- LTL to Büchi automata translation: fast and more deterministic
- Reducing bounded realizability analysis to reachability checking
- SAT-Based Synthesis Methods for Safety Specs
- Solving QBF with counterexample guided refinement
- Solving Sequential Conditions by Finite-State Strategies
- Synthesis of Asynchronous Systems
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
- Towards efficient parameterized synthesis
- Unbeast: Symbolic Bounded Synthesis
Cited in
(29)- Distributed synthesis for parameterized temporal logics
- Computing unrestricted synopses under maximum error bound
- Building strategies into QBF proofs
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- Davis and Putnam meet Henkin: solving DQBF with resolution
- Certified DQBF solving by definition extraction
- Linear temporal logic -- from infinite to finite horizon
- Compositional synthesis of modular systems
- Bounded synthesis for Streett, Rabin, and \(\mathrm{CTL}^*\)
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Synthesis from hyperproperties
- Unbeast: Symbolic Bounded Synthesis
- Temporal synthesis for bounded systems and environments
- Efficient trace encodings of bounded synthesis for asynchronous distributed systems
- Solving QBF by abstraction
- Bounded Synthesis
- Symbolic bounded synthesis
- Bounded Cycle Synthesis
- CAQE and QuAbS: Abstraction Based QBF Solvers
- scientific article; zbMATH DE number 7455737 (Why is no real title available?)
- Building strategies into QBF proofs
- scientific article; zbMATH DE number 7278100 (Why is no real title available?)
- Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis
- Bounded synthesis of reactive programs
- Bounded synthesis of register transducers
- BOCoSy: Small but Powerful Symbolic Output-Feedback Control
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- On strings in software model checking
- Understanding the relative strength of QBF CDCL solvers and QBF resolution
This page was built for publication: Encodings of bounded synthesis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303904)
