Please note: This PhD seminar will take place in DC 2314 and online.
Jianlin Li, PhD candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Yizhou Zhang
We reexamine the problem of verifying Markov chains with respect to step-bounded reachability probabilities. Prevailing approaches to this problem rely on encoding the state-transition matrix using either explicit or symbolic representations. While more recent work frames the verification problem as probabilistic inference, this approach does not appear to improve scalability across the board.
Our insight is to cast probabilistic model checking of Markov chains as computations over 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 easily unlocks massive speedups over state-of-the-art methods on benchmarks from the literature.
To attend this PhD seminar in person, please go to DC 2314. You can also attend virtually on Zoom.