@inproceedings{CHJ+11,
title = {QUASY: Quantitative Synthesis Tool },
author = {Chatterjee, Krishnendu and Henzinger, Thomas A. and Jobstmann, Barbara and Singh, Rohit},
year = {2011},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS },
pages = {267-271},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6605},
team = {DCS},
abstract = {We present the tool QUASY, a quantitative synthesis tool. QUASY 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. The user can choose between a system that satisfies and optimizes the specifications (a) under all possible environment behaviors or (b) under the most-likely environment behaviors given as a probability distribution on the possible input sequences. QUASY solves these two quantitative synthesis problems by reduction to instances of 2-player games and Markov Decision Processes (MDPs) with quantitative winning objectives. QUASY can also be seen as a game solver for quantitative games. Most notable, it can solve lexicographic mean-payoff games with 2 players, MDPs with mean-payoff objectives, and ergodic MDPs with mean- payoff parity objectives.},
}
