Construction of Morphisms over Extended Algebraic Automata Using Z

Algebraic automaton has emerged with several modern applications in computer science and engineering. Design of theorem provers, development of model checkers, optimization of programs are some of its applications. The Z notation is suitable for modeling static while automata are powerful for describing dynamic parts of a system. Consequently, their integration is required. In this paper, we have proposed a relationship between the fundamentals of algebraic automata and Z. Initially, we have given formalization of the extended algebraic automata.Then formal construction of homomorphism is described and extended to isomorphism. Finally, a formal procedure of conversion from homomorphism (isomorphism) to endomorphism (automorphism) is given. The formal specification is analyzed and validated using Z/EVES tool.