POPACheck: A Model Checker for Probabilistic Pushdown Automata
Abstract
We present POPACheck, the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications. POPACheck provides a user-friendly probabilistic modeling language with recursion that automatically translates into Probabilistic Operator Precedence Automata (pOPA). pOPA are a class of pPDA that can express all the behaviors of probabilistic programs: sampling, conditioning, recursive procedures, and nested inference queries. On pOPA, POPACheck can solve reachability queries as well as qualitative and quantitative model checking queries for specifications in Linear Temporal Logic (LTL) and a fragment of Precedence Oriented Temporal Logic (POTL), a logic for context-free properties such as pre/post-conditioning.
Cite
@article{arxiv.2502.03956,
title = {POPACheck: A Model Checker for Probabilistic Pushdown Automata},
author = {Francesco Pontiggia and Ezio Bartocci and Michele Chiari},
journal= {arXiv preprint arXiv:2502.03956},
year = {2025}
}
Comments
16 pages, 10 Figures, 4 Tables. Accepted for publication in the Proceedings of the 37th International Conference on Computer Aided Verification (CAV'25)