发表机构
ETH Zurich（苏黎世联邦理工学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对结合递归与定量行为的无限状态网络，提出基于泵半环的精确定量验证框架，实现了下推系统网络的定量安全性与可达性分析。
AI 中文摘要
许多网络协议和分布式系统结合了递归、无界局部状态以及成本、延迟或可靠性等定量行为。现有的下推系统网络可判定性结果在很大程度上是定性的，无法扩展到需同时跟踪轨迹和权重的定量分析。我们提出了一种用于加权下推系统无环网络定量验证的框架。对递归网络组件进行有限总结需要通过展开其嵌套循环得到的无限运行族进行折叠，而要精确地而非通过过度近似地完成这一点是一个长期存在的难题。我们给出了一类可实现该目标的权重域：泵半环，即此类运行族累积的权重可折叠为闭式形式的半环；通俗地说，该域必须无法对迭代次数进行计数。该类包含具有无限升链的域，例如北极半环和下闭语言。在这些域上，我们给出了一种终止的饱和算法，用于精确计算定量可达性，该算法基于两个思路：段树代数（一种运行的组合表示）和热扩展（其符号分离加速权重，使进一步加速仍保持精确）。我们利用该算法统一计算上下文无关语言的上闭包和下闭包，并将算法提升到“薄”泵半环上的无环网络，从而得到了下推系统网络的首个定量安全性和可达性分析。
英文摘要
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.
Comments45 pages, 13 figures
