TITLE:
Verifying Monoid and Group Morphisms over Strongly Connected Algebraic Automata
AUTHORS:
Nazir Ahmad Zafar, Ajmal Hussain, Amir Ali
KEYWORDS:
Formal Methods, Z notation, Algebraic Automata, Validation and Verification
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.3 No.8,
August
26,
2010
ABSTRACT: Automata theory has played an important role in theoretical computer science since last couple of decades. The alge-braic automaton has emerged with several modern applications, for example, optimization of programs, design of model checkers, development of theorem provers because of having certain interesting properties and structures from algebraic theory of mathematics. Design of a complex system requires functionality and also needs to model its control behavior. Z notation has proved to be an effective tool for describing state space of a system and then defining operations over it. Consequently, an integration of algebraic automata and Z will be a useful computer tool which can be used for modeling of complex systems. In this paper, we have linked algebraic automata and Z defining a relationship between fundamentals of these approaches which is refinement of our previous work. At first, we have described strongly connected algebraic automata. Then homomorphism and its variants over strongly connected automata are specified. Next, monoid endomorphisms and group automorphisms are formalized. Finally, equivalence of endomorphisms and automorphisms under certain assumptions are described. The specification is analyzed and validated using Z/Eves toolset.