Queueing Theory

Tools

`jackson_network`

Analyze a Jackson queueing network. Computes per-node utilization (rho = lambda/mu), stability condition (rho < 1 for all nodes), expected queue lengths via Little's law (L = rho/(1-rho)), and expecte...

`queue_stability`

Check stability bounds for a queue. Supports M/M/1 (single server) and M/M/c (multi-server) models. Returns utilization, stability status, expected queue length (Lq), expected system length (L), expec...

`vacation_queue`

Model a queue with server vacations (warmup/cooldown model from the paper). When the server finishes a vacation it resumes serving. During vacation, arrivals queue but are not served. Returns expected...

`queue_boundary`

Compute the queue boundary: the maximum arrival rate a system can handle before instability. Given service rates and a routing matrix, finds per-node boundaries and the system bottleneck. Uses the tra...

`drain_analysis`

When does a queue drain? Simulates a queue with alternating active and vacation periods. During active periods the queue drains (service_rate > arrival_rate); during vacation it grows. Returns drain t...

`thm_queue_sample_path`

Finite-trace work-conserving single-server queues satisfy the discrete sample-path Little's Law identity independent of discipline choice [LEDGER: THM-QUEUE-SAMPLE-PATH]

`thm_queue_multiclass_network`

Bounded multi-class open networks satisfy the same conservation identity under node-local work-conserving dispatch [LEDGER: THM-QUEUE-MULTICLASS-NETWORK]

`thm_queue_stochastic_mixture`

Finite-support stochastic mixtures of bounded multi-class open-network traces preserve customer-time conservation in expectation [LEDGER: THM-QUEUE-STOCHASTIC-MIXTURE]

`thm_queue_probabilistic_kernel`

Exact finite-state probabilistic queue transitions preserve customer-time conservation at the distribution level [LEDGER: THM-QUEUE-PROBABILISTIC-KERNEL]

`thm_queue_probabilistic_network_kernel`

Exact finite-state probabilistic multiclass open-network transitions preserve customer-time conservation at the distribution level [LEDGER: THM-QUEUE-PROBABILISTIC-NETWORK-KERNEL]

`thm_queue_probabilistic_large_network`

Larger exact finite-support multiclass open-network probabilistic cubes preserve the same weighted conservation law [LEDGER: THM-QUEUE-PROBABILISTIC-LARGE-NETWORK]

`thm_queue_mm1_stability`

Stable `M/M/1` occupancy has the geometric stationary law with finite mean queue length `ρ / (1 - ρ)`, and the same stationary law inherits the queue conservation identities [LEDGER: THM-QUEUE-MM1-STA...

`thm_queue_one_path`

Canonical stable `M/M/1` queues admit a constructive one-path boundary witness: `β₁ = 0`, capacity `β₁ + 1 = 1`, stationary mean occupancy `λ / (μ - λ)`, and the induced identity `λ / (μ - λ) = λ * (1...

`thm_queue_jackson_product`

Finite open networks with a stable throughput witness satisfying the traffic equations admit an exact product-form occupancy law with exact singleton mass and total mean occupancy `∑ᵢ αᵢ / (μᵢ - αᵢ) [...

`thm_queue_jackson_exact`

Finite open networks admit an exact constructive Jackson closure beyond the envelope ladder once an exact stable real traffic fixed point is supplied: under `spectralRadius P < 1`, any nonnegative rea...

`thm_queue_jackson_raw`

Finite open networks satisfying the raw envelope criterion admit the same product-form occupancy and queue-balance laws with no hand-supplied throughput witness: if `maxIncomingRoutingMass < 1` and `m...

`thm_queue_jackson_feedforward`

The bounded two-node feed-forward ceiling witness is a nontrivial raw exact Jackson subclass: its routing matrix is nilpotent (`P^2 = 0`), so the explicit throughput candidate already matches the cons...

`thm_queue_jackson_envelope_ladder`

The finite Jackson raw route sharpens into a descending constructive envelope ladder: if any chosen stage `throughputEnvelopeApprox n` already lies below service rates, then the same product-form occu...

`thm_queue_infinite_support`

Infinite weighted scenario families preserve queue customer-time conservation under exact countable/infinite support aggregation [LEDGER: THM-QUEUE-INFINITE-SUPPORT]

`thm_queue_countable_stochastic`

Countably supported stochastic queue laws preserve the same expectation/conservation identity [LEDGER: THM-QUEUE-COUNTABLE-STOCHASTIC]

`thm_queue_measure_limit`

Measure-theoretic queue observables and monotone truncation families preserve conservation in the unbounded limit [LEDGER: THM-QUEUE-MEASURE-LIMIT]

`thm_queue_ergodic_cesaro`

Unbounded open-network sample-path conservation lifts to long-run Cesaro limits, and vanishing residual open age yields terminal balance [LEDGER: THM-QUEUE-ERGODIC-CESARO]

`thm_queue_state_dependent_schema`

State-dependent open-network stationary and terminal queue balance follow from explicit routing-kernel bridge witnesses, explicit Lyapunov drift bounds outside a finite small set, and a positive drift...

`thm_queue_adaptive_supremum`

Adaptive routing families dominated by a substochastic contractive ceiling kernel inherit the ceiling's throughput bounds constructively, and from that raw ceiling data plus a monotone expected-Lyapun...

`thm_queue_adaptive_raw_ceiling`

A bounded two-node adaptive rerouting family derives its own dominating ceiling kernel, strict-row-substochastic spectral side conditions, constructive throughput bound, and a linear drift witness dir...

`thm_queue_limit_schema`

Stronger queue-limit claims with explicit support-exhaustion and integrable-envelope side conditions remain available as a higher-level theorem schema [LEDGER: THM-QUEUE-LIMIT-SCHEMA]

`thm_queue_containment`

*Superseded by THM-QUEUE-SUBSUMPTION.* Forward direction of queueing subsumption: when the supplied `β₁=0` queue law holds, the framework recovers that one-path boundary, and when `β₁>0` the framework...

`thm_queue_converse`

Converse direction of queueing subsumption: every queueing system (G/G/1, G/G/c, priority, network) admits a fork/race/fold embedding under C3' (probabilistic fold). Arrival processes map to fork dist...

`thm_c3_prime_generalization`

C3' (probabilistic fold) generalizes C3 (deterministic fold): deterministic fold is the Dirac δ special case of probabilistic fold. C3' preserves C1 (fork creates paths), C2 (race selects earliest), a...

`thm_probabilistic_fold_safety`

Under C3' + ergodicity, probabilistic fold preserves all four fork/race/fold axioms and conservation holds in expectation rather than pointwise. The entropy increase is bounded: H(fold) = 0 for determ...

`thm_queue_subsumption`

Bidirectional subsumption of queueing theory by fork/race/fold: (forward) FRF at β₁=0 recovers queueing theory (THM-QUEUE-CONTAINMENT); (converse) every queueing system embeds as FRF under C3' (THM-QU...

`thm_queue_jackson_queueing`

Jackson network fundamentals: spectrum/transpose equality, spectral radius transpose equality, M/M/1 stationary queue length integral equals rho/(1-rho). Measure-theoretic queue analysis with weighted...

`thm_state_dependent_queue_families`

State-dependent queue families: vacation queue state, retrial queue, reneging queue, adaptive routing queue. Queue law structures for multiple service disciplines with customer time, sojourn time, and...