Büchi Automata Optimisations Formalised in Isabelle/HOL
Büchi Automata Optimisations Formalised in Isabelle/HOL
复制标题
Büchi 自动机优化在 Isabelle/HOL 中正式化
DOI：
10.1007/978-3-662-45824-2_11
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Jan-Georg Smaus
中科院分区：
文献类型：
--
作者：
Alexander Schimpf;Jan-Georg Smaus
在自动机理论的应用中，人们感兴趣的是减少自动机的大小，以保持公认的语言。对于Büchi自动机，已经提出了两种优化：互模拟约简，计算状态的等价类并将其折叠，以及α球约简，折叠仅包含一个字母作为边缘标签的自动机的强连接组件（SCC）。在本文中，我们提出了一个形式化的Isabelle/HOL，这些算法提供了一个正式验证的实现。
In applications of automata theory, one is interested in reductions in the size of automata that preserve the recognised language. For Büchi automata, two optimisations have been proposed: bisimulation reduction, which computes equivalence classes of states and collapses them, andα-balls reduction, which collapses strongly connected components (SCCs) of an automaton that only contain one single letter as edge label. In this paper, we present a formalisation of these algorithms in Isabelle/HOL, providing a formally verified implementation.