SCIRP Mobile Website

Why Us? >>

  • - Open Access
  • - Peer-reviewed
  • - Rapid publication
  • - Lifetime hosting
  • - Free indexing service
  • - Free promotion service
  • - More citations
  • - Search engine friendly

Free SCIRP Newsletters>>

Add your e-mail address to receive free newsletters from SCIRP.


Contact Us >>

WhatsApp  +86 18163351462(WhatsApp)
Paper Publishing WeChat
Book Publishing WeChat

Article citations


[15] R. L. Constable, et al., “Constructively formalizing automata theory,” Foundations of Computing Series, MIT Press, 2000.

has been cited by the following article:

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

    AUTHORS: Nazir Ahmad Zafar, Ajmal Hussain, Amir Ali

    KEYWORDS: Formal Methods, Automata, Integration of Approaches, Z Notation, Validation

    JOURNAL NAME: Journal of Software Engineering and Applications, Vol.2 No.2, July 15, 2009

    ABSTRACT: 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.