@incollection{BaierKieferKleinKluppelholzMullerWorrell:CAV:2016,
    doi = {10.1007/978-3-319-41528-4_2},
    url = {https://doi.org/10.1007%2F978-3-319-41528-4_2},
    year = {2016},
    publisher = {Springer International Publishing},
    pages = {23--42},
    author = {Christel Baier and Stefan Kiefer and Joachim Klein and Sascha Klüppelholz and David Müller and James Worrell},
    title = {Markov Chains and Unambiguous Büchi Automata},
    Editor        = "Chaudhuri, Swarat and Farzan, Azadeh",
    Abstract      = {Unambiguous automata, i.e., nondeterministic automata with the restriction of having at most one accepting run over a word, have the potential to be used instead of deterministic automata in settings where nondeterministic automata can not be applied in general. In this paper, we provide a polynomially time-bounded algorithm for probabilistic model checking of discrete-time Markov chains against unambiguous B{\"u}chi automata specifications and report on our implementation and experiments.},
    booktitle = {Computer Aided Verification}
    Address       = "Cham",
    BookTitle     = "Proc. of CAV'16",
    date-added    = "2020-08-11 11:05:40 +0200",
    date-modified = "2020-08-11 11:06:15 +0200",
    ISBN          = "978-3-319-41528-4",
}

@incollection{BaierKieferKleinKluppelholzMullerWorrell:CAV:2016, doi = {10.1007/978-3-319-41528-4_2}, url = {https://doi.org/10.1007%2F978-3-319-41528-4_2}, year = {2016}, publisher = {Springer International Publishing}, pages = {23--42}, author = {Christel Baier and Stefan Kiefer and Joachim Klein and Sascha Klüppelholz and David Müller and James Worrell}, title = {Markov Chains and Unambiguous Büchi Automata}, Editor = "Chaudhuri, Swarat and Farzan, Azadeh", Abstract = {Unambiguous automata, i.e., nondeterministic automata with the restriction of having at most one accepting run over a word, have the potential to be used instead of deterministic automata in settings where nondeterministic automata can not be applied in general. In this paper, we provide a polynomially time-bounded algorithm for probabilistic model checking of discrete-time Markov chains against unambiguous B{\"u}chi automata specifications and report on our implementation and experiments.}, booktitle = {Computer Aided Verification} Address = "Cham", BookTitle = "Proc. of CAV'16", date-added = "2020-08-11 11:05:40 +0200", date-modified = "2020-08-11 11:06:15 +0200", ISBN = "978-3-319-41528-4", }