---
res:
  bibo_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.\r\n\r\nWe 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.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-2985-7724
  - foaf_Person:
      foaf_givenName: Nicolas Adrien
      foaf_name: Mazzocchi, Nicolas Adrien
      foaf_surname: Mazzocchi
      foaf_workInfoHomepage: http://www.librecat.org/personId=b26baa86-3308-11ec-87b0-8990f34baa85
  - foaf_Person:
      foaf_givenName: Naci E
      foaf_name: Sarac, Naci E
      foaf_surname: Sarac
      foaf_workInfoHomepage: http://www.librecat.org/personId=8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  - foaf_Person:
      foaf_givenName: Harun
      foaf_name: Yılmaz, Harun
      foaf_surname: Yılmaz
  bibo_doi: 10.1007/978-3-032-32526-6_20
  bibo_volume: 16683
  dct_date: 2026^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0302-9743
  - http://id.crossref.org/issn/1611-3349
  - http://id.crossref.org/issn/9783032325259
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_title: Extending QuAK with nested quantitative automata@
...