Probabilistic and Topological Semantics for Timed Automata

Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Patricia BouyerPatricia Bouyer, Thomas BrihayeThomas Brihaye, Marcus GrößerMarcus Größer

DOI Link

Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Marcus Größer
Probabilistic and Topological Semantics for Timed Automata
Proc. of the 27th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 4855 of Lecture Notes in Computer Science, 179--191, 2007. Springer

Details
Bibtex

KurzfassungAbstract
In a context of $\omega$-regular specifications for infinite execution sequences, the classical B{\"u}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 \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{\"u}chi Automata (PBA) have been an attempt to generalize B{\"u}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{\"u}chi automaton with the probable semantics is decidable.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2335.

@inproceedings{BBBBG2007,
  author    = {Christel Baier and Nathalie Bertrand and Patricia Bouyer and
               Thomas Brihaye and Marcus Gr{\"{o}}{\ss}er},
  title     = {Probabilistic and Topological Semantics for Timed Automata},
  booktitle = {Proc. of the 27th International Conference on Foundations of
               Software Technology and Theoretical Computer Science (FSTTCS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {4855},
  publisher = {Springer},
  year      = {2007},
  pages     = {179--191},
  doi       = {10.4230/LIPIcs.FSTTCS.2009.2335}
}