A controller is a device that interacts with a plant. At each time point, it reads the plant's state
and issues commands with the goal that the plant operates optimally. Constructing optimal …

We present Rabinizer 4, a tool set for translating formulae of linear temporal logic to different
types of deterministic ω-automata. The tool set implements and optimizes several recent …

Markov decision processes (MDPs) are standard models for probabilistic systems with non-
deterministic behaviours. Long-run average rewards provide a mathematically elegant …

We consider the verification of multiple expected reward objectives at once on Markov
decision processes (MDPs). This enables a trade-off analysis among multiple objectives by …

This paper targets control problems that exhibit specific safety and performance
requirements. In particular, the aim is to ensure that an agent, operating under uncertainty …

We study turn-based stochastic zero-sum games with lexicographic preferences over
objectives. Stochastic games are standard models in control, verification, and synthesis of …

The analysis of formal models that include quantitative aspects such as timing or
probabilistic choices is performed by quantitative verification tools. Broad and mature tool …

We treat the problem of risk-aware control for stochastic shortest path (SSP) on Markov
decision processes (MDP). Typically, expectation is considered for SSP, which however is …

Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze
systems with multiple objectives that may be conflicting and require the analysis of trade …

We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-
making in presence of an antagonistic opponent in a random environment. In this setting, an …