arXiv subjects

Roman Andriushchenko

Publications and source records attributed to Roman Andriushchenko.

12 recordsLinked to original sources

arXiv2026

UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)

This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic systems. UMB addresses the problem that, while probabilistic model checking tools often support common high-level modelling languages, there is no effective mechanism for exchanging low-level model representations. In practice, textual, tool-specific formats are used, hampering interoperability and resulting in large overheads in writing and reading model files. UMB provides a clean, unified, and efficient solution, based on a general underlying mathematical model, and encoded using a small set of bit-level primitive data structures. The format has already been adopted by prominent tools and comes with a convenient Python library for reading, manipulating, creating, and validating models, plus infrastructure for cross-tool installation and continuous validation. We report on both the efficiency of the file format and the new practical use cases that it facilitates.

cs.LO↗

arXiv2026

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

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 POMDP whose observation function is a missingness function, specifying the probability that individual state features are missing (i.e., unobserved) at a time step. The literature distinguishes three canonical missingness types: missing (1) completely at random (MCAR), (2) at random (MAR), and (3) not at random (MNAR). Our planning problem is to compute near-optimal policies for a miss-MDP with an unknown missingness function, given a dataset of action-observation trajectories. Achieving such optimality guarantees for policies requires learning the missingness function from data, which is infeasible for general POMDPs. To overcome this challenge, we exploit the structural properties of different missingness types to derive probably approximately correct (PAC) algorithms for learning the missingness function. These algorithms yield an approximate but fully specified miss-MDP that we solve using off-the-shelf planning methods. We prove that, with high probability, the resulting policies are epsilon-optimal in the true miss-MDP. Empirical results confirm the theory and demonstrate superior performance of our approach over two model-free POMDP methods.

cs.AI↗

arXiv2026

Shields to Guarantee Probabilistic Safety in MDPs

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 guarantees about safety and maximal permissiveness. However, shielding systems for probabilistic safety, where something bad is allowed to happen with an acceptable probability, has proven to be more intricate. This paper presents a formal framework that conservatively extends classical shields to probabilistic safety. In this framework, we (i) demonstrate the impossibility of preserving the strong guarantees on safety and permissiveness, (ii) provide natural shields with weaker guarantees, and (iii) introduce offline and online shield constructions ensuring strong safety guarantees. The empirical evaluation highlights the practical advantages of the new shields, as well as their computational feasibility.

cs.LO↗

arXiv2025

Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs

Partially observable Markov decision processes (POMDPs) model specific environments in sequential decision-making under uncertainty. Critically, optimal policies for POMDPs may not be robust against perturbations in the environment. Hidden-model POMDPs (HM-POMDPs) capture sets of different environment models, that is, POMDPs with a shared action and observation space. The intuition is that the true model is hidden among a set of potential models, and it is unknown which model will be the environment at execution time. A policy is robust for a given HM-POMDP if it achieves sufficient performance for each of its POMDPs. We compute such robust policies by combining two orthogonal techniques: (1) a deductive formal verification technique that supports tractable robust policy evaluation by computing a worst-case POMDP within the HM-POMDP, and (2) subgradient ascent to optimize the candidate policy for a worst-case POMDP. The empirical evaluation shows that, compared to various baselines, our approach (1) produces policies that are more robust and generalize better to unseen POMDPs, and (2) scales to HM-POMDPs that consist of over a hundred thousand environments.

cs.AI↗

arXiv2025

Decentralized Planning Using Probabilistic Hyperproperties

Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set of decentralized agents operating in the environment. We extend existing approaches for model checking probabilistic hyperproperties to handle temporal formulae relating paths of different agents, thus requiring the self-composition between multiple MDPs. Using several case studies, we demonstrate that our approach provides a flexible and expressive framework to broaden the specification capabilities with respect to existing planning techniques. Additionally, we establish a close connection between a subclass of probabilistic hyperproperties and planning for a particular type of Dec-MDPs, for both of which we show undecidability. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.

cs.LO↗

arXiv2025

