Quantitative Verification of Infinite-State Networks

1 INTRODUCTION

• Quantitative network verification must preserve the relationship between traces and weights, which qualitative network techniques do not capture.Existing qualitative reachability algorithms use language closures, but extending them quantitatively is not straightforward.Source: §1 · p. 2

1.1 A Motivating Example

• Isolated component analyses can report infinite costs for runs that no global trace reaching the target can contain.In the client-server example, the target requires the server’s send-dependent route, on which the client pays nothing.Source: §1.1 · p. 4

1.2 Contributions

• Pumping semirings enable exact summaries of nested-loop weights without requiring the weight domain to satisfy the ascending chain condition.The class includes domains with infinite ascending chains, such as the arctic semiring and downward-closed languages.Source: §1.2 · p. 4
• A saturation procedure computes quantitative reachability and treats upward and downward closures of context-free languages as instances of that problem.These closure computations serve as a technical ingredient for the later network-verification algorithms.Source: §1.2 · p. 4
• The framework yields quantitative algorithms for safety, reachability, and cost-bounded reachability of networks of weighted pushdown systems.It supports computing optimal bounds for these properties over acyclic networks.Source: §1.2 · p. 4

2.1 Some Basic Definitions

• Downward and upward closures collect, respectively, the subwords of words in a language and the words containing one of its words.Both kinds of closed languages are closed under union and concatenation.Source: §2.1 · p. 5
• An idempotent semiring supplies the operations and order used to combine weights; semirings can also be combined pointwise into product domains.The background defines lifting a weight function from individual symbols to words by multiplying their weights.Source: §2.1 · p. 5

2.2 Weighted Pushdown Systems

• A weighted pushdown system assigns semiring weights to pushdown transitions and aggregates the weights of runs between configurations.The aggregate may be infinite or fail to exist a priori; Boolean weights recover ordinary reachability.Source: §2.2 · pp. 6–7

3 PUMPING SEMIRINGS AND QUANTITATIVE REACHABILITY

• Pumping semirings require diagonal sums to collapse to a closed form, distributivity over countable sums that exist, and finitely many Kleene closures.The collapse law reduces the family a⊗b^n⊗c^n to a⊛⊗b⊗c⊛.Source: §3 · pp. 8–9
• The regular-language Kleene algebra is not pumping: its regular-expression star fails to capture the required context-free pumping sums.For u ∈ A+, the family {(u^n)* | n ∈ N} is also infinite, violating (C3).Source: §3 · p. 8
• The four-element parity semiring has no pumping operator, despite satisfying the ascending chain condition.Its iteration can count n modulo 2, contradicting (C1).Source: §3 · p. 8
• The collapse requirement rules out weight domains that can count loop iterations, such as tracking iteration counts modulo 2.Source: §3 · p. 8

3.1 Quantitative Reachability

• QuantReach is computable over pumping semirings, and weights between arbitrary configurations can be effectively computed.Source: §3.1 · p. 9
• ACC-based computability results exclude the arctic semiring and downward-closed languages, domains covered by the broader pumping-semiring approach.Source: §3.1 · p. 9

4 SEGMENT TREE ALGEBRAS

• Each labelled tree represents a set of runs, with its root label summarizing their cumulative weight.The construction enriches the state-pair nonterminals of context-free derivation trees with run weights.Source: §4 · pp. 9–10

4.1 Segment Tree Algebras

• A segment tree algebra combines trees through vertical and horizontal operations, and its generated ideal is closed under those operations and their contexts.Source: §4.1 · p. 10

4.2 wPDS vs. Segment Tree Algebras

• For a weighted pushdown system, the algebra’s vertical operation models a matching push-pop pair, while the horizontal operation combines consecutive runs.Source: §4.2 · p. 11
• A run from ⟨p, ⊣⟩ to ⟨q, ⊣⟩ with weight a exists exactly when the generated ideal contains the corresponding root tuple ⟨⟨p,q⟩,a⟩.Source: §4.2 · p. 12
• The trees provide a dual representation of context-free derivation trees suited to inductive reasoning.Source: §4.2 · p. 12

5.2 Computing Quantitative Reachability

• The algorithm builds an increasing sequence of finite thermal-labelled trees whose fixed point provides sufficient root weights for quantitative reachability.The construction uses vertical and horizontal tree operations, then projects the thermal-labelled trees to their canonical images.Source: §5 · p. 13, §5.2 · pp. 16–17

