Probabilistic omega-automata
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
Abstract
Probabilistic ω-automata are variants of nondeterministic automata over infinite words where all choices are resolved by probabilistic distributions. Acceptance of a run for an infinite input word can be defined using traditional acceptance criteria for ω-automata, such as Büchi, Rabin or Streett conditions. The accepted language of a probabilistic ω-automata is then defined by imposing a constraint on the probability measure of the accepting runs. In this paper, we study a series of fundamental properties of probabilistic ω-automata with three different language-semantics: (1) the probable semantics that requires positive acceptance probability, (2) the almost-sure semantics that requires acceptance with probability 1, and (3) the threshold semantics that relies on an additional parameter λ ∈ ]0,1[ that specifies a lower probability bound for the acceptance probability. We provide a comparison of probabilistic ω-automata under these three semantics and nondeterministic ω-automata concerning expressiveness and efficiency. Furthermore, we address closure properties under the Boolean operators union, intersection and complementation and algorithmic aspects, such as checking emptiness or language containment.
Details
| Original language | English |
|---|---|
| Pages (from-to) | 1-52 |
| Journal | Journal of the ACM |
| Volume | 59 |
| Issue number | 1 |
| Publication status | Published - 2012 |
| Peer-reviewed | Yes |
External IDs
| ORCID | /0000-0002-5321-9343/work/142236663 |
|---|
Keywords
Keywords
- Omega-regular languages, Büchi automata, probabilistic automata, Markov decision processes