QUASY: Quantitative synthesis tool 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.
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis: PRISM-games: a model checker for stochastic multi-player games (2013)
- Bulychev, Peter; Cassez, Franck; David, Alexandre; Larsen, Kim Guldstrand; Raskin, Jean-François; Reynier, Pierre-Alain: Controllers with minimal observation power (application to timed systems) (2012)
- Chatterjee, Krishnendu; Henzinger, Thomas A.; Jobstmann, Barbara; Singh, Rohit: QUASY: quantitative synthesis tool (2011)