5 AN ALGORITHM FOR QUANTITATIVE REACHABILITY

• A pumping context’s infinitely many iterations can be replaced by one accelerated tree whose root weight is b⊛a c⊛.The iterative construction then continues from the accelerated tree rather than separately computing every pumped tree.Source: §5 · pp. 13–14
• Thermal extensions separate accelerated weights syntactically so the pumping effect can be recovered and used in further acceleration.Hot expressions merge with other hot expressions, while cold expressions do not merge under multiplication.Source: §5 · pp. 14–15

5.1 Thermal Extensions

• The thermal extension represents weights as hot or cold expressions, and its normal forms allow concatenation and star operations to be computed in linear time.The linear-time claim assumes constant-time semiring multiplication and closure operations.Source: §5.1 · pp. 15–16

5.2 Computing Quantitative Reachability

• The construction terminates because its trees have height at most |Q|^2 and only finitely many labels can occur at each height.The finite-set sequence preserves upper bounds while ensuring they are not too large, capturing the least upper bounds.Source: §5 · p. 13, §5.2 · p. 17
• The procedure is doubly exponential in the number of control states, while the weight domain affects the base through the number of distinct closure values.K is 1 for most pumping semirings, 2 for arctic and probabilistic-union semirings, and at most 2^|Trans| for downward-closed languages.Source: §5.2 · pp. 17–18
• The doubly exponential bound is not tight, and whether label sizes remain polynomial in |Q|—which would make the procedure singly exponential—remains open.The second exponential comes from the horizontal operation that concatenates both children’s labels.Source: §5.2 · p. 18

6 UNIFORM COMPUTATION OF LANGUAGE CLOSURES

• Upward and downward closures of context-free languages are computed as instances of the framework’s quantitative reachability procedure.These closure computations provide a technical ingredient for the subsequent network-verification algorithms.Source: §6 · p. 18

6.1 Upward Closures

• An upward-closed language is represented by a finite set of mutually incomparable minimal words, and the construction computes these closures from weighted reachability summaries.Each transition is mapped to its singleton upward closure; the algorithm also yields minimal traces between configurations.Source: §6.1 · p. 18
• The upward-closure algorithm also generates the minimal traces between the two configurations.These traces provide a trace-generation output alongside the closure computation.Source: §6.1 · p. 18

6.2 Downward Closures

• For downward closures, the construction uses simple regular expressions and a pumping operator that stars the transitions occurring in an expression.Each transition receives weight (ε + δ), and the operator maps an expression e to ∥e∥*; this makes the SRE semiring a pumping semiring.Source: §6.2 · pp. 19–20
• The downward closure of traces between c and c′ is the language denoted by the weighted reachability summary for those configurations.Figure 10 illustrates the translation and iterative construction, whose sequence gives under-approximations of the downward closure.Source: §6.2 · p. 20, Figure 10 · p. 20

7.3 Formalising Threshold and Optimality

• Threshold problems ask whether a given bound holds for safety, reachability, or cost-bounded reachability; optimality problems compute the corresponding optimal bounds.When the relevant optimal sets are finite and computable, the associated threshold problems are decidable.Source: §7 · pp. 20–21, §7.3 · p. 24

7.1 Networks of Weighted Pushdown Systems

• An acyclic network of weighted pushdown systems supports shared-state observations, with each process’s transitions carrying weights and its guards constraining observed state tuples.A network is acyclic when its communication relation has no cycles.Source: §7.1 · p. 21
• The client-server example’s global run has weight ⟨serv:2, cl:4⟩, combining each process’s local transition weights.The client pushes twice after observing message a, then receives b and flushes its stack.Source: §7.1 · p. 22

7.2 Finding the Common Denominator

• GenConfigReach aggregates, for each process, the weights of all global traces between two global configurations and underlies the section’s threshold and optimality problems.The theorem establishes its computability for acyclic networks when each process uses a thin pumping semiring.Source: §7.2 · pp. 22–23
• Thin pumping semirings include the paper’s listed domains, and insertion of transitions moves trace weights in the direction of the semiring order, allowing closure summaries to retain set weights.After linearising the network, each process is constrained by the others through closures of their observations; one procedure computes closures together with their weights.Source: §7.2 · p. 23
• For ≤S-thin semirings the quantitative adaptation uses a top-down approach, whereas ≥S-thin semirings require a bottom-up approach.The proof adapts the qualitative procedure using a joint fixpoint computation of language closures and weight summaries.Source: §7.2 · pp. 23–24

