  We address the problem of model checking temporal logic specifications for
probabilistic programs with recursive procedures, nested queries, and
conditioning expressed with observe statements. We introduce probabilistic
Operator Precedence Automata (pOPA), a new class of probabilistic pushdown
automata suitable to model constructs and behaviors of probabilistic programs.
We develop a model checking algorithm that can verify requirements expressed in
a fragment of Precedence Oriented Temporal Logic (POTL$^f_\mathcal{X}$) on a
pOPA in single EXPTIME. POTL$^f_\mathcal{X}$ is a temporal logic based on
Operator Precedence Languages, which features modalities that interact with the
context-free structure of program traces, matching procedure calls with returns
or observe statements. We provide the first probabilistic model checking
implementation of context-free language properties for probabilistic pushdown
systems.
