Refinement-Based Confirmation of Liveness Properties from Monitor Verdict Traces: A Hensel-Newton Approach
Davide Bragetti · Zenodo (CERN European Organization for Nuclear Research) · 2026
A runtime monitor that observes a finite prefix of an execution can often refute a property but never confirm it, or the reverse, and for some properties it can do neither. We study what an external structure attached to such a monitor has to supply in order to recover the missing verdict, and we introduce a refinement system for that purpose: a chain of candidate configurations, a computable update rule, and a computable error metric that measures how far the current configuration is from certifying the target. When the error metric decreases by a fixed positive quantum at every step at which it is positive, the target is certified within a bound determined by the initial error and that quantum. The main point of the analysis is a separation the argument makes visible. Finite descent yields a statement about a prefix. Turning it into a statement about the infinite execution requires two further ingredients, stated and used separately: that the observed execution belongs to a declared class of admitted behaviours, and, for the persistent form, that the certifying condition once reached is never lost. Neither follows from the descent. Modular inversion by Hensel lifting is the worked instance: the residual squares at each step, so a certified lower bound on the initial precision yields a guaranteed deadline for confirmation, and the confirming condition is absorbing, which supplies the temporal lift in full. Five primality methods are placed against the same scheme as a scope study. Enforcement by adapting monitor parameters rather than editing the observed trace is defined and left open. --- SCOPE AND STATUS. This is a preprint. It has not been peer reviewed and is not under journal acceptance. One statement is labelled a conjecture in the text and is not used in any proof; every other numbered result is either proved or, in one case, an explicit restatement of published complexity bounds that says so. The minimality and convergence claims are relative to hypotheses stated with each result.