Using Sequence Maps to Model Large-Scale State Machines

How primitive recursive functions make state machines practical models for complex software.

Notes on Victor Yodaiken, ‘State Machines for Large Scale Computer Software and Systems’, Formal Aspects of Computing, Vol. 36, No. 2, June 2024

Limits of Traditional State Machines

State machines are fundamental to computer systems design. Whether you’re building distributed systems, operating systems, or real-time controllers, you’re essentially designing state machines. The problem is that traditional representations such as state diagrams, transition tables, and tuple-based definitions don’t scale well. Even modest increases in system complexity lead to a combinatorial explosion in the state space, making the tables and diagrams too large to reason about.

Imagine trying to draw a state diagram for a system with thousands of states, or enumerate every transition in a table this quickly becomes impractical. Yet this is exactly what we need for real-world systems. Victor Yodaiken’s paper in Formal Aspects of Computing proposes an elegant solution: sequence maps based on primitive recursive functions.

What Are Sequence Maps?

A sequence map is a function that takes a finite sequence of events and returns the system’s output in the state reached by following that sequence. Instead of explicitly enumerating states, you define behaviour recursively:

$f(ε) = c$
(output in the initial state, where ε is the empty sequence)

$f(wa) = g(f(w), a)$
(output after event a following sequence w)

This approach stays firmly within classical deterministic state machine theory while being far more practical for complex systems. With sequence maps, you’re encoding the transitions as a function of previous states and the current event, rather than expanding a massive state table. This allows you to defer state exploration and only compute or generate the state space when necessary.

A Concrete Example: The Saturation Counter

Consider a real-world problem: you want to count consecutive occurrences of the same event, with saturation at some maximum. This is common in signal processing, control systems, and network monitoring.

The Specification:

Count how many consecutive 1’s have occurred, saturating at k (meaning once you reach k consecutive 1’s, the counter stays at k until a 0 appears). When a 0 occurs, reset to 0.

The Sequence Map:

SatCounter(ε) = 0
SatCounter(w0) = 0                          (any 0 resets the count)
SatCounter(w1) = min(k, SatCounter(w) + 1)  (increment, but cap at k)

Why This Works:

The empty sequence ε represents the initial state (count = 0)
Any sequence ending in 0 produces count = 0
Any sequence ending in 1 increments the previous count, but never exceeds k

Let’s trace through an example with k=3:

Sequence      | Output
--------------|--------
ε             | 0
1             | 1
11            | 2
111           | 3   (saturated)
1111          | 3   (stays saturated)
11110         | 0   (reset)
111101        | 1   (counting again)

This specification is complete and unambiguous. Compare this to drawing a state diagram with k+1 states and 2(k+1) transitions, or writing out a transition table with the same information.

The Power of Composition

Sequence maps become even more powerful when you compose them. You can:

1. Transform outputs: If $\rm{Counter}(w)$ counts up from 0, then $\rm{k - Counter}(w)$ counts down from $k$ .

2. Connect components: Use connection maps to specify how components interact. For example, in a shift register, each cell’s input comes from the previous cell’s output.

3. Build parallel systems: Multiple components can change state simultaneously, all described through function composition.

The paper proves that sequence primitive recursive (s.p.r.) maps are mathematically equivalent to Moore-type state machines and their products. This means anything you can express with traditional state machines, you can express with sequence maps—but more concisely and at any scale.

We can formalize composition with a connection map (C) that routes outputs to inputs:

F_C(w, a) = G\big(F(w),\; C(F(w), a)\big)

Here (F) is a component (itself a sequence map), (G) is the environment, and (C) wires the signals. Because each piece is primitive recursive on sequences, the composed system remains s.p.r.

Real-World Application: The Paxos Protocol

Yodaiken demonstrates the method’s practical value by specifying and proving the Paxos distributed consensus algorithm, which is notorious for being difficult to understand and implement correctly. Using sequence maps, he:

Defines a packet network as a collection of agents with connection maps
Specifies the four Paxos message types and their transmission rules
Proves the safety property (at most one value can win consensus) with a clear, mathematical proof

The specification is more detailed than Lamport’s original “Paxos Made Simple” and catches subtle issues that the original left implicit—exactly the kind of detail you want nailed down before writing code.

Could this syntax even be used for defining state machines?

// Define the possible events that can trigger state changes
enum Event {
    A,
    B,
    C,
    // Add more events as needed
}

// Define the system's state (for simplicity, just use an integer, but you could have a more complex struct)
struct State {
    value: i32,  // Example of state data
}

// Define the function that computes the state after a sequence of events
fn process_sequence(w: Vec<Event>) -> State {
    // Base case: Empty sequence returns the initial state
    if w.is_empty() {
        return State { value: 0 };  // Initial state (can be any value or struct)
    }

    // Recursive case: Process the sequence one event at a time
    let first_event = w[0].clone();
    let remaining_events = w[1..].to_vec();

    // Process the current event with the result of the recursive call
    let previous_state = process_sequence(remaining_events);
    transition(&previous_state, first_event)
}

// Define the transition function for processing an event
fn transition(state: &State, event: Event) -> State {
    match event {
        Event::A => State { value: state.value + 1 },  // Example logic for event A
        Event::B => State { value: state.value - 1 },  // Example logic for event B
        Event::C => State { value: state.value * 2 },  // Example logic for event C
    }
}

fn main() {
    // Example sequence of events
    let events = vec![Event::A, Event::B, Event::A, Event::C];

    // Compute the resulting state after the sequence of events
    let final_state = process_sequence(events);

    // Print the resulting state
    println!("Final state value: {}", final_state.value);
}

A Note on Implementation

Whilst the recursive implementation above directly mirrors the mathematical definition of sequence maps, it has a critical performance flaw. The line let remaining_events = w[1..].to_vec() creates a new vector on every recursive call.

This makes the function O(n²) in both time and memory. For a sequence of length n, you’re allocating n vectors:

First call: vector of size n-1
Second call: vector of size n-2
…
nth call: vector of size 0

The total memory allocated is 1 + 2 + … + (n-1) = O(n²).

In practice, you’d implement this imperatively:

fn process_sequence(w: &[Event]) -> State {
    let mut state = State { value: 0 };  // Initial state

    for event in w {
        state = transition(&state, event.clone());
    }

    state
}

This processes the sequence in O(n) time with O(1) additional memory. The imperative version is how you’d actually implement sequence maps in production code, whilst the recursive version serves as a clear specification that maps directly to the mathematical definition.

The gap between elegant specification and efficient implementation is a recurring theme in systems design. Here, primitive recursive functions give us the conceptual clarity to reason about correctness, whilst imperative loops give us the performance to run at scale.