---
OA_place: publisher
OA_type: gold
_id: '20253'
abstract:
- lang: eng
text: "A quantitative word automaton (QWA) defines a function from infinite words
to values. For example, every infinite run of a limit-average QWA \U0001D49C obtains
a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained
by nondeterministic runs of \U0001D49C over w. We introduce quantitative language
automata (QLAs) that define functions from language generators (i.e., implementations)
to values, where a language generator can be nonprobabilistic, defining a set
of infinite words, or probabilistic, defining a probability measure over infinite
words. A QLA consists of a QWA and an aggregator function. For example, given
a QWA \U0001D49C, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest
lower bound assigned by \U0001D49C to any word in L. For boolean value sets, QWAs
define boolean properties of traces, and QLAs define boolean properties of sets
of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a
specification language for a generalization of hyperproperties, called quantitative
hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty
assigns a value to each set (resp. distribution) G of traces, e.g., the minimal
(resp. expected) average response time exhibited by the traces in G. We give several
examples of quantitative hyperproperties and investigate three paradigmatic problems
for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem,
given a QLA \U0001D538 and an implementation G, we ask for the value that \U0001D538
assigns to G. In the nonemptiness (resp. universality) problem, given a QLA \U0001D538
and a value k, we ask whether \U0001D538 assigns at least k to some (resp. every)
language. We provide a comprehensive picture of decidability for these problems
for QLAs with common aggregators as well as their restrictions to ω-regular languages
and trace distributions generated by finite-state Markov chains."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LIPIcs
article_number: '21'
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: Pavol
full_name: Kebis, Pavol
id: 2e0132b3-4e98-11ef-b275-cf7281c2802a
last_name: Kebis
- 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
citation:
ama: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Quantitative language automata.
In: 36th International Conference on Concurrency Theory. Vol 348. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.CONCUR.2025.21'
apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2025).
Quantitative language automata. In 36th International Conference on Concurrency
Theory (Vol. 348). Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2025.21'
chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E
Sarac. “Quantitative Language Automata.” In 36th International Conference on
Concurrency Theory, Vol. 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025. https://doi.org/10.4230/LIPIcs.CONCUR.2025.21.
ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Quantitative
language automata,” in 36th International Conference on Concurrency Theory,
Aarhus, Denmark, 2025, vol. 348.
ista: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2025. Quantitative language
automata. 36th International Conference on Concurrency Theory. CONCUR: Conference
on Concurrency Theory, LIPIcs, vol. 348, 21.'
mla: Henzinger, Thomas A., et al. “Quantitative Language Automata.” 36th International
Conference on Concurrency Theory, vol. 348, 21, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025, doi:10.4230/LIPIcs.CONCUR.2025.21.
short: T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 36th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025.
conference:
end_date: 2025-08-29
location: Aarhus, Denmark
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2025-08-26
corr_author: '1'
date_created: 2025-08-31T22:01:32Z
date_published: 2025-08-18T00:00:00Z
date_updated: 2025-12-01T12:36:52Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2025.21
ec_funded: 1
external_id:
arxiv:
- '2506.0515'
isi:
- '001570540800021'
file:
- access_level: open_access
checksum: 9d4054058757a73477e6015b10ed6996
content_type: application/pdf
creator: dernst
date_created: 2025-09-03T10:01:53Z
date_updated: 2025-09-03T10:01:53Z
file_id: '20282'
file_name: 2025_CONCUR_HenzingerT.pdf
file_size: 1257397
relation: main_file
success: 1
file_date_updated: 2025-09-03T10:01:53Z
has_accepted_license: '1'
intvolume: ' 348'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 36th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959773898'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative language 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: 348
year: '2025'
...