Extending QuAK with Nested Quantitative Automata

Harun Y{\i}lmaz; N. Ege Sara\c{c}; Nicolas Mazzocchi; Thomas A. Henzinger

arxiv: 2605.12418 · v4 · pith:QZB762IOnew · submitted 2026-05-12 · 💻 cs.FL · cs.LO

Extending QuAK with Nested Quantitative Automata

Thomas A. Henzinger , Nicolas Mazzocchi , N. Ege Sara\c{c} , Harun Y{\i}lmaz This is my paper

Pith reviewed 2026-05-20 21:29 UTC · model grok-4.3

classification 💻 cs.FL cs.LO

keywords nested quantitative automataquantitative automataflattening proceduresthreshold decision problemsQuAK toolautomata on infinite wordsformal verificationresponse time properties

0 comments

The pith

Flattening procedures reduce nested quantitative automata to ordinary ones while preserving answers to threshold decision problems.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends the QuAK tool so that users can now specify properties with unbounded values using nested quantitative automata. It achieves this by adding flattening procedures that convert NQAs into standard quantitative automata. The conversions keep the results of threshold questions unchanged for the supported cases. A reader would care because this gives practical analysis support for properties such as average response times or resource consumption that involve values growing without bound.

Core claim

The authors implement a suite of flattening procedures that reduce nested quantitative automata to quantitative automata. These reductions preserve the answers to threshold decision problems, allowing QuAK's existing decision procedures to be used on the more expressive NQA formalism for all combinations of parent aggregators including limits and averages and child functions including extrema and monotonic or bounded summations where emptiness and universality are decidable.

What carries the argument

The flattening procedures that translate an NQA into an equivalent QA by composing parent aggregators with child functions.

If this is right

Users can express properties involving arbitrarily large values such as average response times and still obtain correct threshold answers from QuAK.
Emptiness and universality remain decidable for all the listed combinations of aggregators and child functions.
The tool now covers both response-time and resource-consumption benchmarks that require nested structure.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same flattening idea might be tested on other quantitative models that allow nesting or recursion.
Performance of the reductions on large state spaces could be measured to see where direct NQA algorithms would still be useful.

Load-bearing premise

The flattening procedures correctly preserve threshold answers for every supported parent aggregator and child function.

What would settle it

A concrete NQA together with one of its supported aggregator-function pairs and a threshold value where the original NQA and its flattened QA disagree on whether the threshold is met.

Figures

Figures reproduced from arXiv: 2605.12418 by Harun Y{\i}lmaz, N. Ege Sara\c{c}, Nicolas Mazzocchi, Thomas A. Henzinger.

**Figure 1.** Figure 1: A (LimSupAvg, Sum+)-automaton A = (A, C) for average response time. Left: Parent A spawns child C on each request. Child C accumulates weight 1 per step until a grant, then terminates. Right: On the shown prefix, the spawned instances of C return 5 and 2; the third instance is still active. Silent transitions (marked ⊥) do not contribute to the parent’s value, so the running average after the event g is 7 … view at source ↗

**Figure 2.** Figure 2: The extended architecture of QuAK. Shaded components are new in this version. A nested quantitative automaton (NQA) is flattened into a standard quantitative automaton (QA) and fed to existing decision procedures. (4) Limit-average with unbounded children. Recall that the universality problem for limit-average QAs is undecidable, and this extends to NQAs with any child aggregator; we therefore focus on e… view at source ↗

**Figure 3.** Figure 3: The response-time automaton A2,2 = (A2,2, A1). Every parent transition without a child automaton annotation is silent. Availability and Usage QuAK is open-source under the MIT license and available online.1 The tool has no external dependencies other than a C++17 compiler. Instructions and examples are provided in the repository’s README. 4 Experimental Evaluation We evaluate QuAK’s new capabilities along… view at source ↗

**Figure 4.** Figure 4: The resource-consumption automaton B1,2 = (B1,2, B1). Every parent transition without a child automaton annotation is silent. The rejecting sink state of the child automaton and transitions to it are not shown. Every child transition without a weight annotation has weight 0. Universality of (Sup, SumB)-automata Table 2c shows that universality follows a similar pattern: runtime grows rapidly in both para… view at source ↗

read the original abstract

Quantitative automata (QAs) extend finite-state automata on infinite words with weighted transitions to specify quantitative system properties. However, their finite weight sets rule out properties like average response time, where response times can be arbitrarily large. Nested quantitative automata (NQAs) overcome this limitation: a parent automaton spawns child automata to compute unbounded values over finite infixes and aggregates them into a final result. Despite this expressiveness, NQAs have lacked practical tool support to date. We close this gap by extending the Quantitative Automata Kit (QuAK), a software tool for QA analysis, to support NQAs. Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging QuAK's existing decision procedures. These reductions preserve the answers to threshold decision problems, while allowing users to specify properties in the more expressive NQA formalism. The tool handles all combinations of parent aggregators (including limits and averages) and child functions (extrema and monotonic or bounded summations) for which emptiness and universality are known to be decidable. Experiments on response-time and resource-consumption benchmarks demonstrate QuAK's effectiveness.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper adds practical tool support for nested quantitative automata inside QuAK by implementing flattening reductions to existing QA procedures.

read the letter

