Logic in Computer Science (LICS 2005)

Paper: Verifying Infinite Markov Chains with a Finite Attractor or the Global Coarseness Property (at LICS 2005)

Authors: Richard Mayr Parosh Abdulla Noomene Ben Henda

Abstract

We consider infinite Markov chains which either have a finite attractor or satisfy the global coarseness property. Markov chains derived from probabilistic lossy channel systems (PLCS) or probabilistic vector addition systems with states (PVASS) are classic examples for these types, respectively. We consider three different variants of the reachability problem and the repeated reachability problem: The qualitative problem, i.e., deciding if the probability is one (or zero); the approximate quantitative problem, i.e., computing the probability up-to arbitrary precision; the exact quantitative problem, i.e., computing probabilities exactly. We express the qualitative problem in abstract terms for Markov chains with a finite attractor and for globally coarse Markov chains, and show an almost complete picture of its decidability of PLCS and PVASS. We also show that the path enumeration algorithm of [20] terminates for our types of Markov chain and can thus be used to solve the approximate quantitative reachability problem. Furthermore, a modified variant of this algorithm can solve the approximate quantitative repeated reachability problem for Markov chains with a finite attractor. Finally, we show that the exact probability of (repeated) reachability cannot be effectively expressed in the firstorder theory of the reals (IR,+, *,?) for either PLCS or PVASS (unlike for other probabilistic models, e.g., probabilistic pushdown automata [15, 16, 14]).

BibTeX

  @InProceedings{MayrAbdullaHenda-VerifyingInfiniteMa,
    author = 	 {Richard Mayr and Parosh Abdulla and Noomene Ben Henda},
    title = 	 {Verifying Infinite Markov Chains with a Finite Attractor or the Global Coarseness Property},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {127--136},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }