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. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1145/2108242.2108243 | J. ACM |
Keywords | DocType | Volume |
positive acceptance probability,probable semantics,lower probability,accepted language,probability measure,traditional acceptance criterion,threshold semantics,probabilistic distribution,acceptance probability,almost-sure semantics | Journal | 59 |
Issue | Citations | PageRank |
1 | 4 | 0.41 |
References | Authors | |
29 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Christel Baier | 1 | 3053 | 185.85 |
Marcus Grösser | 2 | 4 | 0.41 |
Nathalie Bertrand | 3 | 250 | 17.84 |