7.4 Revisiting Our Example

• In the client-server example, the computed worst-case upper bound is ⟨cl:0, srv:0⟩, so every x in N² satisfies the safety query.This contrasts with the ⟨cl:∞, srv:∞⟩ estimate from analysing the two processes separately.Source: §7.4 · p. 26

• The framework computes QuantReach for weighted pushdown systems over pumping semirings, using segment tree algebras to represent runs and their weight semantics.A saturation procedure computes accelerated trees until it reaches a fixpoint.Source: §8 · pp. 26–27
• GenConfigReach provides the basis for computing optimal bounds for safety, reachability, and cost-bounded reachability in acyclic weighted pushdown networks.The framework treats both threshold and optimality questions.Source: §8 · p. 27
• A unified approach computes upward and downward closures of context-free languages, offering an alternative to enumeration while preserving the relation between traces and weights.Source: §8 · p. 27
• Unlike recurrence analysis that over-approximates loop summaries, this framework computes them exactly over pumping semirings; neither approach subsumes the other.Its domain condition is checked once, rather than requiring a supplied iteration operator for each domain.Source: §8 · p. 27
• Whether the framework can verify quantitative properties of multi-pushdown automata remains an open question.Source: §8 · p. 27
• The network results extend quantitative analyses of finite-state networks to weighted pushdown processes and subsume the prior work’s concrete instances.A weighted extension of StacKAT remains future work.Source: §8 · p. 27
• A practical implementation and case-study evaluation of scalability and performance remain future work.Source: §8 · p. 27

• The proof sets e:=1⊛ and specializes (C1) at a=c=b=1 to obtain an initial identity.Source: A PROOF OF PROPOSITION 3.2 · p. 30
• The powers of e alternate between 1 and e, and two further specializations of (C1) yield identities used in the argument.Source: A PROOF OF PROPOSITION 3.2 · p. 30
• Idempotence, e⊗e=1, and monotonicity give e≤S1 and 1≤Se, so antisymmetry implies e=1.Source: A PROOF OF PROPOSITION 3.2 · p. 30
• The excerpt then begins the proof’s second claim by specializing (C1) at c=b=1.Source: A PROOF OF PROPOSITION 3.2 · p. 30

• Assuming a counterexample, the proof chooses the smallest index i for which a tree belongs to G_i but not the closure.Source: B PROOF OF LEMMA 4.1 · p. 30
• If the tree is formed by a vertical operation from G_(i−1), the induction assumption places its input in the closure and therefore places the tree there too.Source: B PROOF OF LEMMA 4.1 · p. 30
• The horizontal-operation case leads to the same contradiction, so no such smallest index exists.Source: B PROOF OF LEMMA 4.1 · p. 30

• The forward proof begins with generation zero and proceeds by induction on the generation index.Source: C PROOF OF LEMMA 4.5 · p. 30
• For the forward direction, induction on the generation index handles vertical tree construction by bracketing a path with matching push and pop transitions.Source: C PROOF OF LEMMA 4.5 · p. 30
• Horizontal tree construction combines paths through an intermediate state, multiplying their weights to obtain the tree’s weight.Source: C PROOF OF LEMMA 4.5 · p. 30
• For the reverse direction, induction on path length handles a split into two non-empty subpaths by combining their trees horizontally.Source: C PROOF OF LEMMA 4.5 · pp. 30–31
• When no such split exists, the path factors into push, an interior run, and matching pop transitions; the resulting tree has the path’s weight.Source: C PROOF OF LEMMA 4.5 · p. 31

D.1 Correctness

• For every ⟨T, σ⟩∈G_i, some ⟨T′, σ′⟩∈H_i satisfies σ(ε) ≤C fgt σ′(ε), and boundary normalization maps H_{i+1} trees back into H_i.Source: §D.1 · pp. 31–32
• Each H_i tree can be embedded into a sequence of initial FC trees preserving node states and satisfying the stated pumping-context properties.The properties cover root and node-state preservation, pumping contexts, and contexts associated with ancestor-descendant node pairs.Source: §D.1 · p. 32

D.2 Termination

• Every tree in H_i has height at most |Q|^2; a finite set of possible labels at the least recurring height then rules out infinitely many distinct trees and establishes termination.Source: §D.2 · pp. 35–36

