@inproceedings{4569,
  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.},
  author       = {Bloem, Roderick and Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara},
  location     = {Grenoble, France},
  pages        = {140 -- 156},
  publisher    = {Springer},
  title        = {{Better quality in synthesis through quantitative objectives}},
  doi          = {10.1007/978-3-642-02658-4_14},
  volume       = {5643},
  year         = {2009},
}

@misc{5392,
  abstract     = {We consider probabilistic automata on infinite words with acceptance defined by safety, reachability, Büchi, coBüchi and limit-average conditions. We consider quantitative and qualitative decision problems. We present extensions and adaptations of proofs of [GO09] and present a precise characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems.},
  author       = {Chatterjee, Krishnendu},
  issn         = {2664-1690},
  pages        = {17},
  publisher    = {IST Austria},
  title        = {{Probabilistic automata on infinite words: Decidability and undecidability results}},
  doi          = {10.15479/AT:IST-2009-0004},
  year         = {2009},
}

@misc{5393,
  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 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.},
  author       = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara and Radhakrishna, Arjun},
  issn         = {2664-1690},
  pages        = {12},
  publisher    = {IST Austria},
  title        = {{Gist: A solver for probabilistic games}},
  doi          = {10.15479/AT:IST-2009-0003},
  year         = {2009},
}

@misc{5394,
  abstract     = {We consider two-player games played on graphs with request-response and finitary Streett objectives. We show these games are PSPACE-hard, improving the previous known NP-hardness. We also improve the lower bounds on memory required by the winning strategies for the players.},
  author       = {Chatterjee, Krishnendu and Henzinger, Thomas A and Horn, Florian},
  issn         = {2664-1690},
  pages        = {11},
  publisher    = {IST Austria},
  title        = {{Improved lower bounds for request-response and finitary Streett games}},
  doi          = {10.15479/AT:IST-2009-0002},
  year         = {2009},
}

@misc{5395,
  abstract     = {We study observation-based strategies for partially-observable Markov decision processes (POMDPs) with omega-regular objectives. An observation-based strategy relies on partial information about the history of a play, namely, on the past sequence of observa- tions. We consider the qualitative analysis problem: given a POMDP with an omega-regular objective, whether there is an observation-based strategy to achieve the objective with probability 1 (almost-sure winning), or with positive probability (positive winning). Our main results are twofold. First, we present a complete picture of the computational complexity of the qualitative analysis of POMDPs with parity objectives (a canonical form to express omega-regular objectives) and its subclasses. Our contribution consists in establishing several upper and lower bounds that were not known in literature. Second, we present optimal bounds (matching upper and lower bounds) on the memory required by pure and randomized observation-based strategies for the qualitative analysis of POMDPs with parity objectives and its subclasses.},
  author       = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A},
  issn         = {2664-1690},
  pages        = {20},
  publisher    = {IST Austria},
  title        = {{Qualitative analysis of partially-observable Markov decision processes}},
  doi          = {10.15479/AT:IST-2009-0001},
  year         = {2009},
}

@inproceedings{3871,
  abstract     = {Nondeterministic weighted automata are finite automata with numerical weights oil transitions. They define quantitative languages 1, that assign to each word v; a real number L(w). The value of ail infinite word w is computed as the maximal value of all runs over w, and the value of a run as the supremum, limsup liminf, limit average, or discounted sum of the transition weights. We introduce probabilistic weighted antomata, in which the transitions are chosen in a randomized (rather than nondeterministic) fashion. Under almost-sure semantics (resp. positive semantics), the value of a word v) is the largest real v such that the runs over w have value at least v with probability I (resp. positive probability). We study the classical questions of automata theory for probabilistic weighted automata: emptiness and universality, expressiveness, and closure under various operations oil languages. For quantitative languages, emptiness university axe defined as whether the value of some (resp. every) word exceeds a given threshold. We prove some, of these questions to he decidable, and others undecidable. Regarding expressive power, we show that probabilities allow its to define a wide variety of new classes of quantitative languages except for discounted-sum automata, where probabilistic choice is no more expressive than nondeterminism. Finally we live ail almost complete picture of the closure of various classes of probabilistic weighted automata for the following, provide, is operations oil quantitative languages: maximum, sum. and numerical complement.},
  author       = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A},
  location     = {Bologna, Italy},
  pages        = {244 -- 258},
  publisher    = {Springer},
  title        = {{Probabilistic weighted automata}},
  doi          = {10.1007/978-3-642-04081-8_17},
  volume       = {5710},
  year         = {2009},
}

@article{3870,
  abstract     = {Games on graphs with omega-regular objectives provide a model for the control and synthesis of reactive systems. Every omega-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. While for one-shot liveness (reachability) objectives, classical and finitary liveness coincide, for repeated liveness (Buchi) objectives, the finitary formulation is strictly stronger. In this work we study games with finitary parity and Streett objectives. We prove the determinacy of these games, present algorithms for solving these games, and characterize the memory requirements of winning strategies. We show that finitary parity games can be solved in polynomial time, which is not known for infinitary parity games. For finitary Streett games, we give an EXPTIME algorithm and show that the problem is NP-hard. Our algorithms can be used, for example, for synthesizing controllers that do not let the response time of a system increase without bound.},
  author       = {Chatterjee, Krishnendu and Henzinger, Thomas A and Horn, Florian},
  journal      = {ACM Transactions on Computational Logic},
  number       = {1},
  publisher    = {ACM},
  title        = {{Finitary winning in omega-regular games}},
  doi          = {10.1145/1614431.1614432},
  volume       = {11},
  year         = {2009},
}