@inproceedings{19743,
  abstract     = {The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.},
  author       = {Chatterjee, Krishnendu and Quatmann, Tim and Schäffeler, Maximilian and Weininger, Maximilian and Winkler, Tobias and Zilken, Daniel},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906527},
  issn         = {1611-3349},
  location     = {Hamilton, ON, Canada},
  pages        = {130--151},
  publisher    = {Springer Nature},
  title        = {{Fixed point certificates for reachability and expected rewards in MDPs}},
  doi          = {10.1007/978-3-031-90653-4_7},
  volume       = {15697},
  year         = {2025},
}

@inproceedings{19740,
  abstract     = {Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.},
  author       = {Chatterjee, Krishnendu and Jafariraviz, Mahdi and Saona Urmeneta, Raimundo J and Svoboda, Jakub},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906527},
  issn         = {1611-3349},
  location     = {Hamilton, ON, Canada},
  pages        = {217--236},
  publisher    = {Springer Nature},
  title        = {{Value iteration with guessing for Markov chains and Markov decision processes}},
  doi          = {10.1007/978-3-031-90653-4_11},
  volume       = {15697},
  year         = {2025},
}

@inproceedings{19744,
  abstract     = {We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.},
  author       = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Novotný, Petr and Zikelic, Dorde},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906527},
  issn         = {1611-3349},
  location     = {Hamilton, ON, Canada},
  pages        = {279--300},
  publisher    = {Springer Nature},
  title        = {{Refuting equivalence in probabilistic programs with conditioning}},
  doi          = {10.1007/978-3-031-90653-4_14},
  volume       = {15697},
  year         = {2025},
}