Small Decision Trees for MDPs with Deductive Synthesis

Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can efficiently compute policies that are optimal with respect to, e.g., reachability probabilities. However, these policies are then given in a tabular format. A longstanding challenge is to represent optimal or almost-optimal policies concisely, e.g., as decision trees. This paper makes two contributions towards this challenge: first, an SMT-based approach to encode a given (optimal) policy as a small decision tree, and second, an abstraction-refinement loop that searches for policies that are optimal within the set of policies that can be represented with a small tree. Technically, the latter combines the SMT encoding with verification approaches for families of Markov chains. The empirical evaluation demonstrates the feasibility of these approaches and shows how they can outperform the state-of-the-art on various benchmarks, yielding up to 20 times smaller trees representing (almost) optimal policies for models with up to 10k states and 19 variables.

cs.LO↗

arXiv2024

Policies Grow on Trees: Model Checking Families of MDPs

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 winning policy that achieves a desired specification. However, at design time, one typically needs to consider a family of MDPs modelling various system variations. For a given family, we study synthesising (1) the subset of MDPs where a winning policy exists and (2) a preferably small number of winning policies that together cover this subset. We introduce policy trees that concisely capture the synthesis result. The key ingredient for synthesising policy trees is a recursive application of a game-based abstraction. We combine this abstraction with an efficient refinement procedure and a post-processing step. An extensive empirical evaluation demonstrates superior scalability of our approach compared to naive baselines. For one of the benchmarks, we find 246 winning policies covering 94 million MDPs. Our algorithm requires less than 30 minutes, whereas the naive baseline only covers 3.7% of MDPs in 24 hours.

cs.LO↗

arXiv2024

Tools at the Frontiers of Quantitative Verification

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 support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

cs.LO↗

arXiv2023

Deductive Controller Synthesis for Probabilistic Hyperproperties

Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. Our specification language builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach considerably outperforms HyperProb, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g. partial observability) as well as inter-controller constraints (e.g. agreements on a common action).

cs.LO↗

arXiv2023

Search and Explore: Symbiotic Policy Synthesis in POMDPs

This paper marries two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making under uncertainty. A central issue is to find a POMDP controller - that solely decides based on the observations seen so far - to achieve a total expected reward objective. As finding optimal controllers is undecidable, we concentrate on synthesising good finite-state controllers (FSCs). We do so by tightly integrating two modern, orthogonal methods for POMDP controller synthesis: a belief-based and an inductive approach. The former method obtains an FSC from a finite fragment of the so-called belief MDP, an MDP that keeps track of the probabilities of equally observable POMDP states. The latter is an inductive search technique over a set of FSCs, e.g., controllers with a fixed memory size. The key result of this paper is a symbiotic anytime algorithm that tightly integrates both approaches such that each profits from the controllers constructed by the other. Experimental results indicate a substantial improvement in the value of the controllers while significantly reducing the synthesis time and memory footprint.

cs.LO↗

arXiv2022

Inductive Synthesis of Finite-State Controllers for POMDPs

We present a novel learning framework to obtain finite-state controllers (FSCs) for partially observable Markov decision processes and illustrate its applicability for indefinite-horizon specifications. Our framework builds on oracle-guided inductive synthesis to explore a design space compactly representing available FSCs. The inductive synthesis approach consists of two stages: The outer stage determines the design space, i.e., the set of FSC candidates, while the inner stage efficiently explores the design space. This framework is easily generalisable and shows promising results when compared to existing approaches. Experiments indicate that our technique is (i) competitive to state-of-the-art belief-based approaches for indefinite-horizon properties, (ii) yields smaller FSCs than existing methods for several models, and (iii) naturally treats multi-objective specifications.

cs.LO↗

arXiv2021

Inductive Synthesis for Probabilistic Programs Reaches New Horizons

This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a PCTL specification. The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the family. These CEs leverage the semantics of the family in the form of bounds on its best- and worst-case behaviour provided by a deductive oracle using an MDP abstraction. The method further monitors the performance of the synthesis and adaptively switches between the inductive and deductive reasoning. Our experiments demonstrate that the novel CE construction provides a significantly faster and more effective pruning strategy leading to acceleration of the synthesis process on a wide range of benchmarks. For challenging problems, such as the synthesis of decentralized partially-observable controllers, we reduce the run-time from a day to minutes.

cs.LO↗