Verifying Monoid and Group Morphisms over Strongly Connected Algebraic Automata
Verifying Monoid and Group Morphisms over Strongly Connected Algebraic Automata作者机构：不详
出 版 物：《Journal of Software Engineering and Applications》 (软件工程与应用（英文）)
年 卷 期：2010年第3卷第8期
页 面：803-812页
学科分类：07[理学] 0701[理学-数学] 070101[理学-基础数学]
主 题：Formal Methods Z notation Algebraic Automata Validation and Verification
摘 要：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.
维普期刊数据库