Probabilistic omega-automata

Research output: Contribution to journalResearch articleContributedpeer-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 languageEnglish
Pages (from-to)1-52
JournalJournal of the ACM
Volume59
Issue number1
Publication statusPublished - 2012
Peer-reviewedYes

External IDs

ORCID /0000-0002-5321-9343/work/142236663

Keywords

Keywords

  • Omega-regular languages, Büchi automata, probabilistic automata, Markov decision processes