Formal Proof of Equivalence in Endomorphisms and Automorphisms over Strongly Connected Automata

摘要

Automata theory has played an important role in modeling behavior of systems since last couple of decades. The algebraic automaton has emerged with several modern applications because of having properties and structures from algebraic theory. Design of a complex system not only requires behavior but it also needs to model its functionality. Z notation is an ideal one used for describing functionality. Consequently, an integration of algebraic automata and Z will be an effective tool for modeling of complex systems. In this paper, we have combined algebraic automata and Z defining a relationship between fundamentals of these approaches. At first, we have described extended form of algebraic automaton. Then the concepts of homomorphism and its variants are defined over strongly connected automata. Finally, monoid endomorphisms and group automorphisms are defined, and formal proof of their equivalence is given under certain assumptions. The specification is analyzed and validated using Z/EVES tool.