pith. sign in

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-06-30 21:58 UTC · model grok-4.3

classification 💻 cs.FL cs.LO
keywords quantitative automatanested quantitative automataflattening proceduresthreshold decision problemsemptinessuniversalityresponse time propertiesresource consumption
0
0 comments X

The pith

Nested quantitative automata reduce to ordinary quantitative automata through flattening procedures that preserve 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 support for nested quantitative automata in an existing analysis tool by supplying flattening procedures. These procedures convert the nested structures into standard quantitative automata so that existing decision methods can be applied directly. The reductions are designed to keep the answers to threshold questions unchanged. Coverage includes every parent-aggregator and child-function pair for which emptiness and universality remain decidable. The result is that properties involving unbounded values, such as average response time, become checkable in practice.

Core claim

Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging 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.

What carries the argument

Flattening procedures that translate nested quantitative automata into equivalent quantitative automata while preserving threshold answers.

If this is right

  • Users can write specifications in the more expressive NQA syntax and obtain correct threshold answers via the reductions.
  • All supported combinations of parent aggregators and child functions become practically decidable inside the tool.
  • Properties such as average response time and resource consumption over finite infixes can now be analyzed directly.
  • Existing decision procedures for emptiness and universality apply unchanged to the flattened automata.

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 reusable for other forms of nesting that appear in quantitative specification languages.
  • Tool chains that already accept ordinary quantitative automata could gain NQA support with modest additional engineering.
  • Verification tasks involving unbounded quantitative measures over segments of executions become more routinely feasible.

Load-bearing premise

The flattening procedures correctly preserve threshold answers for every parent-aggregator and child-function combination where emptiness and universality are known to be decidable.

What would settle it

A concrete NQA, threshold value, and parent-aggregator/child-function pair for which the emptiness or universality answer on the original NQA differs from the answer on its flattened QA.

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. 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. Figure 2: The extended architecture of QuAK. Shaded components are new in this ver￾sion. 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 prob￾lem 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. Figure 3: The response-time automaton A2,2 = (A2,2, A1). Every parent transition with￾out 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. Figure 4: The resource-consumption automaton B1,2 = (B1,2, B1). Every parent transi￾tion 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 fol￾lows 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.

Referee Report

2 major / 2 minor

Summary. The paper extends the Quantitative Automata Kit (QuAK) to support Nested Quantitative Automata (NQAs). NQAs allow a parent automaton to spawn child automata computing unbounded values over finite infixes, which are then aggregated. The core contribution is a suite of flattening procedures reducing NQAs to standard QAs while preserving answers to threshold decision problems. The tool supports all parent-aggregator/child-function combinations (limits, averages; extrema, monotonic/bounded summations) for which emptiness and universality are known to be decidable. Effectiveness is demonstrated via experiments on response-time and resource-consumption benchmarks.

Significance. If the flattening reductions are correct, the work supplies the first practical tool support for NQAs, enabling specification and analysis of quantitative properties (e.g., average response time) that exceed the finite-weight limitation of ordinary QAs. It directly leverages prior decidability results and existing QuAK procedures, turning theoretical expressiveness into usable verification capability for system properties involving unbounded values.

major comments (2)
  1. [Abstract] Abstract (core contribution paragraph): The central claim that the implemented flattening procedures 'preserve the answers to threshold decision problems' for every listed aggregator/function pair is asserted without any derivation, proof sketch, pseudocode, or case analysis. The preservation guarantee is load-bearing for the entire contribution, yet the manuscript provides no formal argument or verification that each reduction is correct.
  2. [Flattening procedures section] Section describing the flattening procedures (exact section number not visible in metadata): No explicit statement or table enumerates the handling of each parent aggregator (limits, averages, etc.) paired with each child function (extrema, summations), nor shows how threshold preservation is maintained under nesting. Without this, it is impossible to assess whether off-by-one cases, limit handling, or aggregation composition are correctly implemented for all decidable combinations.
minor comments (2)
  1. [Abstract] The abstract and introduction should explicitly reference the prior decidability results (emptiness/universality) that the tool relies upon, including citation to the relevant papers.
  2. [Experiments] Benchmark section: clarify whether the reported experiments test all supported aggregator/function combinations or only a subset; if the latter, state the coverage explicitly.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback highlighting the need for stronger justification of the flattening procedures. We will revise the manuscript to address both major comments by adding explicit arguments and enumerations.

