DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2009.2335

Recurrence and Transience for Probabilistic Automata

Authors: Mathieu Tracol, Christel Baier, and Marcus Grösser

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

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.

Cite as

Mathieu Tracol, Christel Baier, and Marcus Grösser. Recurrence and Transience for Probabilistic Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 395-406, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{tracol_et_al:LIPIcs.FSTTCS.2009.2335,
  author =	{Tracol, Mathieu and Baier, Christel and Gr\"{o}sser, Marcus},
  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 =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.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}
}

Search Results

Documents authored by Grösser, Marcus

Recurrence and Transience for Probabilistic Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message