pith. machine review for the scientific record. sign in

arxiv: 2605.12418 · v1 · submitted 2026-05-12 · 💻 cs.FL · cs.LO

Recognition: no theorem link

Extending QuAK with Nested Quantitative Automata

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

Pith reviewed 2026-05-13 02:28 UTC · model grok-4.3

classification 💻 cs.FL cs.LO
keywords nested quantitative automataquantitative automataflattening proceduresQuAKthreshold decision problemsemptinessuniversalityformal verification
0
0 comments X

The pith

Flattening procedures reduce nested quantitative automata to standard ones so QuAK can reuse its existing decision procedures.

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 to nested quantitative automata, which express properties such as average response time that require unbounded weights. It adds flattening procedures that convert NQAs into equivalent quantitative automata while keeping the answers to threshold questions unchanged. The reductions cover all decidable combinations of parent aggregators like limits and averages with child functions like extrema or bounded summations. Users can therefore write specifications in the richer NQA language and still obtain emptiness and universality results from the original QA routines. Benchmarks on response-time and resource-consumption examples confirm that the approach works in practice.

Core claim

Nested quantitative automata overcome the finite-weight restriction of quantitative automata by letting a parent automaton spawn child automata to compute values over finite infixes and then aggregate those values. The paper implements a suite of flattening procedures that reduce NQAs to QAs. These reductions preserve the answers to threshold decision problems, allowing QuAK to apply its existing procedures for emptiness and universality to the more expressive NQA formalism. The tool supports every combination of parent aggregators and child functions for which decidability is already known.

What carries the argument

Flattening procedures that convert nested quantitative automata into equivalent quantitative automata by resolving parent aggregators over child computations.

If this is right

  • Threshold decision problems for NQAs become solvable with the same algorithms used for QAs.
  • Properties involving unbounded values such as average response time or resource limits can now be checked in QuAK.
  • All combinations of limits, averages, extrema, and monotonic or bounded summations with known decidability results are handled.
  • Existing emptiness and universality procedures apply directly after flattening.

Where Pith is reading between the lines

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

  • Similar flattening techniques could be explored for other nested extensions of automata once their decidability is established.
  • The approach may help embed quantitative timing properties into broader model-checking toolchains without new solvers.
  • Benchmark results suggest the reductions remain practical when applied to larger system models.
  • Tool developers could reuse the same reduction pattern to widen the property languages supported by quantitative verifiers.

Load-bearing premise

The flattening procedures must correctly preserve semantics for every supported combination of parent aggregators and child functions.

What would settle it

An NQA and its flattened QA version that disagree on whether a given threshold property holds would demonstrate that the reduction fails to preserve semantics.

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 omega-automata 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 address 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 describes an extension of the Quantitative Automata Kit (QuAK) to support Nested Quantitative Automata (NQAs). The core contribution is a suite of flattening procedures that reduce NQAs to standard Quantitative Automata (QAs) for all supported combinations of parent aggregators (limits and averages) and child functions (extrema, monotonic or bounded summations). These reductions are claimed to preserve answers to threshold decision problems, allowing use of QuAK's existing decision procedures for emptiness and universality. Positive experimental results are reported on response-time and resource-consumption benchmarks.

Significance. If the flattening implementations are correct, the work supplies the first practical tool support for NQAs, enabling specification and analysis of quantitative properties (such as average response time) that exceed the finite-weight limitation of QAs. It reuses prior decidability results and QuAK infrastructure, with the implementation itself providing independent engineering value demonstrated via benchmarks.

major comments (2)
  1. [Flattening procedures section (implementation details)] The central preservation claim for the flattening procedures (parent limits/averages with all listed child functions) is load-bearing for the entire contribution, yet the manuscript provides neither machine-checked proofs of semantic equivalence nor an exhaustive test suite targeting the flattening logic itself. Only benchmark evidence on response-time and resource examples is given, which does not rule out subtle mismatches in limit or average aggregation cases.
  2. [§5] §5 (Experiments): the reported benchmarks demonstrate tool effectiveness but contain no targeted validation cases exercising the preservation property for edge combinations of aggregators and child functions, leaving the correctness guarantee unverified beyond the specific examples.
