prodigy.analysis.lowerbounds.parameters

Automatic choice of template parameters (rates, periods, tail starts) for the LP synthesis of EVT sub- and superinvariants.

The heuristic explores the loop numerically (a sparse floating-point Kleene iteration of the occupation measure, prodigy.analysis.lowerbounds.explicit.Exploration) and derives, for every program variable,

  • its period p_i: the gcd of the differences of values of x_i among explored states that agree on all other variables (e.g. 2 for the step counter of a +-1 random walk, whose parity is tied to the walk);

  • its kind: bounded (only finitely many small values), decaying (the marginal of the occupation measure decays geometrically, with an estimated rate per period), or persistent (no decay, e.g. the height of a transient random walk);

  • a scale: the value below which (almost) all of the explored occupation mass lies.

Lower certificates truncate bounded and persistent variables and decaying variables with negligible tails (rate 0: a truncated sub-invariant is again a sub-invariant) and give the remaining variables geometric tails with rates slightly below the decay rate of the truncated loop. Upper certificates need geometric tails in every unbounded variable; their rates must make the template a super-invariant far out in the tail, where the body acts as a random walk whose increments delta depend on a finite phase (the bounded variables and the residues of the unbounded ones): for per-unit rates s_i this requires that the matrix M(s)[e', e] = sum_delta P(e -> e', delta) prod_i s_i^(-delta_i) has spectral radius at most one. We minimise the rates of the variables that are unbounded at loop exit subject to this condition. The heuristic only proposes candidates: every certificate is verified exactly, so the parameters affect precision and running time, never soundness.

class TemplateShape(rates, periods, tail_start, reach_box=None, group=0)[source]

Bases: object

Parameters:
rates: List[Fraction]
periods: List[int]
tail_start: List[int]
reach_box: List[int] | None = None
group: int = 0
size()[source]
Return type:

int

describe()[source]
Return type:

str

class VariableProfile(name, kind, period, rate, scale_trunc, scale_bulk, max_value, exit_unbounded)[source]

Bases: object

Parameters:
name: str
kind: str
period: int
rate: float
scale_trunc: int
scale_bulk: int
max_value: int
exit_unbounded: bool
class ParameterPlan(lower, upper, profiles=list(), exploration=dict())[source]

Bases: object

Parameters:
lower: List[TemplateShape]
upper: List[TemplateShape]
profiles: List[VariableProfile]
exploration: Dict[str, object]
nice_rate(x, digits=3, up=False)[source]

Round a positive rate to a fraction with few significant digits (keeps exact arithmetic cheap).

Parameters:
Return type:

Fraction

decay_rate(marg, period)[source]

Estimated geometric decay per period of a marginal v -> mass (least-squares fit of log m(v) = a + b log v + c v on the tail, which removes polynomial factors such as v^(-3/2)).

Parameters:
Return type:

float

profile_loop(init, guard, body, variables, iterations=1500, max_states=300000, cap=5000, max_work=600000, time_limit=8.0)[source]

Explore the loop numerically (about max_work state expansions) and classify its variables.

Parameters:
Return type:

Tuple[List[VariableProfile], Exploration]

class TailKernel(phases, transitions)[source]

Bases: object

The loop far out in the tail as a Markov-modulated random walk: the phase of a state consists of the values of the bounded variables and the residues of the unbounded ones modulo their periods; transitions lists (target phase, source phase, increment of the unbounded variables, probability) for guard-satisfying source phases.

Parameters:
phases: List[tuple]
transitions: List[Tuple[int, int, tuple, float]]
matrix(log_s)[source]

M(s)[e', e] = sum P(e -> e', delta) * prod_i s_i^(-delta_i) for per-unit rates s = exp(log_s).

Parameters:

log_s (ndarray)

Return type:

ndarray

log_radius(log_s)[source]

Logarithm of the spectral radius of M(s) (-inf if it is nilpotent).

Parameters:

log_s (ndarray)

Return type:

float

tail_kernel(guard, body, variables, profiles, seeds=None, base=10080, max_phases=2048)[source]

Explore the phases reachable (far out in the tail) from the phases of the states seeds – the states visited by the exploration of the loop – or, without seeds, from all combinations of bounded values and residues. base is a multiple of every possible period, so that the residue of a seed is that of its tail copy.

Parameters:
Return type:

TailKernel

upper_tail_rates(kernel, profiles, slack=0.0, fixed=None)[source]

Per-unit rates s_i of the unbounded variables minimising the rates of the exit-relevant variables subject to rho(M(s)) <= 1, the condition under which a product tail a_e * prod_i s_i^(n_i) with phase-dependent coefficients a_e > 0 can be super-invariant far out in the tail (Perron–Frobenius: M(s) a <= a has a solution a > 0 iff the spectral radius is at most one). log rho(M(e^t)) is convex in t (Kingman), so the problem is convex. The per-unit rates fixed are not optimised: a variable that is sampled from a geometric distribution before the loop keeps the rate of that distribution, since the denominator of the template has to contain the denominator of the initial measure. Returns None if the optimisation fails.

Parameters:
plan_parameters(init, guard, body, variables, size=1200, upper_size=None, lower_multipliers=(0.95, 0.985, 0.998), upper_steps=(0.01, 0.05, 0.15, 0.35), aspect_factors=(1.0, 0.6), forced=None)[source]

Candidate template shapes for lower and upper certificates. forced maps the variables that are sampled from a geometric distribution before the loop to the rate and period of that distribution.

Parameters:
Return type:

ParameterPlan