activity
20242026
most citedTools at the Frontiers of Quantitative Verification

2 citations · 4 across the 9 of their papers we have counts for

collaborators

10 papers

cs.LO2026★ 1 cited

Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families

Milan Češka, Sebastian Junges, Luko van der Maas +2

Computing optimal conditional reachability probabilities in Markov decision processes (MDPs) is tractable by a reduction to reachability probabilities. Yet, this reduction yields c…

cs.LO2026

Shields to Guarantee Probabilistic Safety in MDPs

Linus Heck, Filip Macák, Roman Andriushchenko +2

Shielding is a prominent model-based technique to ensure safety of autonomous agents. Classical shielding aims to ensure that nothing bad ever happens and comes with strong guarant…

cs.AI2026

Missingness-MDPs: Bridging the Theory of Missing Data and POMDPs

Joshua Wendland, Markel Zubia, Roman Andriushchenko +6

We introduce missingness-MDPs (miss-MDPs), a novel subclass of partially observable Markov decision processes (POMDPs) that incorporates the theory of missing data. A miss-MDP is a…

cs.AI2026★ 1 cited

Finite-State Controllers for (Hidden-Model) POMDPs using Deep Reinforcement Learning

David Hudák, Maris F. L. Galesloot, Martin Tappler +3

Solving partially observable Markov decision processes (POMDPs) requires computing policies under imperfect state information. Despite recent advances, the scalability of existing…

cs.LO2025

Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking

Linus Heck, Filip Macák, Milan Češka +1

The ability to compute reward-optimal policies for given and known finite Markov decision processes (MDPs) underpins a variety of applications across planning, controller synthesis…

cs.AI2025

Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs

Maris F. L. Galesloot, Roman Andriushchenko, Milan Češka +2

Partially observable Markov decision processes (POMDPs) model specific environments in sequential decision-making under uncertainty. Critically, optimal policies for POMDPs may not…

cs.LO2025

Decentralized Planning Using Probabilistic Hyperproperties

Francesco Pontiggia, Filip Macák, Roman Andriushchenko +2

Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected rewar…

cs.LO2025

Small Decision Trees for MDPs with Deductive Synthesis

Roman Andriushchenko, Milan Češka, Sebastian Junges +1

Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can effi…

cs.LO2024

Policies Grow on Trees: Model Checking Families of MDPs

Roman Andriushchenko, Milan Češka, Sebastian Junges +1

Markov decision processes (MDPs) provide a fundamental model for sequential decision making under process uncertainty. A classical synthesis task is to compute for a given MDP a wi…

cs.LO2024★ 2 cited

Tools at the Frontiers of Quantitative Verification

Roman Andriushchenko, Alexander Bork, Carlos E. Budde +20

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 suppo…