Quasy : Quantitative Synthesis Tool

Quasy is a tool for quantitative synthesis of reactive systems which takes qualitative and quantitative specifications in GOAL1 format and outputs a system (in GOAL format) 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 can be downloaded here.
1 Graphical Tool for Omega-Automata and Logics