@MISC{FSM_1.MIZ,
  AUTHOR = {Kaloper, Miroslava and Rudnicki, Piotr},
  TITLE = {Minimization of Finite State Machines},
  NOTE = {This work was partially supported by NSERC Grant OGP9207.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Definitions and Terminology},
  SECTION3 = {Mealy and Moore Machines},
  SECTION4 = {Equivalence of States and Machines},
  SECTION5 = {The Reduction of a Mealy Machine},
  SECTION6 = {Machine Isomorphism},
  SECTION7 = {Reduced and Connected Machines},
  SECTION8 = {Machine Union},
  SECTION9 = {The Minimization Theorem},
  DAY = {18},
  MONTH = {November},
  YEAR = {1994},
  ADDRESS1 = {University of Alberta\\Department of Computing Science},
  ADDRESS2 = {University of Alberta\\Department of Computing Science},
  SUMMARY = {We have formalized deterministic finite state machines closely 
following the textbook \cite{ddq}, pp. 88--119 up to the minimization
theorem. In places, we have changed the approach presented in the book
as it turned out to be too specific and inconvenient.
Our work also revealed several minor mistakes in the book.
After defining a structure for an outputless finite state machine,
we have derived the structures for the transition assigned output
machine (Mealy) and state assigned output machine (Moore).  The machines
are then proved similar, in the sense that for any Mealy (Moore) machine
there exists a Moore (Mealy) machine producing essentially
the same response for the same input.  The rest of work is then done
for Mealy machines.  Next, we define equivalence of machines,
equivalence and $k$-equivalence of states, and characterize a process of
constructing for a given Mealy machine, the machine equivalent to it
in which no two states are equivalent.  The final, minimization
theorem states:
 \begin{quotation}
 \noindent
 {\bf Theorem 4.5:} Let {\bf M}$_1$ and {\bf M}$_2$ be reduced, connected
 finite-state machines.  Then the state graphs of {\bf M}$_1$ and {\bf M}$_2$
 are isomorphic if and only if {\bf M}$_1$ and {\bf M}$_2$ are equivalent.
 \end{quotation}
and it is the last theorem in this article.}}


@BOOK{ddq,
       AUTHOR = {Denning, P. J. and Dennis, J. B. and Qualitz, J. E.},
        TITLE = {Machines, Languages, and Computation},
    PUBLISHER = {Prentice-Hall},
         YEAR = {1978}}
