ChronoSpec
Integrating Linear Temporal Logic into LLMs
ChronoSpec investigates whether one explicit, machine-checkable temporal semantics can connect LLM training or adaptation, learned temporal competence, formal behavioral analysis, runtime monitoring, and enforcement.
Research programPrevious: LTL EvaluationNext: LTL Triangles
Motivation
Sequential agents face rules that cannot be reduced to isolated good or bad outputs: an authorization must precede an action, an obligation must eventually be discharged, a safety condition must persist, recovery must follow a fault, and an irreversible commitment may require a checkpoint first.
As agents operate over longer horizons with greater autonomy, failures of authorization, ordering, recovery, or irreversible-action rules can compound before human intervention. Better temporal generalization and independently enforceable contracts are therefore relevant to reducing high-consequence and potentially catastrophic failure modes.
Predictive and post-training objectives can produce capable behavior without requiring the model to learn the underlying temporal invariant. A behavioral proxy may admit a shortcut that works on the training distribution and fails under a new composition or context. This problem is related to shortcut learning, underspecification, specification gaming, and distribution shift, without making those research literatures equivalent.
External guardrails can compensate at deployment, but they do not by themselves establish what the model has learned. ChronoSpec studies whether an explicit temporal contract can reduce that gap while remaining available outside the model as an independent reference semantics.
Research question
Can one machine-checkable temporal semantics support all four layers below?
Learning
Annotate training traces and counterexamples with explicit temporal obligations, violations, and recovery states.
Analysis
Compare behavioral conformance and, where access permits, probe whether internal representations track temporal state.
Monitoring
Evaluate typed action traces against the same contract under a declared observation model and verdict semantics.
Enforcement
Use an external shield to block, redirect, or request correction when a proposed action would violate the specified property.
The intended connection is not merely prompting a model with a formula. The study compares candidate integration mechanisms—including supervised or preference-based adaptation, counterexample-guided training, constrained generation, and auxiliary objectives or probes—without assuming in advance where useful temporal competence will reside.
Why temporal logic
High-assurance control of sequential AI requires explicit, machine-checkable temporal contracts or equivalent formal semantics. Linear Temporal Logic is a mature candidate for expressing important safety, ordering, progress, recovery, and liveness properties over traces.
LTL is not claimed to be mathematically necessary for every safe AI system, nor does adding LTL to an LLM certify arbitrary real-world safety. It provides a precise language in which specified properties can be analyzed, monitored, and enforced relative to an observation/action abstraction and explicit environment assumptions.
Training and enforcement
The project keeps four claims separate:
- Integration is the general research program: connect explicit temporal semantics to the LLM learning and control stack.
- Internalization is an empirical hypothesis: test whether adaptation produces reusable temporal competence rather than template matching.
- Embedding or latent representation is a possible mechanism or finding, not an established result.
- Formal enforcement remains externally grounded in the specification, monitor, and shield.
This separation preserves an auditable reference contract even if the model’s learned behavior is unreliable or its internal representations are unclear.
Evaluation strategy
Matched baselines and LTL-aware variants will be compared on long-horizon agent tasks with ordering constraints, authorization rules, progress and liveness requirements, recovery obligations, bounded-risk actions, and irreversible commitments. Tests should include held-out temporal compositions, distribution shift, weakened guardrails, and adversarial prompting.
The primary measures are property satisfaction, violating-action proposals, shield interventions, and retained task utility. Where model access permits, representation probes can test whether temporal state, obligations, or distance to violation are decodable and predictive of failure.
Negative results are decision-relevant. If integration does not generalize, internal representations do not track temporal structure, or external enforcement alone gives the same safety–utility trade-off, the evidence would favor keeping formal logic primarily in the monitoring and control layer.
Relationship to prior work
ChronoSpec grows from the existing temporal-property and monitorability line:
- MCK work asks which observer-relative properties and evidence carriers are well enough specified to evaluate.
- LTL/property-class work supplies temporal contracts, prefix verdicts, observation-relative monitorability, and refinement conditions.
- ChronoSpec asks whether those contracts can also shape model behavior while remaining independently verifiable at runtime.
- LTL Triangles applies the temporal layer downstream to interaction, intervention, recovery, and governance after bounded failures.
Current status
ChronoSpec is an active research direction and feasibility design. The public site does not claim successful temporal internalization, completed experiments, general safety certification, or a funding outcome.
Selected prior artifacts
The following public papers and reports supply the strongest current links from temporal property classes, through observation and monitoring, to typed agent actions.
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}
}