-
Algorithms for Synthesizing Priorities in Component-based Systems
Authors:
Chih-Hong Cheng,
Saddek Bensalem,
Yu-Fang Chen,
Rongjie Yan,
Barbara Jobstmann,
Harald Ruess,
Christian Buckl,
Alois Knoll
Abstract:
We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority sy…
▽ More
We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis.
△ Less
Submitted 7 October, 2011; v1 submitted 6 July, 2011;
originally announced July 2011.
-
Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives
Authors:
Christian von Essen,
Barbara Jobstmann
Abstract:
We show how to automatically construct a system that satisfies a given logical specification and has an optimal average behavior with respect to a specification with ratio costs.
When synthesizing a system from a logical specification, it is often the case that several different systems satisfy the specification. In this case, it is usually not easy for the user to state formally which system s…
▽ More
We show how to automatically construct a system that satisfies a given logical specification and has an optimal average behavior with respect to a specification with ratio costs.
When synthesizing a system from a logical specification, it is often the case that several different systems satisfy the specification. In this case, it is usually not easy for the user to state formally which system she prefers. Prior work proposed to rank the correct systems by adding a quantitative aspect to the specification. A desired preference relation can be expressed with (i) a quantitative language, which is a function assigning a value to every possible behavior of a system, and (ii) an environment model defining the desired optimization criteria of the system, e.g., worst-case or average-case optimal.
In this paper, we show how to synthesize a system that is optimal for (i) a quantitative language given by an automaton with a ratio cost function, and (ii) an environment model given by a labeled Markov decision process. The objective of the system is to minimize the expected (ratio) costs. The solution is based on a reduction to Markov Decision Processes with ratio cost functions which do not require that the costs in the denominator are strictly positive. We find an optimal strategy for these using a fractional linear program.
△ Less
Submitted 20 February, 2011;
originally announced February 2011.
-
GIST: A Solver for Probabilistic Games
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Barbara Jobstmann,
Arjun Radhakrishna
Abstract:
Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based p…
▽ More
Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.
△ Less
Submitted 14 April, 2010;
originally announced April 2010.
-
Measuring and Synthesizing Systems in Probabilistic Environments
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Barbara Jobstmann,
Rohit Singh
Abstract:
Often one has a preference order among the different systems that satisfy a given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal-synthesis problem: given an ome…
▽ More
Often one has a preference order among the different systems that satisfy a given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal-synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the given input assumption, synthesize a system that optimizes the measured value.
For safety specifications and measures given by mean-payoff automata, the optimal-synthesis problem amounts to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be done in polynomial time. For general omega-regular specifications, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives.
Our algorithm generates optimal strategies consisting of two memoryless strategies and a counter. This counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter for any ε>0. We also show how to decide in polynomial time if we can construct an optimal finite-state system (i.e., a system without a counter) for a given specification.
We have implemented our approach in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present experimental results showing optimal systems that were generated in this way.
△ Less
Submitted 14 April, 2011; v1 submitted 5 April, 2010;
originally announced April 2010.
-
Better Quality in Synthesis through Quantitative Objectives
Authors:
Roderick Bloem,
Krishnendu Chatterjee,
Thomas A. Henzinger,
Barbara Jobstmann
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…
▽ More
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.
△ Less
Submitted 28 May, 2013; v1 submitted 17 April, 2009;
originally announced April 2009.
-
Environment Assumptions for Synthesis
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Barbara Jobstmann
Abstract:
The synthesis problem asks to construct a reactive finite-state system from an $ω$-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification $φ$…
▽ More
The synthesis problem asks to construct a reactive finite-state system from an $ω$-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification $φ$ by computing an environment assumption $ψ$ such that the new specification $ψ\toφ$ is realizable. Our aim is to construct an assumption $ψ$ that constrains only the environment and is as weak as possible. We present a two-step algorithm for computing assumptions. The algorithm operates on the game graph that is used to answer the realizability question. First, we compute a safety assumption that removes a minimal set of environment edges from the graph. Second, we compute a liveness assumption that puts fairness conditions on some of the remaining environment edges. We show that the problem of finding a minimal set of fair edges is computationally hard, and we use probabilistic games to compute a locally minimal fairness assumption.
△ Less
Submitted 27 May, 2008;
originally announced May 2008.
