Paper: Recognizing omega-regular Languages with Probabilistic Automata (at LICS 2005)

Authors: Christel Baier Marcus Größer

Abstract

Probabilistic finite automata as acceptors for languages over finite words have been studied by many researchers. In this paper, we show how probabilistic automata can serve as acceptors for ?-regular languages. Our main results are that our variant of probabilistic Buchi automata (PBA) is more expressive than non-deterministic ?-automata, but a certain subclass of PBA, called uniform PBA, has exactly the power of ?-regular languages. This also holds for probabilistic ?-automata with Streett or Rabin acceptance. We show that certain ?-regular languages have uniform PBA of linear size, while any nondeterministic Streett automaton is of exponential size, and vice versa. Finally, we discuss the emptiness problem for uniform PBA and the use of PBA for the verification of Markov chains against qualitative lineartime properties.

BibTeX

  @InProceedings{Grer-Recognizingomegareg,
    author = 	 {Christel Baier and Marcus Größer},
    title = 	 {Recognizing omega-regular Languages with Probabilistic Automata},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {137--146},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }