Recurrence and transience for probabilistic automata

Mathieu TracolMathieu Tracol, Christel BaierChristel Baier, Marcus GrößerMarcus Größer

DOI Link

Mathieu Tracol, Christel Baier, Marcus Größer
Recurrence and transience for probabilistic automata
Proc. of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 4 of Leibniz International Proceedings in Informatics, 395--406, 2009. Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Details
Bibtex

KurzfassungAbstract
In a context of ω-regular specifications for infinite execution sequences, the classical B üchi condition, or repeated liveness condition, asks that an accepting state is visited infinitely often. In this paper, we show that in a probabilistic context it is relevant to strengthen this infinitely often condition. An execution path is now accepting if the proportion of time spent on an accepting state does not go to zero as the length of the path goes to infinity. We introduce associated notions of recurrence and transience for non-homogeneous finite Markov chains and study the computational complexity of the associated problems. As Probabilistic B üchi Automata (PBA) have been an attempt to generalize Büchi automata to a probabilistic context, we define a class of Constrained Probabilistic Automata with our new accepting condition on runs. The accepted language is defined by the requirement that the measure of the set of accepting runs is positive (probable semantics) or equals 1 (almost-sure semantics). In contrast to the PBA case, we prove that the emptiness problem for the language of a constrained probabilistic B üchi automaton with the probable semantics is decidable.
Forschungsgruppe:Research Group: Verifikation und formale quantitative Analyse„Verifikation und formale quantitative Analyse“ befindet sich nicht in der Liste (Computational Logic, Automatentheorie, Wissensverarbeitung, Knowledge-Based Systems, Knowledge Systems, Wissensbasierte Systeme, Logische Programmierung und Argumentation, Algebra und Diskrete Strukturen, Knowledge-aware Artificial Intelligence, Algebraische und logische Grundlagen der Informatik) zulässiger Werte für das Attribut „Forschungsgruppe“.Algebraic and Logical Foundations of Computer Science

@inproceedings{TBG2009,
  author    = {Mathieu Tracol and Christel Baier and Marcus Gr{\"{o}}{\ss}er},
  title     = {Recurrence and transience for probabilistic automata},
  booktitle = {Proc. of the {IARCS} Annual Conference on Foundations of Software
               Technology and Theoretical Computer Science (FSTTCS)},
  series    = {Leibniz International Proceedings in Informatics},
  volume    = {4},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2009},
  pages     = {395--406},
  doi       = {10.4230/LIPICS.FSTTCS.2009.2335}
}