While computing reachability probabilities in an infinite Mar-kov chain is a challenging problem, computing an approximation up to an arbitrary precision is possible when the chain is decisive. Some high-level probabilistic formalisms lead to decisive Markov chain but for most of them, the generated chain can be decisive or not depending on the specification. This raises the problem of deciding decisiveness given a high-level probabilistic formalism. In a previous work, some of the authors of this paper have studied the decisiveness status of several formalisms. Here we improve their work in two ways. It was shown that the decisiveness problem was decidable for homogeneous probabilistic one-counter machine (an extension of the quasi-birth-death processes) when some underlying finite Markov chain is irreducible. We show the problem remains decidable without requiring irreducibility. On the other side, it was shown that the decisiveness problem was undecidable for probabilistic Petri nets with polynomial weights for transitions. We show that the problem remains undecidable even when the weights of the transitions are specified by affine functions of a single place marking.

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

Tightening the Frontier of Decidability for Decisiveness

  • Gaspard Fougea,
  • Serge Haddad,
  • Lina Ye,
  • Shreyas Jain,
  • Alain Finkel

摘要

While computing reachability probabilities in an infinite Mar-kov chain is a challenging problem, computing an approximation up to an arbitrary precision is possible when the chain is decisive. Some high-level probabilistic formalisms lead to decisive Markov chain but for most of them, the generated chain can be decisive or not depending on the specification. This raises the problem of deciding decisiveness given a high-level probabilistic formalism. In a previous work, some of the authors of this paper have studied the decisiveness status of several formalisms. Here we improve their work in two ways. It was shown that the decisiveness problem was decidable for homogeneous probabilistic one-counter machine (an extension of the quasi-birth-death processes) when some underlying finite Markov chain is irreducible. We show the problem remains decidable without requiring irreducibility. On the other side, it was shown that the decisiveness problem was undecidable for probabilistic Petri nets with polynomial weights for transitions. We show that the problem remains undecidable even when the weights of the transitions are specified by affine functions of a single place marking.