# Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains (Extended Version)

arXiv: https://arxiv.org/abs/2608.00374 · HTML: https://mlsanity.com/paper/2608.00374/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 33 references that are in the map.
- First posted on arXiv 1 Aug 2026.

## Builds on (most cited first, 5 of 5)

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Parameter Synthesis for Markov Models: Covering the Parameter Space](https://mlsanity.com/paper/1903.07993/) (2019)
- [Parameter Synthesis in Markov Models: A Gentle Survey](https://mlsanity.com/paper/2207.06801/) (2022)
- [MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives](https://mlsanity.com/paper/2305.16796/) (2023)
- [Model Checking Finite-Horizon Markov Chains with Probabilistic Inference](https://mlsanity.com/paper/2105.12326/) (2021)

## Abstract (arXiv)

We reexamine the problem of verifying Markov chains with respect to step-bounded reachability probabilities. Prevailing approaches rely on encoding the state-transition matrix using either explicit or symbolic representations. While these approaches are effective for sparse transition dynamics, they scale less favorably in the dense regime. Our insight is to cast probabilistic model checking of Markov chains as computations over dense tensors. This methodology enables the use of off-the-shelf compiler toolchains for optimized execution of these tensor computations on hardware accelerators. We prove the soundness of the methodology of mapping probabilistic model checking to tensor computations. We implement our approach in a tool called Tessa . Empirical evaluation shows that Tessa unlocks massive speedups over state-of-theart methods on selected benchmarks from the literature.