POPACheck: A Model Checker for Probabilistic Pushdown Automata
arXiv:2502.03956 · doi:10.1007/978-3-031-98679-6_5
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.
16 pages, 10 Figures, 4 Tables. Accepted for publication in the Proceedings of the 37th International Conference on Computer Aided Verification (CAV'25)