← 研踪 PaperTrailarXiv:2610.11991 · v3
Quantitative Verification of Infinite-State Networks
首次提交 2026-10-08 22:00
版本更新 2026-11-08 20:58
雷达观测 2026-11-10 12:16
摘要
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 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.
作者备注：Accepted at POPL 2027. Full version with appendices, 46 pages, and 13 figures
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-08 20:58 · 最新观测版本
Quantitative Verification of Infinite-State Networks
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 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.
查看此版本解读 →查看此版本原文 ↗