Summary
Many computer networks and distributed systems keep track of things like costs or delays while also handling potentially infinite behaviors due to recursion. Previous methods could only check if something was possible or not, without measuring quantities like how long or costly it might be. The authors created a new way to exactly analyze networks with recursive components that accumulate weights (like costs), focusing on specific mathematical structures called pumping semirings that allow precise calculation. Their method can compute exact measures of safety and reachability even in complicated systems where standard counting doesn’t work. This opens up new possibilities for analyzing and verifying systems with unbounded recursive behaviors and quantitative features.
What this means in practice
- •For network protocol engineers: Analyze recursive network protocols to compute exact cost or reliability measures for complex communication patterns.
- •For distributed system developers: Ensure safety properties and estimate quantitative metrics such as latency in distributed systems with recursive behavior and unbounded state.
Abstract
Many network protocols and distributed systems combine recursion, unbounded local state, and quantitative behaviour such as cost, latency, or reliability. Existing decidability results for networks of pushdown systems are largely qualitative, and do not extend to quantitative analyses, which must jointly track traces and weights. We present a framework for the quantitative verification of acyclic networks of weighted pushdown systems. Finitely summarising a recursive network component requires collapsing the infinite family of runs obtained by pumping its nested loops, and doing so \emph{exactly}, rather than by over-approximation, is a standing difficulty. We give a class of weight domains where this is possible: pumping semirings, those in which the weights accumulated by such a family collapse to a closed form; informally, the domain must be unable to count iterations. The class admits domains with infinite ascending chains, such as the arctic semiring and downward-closed languages. Over these, we give a terminating saturation algorithm computing quantitative reachability exactly, resting on two ideas: segment tree algebras, a compositional representation of runs, and thermal extensions, which symbolically separate accelerated weights so that further acceleration remains exact. We use this to compute upward and downward closures of context-free languages uniformly, and to lift the algorithm to acyclic networks over "thin" pumping semirings, yielding the first quantitative safety and reachability analyses for networks of pushdown systems.