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
|