License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2009.2335
URN: urn:nbn:de:0030-drops-23357
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2335/
Go to the corresponding LIPIcs Volume Portal

Tracol, Mathieu ; Baier, Christel ; Grösser, Marcus

Recurrence and Transience for Probabilistic Automata

pdf-format:
09005.TracolM.2335.pdf (0.3 MB)

Abstract

In a context of $\omega$-regular specifications for infinite execution
sequences, the classical B\"uchi 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 \emph{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\"uchi Automata
(PBA) have been an attempt to generalize B\"uchi 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\"uchi automaton with the probable semantics is decidable.

BibTeX - Entry

@InProceedings{tracol_et_al:LIPIcs:2009:2335,
  author =	{Mathieu Tracol and Christel Baier and Marcus Gr{\"o}sser},
  title =	{{Recurrence and Transience for Probabilistic Automata}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{395--406},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Ravi Kannan and K. Narayan Kumar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2335},
  URN =		{urn:nbn:de:0030-drops-23357},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2335},
  annote =	{Keywords: Markov Chains, Probabilistic Automata, Buchi Automata, Recurrence, Omega-Regular Properties}
}

Keywords: Markov Chains, Probabilistic Automata, Buchi Automata, Recurrence, Omega-Regular Properties
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue Date: 2009
Date of publication: 14.12.2009

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI