Markov chains and unambiguous automata
Unambiguous automata are nondeterministic automata in which every word has at most one accepting run. In this paper we give a polynomial-time algorithm for model checking discrete-time Markov chains against ω-regular specifications represented as unambiguous automata. We furthermore show that the co...
| Main Authors: | , , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Elsevier
2023
|
| _version_ | 1826310136888557568 |
|---|---|
| author | Baier, C Kiefer, S Klein, J Müller, D Worrell, J |
| author_facet | Baier, C Kiefer, S Klein, J Müller, D Worrell, J |
| author_sort | Baier, C |
| collection | OXFORD |
| description | Unambiguous automata are nondeterministic automata in which every word has at most one accepting run. In this paper we give a polynomial-time algorithm for model checking discrete-time Markov chains against ω-regular specifications represented as unambiguous automata. We furthermore show that the complexity of this model checking problem lies in NC: the subclass of P comprising those problems solvable in poly-logarithmic parallel time. These complexity bounds match the known bounds for model checking Markov chains against specifications given as deterministic automata, notwithstanding the fact that unambiguous automata can be exponentially more succinct than deterministic automata. We report on an implementation of our procedure, including an experiment in which the implementation is used to model check LTL formulas on Markov chains. |
| first_indexed | 2024-03-07T07:46:09Z |
| format | Journal article |
| id | oxford-uuid:e2bfa3de-6688-4b1d-8f87-ce04ed611c5d |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:46:09Z |
| publishDate | 2023 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:e2bfa3de-6688-4b1d-8f87-ce04ed611c5d2023-06-09T07:56:00ZMarkov chains and unambiguous automataJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e2bfa3de-6688-4b1d-8f87-ce04ed611c5dEnglishSymplectic ElementsElsevier2023Baier, CKiefer, SKlein, JMüller, DWorrell, JUnambiguous automata are nondeterministic automata in which every word has at most one accepting run. In this paper we give a polynomial-time algorithm for model checking discrete-time Markov chains against ω-regular specifications represented as unambiguous automata. We furthermore show that the complexity of this model checking problem lies in NC: the subclass of P comprising those problems solvable in poly-logarithmic parallel time. These complexity bounds match the known bounds for model checking Markov chains against specifications given as deterministic automata, notwithstanding the fact that unambiguous automata can be exponentially more succinct than deterministic automata. We report on an implementation of our procedure, including an experiment in which the implementation is used to model check LTL formulas on Markov chains. |
| spellingShingle | Baier, C Kiefer, S Klein, J Müller, D Worrell, J Markov chains and unambiguous automata |
| title | Markov chains and unambiguous automata |
| title_full | Markov chains and unambiguous automata |
| title_fullStr | Markov chains and unambiguous automata |
| title_full_unstemmed | Markov chains and unambiguous automata |
| title_short | Markov chains and unambiguous automata |
| title_sort | markov chains and unambiguous automata |
| work_keys_str_mv | AT baierc markovchainsandunambiguousautomata AT kiefers markovchainsandunambiguousautomata AT kleinj markovchainsandunambiguousautomata AT mullerd markovchainsandunambiguousautomata AT worrellj markovchainsandunambiguousautomata |