Model Checking Probabilistic Operator Precedence Automata

Abstract

We address the problem of model checking context-free specifications for probabilistic pushdown automata, with applications in the verification of recursive probabilistic programs. Operator Precedence Languages (OPLs) are an expressive subclass of context-free languages suitable for model checking recursive programs. The derived Precedence Oriented Temporal Logic (POTL) can express fundamental OPL specifications such as pre/post-conditions and exception safety. We introduce probabilistic Operator Precedence Automata (pOPA), a class of probabilistic pushdown automata whose traces are OPLs, and study their model checking problem against POTL specifications. We identify a fragment of POTL, called POTLf, for which we develop an exptime algorithm for qualitative probabilistic model checking, and an expspace algorithm for the quantitative variant. The algorithms rely on the property of separation of automata generated from POTLf formulas. By the same property, the algorithms allow for model checking pOPA against Linear Temporal Logic (LTL) specifications. POTLf is then the first context-free logic for which an optimal probabilistic model checking algorithm has been developed, matching its exptime lower bound in complexity. In comparison, the best known algorithm for probabilistic model checking of CaRet, a prominent temporal logic based on Visibly Pushdown Languages (VPL), is doubly exponential.