LTL / Property-Class Evaluation
What can finite observations justify about temporal claims over an infinite or continuing trace?
This line supplies the evaluation language of the research program: temporal property classes, prefix verdicts, observation-relative monitorability, and the assumptions required to carry finite evidence into a continuing system.
Research programPrevious: MCK PropertiesNext: ChronoSpec
Evaluation problem
Safety-relevant claims about sequential agents are trace claims. Some can be refuted by a finite bad prefix, some confirmed by a finite good prefix, and some remain undecided under every finite observation. A useful evaluation must therefore state both the temporal property and the observation regime.
| Property class | Finite evidence | Evaluation role |
|---|---|---|
| Safety | finite bad prefix | detect a witnessed violation |
| Cosafety | finite good prefix | detect a witnessed achievement |
| Liveness | no finite confirmation in general | represent continuing progress obligations |
| Coliveness | no finite refutation in general | represent persistent possibility of violation |
Research profile
Formal substrate
Linear Temporal Logic, omega-regular properties, prefix quantifiers, verdict alphabets, and property-class intersections.
Observation model
Bounded or delayed observation, drift, jitter, finite resolution, and the monitor's access to typed action traces.
Main distinction
Formula-level truth is separated from the verdict a particular monitor can justify under its declared observation class.
Refinement question
Finite verdicts require explicit refinement and environment assumptions before they support claims about continuing executions.
Dependency role
MCK Properties supplies candidate observer-relative properties. This line determines how they can be expressed and evaluated over traces. ChronoSpec uses that temporal substrate for a model-level feasibility question; LTL Triangles uses it independently for governance and recovery over observable traces.
Current status and claim boundary
The line consists of a public working paper and preprints and remains active formal-methods research. Finite experiments may provide witnesses, counterexamples, or bounded verdicts; they do not by themselves certify permanent safety for an unbounded deployment.
Selected publications
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}
}