Scifaro

中文

LTL公式化简中一个细微错误与DiVinE不正确性的简短故事

计算机科学中的逻辑 2016-08-14 v2 形式语言与自动机理论

作者: Tomáš Babiak , Mojmír Křetínský , Vojtěch Řehák , Jan Strejček

在 arXiv 上查看 ↗ PDF ↗

摘要

我们识别了在LTL到Büchi自动机翻译中用作一个优化步骤的LTL公式化简方法中的一个细微错误。该错误导致已建立的模型检查器DiVinE产生了一些不正确的答案。本文应有助于其他模型检查器的作者避免此错误。

关键词

LTL公式化简 Büchi自动机翻译模型检查 DiVinE 错误识别

引用

@article{arxiv.1011.4214,
  title  = {A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness},
  author = {Tomáš Babiak and Mojmír Křetínský and Vojtěch Řehák and Jan Strejček},
  journal= {arXiv preprint arXiv:1011.4214},
  year   = {2016}
}