Model Checking Probabilistic Operator Precedence Automata

TL;DR

This paper introduces probabilistic Operator Precedence Automata (pOPA) and develops efficient algorithms for probabilistic model checking against a new logic, POTLfχ, advancing the verification of recursive probabilistic programs.

Contribution

It presents pOPA models and an EXPTIME algorithm for qualitative probabilistic model checking of a new context-free logic, matching its lower bound and improving over existing methods.

Findings

Developed pOPA class for probabilistic recursive programs

Created EXPTIME algorithm for qualitative model checking of POTLfχ

Achieved optimal complexity matching the lower bound for the logic

Abstract

We address the problem of model checking context-free specifications for probabilistic pushdown automata, which has relevant 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. The same property allows us to employ these algorithms 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.