locus · logic lane · 2026-10-09

The same fork, later

A logic of place and link that follows individual nodes through the reactions of a bigraphical reactive system, with every verdict checked by Lean's kernel.

1. Bigraphs in one paragraph

A bigraph has nodes, each with a control (its kind: phil₀, fork, table) and a number of ports. The place graph is a forest: every node lies inside another node or directly in a region. The link graph puts each port on a link: a private edge or an outer name. A reaction rule R → R′ replaces an occurrence of the pattern R (the redex) by R′ (the reactum); holes in R (sites) match arbitrary content, the parameter, which the rule moves. In locus every rule is linear: each piece of parameter is used at most once. Nodes and edges are numbered, and agents that differ only by renumbering are support equivalent, a ≏ b.

2. What the literature offers

Condensed from a survey of about ninety verified references (docs/research/spatial-behavioural-logics.md).

Spatial logics describe shape at one moment

BiLog for bigraphs, the ambient logic and the spatial logic of the π-calculus can say "this agent is two parallel parts, one satisfying A, the other B". They describe the shape of a state precisely. Their dynamics is at most a next-step modality, and none follows an individual node through time.

They are also, provably, not logics of behaviour. A logic that can say "exactly two parallel parts" can count and inspect components, so two agents that behave alike but are built differently satisfy different formulas: the logic's notion of "the same" is same structure (Sangiorgi 2001; Hirschkoff, Lozes and Sangiorgi 2008). For bigraphs that is ≏, not bisimilarity. This is why we do not ask the new logic to characterise an equivalence.

Located modal logic observes where actions happen

For CCS with localities (Boudol, Castellani, Hennessy and Kiehn 1993), modalities record the location of an action, and logical equivalence is location equivalence. Locations there are labels on actions, not a space that evolves.

Graph-transformation logics follow entities

Temporal logics for graph rewriting with variables for nodes and edges, carried along each step by a counterpart map (Gadducci, Laretto and Trotta 2023/2026, mechanised in Agda; earlier Distefano, Rensink and Katoen 2002). When the counterpart maps are partial functions, the usual laws of fixpoint logic hold. This is the template we port.

For bigraphs: nothing that tracks

No published bigraph logic quantifies over the same node or link across reactions. Tracking maps exist only inside tools.

3. The model: tracked rules and tracked reactions

A tracked rule is a rule with a tracking list τ of pairs (u, w): redex item u becomes reactum item w. It must be well formed: no item twice on either side, nodes to nodes, edges to edges.

For a reaction a → a′ through a decomposition a = D ∘ (R with parameter d), the tracking map f sends each node or edge of a to its counterpart in a′, or nowhere:

We write a →^t_f a′ for a reaction with tag t and tracking map f. Outer names are fixed by the interface and are not tracked.

structure TrRule (α Ctrl : Type) where
  rule : RuleD Ctrl          -- the simulator's rule, unchanged
  tag  : Option α            -- action tag (none = internal)
  τ    : List (Nat × Nat)    -- redex item u becomes reactum item w

Proved (trackDefined). Every library reaction has a tracking map, and with well-formed τ every tracking map is one-to-one and sends nodes to nodes and edges to edges. Linearity is what makes this true: a copied parameter would have two counterparts.

4. The logic

Variables x, y range over nodes, ℓ over links, X over sets of states.

Meaning. A formula holds at a state with a valuation of its variables.

• ∃x. φ: φ holds for some node x present now (likewise ∀, and ℓ for links).
• ⟨t⟩φ: for some step a →^t_f a′, φ holds at a′ with every variable moved along f. [t]φ: for every such step. ⟨→⟩ and [→] ignore the tag.
• μ and ν are least and greatest fixpoints. Two abbreviations: EF ψ := μX. ψ ∨ ⟨→⟩X (ψ is reachable) and AG ψ := νX. ψ ∧ [→]X (ψ always holds).
• Deleted entities. If a step deletes the node a variable points to, the variable becomes undefined and every atom mentioning it is false thereafter. "x still exists" is x = x. (The "dead variable" reading of Distefano, Rensink and Katoen.)

| ρ, a, σ, .dia t φ => ∃ a' f, TrReact S trs t a a' f ∧ PSat trs ρ a' (σ.tr f) φ
| ρ, a, σ, .box t φ => ∀ a' f, TrReact S trs t a a' f → PSat trs ρ a' (σ.tr f) φ
-- σ.tr f : move every variable along the tracking map f

Proved (psatInv). Renumbering a state, with its variables, changes no truth value. The logic is about bigraphs up to ≏.

5. Checking, and why the verdicts are theorems

Asking the kernel to search a state space does not finish, so locus checks models by certificate:

