Share This Article:

Refinement in Formal Proof of Equivalence in Morphisms over Strongly Connected Algebraic Automata

Full-Text HTML Download Download as PDF (Size:428KB) PP. 77-85
DOI: 10.4236/jsea.2009.22012    4,364 Downloads   7,453 Views Citations


Automata theory has played an important role in computer science and engineering particularly modeling behavior of systems since last couple of decades. The algebraic automaton has emerged with several modern applications, for ex-ample, optimization of programs, design of model checkers, development of theorem provers because of having proper-ties and structures from algebraic theory of mathematics. Design of a complex system not only requires functionality but it also needs to model its control behavior. Z notation is an ideal one used for describing state space of a system and then defining operations over it. Consequently, an integration of algebraic automata and Z will be an effective computer tool which can be used for modeling of complex systems. In this paper, we have combined algebraic automata and Z notation defining a relationship between fundamentals of these approaches. At first, we have described algebraic automaton and its extended forms. Then homomorphism and its variants over strongly connected automata are speci-fied. Finally, monoid endomorphisms and group automorphisms are formalized, and formal proof of their equivalence is given under certain assumptions. The specification is analyzed and validated using Z/EVES tool.

Cite this paper

N. Zafar, A. Hussain and A. Ali, "Refinement in Formal Proof of Equivalence in Morphisms over Strongly Connected Algebraic Automata," Journal of Software Engineering and Applications, Vol. 2 No. 2, 2009, pp. 77-85. doi: 10.4236/jsea.2009.22012.

Copyright © 2020 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.