Formal proofs for automata and sticker systems

Hisaharu Tanaka, Issei Sakashita, Shuichi Inokuchi, Yoshihiro Mizoguchi

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    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. Pu{a}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.

    Original languageEnglish
    Title of host publicationProceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013
    Pages563-566
    Number of pages4
    DOIs
    Publication statusPublished - Dec 1 2013
    Event2013 1st International Symposium on Computing and Networking, CANDAR 2013 - Matsuyama, Ehime, Japan
    Duration: Dec 4 2013Dec 6 2013

    Publication series

    NameProceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013

    Other

    Other2013 1st International Symposium on Computing and Networking, CANDAR 2013
    CountryJapan
    CityMatsuyama, Ehime
    Period12/4/1312/6/13

    All Science Journal Classification (ASJC) codes

    • Computer Networks and Communications

    Cite this

    Tanaka, H., Sakashita, I., Inokuchi, S., & Mizoguchi, Y. (2013). Formal proofs for automata and sticker systems. In Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013 (pp. 563-566). [6726962] (Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013). https://doi.org/10.1109/CANDAR.2013.100