1. An untrusted, compiled program explores the reachable states and writes a certificate as literal data: the states, and for each matcher step its target, a renumbering witness, and its tracking list.
2. A Boolean checker, run by the kernel, confirms each step with one run of the matcher and recomputes each tracking list from the matcher's output. Nothing is searched.
3. An evaluator computes the formula's truth value on the certificate's finite graph.

Proved (trackSoundAll). If the checker accepts and the evaluator says φ is true at a listed state, φ is true there in the library's semantics, for every formula. The rules must satisfy three conditions, each checked by decide:

• G1: every redex region contains a node (the matcher's completeness condition, proved earlier as cocc_G1);
• no idle redex edge: every edge of a redex has a point. Otherwise a rule matched against two pointless edges may delete either, and the two tracking maps differ by a symmetry no renumbering of the result removes;
• well-formed tracking lists.

The core is tracked matcher completeness (trCOcc): every tracked library reaction is found by the matcher, with the same tracking map, up to renumbering. Without it a certificate could leave out a step and make a "for every step" formula look true.

False verdicts, by duality (psat_dual, trackFalse). Swapping ∧/∨, ∃/∀, ⟨⟩/[], μ/ν and p/¬p gives the dual of a formula; we prove, constructively, that a true dual makes the formula false. "φ is false" is certified by checking its dual true.

The simulator's matcher and the existing proofs about it are unchanged. The tracked proof reuses them by import and does not replace them: it has extra side conditions, so it does not subsume cocc_G1.

6. The dining philosophers, fork by fork

Three philosophers, three forks, the fair protocol: pick up the left fork, then the right, eat, put both down; a hungry philosopher whose right fork is taken puts its left fork back. Philosophers and forks are tracked; their states are not. Writing onTable(x) := ∃y. ctrl(y)=table ∧ prnt(x,y) and heldBy_j(x) := ∃q. ctrl(q)=phil_j ∧ prnt(x,q):

All six are theorems about the library meaning at the initial state, proved from one 14-state certificate in about 64 seconds of kernel time. With the same rules but no tracking, "returns", "pickSame" and "forksPersist" come out false: after one step the variable has no counterpart, so "the same fork later" cannot be said at all. The gate has been watched failing: corrupting one entry of one tracking list makes the certificate check fail.

7. The alternating bit protocol, message by message

The ABP sends messages over two lossy one-place channels and retransmits until acknowledged. Retransmission shapes the model: a copy of a message is a new node, since linear rules cannot duplicate one. So a message's identity is a link.

• accept creates a message node on a fresh edge: that edge is the message.
• send puts a new copy, on the same link, into the channel.
• deliver hands a node on that link to the user, who later consumes it.

held(ℓ): the sender holds a message on link ℓ; out(ℓ): the user holds one. The model has 224 states and 39 linear rules.

Certified without the kernel exploring anything

Compiled code explores the states and computes every verdict; the kernel only checks certificates, with four checkers each proved sound:

Twelve verdicts in all, eight TRUE and four FALSE (the others: heldStable, dupEntry, dupStep and canDeliverC TRUE; noStrayStrict and canDeliverHeldC FALSE), checked in about six minutes over separately built modules of under 4 GB each, every checker watched rejecting a corrupted certificate. With tracking ignored the model is weakly bisimilar over rule tags to the one-place buffer (accept and deliver visible; messages carry no data): proved, abpTrack_wbisim_buff, built on demand.

A finding: with nothing of any redex tracked, only heldStable changes verdict. Message links mostly survive a step in the context, which is tracked automatically; only the rules that delete a copy need their own tracking.

8. Exactly what is proved

About 4,200 lines of Lean in Logic/Track*.lean; the dining certificate is Logic/Examples/M1Prime/DiningTrackCert.lean. Open: completeness of the checker itself (not needed, since false verdicts go through duality).

9. What is known and what is not

APPARENTLY NEW means searched for and not found. It is not a claim of originality; that decision is Matthew's.

10. Limits

• Closed systems. The logic speaks of one system's own reactions, not of behaviour inside a larger context, (Since this was written: its logical equivalence is support equivalence ≏, theorem c1.)
• Finite state spaces for certified checking. The dining example has 14 states; nothing larger has been tried with tracking.
• Rule conditions. Linear rules, G1, no idle redex edge, and a tracking list chosen by the modeller (or computed and then checked, as here).
• Next. Miolingo, once its data and computation design settles. "Until" needs nothing new: φ U ψ := μX. ψ ∨ (φ ∧ ⟨→⟩X).

Source of record: docs/logic-tracked.md in the locus repository, with statuses in docs/logic-statements.md. Reproduce with lake build Logic and lake env lean Logic/Examples/M1Prime/DiningTrackCert.lean.