Victor Yodaiken

Victor Yodaiken

Classical automata theory is far more capable of modeling complex digital systems than is widely acknowledged in the ``formal methods'' literature. This paper takes a second look at automata theory methods that were mostly developed in the 1950s and 1960s to show how they can be applied to problems of current era specification and verification of systems, including concurrent systems. The explication is partly guided by taking a second look at the critique of automata theory in early formal methods, particularly from the early process algebra literature, Since much of the classic automata theory literature is not well known anymore, the paper also provides brief historical literature survey.

Victor Yodaiken

A product of Moore machines with feedback published in 1962 by Juris Hartmanis and a class of primitive recursive functions on finite sequences published in a textbook by Roza Peter originally in 1950 are keys to a method for working with large scale networks of Moore type state machines. The product provides a basis for connecting Moore machines in an arbitrary network so they construct a new Moore machine in which they act as components that change state in parallel. The functions provide a means of defining machines, machine products, and abstract properties of the machines without enumerating states.