Markov chains and unambiguous Büchi automata
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 polynomia...
| Main Authors: | , , , , , |
|---|---|
| Format: | Conference item |
| Published: |
Springer, Cham
2016
|
| _version_ | 1797076686206926848 |
|---|---|
| author | Baier, C Kiefer, S Klein, J Klüppelholz, S Müller, D Worrell, J |
| author_facet | Baier, C Kiefer, S Klein, J Klüppelholz, S Müller, D Worrell, J |
| author_sort | Baier, C |
| collection | OXFORD |
| description | 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 Buchi automata specifications and report on our implementation and experiments. |
| first_indexed | 2024-03-07T00:07:16Z |
| format | Conference item |
| id | oxford-uuid:77f47690-52a3-4b1b-8a45-3cb69e3cbe75 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:07:16Z |
| publishDate | 2016 |
| publisher | Springer, Cham |
| record_format | dspace |
| spelling | oxford-uuid:77f47690-52a3-4b1b-8a45-3cb69e3cbe752022-03-26T20:27:36ZMarkov chains and unambiguous Büchi automataConference itemhttp://purl.org/coar/resource_type/c_5794uuid:77f47690-52a3-4b1b-8a45-3cb69e3cbe75Symplectic Elements at OxfordSpringer, Cham2016Baier, CKiefer, SKlein, JKlüppelholz, SMüller, DWorrell, JUnambiguous 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 Buchi automata specifications and report on our implementation and experiments. |
| spellingShingle | Baier, C Kiefer, S Klein, J Klüppelholz, S Müller, D Worrell, J Markov chains and unambiguous Büchi automata |
| title | Markov chains and unambiguous Büchi automata |
| title_full | Markov chains and unambiguous Büchi automata |
| title_fullStr | Markov chains and unambiguous Büchi automata |
| title_full_unstemmed | Markov chains and unambiguous Büchi automata |
| title_short | Markov chains and unambiguous Büchi automata |
| title_sort | markov chains and unambiguous buchi automata |
| work_keys_str_mv | AT baierc markovchainsandunambiguousbuchiautomata AT kiefers markovchainsandunambiguousbuchiautomata AT kleinj markovchainsandunambiguousbuchiautomata AT kluppelholzs markovchainsandunambiguousbuchiautomata AT mullerd markovchainsandunambiguousbuchiautomata AT worrellj markovchainsandunambiguousbuchiautomata |