In two-player finite-state stochastic games of partial observation on graphs,
in every state of the graph, the players simultaneously choose an action, and
their joint actions determine a probability distribution over the successor
states. We consider reachability objectives where player 1 tries to ensure a
target state to be visited almost-surely or positively. On the basis of
information, the game can be one-sided with either (a)player 1 or (b)player 2
having partial observation, or two-sided with both players having partial
observation.

We consider Markov Decision Processes (MDPs) with mean-payoff parity and
energy parity objectives. In system design, the parity objective is used to
encode \omega-regular specifications, and the mean-payoff and energy objectives
can be used to model quantitative resource constraints. The energy condition
requires that the resource level never drops below 0, and the mean-payoff
condition requires that the limit-average value of the resource consumption is
within a threshold.

Simulation and bisimulation metrics for stochastic systems provide a
quantitative generalization of the classical simulation and bisimulation
relations. These metrics capture the similarity of states with respect to
quantitative specifications written in the quantitative {\mu}-calculus and
related probabilistic logics. We first show that the metrics provide a bound
for the difference in long-run average and discounted average behavior across
states, indicating that the metrics can be used both in system verification,
and in performance evaluation.

Gist is a tool that (a) solves the qualitative analysis problem of turn-based
probabilistic games with {\omega}-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.

Energy parity games are infinite two-player turn-based games played on
weighted graphs. The objective of the game combines a (qualitative) parity
condition with the (quantitative) requirement that the sum of the weights
(i.e., the level of energy in the game) must remain positive. Beside their own
interest in the design and synthesis of resource-constrained omega-regular
specifications, energy parity games provide one of the simplest model of games
with combined qualitative and quantitative objective.

Nondeterministic weighted automata are finite automata with numerical weights
on transitions. They define quantitative languages L that assign to each word w
a real number L(w). The value of an infinite word w is computed as the maximal
value of all runs over w, and the value of a run as the maximum, limsup,
liminf, limit average, or discounted sum of the transition weights. We
introduce probabilistic weighted automata, in which the transitions are chosen
in a randomized (rather than nondeterministic) fashion. Under almost-sure
semantics (resp.