read point-by-point responses

  1. Referee: [Abstract] Abstract (core contribution paragraph): The central claim that the implemented flattening procedures 'preserve the answers to threshold decision problems' for every listed aggregator/function pair is asserted without any derivation, proof sketch, pseudocode, or case analysis. The preservation guarantee is load-bearing for the entire contribution, yet the manuscript provides no formal argument or verification that each reduction is correct.

    Authors: We agree that the abstract asserts preservation without a supporting argument in the provided manuscript text. The procedures are intended to reduce NQAs to QAs while preserving threshold answers by construction, drawing on the known decidability results for the listed combinations. In revision we will add a proof sketch (or case analysis) either in the main text or an appendix to substantiate the claim. revision: yes

  2. Referee: [Flattening procedures section] Section describing the flattening procedures (exact section number not visible in metadata): No explicit statement or table enumerates the handling of each parent aggregator (limits, averages, etc.) paired with each child function (extrema, summations), nor shows how threshold preservation is maintained under nesting. Without this, it is impossible to assess whether off-by-one cases, limit handling, or aggregation composition are correctly implemented for all decidable combinations.

    Authors: We will revise the flattening procedures section to include an explicit table or enumerated list of all supported parent-aggregator / child-function pairs together with a brief description of the reduction for each pair and how it maintains the threshold decision problem (including notes on limit handling and composition). This will make the coverage of decidable cases transparent. revision: yes

Circularity Check

0 steps flagged

No circularity: flattening procedures are constructive implementations relying on external decidability results

full rationale

The paper describes an implementation of flattening reductions from NQAs to QAs that preserve threshold answers for combinations where emptiness and universality are known to be decidable. The abstract explicitly states these reductions leverage QuAK's existing decision procedures and handle cases based on prior known decidability, without any self-referential definitions, fitted parameters renamed as predictions, or load-bearing self-citations that reduce the central claim to its own inputs. The derivation chain consists of software procedures whose correctness is asserted via reference to independently established decidability results rather than internal construction or renaming.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the prior theoretical result that emptiness and universality are decidable for the listed parent/child combinations; the paper contributes only the implementation of the reductions.

axioms (1)
  • domain assumption Emptiness and universality are decidable for the handled combinations of parent aggregators and child functions
    Abstract states the tool handles exactly those combinations for which decidability is known.

pith-pipeline@v0.9.1-grok · 5743 in / 1248 out tokens · 19558 ms · 2026-06-30T21:58:37.709474+00:00 · methodology

