POPACheck, A Model Checker for Probabilistic Pushdown Automata
POPACheck: A Model Checker for Probabilistic Pushdown Automata
Our paper, co-authored by Francesco Pontiggia, Ezio Bartocci and Michele Chiari, presents POPACheck, a tool that significantly improves the sate-of-the-art on the analysis of recursive probabilistic programs. POPACheck is the implementation of the results obtained in nearly two years of work on the theory of probabilistic pushdown automata, and constitutes the culmination of the CORPORA project.
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.
Read our pre-print on arXiv!