Branching-time model-checking of probabilistic pushdown automata

作者：

Highlights：

• We study the model-checking problem for probabilistic pushdown automata (pPDA).

• Model-checking pPDA against PCTL formulae is undecidable.

• Model-checking pPDA against qualitative PCTL* formulae is decidable.

摘要

•We study the model-checking problem for probabilistic pushdown automata (pPDA).•Model-checking pPDA against PCTL formulae is undecidable.•Model-checking pPDA against qualitative PCTL* formulae is decidable.

论文关键词：Probabilistic systems,Pushdown automata,Branching-time logics,Model-checking

论文评审过程：Received 23 October 2011, Revised 11 June 2013, Accepted 11 July 2013, Available online 18 July 2013.

论文官网地址：https://doi.org/10.1016/j.jcss.2013.07.001