---
OA_place: publisher
OA_type: hybrid
_id: '22754'
abstract:
- lang: eng
text: "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."
acknowledgement: This work was supported by the European Research Council (ERC) Grants
VAMOS (No. 101020093) and HYPER (No. 101055412).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
- first_name: Harun
full_name: Yılmaz, Harun
last_name: Yılmaz
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE, Yılmaz H. Extending QuAK with nested
quantitative automata. In: 38th International Conference on Computer Aided
Verification. Vol 16683. Springer Nature; 2026:418-432. doi:10.1007/978-3-032-32526-6_20'
apa: 'Henzinger, T. A., Mazzocchi, N. A., Sarac, N. E., & Yılmaz, H. (2026).
Extending QuAK with nested quantitative automata. In 38th International Conference
on Computer Aided Verification (Vol. 16683, pp. 418–432). Lisbon, Portugal:
Springer Nature. https://doi.org/10.1007/978-3-032-32526-6_20'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, Naci E Sarac, and Harun
Yılmaz. “Extending QuAK with Nested Quantitative Automata.” In 38th International
Conference on Computer Aided Verification, 16683:418–32. Springer Nature,
2026. https://doi.org/10.1007/978-3-032-32526-6_20.
ieee: T. A. Henzinger, N. A. Mazzocchi, N. E. Sarac, and H. Yılmaz, “Extending QuAK
with nested quantitative automata,” in 38th International Conference on Computer
Aided Verification, Lisbon, Portugal, 2026, vol. 16683, pp. 418–432.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE, Yılmaz H. 2026. Extending QuAK with nested
quantitative automata. 38th International Conference on Computer Aided Verification.
CAV: Computer Aided Verification, LNCS, vol. 16683, 418–432.'
mla: Henzinger, Thomas A., et al. “Extending QuAK with Nested Quantitative Automata.”
38th International Conference on Computer Aided Verification, vol. 16683,
Springer Nature, 2026, pp. 418–32, doi:10.1007/978-3-032-32526-6_20.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, H. Yılmaz, in:, 38th International
Conference on Computer Aided Verification, Springer Nature, 2026, pp. 418–432.
conference:
end_date: 2026-07-29
location: Lisbon, Portugal
name: 'CAV: Computer Aided Verification'
start_date: 2026-07-26
das_tickbox: '1'
dataavailabilitystatement: 'The artifact supporting the experimental results in this
paper is available in the QuAK repository at https://github.com/ista-vamos/nested-quak.
It contains the extended QuAK implementation, benchmark generators, example inputs,
and scripts/logs for reproducing the reported tables. The artifact is intended to
reproduce the experiments under the setup described in Sect. 4; runtimes may vary
across machines, and the reported timeout and memory-exhaustion results depend on
the stated hardware limits. No sensitive or restricted data are used. An archived
version is available on Zenodo at DOI: http://doi.org/10.5281/zenodo.19844606.'
date_created: 2026-08-23T22:01:47Z
date_published: 2026-01-01T00:00:00Z
date_updated: 2026-09-09T06:37:41Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-032-32526-6_20
ec_funded: 1
external_id:
arxiv:
- '2605.12418'
file:
- access_level: open_access
checksum: 043ba7b83f28d036d5a0e6e70a52cc9a
content_type: application/pdf
creator: dernst
date_created: 2026-09-09T06:33:55Z
date_updated: 2026-09-09T06:33:55Z
file_id: '22861'
file_name: 2026_LNCS_HenzingerT.pdf
file_size: 425988
relation: main_file
success: 1
file_date_updated: 2026-09-09T06:33:55Z
fulldoi: https://doi.org/10.1007/978-3-032-32526-6_20
has_accepted_license: '1'
intvolume: ' 16683'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 418-432
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 38th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032325259'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: no
title: Extending QuAK with nested quantitative automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16683
year: '2026'
...