T2-2: Behavioral / trajectory verification layer

[rororowyourboat]

Problem

Structural verification confirms well-formedness. It cannot confirm behavioral correctness. A structurally correct specification can exhibit invariant violations, non-convergence, or inadmissible outputs. Behavioral checks bridge structural verification and full V&V.

Type

[MATH] [DOC] [CODE]

Prioritization

• Criteria: C2 (Completeness), C3 (Production readiness)
• Tier: 2 — Medium Priority
• Phase: 4 — Analysis & Behavioral
• Dependencies: T1-1, T0-1
• Blocks: T3-1, T3-3

Design — Representation-Agnostic Abstract Predicates

Two core check classes over opaque channel trajectories:

Check	Abstract Predicate	Concretized by DSL
BV-001	∀t: P(v[t]) holds on channel c	DSL registers P; e.g., stockflow: stock ≥ 0
BV-002	∃t* ≤ N: Eq(v[t*], v[t*-1]) (fixed-point)	DSL registers Eq; e.g., steady-state

The core provides check structure; DSLs provide concrete predicates.

Steps

1. Define BV-001 and BV-002 as abstract predicate schemas over opaque channel trajectories. Channel values are opaque to the core.

2. Define BehavioralPredicate protocol. DSL authors implement to supply concrete predicates:

   class BehavioralPredicate(Protocol):
       channel: str
       check_type: Literal["invariant", "fixed_point"]
       def evaluate(self, value: Any) -> bool: ...
       def converged(self, prev: Any, curr: Any) -> bool: ...

3. Build abstract check runner in gds-analysis. Executes compiled SystemIR under ExecutionContract, records channel trajectory, evaluates registered predicates. Does not inspect channel values.

4. DSL predicate registrations. Each DSL registers concrete predicates:

   • stockflow: non-negativity (BV-001), steady-state (BV-002), conservation (DSL-specific)
   • control: output admissibility (BV-001), setpoint convergence (BV-002)
   • games: rationality (BV-001), equilibrium reached (BV-002)

5. Document the two-level structure. Framework = abstract BV-001/BV-002 + runner. DSLs = concrete predicates. Framework claims nothing about appropriate predicates.

DSL-Level Instantiations (not part of core — documented for context)

DSL	BV-001 example	BV-002 example	DSL-specific checks
stockflow	Stock ≥ 0	Steady state	Conservation Σ stocks = const
control	y ∈ Y_admissible	Converges to setpoint	Stability margin
games	Rationality	Equilibrium in N rounds	Nash condition
owl	SPARQL ASK invariant	Graph unchanged	SHACL satisfaction

Deliverables

• BV-001 and BV-002 formal definitions
• BehavioralPredicate protocol
• Abstract check runner in gds-analysis
• DSL predicate registrations (stockflow, control, games)
• Documentation
• Tests

---

Part of the GDS-Core Improvement Roadmap

Scientific Context

Evidence level: Level 3 (Behavioral) — bridges "the spec is well-formed" and "the system behaves correctly." This is where GDS moves from structural verification to behavioral verification.

The abstract predicate framework (BV-001 universal invariant, BV-002 existential fixed-point) is intentionally minimal and representation-agnostic. The core says nothing about what predicates are appropriate — that is always the DSL author's domain judgment. This makes the behavioral framework as general as the composition algebra itself.

Verification Strategy

Falsification test suite. Construct systems that are structurally correct but behaviorally pathological:

System	Structural	Behavioral	Expected
Stock-flow with negative stock	G/SC pass	BV-001 (non-negativity) FAIL	Structural ✓, behavioral ✗
Control system that diverges	G/SC pass	BV-002 (convergence) FAIL	Structural ✓, behavioral ✗
Thermostat oscillating forever	G/SC pass	BV-002 (steady-state) FAIL	Structural ✓, behavioral ✗
Well-designed thermostat	G/SC pass	BV-001 + BV-002 pass	Both ✓

Each row demonstrates the gap between structural and behavioral verification. A system that passes structural but fails behavioral is not a bug — it is the verification pyramid working as designed.

DSL predicate correctness. For each DSL predicate registration (stockflow non-negativity, control admissibility, etc.), verify against known-good and known-bad trajectories.

Showcase

The falsification table IS the showcase — it demonstrates concretely that structural verification is necessary but not sufficient, and that behavioral checks catch real pathologies. This is the evidence for the verification pyramid (T1-4).