Abstract: Most algorithms for the synthesis of reactive systems focus on the construction of finite-state machines rather than actual programs. This often leads to badly structured, unreadable code. In this paper, we present a bounded synthesis approach that automatically constructs, from a given specification in linear-time temporal logic (LTL), a program in Madhusudan's simple imperative language for reactive programs. We develop and compare two principal approaches for the reduction of the synthesis problem to a Boolean constraint satisfaction problem. The first reduction is based on a generalization of bounded synthesis to two-way alternating automata, the second reduction is based on a direct encoding of the program syntax in the constraint system. We report on preliminary experience with a prototype implementation, which indicates that the direct encoding outperforms the automata approach.
Recommendations
Cited in
(23)- Reducing bounded realizability analysis to reachability checking
- Incorporating monitors in reactive synthesis without paying the price
- Bounded synthesis for Streett, Rabin, and \(\mathrm{CTL}^*\)
- Type-directed bounding of collections in reactive programs
- Practical synthesis of reactive systems from LTL specifications via parity games
- Synthesizing structured reactive programs via deterministic tree automata
- Lazy synthesis
- Synthesizing reactive programs
- Higher-order functional reactive programming in bounded space
- Encodings of bounded synthesis
- Synthesizing structured reactive programs via deterministic tree automata
- Bounded Synthesis
- scientific article; zbMATH DE number 4085004 (Why is no real title available?)
- scientific article; zbMATH DE number 2000429 (Why is no real title available?)
- Completeness of Conversion between Reactive Programs for Ultrametric Models
- Verification and synthesis of reactive programs
- Synthesizing reactive systems from hyperproperties
- Synthesis of asynchronous reactive programs from temporal specifications
- Bounded synthesis of register transducers
- Synthesizing Computable Functions from Rational Specifications Over Infinite Words
- Taming large bounds in synthesis from bounded-liveness specifications
- Linear temporal constraints for sketch-based synthesizers
- Synthesizing bounded-time 2-phase fault recovery
This page was built for publication: Bounded synthesis of reactive programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6109601)
