Article911331144: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christel |ErsterAutorNachname=Baier |FurtherAuthors=Nathalie Bertrand; Marcus Größer}} {{Article |Journal=Journal of the ACM |Number=1 |Title=Probabilistic $ømega$-Automata |Volume=59 |Year=2012 }} {{Publikation Details |DOI Name=10.1145/2108242.2108243 |Abstract=Probabilistic ω-automata are variants of nondeterministic automata over infinite words where all choices are resolved by probabilis…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 13: | Zeile 13: | ||
|DOI Name=10.1145/2108242.2108243 | |DOI Name=10.1145/2108242.2108243 | ||
|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. | |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. | ||
|Forschungsgruppe= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 14:49 Uhr
Probabilistic $ømega$-Automata
Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Marcus GrößerMarcus Größer
Christel Baier, Nathalie Bertrand, Marcus Größer
Probabilistic $ømega$-Automata
Journal of the ACM, 59(1), 2012
Probabilistic $ømega$-Automata
Journal of the ACM, 59(1), 2012
- KurzfassungAbstract
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. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{BBG2012,
author = {Christel Baier and Nathalie Bertrand and Marcus Gr{\"{o}}{\ss}er},
title = {Probabilistic ${\o}mega$-Automata},
journal = {Journal of the {ACM}},
volume = {59},
number = {1},
year = {2012},
doi = {10.1145/2108242.2108243}
}
