Better Quality in Synthesis through Quantitative Objectives
From MaRDI portal
Abstract: Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another. For example, if a specification asks that every request is followed by a response, one may prefer an implementation that generates responses quickly but does not generate unnecessary responses. We use quantitative properties to measure the "goodness" of an implementation. Using games with corresponding quantitative objectives, we can synthesize "optimal" implementations, which are preferred among the set of possible implementations that satisfy a given specification. In particular, we show how automata with lexicographic mean-payoff conditions can be used to express many interesting quantitative properties for reactive systems. In this framework, the synthesis of optimal implementations requires the solution of lexicographic mean-payoff games (for safety requirements), and the solution of games with both lexicographic mean-payoff and parity objectives (for liveness requirements). We present algorithms for solving both kinds of novel graph games.
Recommendations
Cited in
(71)- Safraless LTL synthesis considering maximal realizability
- Latticed-LTL synthesis in the presence of noisy inputs
- On equilibria in quantitative games with reachability/safety objectives
- Energy parity games
- Quantitative reductions and vertex-ranked infinite games
- On satisficing in quantitative games
- On composition of bounded-recall plans
- Vacuity in synthesis
- Quantitative assume guarantee synthesis
- Equilibria in multi-player multi-outcome infinite sequential games
- Synthesizing robust systems
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Synthesizing optimally resilient controllers
- Qualitative analysis of concurrent mean-payoff games
- Hyperplane separation technique for multidimensional mean-payoff games
- Average-energy games
- Parameterized linear temporal logics meet costs: still not costlier than LTL
- A note on the approximation of mean-payoff games
- Quantitative vs. weighted automata
- Synthesizing efficient controllers
- Temporal specifications with accumulative values
- Synthesizing non-vacuous systems
- Bounding Average-Energy Games
- QUASY: quantitative synthesis tool
- Synthesizing efficient systems in probabilistic environments
- Synthesis with rational environments
- Graph Games and Reactive Synthesis
- Symbolic model checking in non-Boolean domains
- On synthesis of specifications with arithmetic
- Quantitative reductions and vertex-ranked infinite games
- Multiplayer cost games with simple Nash equilibria
- Ranking Automata and Games for Prioritized Requirements
- Symbolic synthesis of finite-state controllers for request-response specifications
- Quantitative simulation games
- Synthesis of Reactive(1) designs
- Minimizing expected cost under hard Boolean constraints, with applications to quantitative synthesis
- Down the Borel hierarchy: solving Muller games via safety games
- Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies
- Parameterized complexity of games with monotonically ordered \(\omega\)-regular objectives
- Average-energy games
- Parameterized linear temporal logics meet costs: still not costlier than LTL
- Optimal strategies in weighted limit games
- Quantifying Bounds in Strategy Logic
- Synthesizing Optimally Resilient Controllers
- Optimally Resilient Strategies in Pushdown Safety Games
- Synthesis for multi-weighted games with branching-time winning conditions
- Faster algorithms for mean-payoff parity games
- Solving mean-payoff games via quasi dominions
- The cost of exactness in quantitative reachability
- Quantitative fair simulation games
- Synthesis from LTL specifications with mean-payoff objectives
- Symbolic approximate time-optimal control
- Measuring and synthesizing systems in probabilistic environments
- On high-quality synthesis
- A weakness measure for GR(1) formulae
- A weakness measure for GR(1) formulae
- Quantitative safety and liveness
- Satisfiability of quantitative probabilistic CTL: rise to the challenge
- Solving mean-payoff games via quasi dominions
- Quantitative program sketching using lifted static analysis
- Synthesis of compact strategies for coordination programs
- LTL reactive synthesis with a few hints
- Stochastic games with lexicographic objectives
- Fair quantitative games
- LTL reactive synthesis with a few hints
- Fast algorithms for energy games in special cases
- Safety and liveness of quantitative automata
- Limit your consumption! Finding bounds in average-energy games
- Multi-objective -regular reinforcement learning
- Simulation distances
- Equilibria for games with combined qualitative and quantitative objectives
This page was built for publication: Better Quality in Synthesis through Quantitative Objectives
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3636858)