minor comments (2)
  1. [Abstract] The abstract states that the tool 'handles all combinations' for which decidability is known; a brief explicit enumeration of the supported parent/child pairs in the introduction or implementation section would improve clarity.
  2. [Preliminaries] Notation for the child functions (extrema, monotonic summations, bounded summations) could be introduced with a small table or diagram to aid readers unfamiliar with the prior NQA literature.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback and positive assessment of the work's significance. We address the concerns about verification of the flattening procedures point by point below, providing clarification on our theoretical grounding while agreeing to strengthen the validation evidence.

read point-by-point responses

  1. Referee: [Flattening procedures section (implementation details)] The central preservation claim for the flattening procedures (parent limits/averages with all listed child functions) is load-bearing for the entire contribution, yet the manuscript provides neither machine-checked proofs of semantic equivalence nor an exhaustive test suite targeting the flattening logic itself. Only benchmark evidence on response-time and resource examples is given, which does not rule out subtle mismatches in limit or average aggregation cases.

    Authors: The flattening reductions are grounded in the decidability results for threshold problems on the supported NQA classes from prior theoretical work, which we cite. The algorithms are described at a level that shows how parent aggregators (limits and averages) are simulated via state constructions that track running aggregates over child outputs, ensuring equivalence for the threshold queries. Machine-checked proofs are not provided, as the paper's focus is the practical tool extension rather than a full formal verification effort. The benchmarks exercise the relevant aggregations in realistic settings. To mitigate the risk of subtle mismatches, we will add a supplementary appendix with expanded unit tests covering all aggregator-child combinations and boundary conditions (e.g., diverging limits, zero averages). revision: partial

  2. Referee: [§5] §5 (Experiments): the reported benchmarks demonstrate tool effectiveness but contain no targeted validation cases exercising the preservation property for edge combinations of aggregators and child functions, leaving the correctness guarantee unverified beyond the specific examples.

    Authors: We agree that the current §5 emphasizes practical applicability on response-time and resource benchmarks rather than exhaustive coverage of edge cases for semantic preservation. In the revised version we will extend §5 with a dedicated validation subsection containing synthetic test suites that systematically exercise every combination of parent aggregator and child function, including edge cases such as infinite limits, constant-zero averages, and monotonic summations over minimal and maximal infix lengths. These cases will directly compare NQA and flattened QA results on threshold queries. revision: yes

Circularity Check

0 steps flagged

No circularity; implementation extends prior decidability results

full rationale

The paper's central contribution is the implementation of flattening procedures reducing NQAs to QAs while preserving threshold decision answers for supported aggregator/function combinations. This relies on previously established decidability results for emptiness and universality in QuAK, but does not reduce any claim to a self-definition, fitted input renamed as prediction, or unverified self-citation chain. The derivation chain consists of software engineering steps (reductions for limits/averages with extrema/summations) whose correctness is an external verification matter, not a circular reduction by construction. No equations or steps in the provided text exhibit the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper adds no new free parameters or invented entities. It relies on standard automata-theoretic background and previously published decidability results for the supported NQA fragments.

axioms (1)
  • domain assumption Emptiness and universality are decidable for the supported combinations of parent aggregators and child functions in NQAs.
    The tool extension is restricted to exactly those fragments for which decidability was already known.

pith-pipeline@v0.9.0 · 5510 in / 1178 out tokens · 49833 ms · 2026-05-13T02:28:43.069884+00:00 · methodology

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 · 23 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 14 T. A. Henzinger, N. Mazzocchi, N. E. Saraç, H. Yılmaz Formal Methods, Verification and Validation. Software Engineering Methodolo- gies - 12th International Symposium, ISoLA 2024, Crete, Greece, Octo...

    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 on Theory and Practice of Software, ET...

    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]

    In: Touili, T., Cook, B., Jackson, P.B

    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]

    Lecture Notes in Computer Science, vol

    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 Extending QuAK with Nested Quantitative Automata 15 the Third International Workshop on Hybrid Systems, Ithaca, NY, USA, October

    work page

  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

    work page 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/

    work page 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]

    paritizing

    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