Model Checking Probabilistic Operator Precedence Automata

TL;DR

The paper advances model checking for probabilistic recursive programs by introducing pOPAs, whose traces are processed via OPAs and OPL-based logics. It develops a separation-based framework using separated omegaOPBA and a support chain to perform qualitative and quantitative model checking against POTLF and LTL specifications, achieving EXPTIME and EXPSPACE complexity, respectively, and proves these bounds are optimal. A key novelty is encoding POTLF via separated OPBA to preserve tractable model checking without full determinization, and applying the approach to a motivating coordination game to illustrate nested queries and conditioning. The work substantially enhances verification capabilities for recursive probabilistic programs and lays groundwork for extending to full POTL and related automata-based techniques, with practical implications for correctness guarantees in probabilistic programming. The methods promise more expressive verification than existing VPL-based approaches, enabling analysis of exception handling, observations, and recursive calls in probabilistic settings.

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$χ$, 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. The same property allows us to employ these algorithms 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.

Figures (8)

• Figure 1: A coordination game adapted from StuhlmullerG14.
• Figure 2: Overview of model checking of probabilistic programs against POTLF.
• Figure 3: OPM $M_\mathbf{call}$, omitting $\#$.
• Figure 4: Top left: OPBA $\mathcal{B}_\mathbf{call}$. Top right: support graph of $\mathcal{B}_\mathbf{call}$. Call edges are solid, shift edges dashed, and pop edges double. In the support graph, support edges are wavy, there are no shift edges, and some edges are both push and support. Bottom: prefix of a run of $\mathcal{B}_\mathbf{call}$ showing, from the top, the input word, the stack growing upwards, the current state, and the PR between the topmost stack symbol and the look-ahead.
• Figure 5: Left: pOPA $\mathcal{A}_\mathbf{call}$. Push, shift and pop moves are depicted resp. as solid, dashed and double arrows, labeled with their probability and, just for pop moves, with the state they pop. Unreachable transitions are omitted (e.g., push edges from $u_2$). Right: prefix of a run of $\mathcal{A}_\mathbf{call}$ showing, from the top, its labeling through $\Lambda_\varepsilon$, the stack growing upwards, the current state, and the PR between the topmost stack symbol and the current state label.

Theorems & Definitions (39)

• definition 1: MP18
• definition 2: LonatiEtAl2015
• definition 3: LonatiEtAl2015
• definition 4: LonatiEtAl2015
• definition 5: ChiariMPP23
• definition 6
• definition 7: ChiariMP21b
• definition 8
• proposition 1
• definition 9