The behavior and architecture of large scale discrete state systems found in computer software and hardware can be specified and analyzed using a particular class of primitive recursive functions. This paper begins with an illustration of the utility of the method via a number of small examples and then via longer specification and verification of the Paxos distributed consensus algorithm. The sequence maps are then shown to provide an alternative representation of deterministic state machines and algebraic products of state machines. Distributed and composite systems, parallel and concurrent computation, and real-time behavior can all be specified naturally with these methods - which require neither extensions to the classical state machine model nor any axiomatic methods or other techniques from formal methods. Compared to state diagrams or tables or the standard set-tuple-transition-maps, sequence maps are more concise and better suited to describing the behavior and compositional architecture of computer systems. Staying strictly within the boundaries of classical deterministic state machines anchors the methods to the algebraic structures of automata and makes the specifications faithful to engineering practice.

翻译：在计算机软件与硬件中发现的大规模离散状态系统的行为与架构，可通过一类特定的原始递归函数进行规范描述与分析。本文首先通过若干小型示例展示该方法的实用性，继而通过Paxos分布式共识算法的详细规范与验证加以说明。随后证明序列映射可为确定性状态机及其代数积提供替代表示。分布式与复合系统、并行与并发计算、实时行为等均可通过该方法自然规范——该方法既不需要对经典状态机模型进行扩展，也不依赖任何公理化方法或其他形式化技术。相较于状态图、状态表或标准的集合-元组-转换映射，序列映射更加简洁，且更适合描述计算机系统的行为与组合架构。严格遵循经典确定性状态机边界，使该方法扎根于自动机的代数结构，并确保规范忠实于工程实践。