The main takeaway is that the authors have extended the QuAK tool with flattening procedures that turn nested quantitative automata into ordinary quantitative automata. This lets users write properties involving unbounded values such as average response time while still using the existing decision procedures for emptiness and universality. The work stays within the fragments where those problems are already known to be decidable, covering parent aggregators like limits and averages paired with child functions like extrema or monotonic summations. Experiments on response-time and resource-consumption benchmarks are included to show the implementation runs on realistic cases. That is the concrete advance: prior papers defined NQAs but left them without a working tool. The reductions are presented as preserving threshold answers, which aligns with the goal of reusing QuAK without new algorithms from scratch. The engineering choice to delegate to prior procedures keeps the scope manageable and avoids reinventing the core decision machinery. A reader who already knows QuAK or works on quantitative properties in automata will see a direct path to specifying more expressive properties without leaving the framework. The soft spots are mostly about presentation and verification depth. The text asserts that the flattening steps preserve the answers but supplies no proof sketches, reduction rules, or small examples that would let a reader check the claim quickly. The benchmark results are described as successful without numbers on runtime, memory, or how the instances were selected. These gaps are typical for a tool-extension paper rather than fatal, yet they make it harder to assess the reductions without reading the code or the earlier NQA theory papers. The scope limitation to decidable cases is stated clearly, so there is no overclaim. This paper is for the formal-methods subgroup that builds or uses automata tools for quantitative verification. A specialist in that area would get value from seeing how the reductions are realized in practice and from having a working implementation to try. It does not change broad verification practice, but it removes a practical barrier for NQA users. I would send it to peer review. The contribution is focused and the central claim is plausible given the cited prior work on NQAs and QuAK. Referees could usefully comment on the reduction details and the benchmark design.

Referee Report

1 major / 2 minor

Summary. The paper claims to extend the Quantitative Automata Kit (QuAK) to support Nested Quantitative Automata (NQAs) via a suite of flattening procedures that reduce NQAs to standard Quantitative Automata (QAs). These reductions are asserted to preserve answers to threshold decision problems for all combinations of parent aggregators (including limits and averages) and child functions (extrema, monotonic or bounded summations) for which emptiness and universality are known to be decidable. The work includes experiments on response-time and resource-consumption benchmarks to demonstrate effectiveness.

Significance. If the flattening procedures correctly preserve threshold answers, the contribution would be significant by providing the first practical tool support for NQAs, enabling analysis of quantitative properties with unbounded values (such as average response time) that finite-weight QAs cannot express. It leverages existing QuAK decision procedures and supplies an implementation with benchmark experiments, which are strengths for reproducibility in the field.

major comments (1)

[Flattening procedures (and Abstract)] The manuscript asserts that the flattening procedures preserve threshold answers for the supported parent aggregators and child functions, but provides no proof sketch, derivation, or formal argument establishing this preservation (see Abstract and the section on flattening procedures). This is load-bearing for the central claim, as the reductions are the core contribution and the text delegates correctness to prior QuAK procedures without detailing how the new flattening steps maintain the property for limits, averages, extrema, and summations.

minor comments (2)

[Experiments section] The description of the benchmark experiments lacks specific metrics, success rates, or comparison baselines, which would clarify the effectiveness claim.
[Preliminaries or definitions] Notation for parent aggregators and child functions could be introduced more explicitly with examples to aid readers unfamiliar with the NQA formalism.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for recognizing the potential significance of extending QuAK to support Nested Quantitative Automata. We address the major comment below.

read point-by-point responses

Referee: [Flattening procedures (and Abstract)] The manuscript asserts that the flattening procedures preserve threshold answers for the supported parent aggregators and child functions, but provides no proof sketch, derivation, or formal argument establishing this preservation (see Abstract and the section on flattening procedures). This is load-bearing for the central claim, as the reductions are the core contribution and the text delegates correctness to prior QuAK procedures without detailing how the new flattening steps maintain the property for limits, averages, extrema, and summations.

Authors: We agree that the current version of the manuscript lacks an explicit proof sketch or derivation for why the flattening procedures preserve the answers to threshold decision problems. While the procedures are constructed to reduce NQAs to QAs in a manner that composes with the existing decidability results for the supported parent aggregators (limits and averages) and child functions (extrema, monotonic summations, and bounded summations), we acknowledge that delegating correctness solely to prior QuAK results without detailing the preservation invariants leaves a gap. In the revised manuscript we will add a proof sketch to the flattening procedures section (and update the abstract accordingly). The sketch will outline the key steps: how each flattening transformation maintains the threshold value by preserving the aggregation semantics over finite infixes, ensuring that emptiness and universality queries on the resulting QA yield the same answers as on the original NQA for the listed combinations. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The manuscript describes a software implementation of flattening reductions from NQAs to QAs that delegate to QuAK's pre-existing decision procedures for emptiness and universality. No equations, fitted parameters, or self-referential definitions appear in the provided text. The central claim is an engineering reduction whose correctness is asserted by explicit construction and scope restriction to decidable cases, without any load-bearing self-citation chain or renaming of prior results as new derivations. This is a self-contained tool-extension paper whose claims rest on independent implementation details and benchmark experiments rather than any circular reduction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that the chosen flattening procedures are semantics-preserving for the listed aggregator and child-function combinations. No free parameters, new entities, or ad-hoc axioms are introduced beyond standard decidability results for quantitative automata.

axioms (1)

domain assumption Emptiness and universality are decidable for the parent/child combinations handled by the flattening procedures.
Abstract states that the tool covers exactly those combinations for which decidability is already known.

pith-pipeline@v0.9.0 · 5743 in / 1183 out tokens · 41787 ms · 2026-05-20T21:29:50.571342+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging QuAK's existing decision procedures. These reductions preserve the answers to threshold decision problems.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.