Review history (3 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 20 canonical work pages

  1. [1]

    In: Abdulla, P.A., Leino, K.R.M

    Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-taliro: A tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Con- ferences on Theory and Practice of ...

    work page doi:10.1007/978-3-642-19835-9_21 2011

  2. [2]

    In: Pérez, G.A., Raskin, J

    Boker, U., Henzinger, T.A., Mazzocchi, N., Saraç, N.E.: Safety and liveness of quantitative automata. In: Pérez, G.A., Raskin, J. (eds.) 34th International Con- ference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium. LIPIcs, vol. 279, pp. 17:1–17:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023).https://doi.org/10.4...

    work page doi:10.4230/lipics.concur.2023.17 2023

  3. [3]

    Boker,U.,Henzinger,T.A.,Mazzocchi,N.,Saraç,N.E.:Safetyandlivenessofquan- titative properties and automata. Log. Methods Comput. Sci.21(2) (2025).https: //doi.org/10.46298/LMCS-21(2:2)2025,https://doi.org/10.46298/lmcs-21(2: 2)2025

    work page doi:10.46298/lmcs-21(2:2)2025 2025

  4. [4]

    In: 26th IEEE/ACM Interna- tional Conference on Automated Software Engineering, ASE 2011

    Bokor, P., Kinder, J., Serafini, M., Suri, N.: Supporting domain-specific state space reductions through local partial-order reduction. In: 26th IEEE/ACM Interna- tional Conference on Automated Software Engineering, ASE 2011. pp. 113–122. IEEE (2011).https://doi.org/10.1109/ASE.2011.6100044

    work page doi:10.1109/ase.2011.6100044 2011

  5. [5]

    Information and Computation98(2), 142–170 (1992).https://doi.org/10.1016/0890-5401(92)90017-A

    Burch,J.R.,Clarke,E.M.,McMillan,K.L.,Dill,D.L.,Hwang,L.J.:Symbolicmodel checking: 10ˆ20 states and beyond. Information and Computation98(2), 142–170 (1992).https://doi.org/10.1016/0890-5401(92)90017-A

    work page doi:10.1016/0890-5401(92)90017-a 1992

  6. [6]

    In: Margaria, T., Steffen, B

    Chalupa, M., Henzinger, T.A., Mazzocchi, N., Saraç, N.E.: Quak: Quantitative automata kit. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodolo- gies - 12th International Symposium, ISoLA 2024, Crete, Greece, October 27-31, 2024, Proceedings, Part IV. Lecture Notes in C...

    work page doi:10.1007/978-3-031-75387-9_1 2024

  7. [7]

    In: Gurfinkel, A., Heule, M

    Chalupa, M., Henzinger, T.A., Mazzocchi, N., Saraç, N.E.: Automating the anal- ysis of quantitative automata with quak. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences 14 T. A. Henzinger, N. Mazzocchi, N. E...

    work page doi:10.1007/978-3-031-90643-5_16 2025

  8. [8]

    ACM Trans

    Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log.11(4), 23:1–23:38 (2010).https://doi.org/10.1145/1805950. 1805953

    work page doi:10.1145/1805950 2010

  9. [9]

    In: Faliszewski, P., Muscholl, A., Niedermeier, R

    Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted limit-average automata of bounded width. In: Faliszewski, P., Muscholl, A., Niedermeier, R. (eds.) 41st In- ternational Symposium on Mathematical Foundations of Computer Science, MFCS 2016, Kraków, Poland, August 22-26, 2016. LIPIcs, vol. 58, pp. 24:1–24:14. Schloss Dagstuhl - Leibniz-Zentrum für ...

    work page doi:10.4230/lipics.mfcs.2016.24 2016

  10. [10]

    In: Rival, X

    Chatterjee, K., Henzinger, T.A., Otop, J.: Quantitative monitor automata. In: Rival, X. (ed.) Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings. Lecture Notes in Com- puter Science, vol. 9837, pp. 23–38. Springer (2016).https://doi.org/10.1007/ 978-3-662-53413-7 _2,https://doi.org/10.1007/978-3-662-...

    work page doi:10.1007/978-3-662-53413-7 2016

  11. [11]

    ACM Trans

    Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted automata. ACM Trans. Comput. Log.18(4), 31:1–31:44 (2017).https://doi.org/10.1145/3152769

    work page doi:10.1145/3152769 2017

  12. [12]

    In: Konstantinidis, S

    Demaille, A., Duret-Lutz, A., Lombardy, S., Sakarovitch, J.: Implementation con- cepts in vaucanson 2. In: Konstantinidis, S. (ed.) Implementation and Application of Automata - 18th International Conference, CIAA 2013, Halifax, NS, Canada, July 16-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7982, pp. 122–133. Springer (2013).https://doi...

    work page doi:10.1007/978-3-642-39274-0_12 2013

  13. [13]

    Abc: an academic industrial- strength verification tool,

    Donzé, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verifica- tion, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6174, pp. 167–170. Springer (2010).https://doi.org/10.1007/978-...

    work page doi:10.1007/978-3-642-14295-6 2010

  14. [14]

    In: Shoham, S., Vizel, Y

    Doveri, K., Ganty, P., Mazzocchi, N.: Forq-based language inclusion formal test- ing. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th Interna- tional Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 109–129. Springer (2022). https://doi.org/10.1007/978-3-03...

    work page doi:10.1007/978-3-031-13188-2 2022

  15. [15]

    Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilis- tic model checker storm. Int. J. Softw. Tools Technol. Transf.24(4), 589– 610 (2022).https://doi.org/10.1007/S10009-021-00633-Z,https://doi.org/ 10.1007/s10009-021-00633-z

    work page doi:10.1007/s10009-021-00633-z 2022

  16. [16]

    In: Antsak- lis, P.J., Kohn, W., Nerode, A., Sastry, S

    Henzinger, T.A., Ho, P.: HYTECH: the cornell hybrid technology tool. In: Antsak- lis, P.J., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems II, Proceedings of the Third International Workshop on Hybrid Systems, Ithaca, NY, USA, October

  17. [17]

    Lecture Notes in Computer Science, vol. 999, pp. 265–293. Springer (1994). https://doi.org/10.1007/3-540-60472-3 _14

    work page doi:10.1007/3-540-60472-3 1994

  18. [18]

    In: Kupferman, O., Sobocinski, P

    Henzinger, T.A., Mazzocchi, N., Saraç, N.E.: Quantitative safety and liveness. In: Kupferman, O., Sobocinski, P. (eds.) Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Pr...

    work page doi:10.1007/978-3-031-30829-1 2023

  19. [19]

    In: Field, T., Harrison, P.G., Bradley, J.T., Harder, U

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J.T., Harder, U. (eds.) Com- puter Performance Evaluation, Modelling Techniques and Tools 12th Interna- tional Conference, TOOLS 2002, London, UK, April 14-17, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2324, pp. ...

    work page doi:10.1007/3-540-46029-2 2002

  20. [20]

    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf.1(1-2), 134–152 (1997).https://doi.org/10.1007/ S100090050010

    1997

  21. [21]

    Lombardy, S., Marsault, V., Sakarovitch, J.: Awali, a library for weighted automata and transducers (version 2.3) (2022), software available at http://vaucanson- project.org/Awali/2.3/

    2022

  22. [22]

    In: Ibarra, O.H., Dang, Z

    Lombardy, S., Poss, R., Régis-Gianas, Y., Sakarovitch, J.: Introducing VAUCAN- SON. In: Ibarra, O.H., Dang, Z. (eds.) Implementation and Application of Au- tomata,8thInternationalConference,CIAA2003,SantaBarbara,California,USA, July 16-18, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2759, pp. 96–107. Springer (2003).https://doi.org/10.1007/...

    work page doi:10.1007/3-540-45089-0_10 2003

  23. [23]

    In: Hung, D.V., Sokolsky, O

    Nickovic, D., Yamaguchi, T.: RTAMT: online robustness monitors from STL. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Anal- ysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12302, pp. 564–571. Springer (2020).https://doi.org/10.1007/97...

    work page doi:10.1007/978-3-030-59152-6 2020