Probabilistic Model Checking of Recursive Programs with Conditioning

This paper introduces a new class of probabilistic pushdown automata, called Probabilistic Operator Precedence Automata (pOPA), that can model recursive probabilistic programs with conditioning. It develops a model checking algorithm for verifying temporal logic specifications expressed in a fragment of Precedence Oriented Temporal Logic (POTLf X) on pOPA in single exponential time.