Source-linked AI summary
Better Quality in Synthesis through Quantitative Objectives
Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann
TL;DR
The paper addresses the inability of qualitative specifications to distinguish among multiple satisfying implementations. It adds quantitative objectives and uses lexicographic mean-payoff game algorithms to synthesize preferred implementations, with separate treatments for safety and liveness requirements.
Problem
Boolean specifications treat all satisfying implementations alike, although synthesis may need to prefer implementations with better measurable behavior.
Method
The paper adds lexicographic mean-payoff objectives to qualitative specifications and reduces synthesis to lexicographic mean-payoff games or parity games with such objectives.
Results
The paper presents algorithms for both game classes, with optimal solutions for safety and ε-optimal finite-state implementations for liveness when exact optimal strategies require infinite memory.
Takeaways & Limitations
Quantitative objectives provide a way to synthesize implementations preferred by long-run behavioral criteria while preserving qualitative correctness.
Takeaways & Limitations
The framework evaluates an implementation by the worst reward among all runs it may produce, rather than an average-case value under an input distribution.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper extends Boolean specifications with quantitative preferences so synthesis can choose implementations that satisfy qualitative requirements while optimizing measurable behavior. It develops lexicographic mean-payoff objectives and corresponding game-solving algorithms for safety and liveness synthesis.
- Motivation: Quantitative objectives impose a preference order over implementations that satisfy the qualitative specification, enabling synthesis of optimal or near-optimal implementations.The approach addresses the limitation that Boolean specifications accept all satisfying implementations equally.
- Motivation: The arbiter example penalizes unnecessary grants, where a grant is unnecessary when no request remains outstanding.The paper argues this quantitative formulation preserves the abstraction of a clean specification better than adding ad hoc Boolean requirements.
- Quantitative objectives: Lexicographic mean-payoff automata combine long-run costs for unnecessary grants and request-to-grant delays, supporting both objectives and their combinations.Each transition carries a cost tuple, and each component is evaluated by its long-run average.
- Synthesis and games: Safety synthesis reduces to lexicographic mean-payoff games with optimal solutions, whereas liveness synthesis uses lexicographic mean-payoff parity games.The paper presents algorithms for solving both novel graph-game classes.
- Synthesis and games: Lexicographic mean-payoff games are memorylessly determined and decidable in NP ∩coNP, while optimal parity-game strategies may require infinite memory.Finite-state strategies can nevertheless achieve values within any specified ε of optimal, yielding ε-optimal implementations; optimal synthesis is in NP.
- Related work: Existing quantitative formalisms generally do not focus on using quantitative specifications to obtain better implementations for synthesis.The paper distinguishes its goal from metrics that compare systems across all temporal properties expressible in a logic.
2 Examples
The examples show how quantitative specifications distinguish implementations that all satisfy the same qualitative requirements. Mean-payoff and lexicographic objectives express preferences about unnecessary grants, response speed, and client priority, while liveness objectives can create finite optima or unattained limits.
- Formal setup: A Mealy machine is deterministic and input-enabled, producing a unique output and successor state for every input.Its language contains the resulting infinite input/output words.
- Formal setup: Quantitative languages assign values to infinite words, and a machine’s value is the infimum over the values of its possible words.Lexicographic mean-payoff automata assign average edge-reward vectors to words.
- One-client arbiter: For G(r →g ∨X g), three implementations satisfy the qualitative specification but differ in whether they always grant, respond directly, or delay when possible.The examples motivate selecting among qualitatively correct implementations using quantitative preferences.
- One-client arbiter: A1 rewards fewer grants overall, whereas A2 withholds reward only for unnecessary grants, producing different values and implementation preferences.For w1 and w2, A1 assigns 1/2 and 1/3, while A2 assigns 1 and 2/3; A1 prefers M3, whereas A2 prefers M2 and M3 over M1.
- Two-client arbiter: A3 rewards short request-to-grant distances, while A4 combines client payoffs lexicographically so Client 1 receives priority over Client 2.The example compares values ⟨1, 1/2⟩ and ⟨1/2, 1⟩ for words prioritizing Client 1 and Client 2, respectively.
3 Lexicographic Mean-Payoff (Parity) Games
This section develops lexicographic mean-payoff games for quantitative objectives and extends them with parity conditions for liveness. It establishes determinacy, strategy-memory, complexity, and algorithmic results for both game classes.
- Overview: Lexicographic mean-payoff games support synthesis for safety requirements, while lexicographic mean-payoff parity games additionally enforce liveness through parity objectives.The paper presents solution methods for both game types and uses them for quantitative synthesis.
- Notation and known results: Game graphs partition states between two players, whose strategies generate infinite plays from the initial state.Labels and initial states later connect games to specifications and Mealy machines; memoryless strategies depend only on the current state.
- Notation and known results: Strategies are memoryless when they depend only on the current game location; strategies requiring finite-state history are finite-memory, and all others require infinite memory.The strategy selects moves using the current location and, for finite-memory strategies, the state of a finite-state machine tracking play history.
- Lexicographic mean-Payoff Games: Lexicographic mean-payoff values can be solved through finite-cycle forming games, whose memoryless optimal strategies remain optimal for the original game.The cycle payoff prioritizes the first reward component and uses the second when the first equals the relevant value class.
- Lexicographic mean-Payoff Games: Lexicographic mean-payoff games are determined, admit memoryless optimal strategies for both players, and have value decision in NP ∩coNP.The value vector for all states can be computed in time O(|S|2d+3 · |E| · |r|).
- Lexicographic Mean-Payoff Parity Games: Lexicographic mean-payoff parity games are determined and have memoryless optimal strategies for Player 2, but Player 1’s optimal strategies may require infinite memory.Their value decision problem is in NP ∩coNP, and the value for all states can be computed algorithmically.
- Lexicographic Mean-Payoff Parity Games: For every ε > 0, Player 1 has a constructible finite-memory ε-optimal strategy, and any finite-memory optimal strategy can be replaced by a memoryless optimal strategy.The finite-memory ε-optimal strategy is constructed using the recursive solution procedure.
4 Quantitative Verification and Synthesis
Quantitative verification evaluates whether implementations achieve specified values, while synthesis constructs optimal or approximately optimal Mealy machines from lexicographic mean-payoff automata. Safety specifications yield lexicographic mean-payoff games; liveness specifications additionally require parity objectives.
- Quantitative Specifications: Lexicographic mean-payoff automata can combine quantitative objectives with safety or liveness requirements.A product with a parity automaton assigns −1 to rejected runs and otherwise preserves the quantitative mean payoff.
- Quantitative Verification: Quantitative verification determines an implementation’s value and whether it reaches a given cutoff independently of inputs.The value can be computed in time O(|S| · |Q| · |E| · |δ| · d · lg(|Q| · |δ| · |r|)).
- Quantitative Verification: Specification A2 prefers implementations that avoid unnecessary grants, while combining quantitative languages by addition can prefer lazy over eager implementations.A2 prefers M2 and M3 to M1; addition resolves the preference between M2’s eagerness and M3’s laziness in favor of lazy implementations.
- Quantitative Synthesis: Synthesis automatically constructs implementations by translating automata into games and strategies into Mealy machines.The game separates input moves controlled by Player 2 from output moves controlled by Player 1, and the resulting machine follows the chosen strategy.
- Quantitative Synthesis: An optimal Mealy machine for a lexicographic mean-payoff automaton is constructible in time O(|E|4d+6 · |r|), with realizability and cutoff-realizability decidable in NP ∩ coNP.These results rely on memoryless optimal strategies for lexicographic mean-payoff games.
- Quantitative Synthesis: For lexicographic mean-payoff parity automata, limit-realizability may not imply realizability, and finite-memory ε-optimal machines are constructible.Realizability is decidable in NP, limit-c-realizability in coNP, and an ε-optimal machine has the stated polynomial construction bound.
5 Conclusions and Future Work
The paper measures implementation goodness by adding lexicographically combined mean-payoff objectives to qualitative specifications. It adopts a worst-case valuation, while noting average-case valuation as an alternative.
- Conclusions and Future Work: The paper measures implementation goodness by adding lexicographically combined mean-payoff objectives to qualitative specifications.Mean-payoff objectives are described as sufficiently expressive for the paper’s purposes, though discounted objectives are another possible choice.
- Conclusions and Future Work: The quantitative value of an implementation is evaluated using the worst reward among all runs it may produce.The paper identifies expected cost under an input distribution as an alternative average-case perspective.