Tag: moore machines

Categories
vy papers

Specifying digital systems using sequential functions

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. 

Categories
Uncategorized

Recursion and state

automata 071 Despite some deep results, algebraic automata theory has fallen out of favor in theoretical computer science. Reasons include the disciplines failings such as a love of over-generality, weak mathematical background of people working on “formal methods”, and gap between theoreticians and engineers. But perhaps the key reason is that traditional state machine presentations in terms of state sets and transition maps are awkward and carry too much irrelevant information.

The standard presentation of a Moore machine is  M=(A,X,S,st,δ,γ)  where  “A” is the alphabet of events, “X” is the set of outputs, “st” is the start state,  δ:S x A→ S is the transition function and γ:S → X is the output function.  But  we really don’t care about the state set in all but the simplest state machines. Interesting systems have ridiculously large numbers of states.  Names of states don’t matter.  Extra states don’t matter. Suppose “s” is an element of “S” that is unreachable – no sequence of inputs will drive M to “s” from “st”. In that case what difference does removing “s” from “S” make? Or suppose s and s’ are both reachable but not only is γ(s)=γ(s’) but for any sequence of inputs that can drive the machine from s to a new state, the output of that new state is identical to the output of the state reached by following the same sequence of inputs from s’.  In that case, we could simplify S and δ by removing one of the duplicative states and merging paths.

What’s more interesting is to consider what output a Moore machine will produce from a sequence of inputs: thinking of the Moore machine as a map from input strings to outputs. This is  a function that can be constructed by primitive recursion on strings.  First, extend δ to strings to define a new function Δ. The   empty string that has zero length doesn’t cause any state change Δ(s,empty)=s   and if “w” is a string and “wa” is the string obtained by appending “a” to “w”, then Δ(s,wa)= δ(Δ(s,w),a).  Define  M*(w) = γ(Δ(st,w)). The idea is that M*(w) is the output produced by M in the state reached by following “w” from the initial state.  If you look at M* you see it contains all the interesting information in M -  because the names of states and unreachable states and duplicate states are not interesting. In fact in the 1950s Myhill and Nerode described how to generate a state machine (not necessarily a finite state one) from any function on the set of strings over an alphabet.milenr 001

These functions are much more useful in describing complex state systems than are Moore machines – not least because they can be partially specified when we don’t know or care about all the possible behaviors of the system and because they can be composed in a way to represent any interconnection.

In the next post, I’m going to discuss composition of message passing processes and compare to the “formal methods” approach which is based on the incorrect assumption that automata need to be “enhanced” in some way and that replaces automata with things that have very little mathematical structure at all.

Categories
operating systems

New paper “H2” on operating system semantics

Please see a new version here. I am continuing to try to develop a practical engineering mathematics for operating system and other complex system code.