Part 2 — Modeling  ::  Chapter 7

2.3 Behavioral Models: What May Happen?

Behavioral models add time. They represent states, transitions, and legal sequences while suppressing the implementation that realizes them. Where a structural model holds the system still, a behavioral model asks what it is allowed to do, and in what order.

DocAble's recovery path provides a compact example. Suppose processing fails after the system has prepared a fallback artifact. Recovery must eventually make that artifact durable and update the database to point to it. The engineering question is not how the upload client works or how the database transaction is implemented.

MODEL CARD

Recovery-ordering model · Behavioral

The relevant model contains three states, and Figure 2.3-1 draws them in order: FALLBACK_STAGED, then FALLBACK_UPLOADED once the upload succeeds, then DB_UPDATED once durable state is written. The most important fact in the model is an edge that does not exist — the jump from FALLBACK_STAGED directly to DB_UPDATED, drawn broken and marked not legal. That missing edge is an engineering obligation: recovery may not declare the database update complete while skipping durable publication of the artifact it names.

Recovery-ordering model: three legal states and one forbidden edge Three states in legal order. FALLBACK_STAGED transitions on upload success to FALLBACK_UPLOADED, which transitions when durable state is updated to DB_UPDATED. The load-bearing fact is a forbidden edge: FALLBACK_STAGED may not go directly to DB_UPDATED. Durable state may not name an artifact recovery has not yet published. RECOVERY MODEL FALLBACK_STAGED upload succeeds FALLBACK_UPLOADED durable state updated DB_UPDATED forbidden / absent transition not part of the model The load-bearing fact is the edge that does not exist. The fallback artifact must become durable before database state may refer to it.
Figure 2.3-1. Recovery-ordering model. The fallback artifact must become durable before database state may refer to it. The load-bearing fact is the absent transition from FALLBACK_STAGED directly to DB_UPDATED.

The production implementation encodes this model as an explicit transition relation. That encoding can be executed, tested, and checked. But the model is not the transition-table syntax. The implementation contains uploads, exceptions, retries, logging, persistence, and other concerns; the model removes them to preserve one property: the fallback artifact becomes durable before database state may refer to it.

Executability does not change the underlying abstraction. It lets machines run, test, and check the representation without changing the reduction it expresses. Figure 2.3-2 reads top to bottom: the engineering question yields the reduced model, the model is realized as an explicit legal-transition relation, and only beneath that sits the implementation of uploads, persistence, retries, and error handling.

Model first, encoding second: the model is the legal-transition relation, not its syntax A vertical ladder of four layers. The engineering question: can durable state name an artifact recovery has not yet published? The model: a legal chain from STAGED to UPLOADED to DB_UPDATED, with a forbidden bypass edge from STAGED directly to DB_UPDATED. The encoding: an explicit legal-transition relation. The implementation: upload, persistence, retry, logging, error handling. The model is the reduced relation, distinct from the syntax and code that encode it. ENGINEERING QUESTION Can durable state name an artifact recovery has not yet published? MODEL STAGED UPLOADED DB_UPDATED may not skip publication ONE EXECUTABLE REPRESENTATION explicit legal-transition relation IMPLEMENTATION upload + persistence + retry + logging + error handling + … The behavioral model is the reduced legal-transition relation — not the syntax used to encode it. Its value: making one temporal obligation explicit.
Figure 2.3-2. Model, representation, implementation. The engineering question determines a reduced temporal model; an explicit transition relation is one executable representation of that model; implementation adds the operational machinery omitted by the reduction.

An explicit behavioral model does more than name legal transitions. It gives a checker an object over which larger behavioral claims can be stated. The simplest question is local: is this transition permitted? A transition primitive can answer that directly. A stronger question ranges over reachable states: can any legal sequence leave the system with two owners, a stale lease, or some other forbidden combination? Once the states and transitions are explicit, a checker can explore those sequences rather than waiting for a test author to guess the right one.

Some properties are different again. "This state never occurs" is a safety claim: one counterexample trace is enough to refute it. "Every submitted job eventually terminates" is a liveness claim: no finite successful trace establishes that the system cannot remain stuck forever. Those questions may require different checking machinery, but the modeling move is the same. First construct the reduced behavioral object on which the property can be stated.

A state machine can also support formal reasoning. The engineering objective is to make the relevant property explicit in a defined behavioral model so that an appropriate checker can evaluate it. Figure 2.3-3 places the three question classes side by side.

Behavioral models expose different classes of properties A single behavioral model of states, transitions, and legal sequences forks into three property questions. A local rule asks whether an edge is legal and is answered by a transition check. A reachable-state question asks whether a state can occur and is answered by a state-space search. A temporal property asks whether something will eventually occur and is answered by temporal model checking. All three converge on evidence about behavior. Same model family; different property, different checker. BEHAVIORAL MODEL states · transitions · legal sequences LOCAL RULE REACHABLE-STATE TEMPORAL PROPERTY is this edge legal? can this state occur? will this eventually occur? transition check state-space search temporal model checking EVIDENCE ABOUT BEHAVIOR Same model family; different property, different checker.
Figure 2.3-3. Behavioral models expose different classes of properties. A transition relation can support local legality checks, reasoning over reachable states, or temporal claims over executions. The appropriate checker follows from the property; richer machinery is not automatically stronger for every question.

The recovery ordering is a sharp slice of a larger behavioral model. A DocAble job also carries a full lifecycle — queued, leased, remediating, awaiting-merge, completed or failed — with its own legal transitions and its own invariants. The full lifecycle answers broader workflow questions; the three-state recovery ordering is the sharper reduction for crash-safe publication.

The next chapter turns from what may happen, and in what order, to ownership: who may hold the work while it happens, and for how long.

© James C. Davis, 2026–present