A sound and complete axiomatization of the equational theory of Mealy machines.

Pierre Pradic 1, 2
This small development in the Coq proof assistant introduces a term language and a basic equational theory for Mealy machines., i.e. finite-state letter-to-letter transducer. Soundness and completeness are proved for the equational theory.
Document type :
Software
Complete list of metadatas

Browse

- Identifier : swh:1:dir:d26d7ad1514340934a5b546032e21ad2fcc87441  Browse

https://hal.inria.fr/hal-02155786
Contributor : Pierre Pradic <>
Submitted on : Thursday, June 13, 2019 - 8:26:26 PM
Last modification on : Thursday, November 21, 2019 - 2:02:56 AM

Collections

Citation

Pierre Pradic. A sound and complete axiomatization of the equational theory of Mealy machines.. 2019, ⟨swh:1:dir:d26d7ad1514340934a5b546032e21ad2fcc87441⟩. ⟨hal-02155786⟩

Share

Metrics

Record views

38

Files downloads

415