Research
Machine-checkable temporal semantics for learning, evaluating, monitoring, and governing agentic systems.
The research program asks how safety-relevant properties can be represented, learned, observed, and preserved when agents act over time and under imperfect governance. The public dependency runs from observer-relative properties and temporal evidence, through ChronoSpec’s model-level integration question, to post-failure governance and role dynamics in multi-agent interaction.
Research Program
Preprint cluster
MCK Properties
What properties should an agent, artifact, or governance relationship make observable?
MCK is an observer-relative vocabulary for meaning, residual opacity, function, and agent property attribution. It supports property candidates such as identity, integrity, and freedom only when the carrier, evidence, and observer assumptions are declared.
Working paper + preprints
LTL / Property-Class Evaluation
What can finite observations justify about temporal claims over an infinite or continuing trace?
This line supplies the temporal evaluation language: safety, cosafety, liveness, coliveness, verdict alphabets, observation classes, and refinement-confirmation conditions for monitor verdict traces.
Active research / feasibility design
ChronoSpec
Integrating Linear Temporal Logic into LLMs
Can one machine-checkable temporal semantics connect learning, behavioral analysis, runtime monitoring, and enforcement?
ChronoSpec moves the temporal-property program upstream: it tests whether explicit LTL contracts can shape an LLM's learned behavior while remaining available outside the model as an independent reference semantics. Integration is the research program; internalization is an empirical hypothesis, and a latent temporal representation is a possible result rather than an assumption.
Active research / experimental design
LTL Triangles / Post-Failure Governance
Which governance protocols contain a bounded failure while preserving unaffected invariants and restoring useful operation?
The testbed evaluates what a governance intervention repairs, preserves, and newly makes unsafe after one bounded safety failure. It separates coordination, execution, and audit/challenge positions under asymmetric information, authority, incentives, observation rights, and intervention rights.
Active research
Drama to Empowerment
Can multi-agent role transitions be treated as measurable protocol dynamics rather than descriptive labels?
The public evidence is a finite-trace LTL treatment of transactional games over projected role traces. The empowerment direction remains an active extension about moving away from reactive role lock-in while preserving relevant agent properties.
Current focus
Feasibility testing for ChronoSpec: can explicit temporal contracts shape learned behavior while remaining independently monitorable and enforceable?
Downstream testbed
LTL Triangles continues the program at the governance layer by comparing recovery strategies across clean, honest-error, and adversarial traces.
Progress & Roadmap
Framed safety as an evaluation and governance problem
Foundational questions
Public essays separated model-local safety from ecosystem behavior, evaluator gaming, and reactive misalignment under coarse intervention.
Released the temporal property-class substrate
LTL / Property-Class Evaluation
Classified safety, cosafety, liveness, and coliveness as distinct evidence regimes for finite and continuing traces.
Defined observation-relative monitorability
Observation and monitoring
Separated formula-level temporal claims from what a bounded, delayed, drifting, or finite-resolution monitor can actually observe.
Formalized observer-relative property attribution
MCK Properties
Built the MCK vocabulary for meaning, residual opacity, function, region transitions, and agent self-attribution.
Published temporal signatures for transactional games
Role traces
Represented role dynamics as finite-trace LTL properties and connected action types to prefix-verdict semantics.
Designing a falsifiable LTL-integration study
ChronoSpec / model-level temporal integration
The active upstream question is whether a shared temporal contract can improve held-out temporal generalization and reduce violating proposals or shield interventions without sacrificing task utility.
Freezing the post-failure governance testbed
LTL Triangles / Post-Failure Governance
The active dependency is a replayable trace schema, bounded fault model, observer vocabulary, temporal properties, and protocol baselines for recovery after failure.
Compare recovery protocols across bounded failure regimes
Experimental validation
The next falsifiable milestone is to test halt or lock, retry or reassign, and constrained recovery against clean, honest-error, and adversarial traces.
Publish benchmark traces, verdicts, and counterexamples
Public release
A planned output is a public benchmark slice with temporal specifications, model-checking artifacts, replayable traces, evaluation cards, and a claim-boundary report.
Connect role transitions to preserved agent properties
Drama to Empowerment
The longer-horizon question is whether governance interventions can move systems away from reactive role lock-in while preserving identity, integrity, freedom, and corrigible participation.
Publications
Preprint, 2026 / MCK Properties
When Can an Agent Attribute Properties to Itself? A Cognitive Algebra for Identity, Integrity, and Freedom
Zenodo preprint, version 3
Develops the MCK self-attribution layer with a two-layer state separating structural carriers from semantic content, then studies continuity, viability, and owned branching as property signatures.
ABS
This preprint distinguishes structural realizability from semantic calibration in agent self-attribution. It uses the MCK observer-relative framework to model capability carriers, evidence content, self-reference, other-models, operator composition, and finite decision procedures for continuity, viability, and owned branching.
CITE
@misc{bragetti2026agentattributeproperties,
title = {When Can an Agent Attribute Properties to Itself? A Cognitive Algebra for Identity, Integrity, and Freedom},
author = {Bragetti, Davide and Micali, Silvio and Italiano, Giuseppe Francesco},
year = {2026},
month = sep,
doi = {10.5281/zenodo.23041633},
publisher = {Zenodo},
note = {Preprint}
}
Preprint, 2026 / MCK Properties
MCK Region Transitions: Restricted Realization Mechanisms and Their Limits
Zenodo preprint
Studies restricted mechanisms for moving artifacts across MCK regions, including assimilation, operator admission, denotation, and reconstruction certificates.
ABS
This preprint starts from the MCK region system and asks which restricted realization families can actually move artifacts between observer-relative regions. It separates algebraic transition possibility from concrete procedures and records where each mechanism stops.
CITE
@misc{bragetti2026mckregiontransitions,
title = {MCK Region Transitions: Restricted Realization Mechanisms and Their Limits},
author = {Bragetti, Davide and Palumbo, Edoardo and Asaro, Carmelo and Italiano, Giuseppe Francesco},
year = {2026},
month = sep,
doi = {10.5281/zenodo.23041603},
publisher = {Zenodo},
note = {Preprint}
}
Preprint, 2026 / MCK Properties
Meaning, Opacity, and Function: An Observer-Relative Classification of Artifacts
Zenodo preprint
Defines the observer-relative MCK region system over meaning, residual opacity, and functionality, fixing the vocabulary used by later MCK work.
ABS
This preprint treats meaning, opacity, and functionality as observer-relative predicates over artifacts. It studies the finite region system induced by those predicates and supplies the baseline vocabulary later used for property attribution.
CITE
@misc{bragetti2026meaningopacityfunction,
title = {Meaning, Opacity, and Function: An Observer-Relative Classification of Artifacts},
author = {Bragetti, Davide and Asaro, Carmelo and Italiano, Giuseppe Francesco},
year = {2026},
month = aug,
doi = {10.5281/zenodo.22016203},
publisher = {Zenodo},
note = {Preprint}
}
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}
}
Research Notes
To Be or to Game
Motivates the science-of-evaluations problem: open-ended domains, evaluator gaming, and the need for formal property specifications.
Does Safe AI mean nothing bad can ever happen?
Motivates relational and ecosystem-level evaluation, where safety is not reducible to one isolated model.
Misalignment by Reaction
Motivates governance-stability evaluation: coarse regimes can induce autonomy-seeking responses under reward disruption.
Uno, nessuno, centomila e tutti
Develops the persona and mask-coupling vocabulary that connects agent identity, role selection, and evaluation under adversarial context shifts.
Current Questions
- Can explicit temporal contracts improve compositional generalization and reduce violating proposals or shield interventions without sacrificing task utility?
- Which candidate agent properties have enough structural and semantic support to be monitored rather than merely named?
- When does finite evidence license a continuing temporal claim, and which extra assumptions perform that lift?
- How can governance interventions prevent reactive role lock-in without destroying the agent properties they are meant to preserve?