Markov Chains and Unambiguous Buchi Automata

被引：19

作者：

Baier, Christel ^{[1
]}

Kiefer, Stefan ^{[2
]}

Klein, Joachim ^{[1
]}

Klueppelholz, Sascha ^{[1
]}

Mueller, David ^{[1
]}

Worrell, James ^{[2
]}

机构：

[1] Tech Univ Dresden, Dresden, Germany

[2] Univ Oxford, Oxford, England

来源：

COMPUTER AIDED VERIFICATION, (CAV 2016), PT I | 2016年 / 9779卷

关键词：

OMEGA-AUTOMATA; EQUIVALENCE;

D O I：

10.1007/978-3-319-415284_2

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：23 / 42

页数：20

共 39 条

[1] [Anonymous], 2004, COLT DISTRIBUTION OP
[2] [Anonymous], 2013, Matrix Analysis
[3] [Anonymous], 1995, IFIP
[4] [Anonymous], 1979, NONNEGATIVE MATRICES
[5] [Anonymous], LIPICS
[6] [Anonymous], 1986, P 1 S LOG COMP SCI L
[7] [Anonymous], 2002, Automata Logics, and Infinite Games
[8] ARNOLD A, 1985, LECT NOTES COMPUT SC, V192, P18
[9] The Hanoi Omega-Automata Format
Babiak, Tomas
Blahoudek, Frantisek
Duret-Lutz, Alexandre
Klein, Joachim
Kretinsky, Jan
Mueller, David
Parker, David
Strejcek, Jan
[J]. COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 : 479 - 486
[10] Baier C., 2016, MARKOV CHAINS UNAMBI

← 1 2 3 4 →