Title :
Formal Proofs for Automata and Sticker Systems
Author :
Tanaka, Hiroya ; Sakashita, Issei ; Inokuchi, Shuichi ; Mizoguchi, Yoshihiro
Author_Institution :
Grad. Sch. of Sci. & Eng., Saga Univ., Saga, Japan
Abstract :
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.
Keywords :
automata theory; formal verification; theorem proving; Coq proof-assistant; Coq system; automata theory; automaton; formal proofs; infinite elements; language; machine-checkable proofs; small scale reflection extension; ssreflect; sticker systems modules; transformation correctness; Automata; Color; Computers; Concrete; Educational institutions; Transforms;
Conference_Titel :
Computing and Networking (CANDAR), 2013 First International Symposium on
Conference_Location :
Matsuyama
Print_ISBN :
978-1-4799-2795-1
DOI :
10.1109/CANDAR.2013.100
