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
To specify the design of operating systems and other “systems level” software, it’s possible to use temporal-logic style qualifiers like “always” or “eventually” or more detailed similar qualifiers in just ordinary algebra and state machines. https://www.yodaiken.com/wp-content/uploads/2025/10/temporal.pdf
Sequential functions can be used to define and compose large scale state machines that represent computer software and hardware. The mathematical basis is introduced and there are motivating examples, including a proof of the safety of the Paxos algorithm. https://www.yodaiken.com/wp-content/uploads/2023/12/fac_sm_published_acm.pdf
Milner’s Communication and Concurrency contrasts a notion of “bisimulation” with what he characterizes as the view in standard automata theory. Standard automata theory, however, has a much more interesting and well defined notion of both equivalence and concurrency than what