Formal Proofs for Automata and Sticker Systems
Formal Proofs for Automata and Sticker Systems
复制标题
自动机和贴纸系统的形式证明
DOI：
10.1109/candar.2013.100
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Y.Mizoguchi
中科院分区：
文献类型：
--
作者：
H.Tanaka;I.Sakashita;S.Inokuchi;Y.Mizoguchi
我们使用Coq证明助手实现了自动机理论中出现的操作。包含无限元素的语言是使用ssreflect（Coq系统的小规模反射扩展）定义的。我们还实现了贴纸系统的模块。Paun和Rozenberg在1998年介绍了一种将自动机转换为贴纸系统的具体方法。我们的目标之一是提出正式的证明其转换的正确性。我们修改了他们的一些定义，以改善其不充分的结果。我们注意到我们所有的公式都是用Coq写的，我们展示了一些机器可检查证明的例子。
We implemented operations appeared in the theory of automata using the Coq proof-assistant. A language which contains infinite elements is defined using ssreflect (a Small Scale Reflection Extension for the Coq system). We also implemented the modules for sticker systems. Paun and Rozenberg introduced a concrete method to transform an automaton to a sticker system in 1998. One of our aims is to present formal proofs of the correctness of their transformation. We modified some of their definitions to improve their insufficient results. We note that all of our formulation are written in Coq and we show some examples of machine-checkable proofs.