POPACheck: A Model Checker for Probabilistic Pushdown Automata

TL;DR

POPACheck is a novel model checking tool designed for probabilistic Pushdown Automata, supporting temporal logic specifications and enabling analysis of recursive probabilistic programs.

Contribution

It introduces a user-friendly modeling language and translates models into Probabilistic Operator Precedence Automata, allowing comprehensive probabilistic and temporal property verification.

Findings

Supports reachability and model checking for LTL and POTL

Handles recursive procedures and nested inference queries

First tool for probabilistic pushdown automata with temporal logic

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.