This paper introduces k-d PCPs – the class of probabilistic counter programs with \(k \in \mathbb {N}\) counter variables inducing possibly infinite-state Markov chains. We show that the universal (positive) almost-sure termination problem is undecidable for k-d PCPs in general, yet decidable for 1-d PCPs. We present an efficient decision procedure for the latter leveraging the technique of Markov chain finitization. Moreover, we identify several classes of k-d PCPs that are reducible to 1-d PCPs – thus their termination properties can be inferred automatically. Experiments demonstrate that our decision procedure can certify (positive) almost-sure termination – without resorting to invariants or supermartingales – of non-trivial probabilistic programs beyond the scope of existing tools.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On the Almost-Sure Termination of Probabilistic Counter Programs

  • Sergei Novozhilov,
  • Mingqi Yang,
  • Mingshuai Chen,
  • Zhiyang Li,
  • Jianwei Yin

摘要

This paper introduces k-d PCPs – the class of probabilistic counter programs with \(k \in \mathbb {N}\) counter variables inducing possibly infinite-state Markov chains. We show that the universal (positive) almost-sure termination problem is undecidable for k-d PCPs in general, yet decidable for 1-d PCPs. We present an efficient decision procedure for the latter leveraging the technique of Markov chain finitization. Moreover, we identify several classes of k-d PCPs that are reducible to 1-d PCPs – thus their termination properties can be inferred automatically. Experiments demonstrate that our decision procedure can certify (positive) almost-sure termination – without resorting to invariants or supermartingales – of non-trivial probabilistic programs beyond the scope of existing tools.