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, which has relevant applications in the verification of recursive probabili…