| 作成者 |
|
|
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 開始ページ |
|
| 終了ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| 関連DOI |
|
|
|
| 関連URI |
|
|
|
| 関連情報 |
|
|
|
| 概要 |
有限オートマトンを構成する演算子や文字列の(無限) 集合をCoq 証明支援系を用いて形式的に定義しました. ここでは, Ssreflect (Small Scale Reflection Extension for the Coq system) も利用します. スティッカー系はPăun とRozenberg により1998 年に紹介されたDNA計算のための形式モデルです. 彼らは有限オートマトン...と同等の能力を持つスティッカー系を構成する具体的な構成方法を示し, スティッカー系の計算能力が有限オートマトンのそれを含むことを示しました. しかし, その構成方法には小さな誤りがありました. それを修正した構成方法を示すことと同時に私たちの構成方法の正当性に対して,コンピュータで検証可能な形式的証明を与えることが本研究の目的です. 現在までに, 諸性質を形式証明するための有限オートマトンとスティッカー系の定義や関数の形式化が出来ました. いくつかの具体例の形式的証明, Păun らの構成に誤りがあることの形式証明を含めて報告します.
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. Păun 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.続きを見る
|
Mendeley出力
msj20140315d