D.3 Complexity

• Labels grow at most exponentially with tree height, giving maximum label size 2^O(|Q|^2), while the binary trees have at most 2^(|Q|^2+1) nodes.Source: §D.3 · p. 36

F QUALITATIVE NETWORK REACHABILITY IS DECIDABLE

• The qualitative reachability problem from asks whether a global configuration c′ is reachable from c and, if so, for a global trace.Source: F QUALITATIVE NETWORK REACHABILITY IS… · p. 37
• Atig et al. reduce acyclic networks to linear ones by topologically ordering processes and storing copies of preceding processes’ states, without merging or duplicating processes [8, Prop. 3].Copies are refreshed by observing the immediately preceding process, and guards are checked against the copy.Source: F QUALITATIVE NETWORK REACHABILITY IS… · p. 37
• For each root process, the downward closure of its context-free stuttering trace language is effectively regular, and an NFA product models asynchronous child observations.The downward closure accounts for a child missing some state occurrences in its parent’s trace.Source: F QUALITATIVE NETWORK REACHABILITY IS… · p. 37
• Repeating the construction to a leaf yields a product whose run exists exactly when ancestor runs are compatible; deciding it takes polynomial time in the final product size [8].A dual bottom-up approach iteratively computes upward closures to capture cases where a child need not observe every parent state.Source: F QUALITATIVE NETWORK REACHABILITY IS… · p. 37

G PROOF OF THEOREM 7.2

• The adapted fixpoint algorithm computes the required trace-language closures and corresponding trace weights simultaneously.In the Boolean-semiring case, the procedure reduces to the classical one.Source: G PROOF OF THEOREM 7.2 · p. 37
• The procedure first linearises the network, then reduces the task to computing GenConfigReach for linear networks.The proof relies on Lemma G.6 to show linearisation preserves each process’s weight.Source: G PROOF OF THEOREM 7.2 · p. 37
• The proof first establishes that the fixpoint computation preserves properties used later in the algorithm.Source: G PROOF OF THEOREM 7.2 · p. 38

G.1 Revisiting the Fixpoint Algorithm

• For ≥-thin pumping semirings, the product remains ≥-thin; for ≤-thin semirings, the nonzero-component product is a ≤-thin pumping subsemiring.The restriction to nonzero components is necessary: the unrestricted arctic-semiring product can violate condition (C1).Source: §G.1 · p. 38
• For ≤-thin weights, the auxiliary system tracks downward-closed traces and weights, with fixpoints supporting countable, totally ordered trace witnesses that cover specified words and sum to the tracked weight.The construction combines the downward closure of traces with their original weights; the witness property applies to every countable word set in the fixpoint expression.Source: §G.1 · pp. 38–39
• For ≥-thin weights, the auxiliary system tracks upward closures and weights, and each word in a fixpoint closure has a same-weight trace contained in that word’s downward closure.The upward-closure construction uses the product of the transition-language semiring and the weight semiring.Source: §G.1 · pp. 39–40

G.2 Asynchronous product

• Asynchronous products pad component alphabets with idling symbols, and the asynchronous product of regular languages is effectively computable.Each component’s projection erases idling symbols and must belong to that component’s language.Source: §G.2 · p. 40

G.3 The Algorithms

• A topological ordering linearizes the acyclic network by copying preceding processes’ states into each process’s control state, with refresh transitions updating those copies.The reduction preserves per-process weight aggregates because refresh steps have weight 1, and computes reachability for the original network.Source: §G.3 · pp. 40–41
• The top-down algorithm for ≤-thin semirings computes each child’s fixpoint for parent fixpoints, using downward-closure observations whose weights are supported by runs.Its observation automaton constrains the parent-state sequences a child can observe.Source: §G.3 · p. 41
• For ≥-thin semirings, the bottom-up algorithm uses an automata product that simulates a process while consuming constraints on its current state.The procedure is described as a weighted extension of the bottom-up approach.Source: §G.3 · p. 43
• Algorithm 4 gives the main routine of the bottom-up approach for ≥S-thin semirings.Source: §G.3 · p. 44
• The routine normalizes notation and intersects upward-closed constraint languages associated with child valuations.Source: §G.3 · p. 45
• Its fixpoint computation runs from an initial state to accepting states of the observation automaton, then returns fixpoints for the caller to extend val.Source: §G.3 · p. 45