The two boxes that agree once
Feed the binary string 1010 into two sealed boxes. Both display EVEN. You are told that one box computes the parity of the string, meaning whether it contains an even or odd number of ones. Which box is the computer?
Opening the boxes does not immediately settle the matter. Each contains two labelled conditions, EVEN and ODD, plus wires that react to the next input bit. In Box A, a 1 toggles the condition and a 0 preserves it. In Box B, a 1 sets ODD and a 0 sets EVEN. Both finish in EVEN for 1010, although their intermediate paths differ.
Now enter 10. Box A ends in ODD because the string contains one 1. Box B ends in EVEN because it merely copies the last bit. The first observation did not identify the computation. It exposed only one trace, a path that several incompatible rules could produce.
The central claim is that computation resides in a lawful organisation of possible state transformations, not in isolated symbols or one observed sequence. Three tests make that claim operational. First, the chosen state must retain enough information for the modelled future. Second, the transition law must cover relevant alternatives, including branches not seen in the current run. Third, a physical or software implementation must preserve those relations under controlled changes, rather than merely admitting a clever retrospective description.
This framing does not reduce every computer to a tiny finite-state diagram. Turing's original machine joined a finite control condition to a tape, a scanned square and a position, creating a potentially unbounded configuration.[1] Modern operational semantics, temporal specifications, probabilistic programs and neural inference all enlarge the state and transition vocabulary. The durable idea is simpler: to explain a computation, say what can be different now, what event may occur, and how that difference constrains what comes next.
The benefit is diagnostic as well as philosophical. When a system surprises us, the framework asks whether the recorded state omitted a relevant fact, whether the transition rule was incomplete, or whether the implementation departed from the rule. Those are different failures and require different repairs.
What a state must remember
Imagine two payment terminals that both display READY. The first has no transaction in progress. The second has already reserved money but has not yet received the merchant's confirmation. Pressing Cancel should leave the first unchanged and release the reservation in the second. If the state description records only the word READY, it merges conditions with different legitimate futures.
This is the first thought experiment: hold the visible label constant while changing one hidden fact. When the appropriate next action changes, the hidden fact belongs inside the state for that purpose. A state is therefore not a decorative status. It is a claim that the distinctions retained now are sufficient to determine, constrain or probabilistically shape the next modelled step once an input arrives.
That sufficiency is always relative to a boundary. A parity detector need not record the entire prefix. It needs only whether the number of ones seen so far is even or odd. A processor instruction requires register values, memory, a program counter and machine mode. A distributed service may require pending messages, leases, clocks and failure assumptions. The microscopic positions of every atom are usually irrelevant to the engineering question, even though they participate in the physical evolution.
State is the smallest explicit distinction set that makes the next-step contract honest. Too little state makes different futures look identical. Too much state obscures the mechanism, inflates verification cost and may expose data that the decision never needed.
A compact formal skeleton
A useful deterministic machine can be written as a tuple:
M = (S, I, O, δ, λ, s₀)
S is the set of states, I the possible inputs, O the outputs, and s₀ the starting state. The transition function δ(s, i) returns the next state after input i in state s. The output function λ says what is observed, either from the state or from a state-input pair. A run over inputs i₀, i₁, … is the sequence s₀, s₁, … where sₜ₊₁ = δ(sₜ, iₜ).
Nothing forces δ to be a single-valued function. A nondeterministic transition relation can permit several successors. A stochastic kernel can assign probabilities P(s' | s, i). A continuous system can evolve through differential equations. The shared burden is to state which current distinctions and incoming conditions govern the future, then specify what counts as a legitimate successor.
Histories become states by sharing a future
There is a sharper way to decide what belongs in a state. Take two different histories and append every possible future input sequence. If the system produces the same future behaviour for every suffix, the histories may be represented by the same state for that task. If one suffix separates them, merging them loses a distinction the computation needs.
For parity, the prefixes 101 and 11 can share the state EVEN. Both contain an even number of ones, so any common suffix will change their parity in exactly the same way. The prefixes 10 and 111 can share ODD. Their surface forms and lengths differ, yet their future relationship to every suffix is identical.
The last-bit machine makes a different compression. It groups histories by their final symbol. That grouping is adequate for the task “report the last bit”, but inadequate for parity. Prefixes 00 and 10 both end in zero, although one has even parity and the other odd. The suffix 0 preserves their disagreement, so a parity machine must keep them in different state classes.
This view gives state a precise job: state is a causal compression of history by future equivalence. Splitting every distinct history into a new state remains correct but wastes structure and may create an unbounded machine. Merging too aggressively creates false equivalences and wrong transitions. Good state design finds the coarsest partition that preserves the future distinctions the task and safety properties require.
The same test applies beyond strings. Two workflow cases may share a state only when every permitted event leads to equivalent obligations, authority checks and effects. Two physical configurations may share an abstract state only when disturbances inside the declared tolerance do not change the relevant successor. State sufficiency is therefore testable through paired histories and common interventions, not merely asserted in a schema.
State is more than a symbol
The label EVEN has no computational power by itself. It could be ink on paper, a voltage interval, a Boolean variable or a word in a log. It becomes part of a computation when the surrounding mechanism treats the distinction consistently. On input 1, the parity machine must move from EVEN to ODD; on input 0, it must remain EVEN. The label is replaceable. The relation is load-bearing.
This is why symbol manipulation, stated without an account of state and transition, feels mysterious. What makes one mark act as an instruction and another as data? The answer comes from the machine configuration. A program counter, control state or evaluation context determines how the current mark participates in the next transformation. Plotkin's structural operational semantics made this explicit for programming languages by giving inference rules whose premises describe component transitions and whose conclusions license a compound transition.[5]
In a Turing machine, the same tape symbol can have different consequences under different control configurations. Turing called the finite control conditions m-configurations, and described a complete configuration using the control condition, tape contents and scanned position.[1] The tape mark does not explain the step on its own. The complete configuration and machine table do.
The reachable-state river
A transition specification contains more states than any single execution will visit. Starting from s₀, the input sequence selects one channel through a larger landscape. The first set of reachable states is the start set. Each later set is obtained by applying allowed transitions to states already reached. For a deterministic machine and a fixed input sequence, the set narrows to one path. Under unknown inputs, nondeterminism or concurrency, it fans out.
R₀ = {s₀}Rₜ₊₁ = {s' : ∃s ∈ Rₜ, ∃i ∈ I, s' ∈ δ(s, i)}
Here Rₜ is the set of states reachable in t steps. The symbol ∃ means “there exists”. This recurrence reveals two practical questions. Which desirable states can never be reached because a guard is missing? Which dangerous states are reachable through an unexpected sequence? A state diagram becomes useful when it answers both.
An invariant is a property intended to hold in every reachable state. “A payment cannot be both settled and cancelled” is an invariant. “Execution requires an unexpired authority token” is another. To prove an invariant, show that it holds initially and that every permitted transition preserves it. The proof works because the transition relation exposes the only legitimate ways the system can change.
Reachability also distinguishes an impossible state from an unobserved one. A state absent from test logs may still be reachable tomorrow. Conversely, a state can be represented in the schema but unreachable from the start under all legal transitions. This difference matters in testing: absence of evidence in traces is not evidence of impossibility.
One transition can contain many smaller transitions
State descriptions also choose a grain of time. An abstract payment transition from SUBMITTED to CONFIRMED may contain message publication, queue delivery, database locking, ledger mutation and readback. At the service boundary those steps may be hidden. Inside the payment platform they are separate states with their own retries and invariants.
A sound abstraction does not require one abstract step to equal one physical instruction. It requires the lower-level sequence to preserve the relation claimed at the higher level. Internal steps that leave the abstract state unchanged are often called stuttering steps. They can be ignored by one observer while remaining crucial to another, provided they cannot violate the higher-level safety property.
This creates a refinement obligation. Map each detailed state to an abstract state, then show that every detailed execution either corresponds to an allowed abstract transition or leaves the abstract observation unchanged. If a low-level retry can debit twice while the abstract model says “still submitted”, the refinement fails even though the final labels look plausible.
Computation can be described at several grains, but the abstraction must preserve the decisions made at its boundary. A compiler, virtual machine and processor may realise the same programme through different step counts. A workflow and its database may expose different state spaces. The right grain is the one at which the claimed invariants, outputs and interventions remain meaningful.
A trace is not a transition law
A trace says what happened. A transition system says what would happen under each relevant state-input combination. The distinction is causal. If a machine followed states A, B, A, B during one run, that sequence does not tell us whether A reliably causes B, whether a clock forced the alternation, or whether an analyst assigned the labels after seeing the data.
Consider a cooling stone observed for seven minutes. Divide its temperature curve into alternating intervals and label them A and B. The stone now “executes” ABABABA on paper. With enough inventive partitions, one trajectory can be mapped onto many automata. The mapping records resemblance between two sequences, but it does not show that the stone would take the required branch if an alternative input arrived or an unvisited state were imposed.
This is the second thought experiment: keep the physical trajectory fixed while changing the retrospective labels. If the alleged computation changes without any change in the mechanism, the description is carrying too much of the explanatory burden. Chalmers used the rock implementation problem to show why an actual trace is insufficient. He argued that genuine implementation must support the relevant state-transition conditionals, including transitions absent from the observed run.[9]
The negative control: a plausible impostor
The last-bit box is a serious negative control because it is not random and it is not broken. It implements a coherent two-state machine. It even matches parity on many strings. Its failure is specific: it preserves the wrong distinction. After reading a prefix, it remembers only the latest symbol, while parity requires the cumulative parity of all ones seen so far.
Testing only 1010 makes the preferred explanation unnecessary. The impostor fits the observation with equal success. Testing all 63 binary strings of length zero through five changes the evidence: the parity machine is correct on 63; the last-bit machine on 33. A discriminating test varies the causal feature the explanation claims to use, here the relationship between prefix history and current state.
Rabin and Scott formalised finite automata as finite collections of states with transition behaviour over tapes, and showed that nondeterministic and deterministic forms can recognise the same languages despite different internal structures.[2] The result is an equivalence under a specified observable, language acceptance. It does not make the step-by-step machines identical.
Different kinds of transition law
Determinism is one point in a larger design space. A nondeterministic relation says that several successors are permitted, which can model unresolved scheduling or abstract away an implementation choice. A stochastic transition assigns probabilities, allowing calibration and expected outcomes to matter. A timed or hybrid system adds clocks and continuous variables. A concurrent system may represent local component moves and synchronisation rather than one global instruction stream.
For concurrent systems, Plotkin-style rules and process calculi describe how local transitions compose. Keller's transition-system method treated control and data states together when verifying parallel programs.[6] Petri nets represent distributed enabling conditions through places, tokens and firing transitions, making concurrency visible without forcing every event into a single arbitrary order.[8]
Lamport's Temporal Logic of Actions takes a related route. An action is a relation between an old state and a new state, written using unprimed and primed variables. A specification combines initial conditions, next-state actions and temporal constraints so that system behaviour is a set of possible state sequences.[7] This is especially useful when no single trace can stand in for all legal interleavings.
Observation decides which equivalence matters
Two machines can differ internally and still be equivalent for one observer. A deterministic and a nondeterministic automaton may accept the same language. Two service implementations may return the same externally visible responses while using different caches and retries. Equivalence must therefore name the observable: final acceptance, emitted outputs, timing, probability distribution, resource cost, or the entire transition trace.
This prevents a common category error. Matching final answers establishes only final-answer equivalence on the tested inputs. It says nothing by itself about latency, intermediate safety, recoverability or the faithfulness of an explanation trace. As the observable becomes richer, fewer machines remain equivalent. Evaluation should select the weakest observable that still protects the decision, then avoid claiming more than it measures.
When matter implements the rule
Abstract transition systems are mathematical objects. Computers are also physical systems: relay contacts move, transistors switch, magnetic domains change and photons propagate. Connecting these levels requires more than noticing that both evolve. It requires a representation that maps selected physical conditions to abstract states and an implementation that preserves the transition structure within stated tolerances.
Let P be relevant physical states, S abstract states, and ρ : P → S a representation map. Let Hᵢ be the physical evolution under input i, and δᵢ the abstract transition. A basic implementation test asks whether:
ρ(Hᵢ(p)) ≈ δᵢ(ρ(p))
The approximation sign matters. A voltage does not need one exact microscopic value to represent 1; it needs to remain inside a robust region that the next circuit stage interprets consistently. The equation must hold across the relevant state-input domain, not merely at points sampled from one successful run. It also needs a declared time scale. Reading too early, after metastability or before a handshake completes, can produce an abstract transition that the physical mechanism has not yet settled.
Horsman, Stepney, Wagner and Kendon formalise physical computation through relations between physical systems and abstract evolutions, with an explicit representation step rather than an assumption that all physical change computes.[10] Stepney and Kendon later make the representational entity explicit and examine who or what establishes and uses the relation.[11]
Multiple realisations, one relation
The parity machine can be implemented with relays, transistor gates, a mechanical wheel, software variables or marks moved by a person following a table. The physical details differ. What is preserved is the two-way distinction and the input-conditioned transition pattern. Shannon showed how Boolean algebra could express relay and switching circuits, connecting symbolic relations to physical switching arrangements.[3] Mealy's sequential-circuit synthesis treated output and next state as formal functions of present state and input.[4]
Multiple realisability does not mean arbitrary realisability. A pencil mark can represent EVEN, but a static page does not by itself update the mark when a new bit arrives. A human following the rule supplies the transition mechanism. Likewise, a log entry can describe a service state without controlling it. The implementation boundary must include the components that sense input, preserve state, perform the transition and expose the result.
Logical merging has physical consequences
State transformation also clarifies logical irreversibility. If two distinct prior states map to one successor, the successor alone cannot identify which prior state occurred. Landauer connected such logical irreversibility, particularly erasure, to a minimum thermodynamic cost under specified assumptions.[12] Bennett showed that ordinary computation can be simulated reversibly by retaining enough history and later uncomputing intermediate information.[13]
The boundary is important. Logical reversibility does not guarantee a fabricated device dissipates no energy, and Landauer's bound is not the energy consumed by every state transition. The papers support a narrower lesson: the many-to-one shape of an abstract transition can matter to the physical cost of reliably implementing it. Formal structure and material mechanism are distinct, yet they are not unrelated.
Build and break the machine
The parity detector is deliberately small enough to inspect completely. Its state set is {EVEN, ODD}. It starts in EVEN because the empty prefix contains zero ones. Reading 0 preserves the current state. Reading 1 toggles it. The final state is also the output.
| Current state | Input | Parity next state | Last-bit next state |
|---|---|---|---|
| EVEN | 0 | EVEN | EVEN |
| EVEN | 1 | ODD | ODD |
| ODD | 0 | ODD | EVEN |
| ODD | 1 | EVEN | ODD |
The first two rows do not separate the machines. Their disagreement appears only after the prefix has placed the machine in ODD. This shows why tests should cover state-input pairs rather than only raw examples. A dataset can contain many inputs while still missing the branch where a hypothesis earns its keep.
Interactive state-machine simulator
The laboratory below executes both transition laws. Step through a string to inspect the state trace, then run the exhaustive counterfactual suite. The positive case is 1010, where both machines finish EVEN. The negative case is 10, where parity finishes ODD and the last-bit impostor finishes EVEN. The exhaustive test generates every binary string of length zero through five and compares each machine with the mathematical parity oracle.
Configure and run
Trace and counterfactual evidence
| Step | Input | Before | After |
|---|---|---|---|
| 0 | start | EVEN | EVEN |
The simulator reveals logic that prose can hide. Both machines use the same state names, input alphabet and output vocabulary. Only two transitions differ. That small change is enough to alter the function. The artefact also demonstrates a general evaluation principle: match the preferred mechanism with a coherent alternative, then choose cases that force their state summaries to disagree.
Runnable core, assumptions and expected output
Assumptions. Inputs are finite binary strings. Both machines start in EVEN. The output is the terminal state. The oracle labels a string ODD when it contains an odd number of ones.
Expected output. The positive case 1010 returns EVEN for both machines. The negative case 10 returns ODD for parity and EVEN for the last-bit machine. Exhaustive testing through length five gives 63/63 and 33/63.
const machines = {
parity: {
EVEN: { "0": "EVEN", "1": "ODD" },
ODD: { "0": "ODD", "1": "EVEN" }
},
lastBit: {
EVEN: { "0": "EVEN", "1": "ODD" },
ODD: { "0": "EVEN", "1": "ODD" }
}
};
function run(machineName, input) {
if (!/^[01]*$/.test(input)) throw new Error("Binary input only");
let state = "EVEN";
const trace = [{ step: 0, symbol: "start", before: state, after: state }];
for (const [index, symbol] of [...input].entries()) {
const before = state;
state = machines[machineName][state][symbol];
trace.push({ step: index + 1, symbol, before, after: state });
}
return { state, trace };
}
const parityOracle = input =>
[...input].filter(symbol => symbol === "1").length % 2 ? "ODD" : "EVEN";
function allBinaryStrings(maxLength) {
const strings = [""];
for (let length = 1; length <= maxLength; length += 1) {
for (let value = 0; value < 2 ** length; value += 1) {
strings.push(value.toString(2).padStart(length, "0"));
}
}
return strings;
}
console.assert(run("parity", "1010").state === "EVEN");
console.assert(run("lastBit", "1010").state === "EVEN");
console.assert(run("parity", "10").state === "ODD");
console.assert(run("lastBit", "10").state === "EVEN");
for (const name of Object.keys(machines)) {
const cases = allBinaryStrings(5);
const passed = cases.filter(input => run(name, input).state === parityOracle(input));
console.log(`${name}: ${passed.length}/${cases.length}`);
}
From toy machine to controlled action
A two-state detector is easy to exhaust. A consequential workflow is larger, but the same discipline applies. Consider a synthetic address-change service in which a language model may interpret evidence and propose an update. The model is not allowed to turn fluent text directly into an effect. The system separates request, evidence, proposal, authority, action and verified outcome into distinct states.
A customer asks to change an address. The system resolves identity, reads the current record, checks acceptable evidence, lets a model draft a structured proposal, obtains the required approval, submits an idempotent command, and reads the source system back. A network interruption after submission leads to UNKNOWN OUTCOME, not an invented success or an automatic retry.
The full state must carry more than a status string. It includes intent, identity, the version of world state read, the authorised evidence set, the model proposal, the decision right exercised, the action identifier, and any effect receipt. Context used for reasoning is not automatically authority. A successful API response is not automatically a verified business outcome. Each distinction changes which transition is legal next.
Three invariants govern the path. First, no state after PROPOSED is reachable without a valid authority record. Second, the command's idempotency key is stable across recovery, preventing duplicate effects. Third, CONFIRMED is reachable only after readback shows the intended address and the expected record version. These rules give tests somewhere precise to attach.
Notice how state design changes the architecture. A free-form agent transcript cannot reliably answer whether evidence was current, whether approval applied to this exact proposal, or whether the source system changed. A typed case state can. The language model remains useful for interpretation and drafting, while a deterministic transition layer decides which state changes are permitted.
For compound AI workflows, a state-first specification with explicit unknown-outcome handling should reduce duplicate effects and false completion claims compared with transcript-led orchestration. That expectation is plausible, but it needs matched incident and recovery studies rather than architecture rhetoric.
Where the abstraction fails
“Everything changes state” is a valid objection. A falling stone, a storm and a brain all move through physical state spaces. If state transformation alone defined computation, the concept would spread until it explained nothing. The three tests prevent that collapse: the state abstraction must be adequate for a task, the transition law must cover relevant counterfactuals, and the implementation relation must be stable enough to support use, prediction or control.
Even with those constraints, a small finite-state machine can be the wrong instrument. Four pressures matter most.
Hidden state. If two histories mapped to one state produce different futures under the same input, the state is insufficient. The repair may be to add memory, use a belief state over hidden conditions, or admit partial observability rather than pretending the process is Markovian.
Concurrency. Enumerating one global state for every combination of component states causes state explosion. Petri nets, process algebra, partial-order reduction or compositional verification may preserve independence more economically. A single sequence can also invent an order between events that were genuinely concurrent.
Time and continuity. A discrete transition may hide duration, deadlines, control dynamics or unsafe transient regions. Timed automata, hybrid systems and differential models are better when the path between labelled states changes the outcome. Sampling faster does not automatically solve the modelling problem.
Changing laws. A learning system updates parameters, tools or policies, so the transition mechanism itself changes. One can expand the state to include parameters and release versions, but the model may become too large to explain or verify directly. The state-transition view remains useful around the system's control envelope, release gates and observable actions without claiming a neat finite diagram of every internal activation.
The state-machine account ceases to help when the proposed state cannot be made future-sufficient at a usable scale, or when the transition abstraction removes timing, interaction or continuous dynamics that determine the decision. At that point, enrich the formalism or change the system boundary. Do not force the phenomenon into a tidy diagram.
Open, interacting computation adds another complication. Classical Turing machines are commonly presented as closed calculations over a supplied input. Reactive Turing machines and process-theoretic models extend the transition perspective to ongoing interaction, where observations and actions continue to arrive.[14] The state-transformation thesis survives, but the run is no longer a single input followed by a final answer.
The state-transition adequacy card
Use this instrument before choosing an orchestration framework, model architecture or verification tool. It is intentionally demanding. A blank answer identifies a modelling debt, not a documentation inconvenience.
| Test | Question to answer | Evidence that passes | Warning sign |
|---|---|---|---|
| Boundary | What system and time scale does the state describe? | Components, environment assumptions and observation points are named. | The boundary changes whenever a failure appears. |
| Sufficiency | Can equal states have different legitimate futures under the same input? | Hidden-history tests find no decision-relevant divergence, or uncertainty is explicit. | A transcript or status label carries facts the schema omits. |
| Transition law | Which event, guard and rule permit each next state? | A total table, relation, rule set or stated exceptional domain. | “The agent decides” replaces the mechanism. |
| Alternatives | What happens on branches absent from the happy-path trace? | Counterfactual cases cover state-input pairs, timeouts and conflicting events. | Evaluation contains only successful demonstrations. |
| Reachability | Which states must be reachable, and which must never be? | Reachability analysis, invariants and explicit terminal conditions. | Forbidden states exist only as comments. |
| Implementation | How do software or physical conditions map to abstract states? | Read/write criteria, tolerances, timing and intervention tests are defined. | Labels are assigned retrospectively from logs. |
| Outcome | How is an accepted action distinguished from a verified effect? | Effect receipts, readback and an unknown-outcome state. | HTTP success or fluent text is treated as completion. |
| Change | What happens when the transition law, model or policy version changes? | Versioned state, migration rules, replay tests and rollback boundaries. | Old cases silently continue under new semantics. |
Decision instrument. Design inference. These questions convert the causal claim into an architecture and evaluation review; they are design prompts, not a certification standard.
A small system may answer the card with one transition table and a dozen tests. A distributed service may need temporal logic, model checking and failure injection. A learned system may answer some rows statistically and reserve consequential transitions for deterministic control. The artefact scales by changing the evidence, not by weakening the questions.
The key architectural decision is whether the state and transition boundary matches the consequence boundary. If a model can suggest text but cannot directly alter the world, the proposal state may be probabilistic while the authority and action transitions remain mechanical. If an actuator can create irreversible harm, implementation tolerances and outcome verification deserve more effort than a polished internal rationale.
Compact glossary
- State
- A selected description of current conditions intended to retain the distinctions needed for future behaviour at a declared boundary.
- Transition
- A permitted change from one state to another, conditioned by an input, event, guard, probability or continuous law.
- Trace
- One realised sequence of states and events. It is evidence about a transition system, not the whole system.
- Reachability
- Whether a state can occur from the initial conditions through a legal sequence of transitions.
- Invariant
- A property intended to hold in every reachable state and preserved by every permitted transition.
- Implementation relation
- The mapping and causal organisation by which physical or software conditions realise an abstract transition structure.
Design the possible transitions before naming the intelligence
The parity puzzle changes the order of explanation. Do not begin with a symbol, an output or a fluent trace and ask what intelligence it resembles. Begin with the state distinctions, the permitted transitions and the counterfactual branches. Then ask whether the implementation preserves that organisation under the inputs, disturbances and time scales that matter.
A computation is defensible when three layers line up: an adequate state, a lawful space of alternatives, and an implementation that survives intervention. The first prevents hidden history from being erased. The second separates a machine from one lucky path. The third stops arbitrary physical change or retrospective labelling from doing all the explanatory work.
For research, this means designing discriminating inputs before celebrating a result. For software, it means specifying reachability, invariants and unknown outcomes before choosing an orchestration library. For AI systems, it means keeping model proposals separate from authority and verified effects. The practical programme changes from “make the system produce the answer” to “make every consequential state change explicit, testable and recoverable.”
That discipline does not explain every dynamical system, nor does it settle the philosophy of physical computation. It does something more useful for the next design decision: it reveals what the current explanation commits us to, which alternative would defeat it, and where the mechanism must be observed to earn the word computation.
References and source ledger
Open the source register and extended notes
- Primary paper. Turing, A. M. “On Computable Numbers, with an Application to the Entscheidungsproblem,” 1936. Primary journal record.
- Primary paper. Rabin, M. O., and Scott, D. “Finite Automata and Their Decision Problems.” IBM Journal of Research and Development, 3(2), 1959, 114–125. DOI record.
- Primary thesis and paper. Shannon, C. E. “A Symbolic Analysis of Relay and Switching Circuits.” Massachusetts Institute of Technology. MIT archive.
- Primary paper. Mealy, G. H. “A Method for Synthesizing Sequential Circuits.” Bell System Technical Journal, 34, 1955, 1045–1079. DOI record.
- Foundational technical report and journal republication. Plotkin, G. D. “A Structural Approach to Operational Semantics.” Aarhus University, 1981; Journal of Logic and Algebraic Programming, 60–61, 2004, 17–139. DOI record.
- Primary paper. Keller, R. M. “Formal Verification of Parallel Programs.” Communications of the ACM, 19(7), 1976, 371–384. DOI record.
- Primary paper and official author summary. Lamport, L. “The Temporal Logic of Actions.” ACM Transactions on Programming Languages and Systems, 16(3), 1994, 872–923. DOI record; official summary.
- Authoritative survey. Murata, T. “Petri Nets: Properties, Analysis and Applications.” Proceedings of the IEEE, 77(4), 1989, 541–580. DOI record.
- Peer-reviewed competing analysis. Chalmers, D. J. “Does a Rock Implement Every Finite-State Automaton?” Synthese, 108, 1996, 309–333. DOI record; author-hosted text.
- Primary theoretical framework. Horsman, D., Stepney, S., Wagner, R. C., and Kendon, V. “When Does a Physical System Compute?” Proceedings of the Royal Society A, 470, 2014. DOI record; preprint.
- Primary theoretical extension. Stepney, S., and Kendon, V. “The Representational Entity in Physical Computing.” Natural Computing, 20, 2021, 267–284. DOI record.
- Primary physics paper. Landauer, R. “Irreversibility and Heat Generation in the Computing Process.” IBM Journal of Research and Development, 5(3), 1961, 183–191. DOI record.
- Primary physics and computation paper. Bennett, C. H. “Logical Reversibility of Computation.” IBM Journal of Research and Development, 17(6), 1973, 525–532. DOI record.
- Primary theory paper. Baeten, J. C. M., Luttik, B., and van Tilburg, P. “Reactive Turing Machines.” Information and Computation, 231, 2013, 143–166. DOI record; author preprint.