DOI: 10.1145/3822593 ISSN: 1529-3785
Model Checking Probabilistic Operator Precedence Automata
Francesco Pontiggia, Ezio Bartocci, Michele Chiari 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
\(\chi\)
, 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
\(\chi\)
formulas. By the same property, the algorithms allow for model checking pOPA against Linear Temporal Logic (LTL) specifications. POTLf
\(\chi\)
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.