Verification methods improve models with uncertain probabilities
Automata-Theoretic Verification of Interval Markov Decision Processes
Formal Languages and Automata Theory
Summary
Computer systems often have uncertain behaviors, especially when data about their actions is incomplete or noisy. The authors focus on a type of model called interval Markov decision processes, which capture these uncertainties by using ranges of probabilities instead of exact numbers. They show how existing tools used to check systems against rules and properties can be adapted to handle these intervals, depending on the nature of uncertainty. Their work enables more reliable checking of systems when probabilities are learned from limited data.
What this means in practice
- •For autonomous system developers: Verify safety and performance guarantees for systems whose behavior probabilities are unknown or learned from data using interval-based probabilistic models.
- •For control system engineers: Analyze uncertain stochastic controllers to ensure compliance with complex timing and sequencing requirements despite incomplete probability knowledge.
Authors
Sarvin Bahmani, Soumyajit Paul, Sven Schewe, Sadegh Soudjani, Ashutosh Trivedi
Abstract
Interval Markov decision processes (IMDPs) provide a natural framework for modeling stochastic systems with uncertain transition probabilities, represented by probability intervals and resolved adversarially. Such uncertainty arises naturally, for example, when the transition model is learned from finite data or obtained through model-based reinforcement learning. In this paper, we study the automata-theoretic verification of IMDPs against rich temporal specifications, including all LTL specifications, by considering the broader class of ω-regular objectives. We show that classical automata-theoretic verification techniques extend to IMDPs, but with a sharp distinction determined by the structure of the transition intervals. For stable IMDPs, where either the upper bound is zero or the lower bound is strictly positive, verification reduces to ordinary MDP analysis and can be carried out using the standard automata used in that setting (good-for-MDP automata). For unstable IMDPs, where intervals may include zero while the upper bound is strictly positive, verification becomes game-like and requires automata whose nondeterminism can be resolved on the fly (good-for-games automata). Building on these insights, we develop algorithms for verifying ω-regular specifications over IMDPs and derive probabilistic guarantees when the interval model is learned from sampled data. The resulting framework enables principled verification of stochastic systems under probabilistic model uncertainty, connecting automata-based verification with data-driven stochastic modeling.