These papers introduce sequential functions for specifying digital systems like operating systems and networks. The mathematical basis comes from Moore machines, Moore machine products, and primitive recursive functions on finite sequences. Primitive recursive functions on sequences were described by Rózsa Péter in the 1950s but their connection with automata was not explored. They provide an alternative to state diagrams and other traditional methods of defining Moore machines, and can concisely define very large scale state machines, interconnected machines, and abstract properties of the machines. Composition of primitive recursive sequential functions corresponds to automata products. The method is aimed at system designs, not verification of program text and is intended as an aid to system designers so that they can understand properties of their systems before writing code. The first paper is an introduction to the method and includes a number of examples, one of which is a proof that Paxos is safe.
State machines for large scale computer software and systems
The second paper shows how to use sequential functions define temporal logic like properties – for example, that something is always true, or must become true “eventually”. The sequential function analogs are more expressive – for example, eventually can be made to depend on different types of events and to work with systems that combine components that change state at different rates and in response to different events.
Specifications like temporal logic but with ordinary mathematics
The third paper gives some historical background on automata theory and argues that the 1970s consensus in Computer Science, that classical automata theory is too limited, was incorrect and ignored, in particular algebraic automata theory and automata products. The paper includes a discussion of “machine homomorphism” introduced in the 1960s, then modified in process algebra, and then eventually forgotten in the process algebra and larger formal methods literature. By the mid 1960s, Moore machines and concurrent products of Moore machines were well understood in the automata theory literature, but for a number of reasons, they were not applied to software specification.
Process algebra and automata theory
Also see Digital Circuits as Moore Machines for models of the real-time behavior of simple digital circuits
Unlike most Computer Science research on specification, there is no formal logic or other use of axiomatic methods, no lambda calculus, no non-determinism, no completed infinities (e.g. infinite sequences of events), not even any category theory needed for sequential functions. Then there is a paper defining modularity mathematically in terms of automata products (improving A mathematical basis for understanding software modularity ). And there is a paper that just presents the theory of sequential functions focused on the mathematics, not the CS applications.
The works are released under the creative commons NC-ND license with the added condition that use for training or other purpose in Artificial Intelligence systems is specifically prohibited as violating the prohibition on creating derivative works and/or use for profit.