用于概率模型检测与 LTL 综合的具广义 Rabin 对的自动机
计算机科学中的逻辑
2013-04-22 v1 形式语言与自动机理论
摘要
概率系统的模型检测问题关键依赖于将 LTL 翻译为确定性 Rabin 自动机 (DRW)。我们近期针对 LTL(F,G) 片段的无 Safra 翻译方法生成的自动机比传统方法更小。在本文中，我们不使用 DRW，而是考虑接受条件由广义 Rabin 对的析取给出的确定性自动机 (DGRW)。将 LTL(F,G) 公式无 Safra 翻译为 DGRW 所产生的自动机比 DRW 更小。我们提出了针对 DGRW 条件的概率模型检测算法以及博弈求解算法。我们的新算法在理论界限和实际评估方面均带来了改进。我们对比了使用与不使用新翻译方法的 PRISM 工具，结果表明新翻译方法带来了显著的提升。
引用
@article{arxiv.1304.5281,
title = {Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis},
author = {Krishnendu Chatterjee and Andreas Gaiser and Jan Křetínský},
journal= {arXiv preprint arXiv:1304.5281},
year = {2013}
}