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 \omega-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.

翻译：无歧义自动机是一种非确定性自动机，其中每个单词至多存在一个接受运行路径。本文针对以无歧义自动机表示的ω-正则规范，给出了离散时间马尔可夫链模型检测的多项式时间算法。我们进一步证明，该模型检测问题的复杂度属于NC类——即P类中可在多对数级并行时间内求解的子类。这些复杂度边界与针对确定性自动机表示的规范进行马尔可夫链模型检测的已知复杂度结果相匹配，尽管无歧义自动机可能比确定性自动机具有指数级的简洁性。我们报告了该算法的实现情况，包括一项使用该实现工具对马尔可夫链进行LTL公式模型检测的实验。