Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
复制标题
用于 LTL 模型检查的 Büchi 自动机构建在 Isabelle/HOL 得到验证
DOI：
10.1007/978-3-642-03359-9_29
复制
发表时间：
2009
影响因子：
0.8
通讯作者：
J. Smaus
中科院分区：
文献类型：
--
作者：
A. Schimpf;Stephan Merz;J. Smaus
我们提出了在Isabelle/HOL的翻译LTL公式到Buchi自动机的实现。在基于自动机的模型检测中，系统被建模为变迁系统，并且以时序逻辑公式表示的正确性属性被转换为相应的自动机。LTL公式由（广义）Buchi自动机表示，该自动机精确地接受公式所允许的那些行为。模型检测问题，然后减少到检查两个自动机之间的语言包含。因此，自动机构造是LTL模型检测算法的重要组成部分。我们实现了一个标准的翻译算法，由于Gerth等人。我们的实现的正确性和终止性在Isabelle/HOL中得到证明，并使用Isabelle/HOL代码生成器生成可执行代码。
We present the implementation in Isabelle/HOL of a translation of LTL formulae into Buchi automata. In automaton-based model checking, systems are modelled as transition systems, and correctness properties stated as formulae of temporal logic are translated into corresponding automata. An LTL formula is represented by a (generalised) Buchi automaton that accepts precisely those behaviours allowed by the formula. The model checking problem is then reduced to checking language inclusion between the two automata. The automaton construction is thus an essential component of an LTL model checking algorithm. We implemented a standard translation algorithm due to Gerth et al . The correctness and termination of our implementation are proven in Isabelle/HOL, and executable code is generated using the Isabelle/HOL code generator.