DocumentCode
3130760
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
fYear
2013
fDate
4-6 Dec. 2013
Firstpage
563
Lastpage
566
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computing and Networking (CANDAR), 2013 First International Symposium on
Conference_Location
Matsuyama
Print_ISBN
978-1-4799-2795-1
Type
conf
DOI
10.1109/CANDAR.2013.100
Filename
6726962
Link To Document