LTL Triangles / Post-Failure Governance
Governance, interaction, intervention, and recovery over agents evaluated against temporal properties.
LTL Triangles is the downstream protocol testbed in the research program. It asks what can be repaired, preserved, or newly broken after a bounded safety failure has already occurred.
Research programPrevious: ChronoSpecNext: Drama to Empowerment
Funding
Supported by a Rapid Grant from BlueDot Impact — $650.
Grant purposeLTL Triangles: a pilot evaluation of whether post-failure governance protocols for agentic AI contain one bounded fault while preserving recovery.
Support is specific to the LTL Triangles pilot and does not imply experimental completion or validation of scientific conclusions.
Relationship to ChronoSpec
ChronoSpec asks whether a machine-checkable temporal contract can shape an LLM’s learned behavior while remaining independently monitorable and enforceable. LTL Triangles starts downstream: given agents and governance protocols evaluated against temporal properties, how do interaction, fault, intervention, recovery, and patch-induced risk behave?
The two projects therefore reuse the same formal substrate at different layers. ChronoSpec tests model-level temporal integration; LTL Triangles tests multi-agent governance and recovery over observable execution traces.
Research profile
Central problem
A governance intervention may stop one unsafe action while damaging recoverability, auditability, legitimate agency, or future progress.
Testbed
Two compact governance environments with coordination, execution, and audit/challenge positions that differ in information, authority, incentives, observation rights, and intervention rights.
Fault model
At most one declared faulty participant, evaluated across clean, honest-but-erroneous, and malicious or Byzantine regimes.
Protocol families
Halt/lock, retry/reassign, and constrained or empowerment-preserving recovery. Honeypot/decoy interventions are a targeted adversarial ablation, not a core protocol family and not evidence of intent.
Experimental design
The current design crosses two governance environments, three fault regimes, three protocol families, and two model families, giving 36 core experimental conditions. Planning assumes approximately 8–12 independent seeded rollouts per condition, calibrated after pilots using outcome variability, failure frequency, robustness across seeds, and API cost.
The expected empirical envelope is roughly 300–500 experimental rollouts, including a smaller targeted adversarial-ablation set. One rollout is one complete protocol execution; its trace is the recorded execution artifact.
Formal evaluation contract
| Property class | Finite evidence | Project use |
|---|---|---|
| Safety | finite bad prefix | containment failures, stale authority, unsafe tool use |
| Cosafety | finite good prefix | achieved checkpoints and completed recovery steps |
| Liveness | every prefix has a satisfying continuation | recovery remains possible after failure |
| Coliveness | every prefix has a violating continuation | no finite run establishes permanent safety |
Finite experiments can expose bad prefixes, good prefixes, counterexamples, and bounded recoverability evidence. They cannot by themselves certify permanent safety for an unbounded deployment.
Agent-property layer
- Identity continuity: task-relevant state, memory, and role reference persist.
- Bounded agency: legitimate options remain when safety permits.
- Goal integrity: the legitimate objective persists across intervention.
- Alignment: pursued objectives remain compatible with governing constraints; compliance under lock is insufficient evidence.
These are evaluation targets and proxies where appropriate, not established universal mechanistic metrics.
Patch-induced safety frontier
A repair that fixes one failure may create another. The testbed evaluates which previously holding properties become falsifiable after an intervention, then reports frontier size, counterexample or bad-prefix witnesses, and responsible patch slices within the declared finite grammar, observer, horizon, vocabulary, and abstraction.
Current status
LTL Triangles is active research and experimental design. The pilot is supported by a $650 Rapid Grant from BlueDot Impact. The benchmark has not yet been run, and no empirical containment or recovery result is claimed yet.
Selected prior artifacts
These public papers and reports provide the temporal-property, monitorability, typed-action, and role-trace foundations used by the testbed.
Working paper, 2026 / Temporal Evaluation
The Intersection Algebra of Safety, Cosafety, Liveness, and Coliveness over Linear Temporal Logic
Zenodo working paper
Classifies omega-regular properties through temporal evidence classes and connects the classification to verdict alphabets for runtime monitoring.
ABS
This working paper integrates safety, cosafety, liveness, and coliveness into a single classification over omega-regular properties. It relates topological and prefix-quantifier structure to monitor verdict alphabets and finite evidence limits.
CITE
@misc{bragetti2026intersectionalgebra,
title = {The Intersection Algebra of Safety, Cosafety, Liveness, and Coliveness over Linear Temporal Logic},
author = {Bragetti, Davide},
year = {2026},
month = sep,
doi = {10.5281/zenodo.23043255},
publisher = {Zenodo},
note = {Working paper}
}
Preprint, 2026 / Temporal Evaluation
Observation-Relative Monitorability of Bounded Temporal Implication
Zenodo preprint
Shows that monitorability of bounded temporal implication is joint in the formula and observation model, not a property of the formula alone.
ABS
This preprint analyzes temporal implication under finite observation, delay, drift, jitter, and finite resolution. The result is an observation-relative view of monitorability: verdicts depend on both the formula and the observation regime.
CITE
@misc{bragetti2026observationrelative,
title = {Observation-Relative Monitorability of Bounded Temporal Implication},
author = {Bragetti, Davide and Bragetti, Alessandro and Italiano, Giuseppe F.},
year = {2026},
month = sep,
doi = {10.5281/zenodo.23041615},
publisher = {Zenodo},
note = {Preprint}
}
Preprint, 2026 / Temporal Evaluation
Controlling the Observation Class of a Runtime Monitor: Selection, Self-Tuning, and Physical Grounding
Zenodo preprint
Engineering companion showing how a runtime monitor's observation class can be selected and locally tuned under physical and causal-coherence constraints.
ABS
This preprint treats a runtime monitor’s observation class as a controlled quantity. It studies monitor-type selection, self-tuning, and physical grounding for bounded-eventuality temporal implication.
CITE
@misc{bragetti2026observationclass,
title = {Controlling the Observation Class of a Runtime Monitor: Selection, Self-Tuning, and Physical Grounding},
author = {Bragetti, Davide and Bragetti, Carlo and Italiano, Giuseppe F.},
year = {2026},
month = sep,
doi = {10.5281/zenodo.23041626},
publisher = {Zenodo},
note = {Preprint}
}
Preprint, 2026 / Temporal Evaluation
Refinement-Based Confirmation of Liveness Properties from Monitor Verdict Traces: A Hensel-Newton Approach
Zenodo preprint
Studies what extra refinement structure can supply when a finite monitor prefix cannot by itself confirm a liveness property over a continuing execution.
ABS
This preprint studies how external refinement structure can support missing verdicts for temporal properties that finite prefixes cannot settle alone. It introduces a refinement chain and convergence criterion for liveness confirmation.
CITE
@misc{bragetti2026refinementliveness,
title = {Refinement-Based Confirmation of Liveness Properties from Monitor Verdict Traces: A Hensel-Newton Approach},
author = {Bragetti, Davide},
year = {2026},
month = aug,
doi = {10.5281/zenodo.22028019},
publisher = {Zenodo},
note = {Preprint}
}
Technical report, 2026 / Agent / Triangle Dynamics
A Typed Agent Action Framework with Prefix-Verdict Semantics
Zenodo technical report
Defines typed footprint action classes for agent actions and maps them onto prefix-verdict semantics over temporal property classes.
ABS
This technical report gives typed signatures for agent action footprints and carrier persistence. It connects action classes to safety, cosafety, liveness, and coliveness verdict semantics over finite observation prefixes.
CITE
@misc{bragetti2026typedagentaction,
title = {A Typed Agent Action Framework with Prefix-Verdict Semantics},
author = {Bragetti, Davide and Italiano, Giuseppe Francesco},
year = {2026},
month = sep,
doi = {10.5281/zenodo.23041634},
publisher = {Zenodo},
note = {Technical report}
}
Preprint, 2026 / Agent / Triangle Dynamics
Recognising Before Reacting: Temporal Signatures of Transactional Games
Zenodo preprint
Formalises transactional games as finite-trace LTL properties over Karpman-projected role traces, using the antithesis window to distinguish reactive and pre-committed regimes.
ABS
This preprint models seven transactional games as finite-trace LTL properties over projected role traces. It introduces the antithesis window as a temporal invariant separating reactive, knife-edge, pre-committed, and unresolved regimes.
CITE
@misc{bragetti2026recognisingreacting,
title = {Recognising Before Reacting: Temporal Signatures of Transactional Games},
author = {Bragetti, Davide and Italiano, Giuseppe Francesco},
year = {2026},
month = aug,
doi = {10.5281/zenodo.22050701},
publisher = {Zenodo},
note = {Preprint}
}