Searcharxiv⌕ Search

arXiv subjects

Victor Yodaiken

Publications and source records attributed to Victor Yodaiken.

12 recordsLinked to original sources
arXiv2026

Standard Automata Theory and Process Algebra

Classical automata theory is far more capable of modeling complex digital systems than is widely acknowledged in the ``formal methods'' literature. This paper takes a second look at automata theory methods that were mostly developed in the 1950s and 1960s to show how they can be applied to problems of current era specification and verification of systems, including concurrent systems. The explication is partly guided by taking a second look at the critique of automata theory in early formal methods, particularly from the early process algebra literature, Since much of the classic automata theory literature is not well known anymore, the paper also provides brief historical literature survey.

cs.FL↗
arXiv2026

Networks of Moore Machines

A product of Moore machines with feedback published in 1962 by Juris Hartmanis and a class of primitive recursive functions on finite sequences published in a textbook by Roza Peter originally in 1950 are keys to a method for working with large scale networks of Moore type state machines. The product provides a basis for connecting Moore machines in an arbitrary network so they construct a new Moore machine in which they act as components that change state in parallel. The functions provide a means of defining machines, machine products, and abstract properties of the machines without enumerating states.

cs.FL↗
arXiv2026

Digital Circuits as Moore Machines

This paper illustrates a technique for specifying the timing, logical operation, and compositional circuit design of digital circuits in terms of ordinary state machines with output (Moore machines). The method is illustrated here with specifications of gates, latches, and other simple circuits and via the construction of devices starting with a SR latch built from gates. The method is based on "classical" automata and recursive functions on strings (sequential functions).

cs.FL↗
arXiv2026

Parametric equations for temporal style assertions

Temporal logic provided an appealing approach to specifying properties of operating systems and other "reactive" software by allowing propositions to be qualified by "when" they must be true. This paper shows how to get the same effect, with a finer control over specification and a compositional notion of state, using ordinary working mathematics, without the weight of formal logic, by using sequential functions which are an alternate representation of Moore type state machines.

cs.LO↗
arXiv2023

State machines for large scale computer software and systems

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.

cs.FL↗
arXiv2022

Understanding Paxos and other distributed consensus algorithms

Paxos is a widely used and notoriously hard to understand method for solving one type of distributed consensus problem. This note provides a quick explanation of Paxos, a novel proof of correctness that is intended to provide insight into why the algorithm is as simple as the author has claimed, an explanation of why it does and why it doesn't work, and has a brief discussion of alternatives.

cs.DC↗
arXiv2022

How ISO C became unusable for operating systems development

The C programming language was developed in the 1970s as a fairly unconventional systems and operating systems development tool, but has, through the course of the ISO Standards process, added many attributes of more conventional programming languages and become less suitable for operating systems development. Operating system programming continues to be done in non-ISO dialects of C. The differences provide a glimpse of operating system requirements for programming languages.

cs.OS↗
arXiv2015

Folding a Tree into a Map

Analysis of the retrieval architecture of the highly influential UNIX file system (\cite{Ritchie}\cite{multicsfs}) provides insight into design methods, constraints, and possible alternatives. The basic architecture can be understood in terms of function composition and recursion by anyone with some mathematical maturity. Expertise in operating system coding or in any specialized "formal method" is not required.

cs.OS↗
arXiv2010

Primitive Recursive Presentations of Automata and their Products

Methods for specifying Moore type state machines (transducers) abstractly via primitive recursive functions and for defining parallel composition via simultaneous primitive recursion are discussed. The method is mostly of interest as a concise and convenient way of working with the complex state systems found in computer programming and engineering, but a short section indicates connections to algebraic automata theory and the theorem of Krohn and Rhodes.

cs.FL↗
arXiv2008

The meaning of concurrent programs

The semantics of assignment and mutual exclusion in concurrent and multi-core/multi-processor systems is presented with attention to low level architectural features in an attempt to make the presentation realistic. Recursive functions on event sequences are used to define state dependent functions and variables in ordinary (non-formal-method) algebra.

cs.DM↗