---
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'
...
---
OA_place: publisher
_id: '20147'
abstract:
- lang: eng
text: "Quantitative properties offer a framework for specifying and verifying system
behaviors beyond the traditional boolean perspective. For example, while a boolean
property may specify whether a server eventually grants every request it receives,
a quantitative one may map each server execution to its average response time.
This quantitative view is relatively well-studied in the context of static verification.
However, although such properties often appear in practice as performance or robustness
measures in a dynamic verification context, a general theoretical framework for
their analysis and classification from a monitoring perspective is still missing.\r\n\r\nIn
this thesis, we aim to develop such a framework that takes resource-precision
tradeoffs of monitors as a central consideration. We present the first theory
of monitorability for quantitative properties where monitors can be naturally
approximate and compared regarding their precision and resource use. In particular,
we show that additional monitor resources such as registers or states lead to
strictly better approximations for some properties. To enable such analyses in
a machine-model independent way, we describe an abstract notion of monitors that
can be instantiated with concrete models of monitors. Within this framework, we
study how abstract monitors behave and identify classes of properties amenable
to approximate monitoring with resource-precision considerations. We then extend
the boolean safety-liveness dichotomy and safety-progress hierarchy to the quantitative
setting with a monitoring perspective. In particular, we prove that every property
is the pointwise minimum of a safety property and a liveness property, and properties
that are both safe and co-safe can be approximately monitored arbitrarily precisely
using only finitely many states. We also study the classes of quantitative properties
definable by finite-state quantitative automata and provide algorithms for deciding
their safety or liveness as well as their safety-liveness decompositions. Finally,
we present the first general-purpose tool for automating the analysis, verification,
and monitoring of quantitative automata.\r\n\r\n--------------------------------------------------------------------------------------------------------------------------------------------------------------
In reference to IEEE copyrighted material which is used with permission in this
thesis, the IEEE does not\r\nendorse any of ISTA's products or services. Internal
or personal use of this\r\nmaterial is permitted. If interested in reprinting/republishing
IEEE copyrighted material for advertising or promotional\r\npurposes or for creating
new collective works for resale or redistribution, please go to\r\nhttp://www.ieee.org/publications_standards/publications/rights/rights_link.html
to learn how to obtain a License from\r\nRightsLink.\r\n"
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)\r\nunder
grant Z211-N23 (Wittgenstein Award) and the ERC-2020-AdG 101020093.\r\n"
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: Sarac NE. A monitoring-oriented theory and classification of quantitative specifications.
2025. doi:10.15479/AT-ISTA-20147
apa: Sarac, N. E. (2025). A monitoring-oriented theory and classification of
quantitative specifications. Institute of Science and Technology Austria.
https://doi.org/10.15479/AT-ISTA-20147
chicago: Sarac, Naci E. “A Monitoring-Oriented Theory and Classification of Quantitative
Specifications.” Institute of Science and Technology Austria, 2025. https://doi.org/10.15479/AT-ISTA-20147.
ieee: N. E. Sarac, “A monitoring-oriented theory and classification of quantitative
specifications,” Institute of Science and Technology Austria, 2025.
ista: Sarac NE. 2025. A monitoring-oriented theory and classification of quantitative
specifications. Institute of Science and Technology Austria.
mla: Sarac, Naci E. A Monitoring-Oriented Theory and Classification of Quantitative
Specifications. Institute of Science and Technology Austria, 2025, doi:10.15479/AT-ISTA-20147.
short: N.E. Sarac, A Monitoring-Oriented Theory and Classification of Quantitative
Specifications, Institute of Science and Technology Austria, 2025.
corr_author: '1'
date_created: 2025-08-07T15:57:57Z
date_published: 2025-08-07T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '07'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/AT-ISTA-20147
ec_funded: 1
file:
- access_level: closed
checksum: 0f3015f1db36576a23d8d669afb60b41
content_type: application/x-zip-compressed
creator: esarac
date_created: 2025-08-21T09:40:28Z
date_updated: 2025-09-10T08:19:51Z
file_id: '20200'
file_name: 2025_Sarac_NaciEge_Thesis.zip
file_size: 8884801
relation: source_file
- access_level: open_access
checksum: 332ed2fe61f580641664ec3f05d30f14
content_type: application/pdf
creator: esarac
date_created: 2025-08-21T09:40:34Z
date_updated: 2025-08-21T09:40:34Z
file_id: '20201'
file_name: 2025_Sarac_NaciEge_Thesis.pdf
file_size: 2955584
relation: main_file
success: 1
file_date_updated: 2025-09-10T08:19:51Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: '149'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '11775'
relation: part_of_dissertation
status: public
- id: '13140'
relation: part_of_dissertation
status: deleted
- id: '19741'
relation: part_of_dissertation
status: public
- id: '9356'
relation: part_of_dissertation
status: public
- id: '19643'
relation: part_of_dissertation
status: deleted
- id: '17634'
relation: part_of_dissertation
status: public
- id: '20342'
relation: part_of_dissertation
status: public
- id: '13221'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: A monitoring-oriented theory and classification of quantitative specifications
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: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2025'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
PlanS_conform: '1'
_id: '20342'
abstract:
- lang: eng
text: Safety and liveness stand as fundamental concepts in formal languages, playing
a key role in verification. The safety-liveness classification of boolean properties
characterizes whether a given property can be falsified by observing a finite
prefix of an infinite computation trace (always for safety, never for liveness).
In the quantitative setting, properties are arbitrary functions from infinite
words to partially-ordered domains. Extending this paradigm to the quantitative
domain, where properties are arbitrary functions mapping infinite words to partially-ordered
domains, we introduce and study the notions of quantitative safety and liveness.
First, we formally define quantitative safety and liveness, and prove that our
definitions induce conservative quantitative generalizations of both the safety-progress
hierarchy and the safety-liveness decomposition of boolean properties. Consequently,
like their boolean counterparts, quantitative properties can be min-decomposed
into safety and liveness parts, or alternatively, max-decomposed into co-safety
and co-liveness parts. We further establish a connection between quantitative
safety and topological continuity and provide alternative characterizations of
quantitative safety and liveness in terms of their boolean analogs. Second, we
instantiate our framework with the specific classes of quantitative properties
expressed by automata. These quantitative automata contain finitely many states
and rational-valued transition weights, and their common value functions Inf,
Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the
totally-ordered domain of real numbers. For all common value functions, we provide
a procedure for deciding whether a given automaton is safe or live, we show how
to construct its safety closure, and we present a min-decomposition into safe
and live automata.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093 and
the Israel Science Foundation grant 2410/22. N. Mazzocchi was affiliated with ISTA
when this work was submitted for publication.
article_number: '13149'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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
citation:
ama: Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative
properties and automata. Logical Methods in Computer Science. 2025;21(2).
doi:10.46298/lmcs-21(2:2)2025
apa: Boker, U., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2025). Safety
and liveness of quantitative properties and automata. Logical Methods in Computer
Science. EPI Sciences. https://doi.org/10.46298/lmcs-21(2:2)2025
chicago: Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac.
“ Safety and Liveness of Quantitative Properties and Automata.” Logical Methods
in Computer Science. EPI Sciences, 2025. https://doi.org/10.46298/lmcs-21(2:2)2025.
ieee: U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “ Safety and
liveness of quantitative properties and automata,” Logical Methods in Computer
Science, vol. 21, no. 2. EPI Sciences, 2025.
ista: Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Safety and liveness
of quantitative properties and automata. Logical Methods in Computer Science.
21(2), 13149.
mla: Boker, Udi, et al. “ Safety and Liveness of Quantitative Properties and Automata.”
Logical Methods in Computer Science, vol. 21, no. 2, 13149, EPI Sciences,
2025, doi:10.46298/lmcs-21(2:2)2025.
short: U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, Logical Methods in
Computer Science 21 (2025).
corr_author: '1'
date_created: 2025-09-11T12:17:52Z
date_published: 2025-04-08T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '08'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.46298/lmcs-21(2:2)2025
ec_funded: 1
external_id:
arxiv:
- '2307.06016'
isi:
- '001468887900001'
file:
- access_level: open_access
checksum: 0b4d477bd981379724c35a4de2c176e5
content_type: application/pdf
creator: esarac
date_created: 2025-09-11T12:17:12Z
date_updated: 2025-09-11T12:17:12Z
file_id: '20343'
file_name: 2307.06016.pdf
file_size: 709584
relation: main_file
success: 1
file_date_updated: 2025-09-11T12:17:12Z
has_accepted_license: '1'
intvolume: ' 21'
isi: 1
issue: '2'
language:
- iso: eng
month: '04'
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: Logical Methods in Computer Science
publication_identifier:
eissn:
- 1860-5974
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
record:
- id: '13221'
relation: earlier_version
status: public
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: ' Safety and liveness of quantitative properties and 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: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 21
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19741'
abstract:
- lang: eng
text: 'Quantitative automata model beyond-boolean aspects of systems: every execution
is mapped to a real number by incorporating weighted transitions and value functions
that generalize acceptance conditions of boolean w-automata. Despite the theoretical
advances in systems analysis through quantitative automata, the first comprehensive
software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was
developed only recently. QuAK implements algorithms for solving standard decision
problems, e.g., emptiness and universality, as well as constructions for safety
and liveness of quantitative automata. We present the architecture of QuAK, which
reflects that all of these problems reduce to either checking inclusion between
two quantitative automata or computing the highest value achievable by an automaton—its
so-called top value. We improve QuAK by extending these two algorithms with an
option to return, alongside their results, an ultimately periodic word witnessing
the algorithm’s output, as well as implementing a new safety-liveness decomposition
algorithm that can handle nondeterministic automata, making QuAK more informative
and capable.'
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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
citation:
ama: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of
quantitative automata with QuAK. In: 31st International Conference on Tools
and Algorithms for the Construction and Analysis of Systems. Vol 15696. Springer
Nature; 2025:303-312. doi:10.1007/978-3-031-90643-5_16'
apa: Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2025).
Automating the analysis of quantitative automata with QuAK. In 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 15696, pp. 303–312). Springer Nature. https://doi.org/10.1007/978-3-031-90643-5_16
chicago: Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, 15696:303–12. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90643-5_16.
ieee: M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating
the analysis of quantitative automata with QuAK,” in 31st International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 2025,
vol. 15696, pp. 303–312.
ista: Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Automating the analysis
of quantitative automata with QuAK. 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 15696, 303–312.
mla: Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with
QuAK.” 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:10.1007/978-3-031-90643-5_16.
short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Springer Nature, 2025, pp. 303–312.
corr_author: '1'
date_created: 2025-05-25T22:17:07Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90643-5_16
ec_funded: 1
external_id:
arxiv:
- '2501.16088'
file:
- access_level: open_access
checksum: a27fa245be8d83421e9127b48a09c8af
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T08:13:11Z
date_updated: 2025-06-02T08:13:11Z
file_id: '19768'
file_name: 2025_TACAS_ChalupaMarek.pdf
file_size: 420669
relation: main_file
success: 1
file_date_updated: 2025-06-02T08:13:11Z
has_accepted_license: '1'
intvolume: ' 15696'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 303-312
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906428'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Automating the analysis of quantitative automata with QuAK
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: 15696
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '18068'
abstract:
- lang: eng
text: "We study the following refinement relation between nondeterministic state-transition
models: model ℬ strategically dominates model \U0001D49C iff every deterministic
refinement of \U0001D49C is language contained in some deterministic refinement
of ℬ. While language containment is trace inclusion, and the (fair) simulation
preorder coincides with tree inclusion, strategic dominance falls strictly between
the two and can be characterized as \"strategy inclusion\" between \U0001D49C
and ℬ: every strategy that resolves the nondeterminism of \U0001D49C is dominated
by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be
checked in 2-ExpTime by a decidable first-order Presburger logic with quantification
over words and strategies, called resolver logic. We give several other applications
of resolver logic, including checking the co-safety, co-liveness, and history-determinism
of boolean and quantitative automata, and checking the inclusion between hyperproperties
that are specified by nondeterministic boolean and quantitative automata."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. N.
Mazzocchi was affiliated with ISTA when this work was submitted for publication.
alternative_title:
- LIPIcs
article_number: '29'
article_processing_charge: Yes
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
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder
for nondeterministic processes. In: 35th International Conference on Concurrency
Theory. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024.
doi:10.4230/LIPIcs.CONCUR.2024.29'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2024). Strategic dominance:
A new preorder for nondeterministic processes. In 35th International Conference
on Concurrency Theory (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2024.29'
chicago: 'Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Strategic
Dominance: A New Preorder for Nondeterministic Processes.” In 35th International
Conference on Concurrency Theory, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2024. https://doi.org/10.4230/LIPIcs.CONCUR.2024.29.'
ieee: 'T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance:
A new preorder for nondeterministic processes,” in 35th International Conference
on Concurrency Theory, Calgary, Canada, 2024, vol. 311.'
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2024. Strategic dominance: A new preorder
for nondeterministic processes. 35th International Conference on Concurrency Theory.
CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 29.'
mla: 'Henzinger, Thomas A., et al. “Strategic Dominance: A New Preorder for Nondeterministic
Processes.” 35th International Conference on Concurrency Theory, vol. 311,
29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.CONCUR.2024.29.'
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 35th International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
conference:
end_date: 2024-09-13
location: Calgary, Canada
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2024-09-09
corr_author: '1'
date_created: 2024-09-15T22:01:40Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2025-12-02T13:45:38Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.4230/LIPIcs.CONCUR.2024.29
ec_funded: 1
external_id:
arxiv:
- '2407.10473'
isi:
- '001556847400029'
file:
- access_level: open_access
checksum: 555bd343e1fb38adeab8fc465ff4fad8
content_type: application/pdf
creator: dernst
date_created: 2024-09-17T07:48:56Z
date_updated: 2024-09-17T07:48:56Z
file_id: '18081'
file_name: 2024_LIPICS_Henzinger.pdf
file_size: 964124
relation: main_file
success: 1
file_date_updated: 2024-09-17T07:48:56Z
has_accepted_license: '1'
intvolume: ' 311'
isi: 1
language:
- iso: eng
month: '09'
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: 35th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959773393'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Strategic dominance: A new preorder for nondeterministic processes'
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: 311
year: '2024'
...
---
APC_amount: 2748 EUR
OA_place: publisher
OA_type: hybrid
_id: '17634'
abstract:
- lang: eng
text: System behaviors are traditionally evaluated through binary classifications
of correctness, which do not suffice for properties involving quantitative aspects
of systems and executions. Quantitative automata offer a more nuanced approach,
mapping each execution to a real number by incorporating weighted transitions
and value functions generalizing acceptance conditions. In this paper, we introduce
QuAK, the first tool designed to automate the analysis of quantitative automata.
QuAK currently supports a variety of quantitative automaton types, including Inf,
Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg automata, and implements decision
procedures for problems such as emptiness, universality, inclusion, equivalence,
as well as for checking whether an automaton is safe, live, or constant. Additionally,
QuAK is able to compute extremal values when possible, construct safety-liveness
decompositions, and monitor system behaviors. We demonstrate the effectiveness
of QuAK through experiments focusing on the inclusion, constant-function check,
and monitoring problems.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. N.
Mazzocchi was affiliated with ISTA when his collaboration started.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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
citation:
ama: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata
Kit. In: 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. Vol 15222. Springer Nature; 2024:3-20.
doi:10.1007/978-3-031-75387-9_1'
apa: 'Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2024).
QuAK: Quantitative Automata Kit. In 12th International Symposium on Leveraging
Applications of Formal Methods, Verification and Validation (Vol. 15222, pp.
3–20). Crete, Greece: Springer Nature. https://doi.org/10.1007/978-3-031-75387-9_1'
chicago: 'Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
E Sarac. “QuAK: Quantitative Automata Kit.” In 12th International Symposium
on Leveraging Applications of Formal Methods, Verification and Validation,
15222:3–20. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-75387-9_1.'
ieee: 'M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “QuAK: Quantitative
Automata Kit,” in 12th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation, Crete, Greece, 2024, vol. 15222,
pp. 3–20.'
ista: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2024. QuAK: Quantitative
Automata Kit. 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. ISoLA: International Symposium on Leveraging
Applications, LNCS, vol. 15222, 3–20.'
mla: 'Chalupa, Marek, et al. “QuAK: Quantitative Automata Kit.” 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
vol. 15222, Springer Nature, 2024, pp. 3–20, doi:10.1007/978-3-031-75387-9_1.'
short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
Springer Nature, 2024, pp. 3–20.
conference:
end_date: 2024-10-31
location: Crete, Greece
name: 'ISoLA: International Symposium on Leveraging Applications'
start_date: 2024-10-27
corr_author: '1'
date_created: 2024-09-05T14:27:08Z
date_published: 2024-10-26T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '26'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-75387-9_1
ec_funded: 1
external_id:
arxiv:
- '2409.03569'
isi:
- '001419008700001'
file:
- access_level: open_access
checksum: 43e432f82be376434b358f3dd7a94b71
content_type: application/pdf
creator: esarac
date_created: 2024-09-05T14:26:02Z
date_updated: 2024-09-05T14:26:02Z
file_id: '17635'
file_name: isola24.pdf
file_size: 847422
relation: main_file
success: 1
- access_level: open_access
checksum: 6bc04f07bb5612c0e7ea00ac121a69b6
content_type: application/pdf
creator: dernst
date_created: 2025-01-21T14:39:49Z
date_updated: 2025-01-21T14:39:49Z
file_id: '18865'
file_name: 2024_LNCS_Chalupa.pdf
file_size: 1358706
relation: main_file
success: 1
file_date_updated: 2025-01-21T14:39:49Z
has_accepted_license: '1'
intvolume: ' 15222'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 3-20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 12th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031753862'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'QuAK: Quantitative Automata Kit'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15222
year: '2024'
...
---
APC_amount: 2748 EUR
OA_place: publisher
OA_type: hybrid
_id: '18521'
abstract:
- lang: eng
text: In distributed systems with processes that do not share a global clock, partial
synchrony is achieved by clock synchronization that guarantees bounded clock skew
among all applications. Existing solutions for distributed runtime verification
under partial synchrony against temporal logic specifications are exact but suffer
from significant computational overhead. In this paper, we propose an approximate
distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates
this issue by abstracting away potential interleaving behaviors. This conservative
abstraction enables a significant speedup of the distributed monitors, albeit
with a tradeoff in accuracy. We address this tradeoff with a methodology that
combines our approximate monitor with its exact counterpart, resulting in enhanced
efficiency without sacrificing precision. We evaluate our approach with multiple
experiments, showcasing its efficacy in both real-world applications and synthetic
examples.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. This
work is sponsored in part by the United States NSF CCF-2118356 award. This research
was partially funded by A-IQ Ready (Chips JU, grant agreement No. 101096658).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
- first_name: Anik
full_name: Momtaz, Anik
last_name: Momtaz
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring
under partial synchrony: Balancing speed & accuracy. In: 24th International
Conference on Runtime Verification. Vol 15191. Springer Nature; 2024:282-301.
doi:10.1007/978-3-031-74234-7_18'
apa: 'Bonakdarpour, B., Momtaz, A., Nickovic, D., & Sarac, N. E. (2024). Approximate
distributed monitoring under partial synchrony: Balancing speed & accuracy.
In 24th International Conference on Runtime Verification (Vol. 15191, pp.
282–301). Istanbul, Turkey: Springer Nature. https://doi.org/10.1007/978-3-031-74234-7_18'
chicago: 'Bonakdarpour, Borzoo, Anik Momtaz, Dejan Nickovic, and Naci E Sarac. “Approximate
Distributed Monitoring under Partial Synchrony: Balancing Speed & Accuracy.”
In 24th International Conference on Runtime Verification, 15191:282–301.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-74234-7_18.'
ieee: 'B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy,” in 24th
International Conference on Runtime Verification, Istanbul, Turkey, 2024,
vol. 15191, pp. 282–301.'
ista: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. 2024. Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy. 24th International
Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS,
vol. 15191, 282–301.'
mla: 'Bonakdarpour, Borzoo, et al. “Approximate Distributed Monitoring under Partial
Synchrony: Balancing Speed & Accuracy.” 24th International Conference on
Runtime Verification, vol. 15191, Springer Nature, 2024, pp. 282–301, doi:10.1007/978-3-031-74234-7_18.'
short: B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International
Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301.
conference:
end_date: 2024-10-17
location: Istanbul, Turkey
name: 'RV: Conference on Runtime Verification'
start_date: 2024-10-15
corr_author: '1'
date_created: 2024-11-10T23:01:58Z
date_published: 2024-10-12T00:00:00Z
date_updated: 2026-05-20T08:43:20Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.1007/978-3-031-74234-7_18
ec_funded: 1
external_id:
arxiv:
- '2408.05033'
isi:
- '001420093700018'
file:
- access_level: open_access
checksum: 7b8ca21b8c19ab796fa445b0e54003ca
content_type: application/pdf
creator: dernst
date_created: 2024-11-11T09:42:28Z
date_updated: 2024-11-11T09:42:28Z
file_id: '18539'
file_name: 2024_LNCS_Bonakdarpour.pdf
file_size: 1897101
relation: main_file
success: 1
file_date_updated: 2024-11-11T09:42:28Z
has_accepted_license: '1'
intvolume: ' 15191'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 282-301
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 24th International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031742330'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Approximate distributed monitoring under partial synchrony: Balancing speed
& accuracy'
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: 15191
year: '2024'
...
---
_id: '12467'
abstract:
- lang: eng
text: Safety and liveness are elementary concepts of computation, and the foundation
of many verification paradigms. The safety-liveness classification of boolean
properties characterizes whether a given property can be falsified by observing
a finite prefix of an infinite computation trace (always for safety, never for
liveness). In quantitative specification and verification, properties assign not
truth values, but quantitative values to infinite traces (e.g., a cost, or the
distance to a boolean property). We introduce quantitative safety and liveness,
and we prove that our definitions induce conservative quantitative generalizations
of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness
decomposition of boolean properties. In particular, we show that every quantitative
property can be written as the pointwise minimum of a quantitative safety property
and a quantitative liveness property. Consequently, like boolean properties, also
quantitative properties can be min-decomposed into safety and liveness parts,
or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover,
quantitative properties can be approximated naturally. We prove that every quantitative
property that has both safe and co-safe approximations can be monitored arbitrarily
precisely by a monitor that uses only a finite number of states.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported in part by the ERC-2020-AdG 101020093.
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
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In:
26th International Conference Foundations of Software Science and Computation
Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative
safety and liveness. In 26th International Conference Foundations of Software
Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France:
Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative
Safety and Liveness.” In 26th International Conference Foundations of Software
Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and
liveness,” in 26th International Conference Foundations of Software Science
and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness.
26th International Conference Foundations of Software Science and Computation
Structures. FOSSACS: Foundations of Software Science and Computation Structures,
LNCS, vol. 13992, 349–370.'
mla: Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International
Conference Foundations of Software Science and Computation Structures, vol.
13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference
Foundations of Software Science and Computation Structures, Springer Nature, 2023,
pp. 349–370.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FOSSACS: Foundations of Software Science and Computation Structures'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-01-31T07:23:56Z
date_published: 2023-04-21T00:00:00Z
date_updated: 2025-09-09T12:21:08Z
day: '21'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-30829-1_17
ec_funded: 1
external_id:
arxiv:
- '2301.11175'
isi:
- '001288609300017'
file:
- access_level: open_access
checksum: 981025aed580b6b27c426cb8856cf63e
content_type: application/pdf
creator: esarac
date_created: 2023-01-31T07:22:21Z
date_updated: 2023-01-31T07:22:21Z
file_id: '12468'
file_name: qsl.pdf
file_size: 449027
relation: main_file
success: 1
- access_level: open_access
checksum: f16e2af1e0eb243158ab0f0fe74e7d5a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T10:28:09Z
date_updated: 2023-06-19T10:28:09Z
file_id: '13153'
file_name: 2023_LNCS_HenzingerT.pdf
file_size: 1048171
relation: main_file
success: 1
file_date_updated: 2023-06-19T10:28:09Z
has_accepted_license: '1'
intvolume: ' 13992'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 349-370
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 26th International Conference Foundations of Software Science and Computation
Structures
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308284'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative safety and liveness
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13992
year: '2023'
...
---
_id: '13292'
abstract:
- lang: eng
text: The operator precedence languages (OPLs) represent the largest known subclass
of the context-free languages which enjoys all desirable closure and decidability
properties. This includes the decidability of language inclusion, which is the
ultimate verification problem. Operator precedence grammars, automata, and logics
have been investigated and used, for example, to verify programs with arithmetic
expressions and exceptions (both of which are deterministic pushdown but lie outside
the scope of the visibly pushdown languages). In this paper, we complete the picture
and give, for the first time, an algebraic characterization of the class of OPLs
in the form of a syntactic congruence that has finitely many equivalence classes
exactly for the operator precedence languages. This is a generalization of the
celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of
the consequences, we show that universality and language inclusion for nondeterministic
operator precedence automata can be solved by an antichain algorithm. Antichain
algorithms avoid determinization and complementation through an explicit subset
construction, by leveraging a quasi-order on words, which allows the pruning of
the search space for counterexample words without sacrificing completeness. Antichain
algorithms can be implemented symbolically, and these implementations are today
the best-performing algorithms in practice for the inclusion of finite automata.
We give a generic construction of the quasi-order needed for antichain algorithms
from a finite syntactic congruence. This yields the first antichain algorithm
for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem
for OPLs in exponential time.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe
thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful
comments.\r\n"
alternative_title:
- LIPIcs
article_processing_charge: Yes
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
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. Regular methods for operator
precedence languages. In: 50th International Colloquium on Automata, Languages,
and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2023:129:1--129:20. doi:10.4230/LIPIcs.ICALP.2023.129'
apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2023).
Regular methods for operator precedence languages. In 50th International Colloquium
on Automata, Languages, and Programming (Vol. 261, p. 129:1--129:20). Paderborn,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.129'
chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E
Sarac. “Regular Methods for Operator Precedence Languages.” In 50th International
Colloquium on Automata, Languages, and Programming, 261:129:1--129:20. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.129.
ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods
for operator precedence languages,” in 50th International Colloquium on Automata,
Languages, and Programming, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.
ista: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for
operator precedence languages. 50th International Colloquium on Automata, Languages,
and Programming. ICALP: Automata, Languages and Programming, LIPIcs, vol. 261,
129:1--129:20.'
mla: Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.”
50th International Colloquium on Automata, Languages, and Programming,
vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20,
doi:10.4230/LIPIcs.ICALP.2023.129.
short: T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International
Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2023, p. 129:1--129:20.
conference:
end_date: 2023-07-14
location: Paderborn, Germany
name: 'ICALP: Automata, Languages and Programming'
start_date: 2023-07-10
corr_author: '1'
date_created: 2023-07-24T15:11:41Z
date_published: 2023-07-05T00:00:00Z
date_updated: 2025-07-10T11:50:41Z
day: '05'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.4230/LIPIcs.ICALP.2023.129
ec_funded: 1
external_id:
arxiv:
- '2305.03447'
file:
- access_level: open_access
checksum: 5d4c8932ef3450615a53b9bb15d92eb2
content_type: application/pdf
creator: esarac
date_created: 2023-07-24T15:11:05Z
date_updated: 2023-07-24T15:11:05Z
file_id: '13293'
file_name: icalp23.pdf
file_size: 859379
relation: main_file
success: 1
file_date_updated: 2023-07-24T15:11:05Z
has_accepted_license: '1'
intvolume: ' 261'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 129:1--129:20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 50th International Colloquium on Automata, Languages, and Programming
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959772785'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Regular methods for operator precedence languages
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: 261
year: '2023'
...
---
_id: '13221'
abstract:
- lang: eng
text: The safety-liveness dichotomy is a fundamental concept in formal languages
which plays a key role in verification. Recently, this dichotomy has been lifted
to quantitative properties, which are arbitrary functions from infinite words
to partially-ordered domains. We look into harnessing the dichotomy for the specific
classes of quantitative properties expressed by quantitative automata. These automata
contain finitely many states and rational-valued transition weights, and their
common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum
map infinite words into the totallyordered domain of real numbers. In this automata-theoretic
setting, we establish a connection between quantitative safety and topological
continuity and provide an alternative characterization of quantitative safety
and liveness in terms of their boolean counterparts. For all common value functions,
we show how the safety closure of a quantitative automaton can be constructed
in PTime, and we provide PSpace-complete checks of whether a given quantitative
automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata,
for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf,
and LimSup automata, we give PTime decompositions into safe and live automata.
These decompositions enable the separation of techniques for safety and liveness
verification for quantitative specifications.
acknowledgement: We thank Christof Löding for pointing us to some results on PSpace-hardess
of universality problems and the anonymous reviewers for their helpful comments.
This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science
Foundation grant 2410/22.
alternative_title:
- LIPIcs
article_number: '17'
article_processing_charge: No
arxiv: 1
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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
citation:
ama: 'Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative
automata. In: 34th International Conference on Concurrency Theory. Vol
279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.17'
apa: 'Boker, U., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023).
Safety and liveness of quantitative automata. In 34th International Conference
on Concurrency Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17'
chicago: Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac.
“Safety and Liveness of Quantitative Automata.” In 34th International Conference
on Concurrency Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2023. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17.
ieee: U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness
of quantitative automata,” in 34th International Conference on Concurrency
Theory, Antwerp, Belgium, 2023, vol. 279.
ista: 'Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness
of quantitative automata. 34th International Conference on Concurrency Theory.
CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17.'
mla: Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” 34th
International Conference on Concurrency Theory, vol. 279, 17, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.17.
short: U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 34th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2023.
conference:
end_date: 2023-09-23
location: Antwerp, Belgium
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2023-09-18
corr_author: '1'
date_created: 2023-07-14T10:00:15Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.17
ec_funded: 1
external_id:
arxiv:
- '2307.06016'
isi:
- '001570542500017'
file:
- access_level: open_access
checksum: d40e57a04448ea5c77d7e1cfb9590a81
content_type: application/pdf
creator: esarac
date_created: 2023-07-14T12:03:48Z
date_updated: 2023-07-14T12:03:48Z
file_id: '13224'
file_name: CONCUR23.pdf
file_size: 755529
relation: main_file
success: 1
file_date_updated: 2023-07-14T12:03:48Z
has_accepted_license: '1'
intvolume: ' 279'
isi: 1
language:
- iso: eng
month: '09'
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: 34th International Conference on Concurrency Theory
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959772990'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '20342'
relation: later_version
status: public
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Safety and liveness of 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: 279
year: '2023'
...
---
_id: '11775'
abstract:
- lang: eng
text: 'Quantitative monitoring can be universal and approximate: For every finite
sequence of observations, the specification provides a value and the monitor outputs
a best-effort approximation of it. The quality of the approximation may depend
on the resources that are available to the monitor. By taking to the limit the
sequences of specification values and monitor outputs, we obtain precision-resource
trade-offs also for limit monitoring. This paper provides a formal framework for
studying such trade-offs using an abstract interpretation for monitors: For each
natural number n, the aggregate semantics of a monitor at time n is an equivalence
relation over all sequences of at most n observations so that two equivalent sequences
are indistinguishable to the monitor and thus mapped to the same output. This
abstract interpretation of quantitative monitors allows us to measure the number
of equivalence classes (or “resource use”) that is necessary for a certain precision
up to a certain time, or at any time. Our framework offers several insights. For
example, we identify a family of specifications for which any resource-optimal
exact limit monitor is independent of any error permitted over finite traces.
Moreover, we present a specification for which any resource-optimal approximate
limit monitor does not minimize its resource use at any time. '
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: Yes
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
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications.
In: 22nd International Conference on Runtime Verification. Vol 13498. Springer
Nature; 2022:200-220. doi:10.1007/978-3-031-17196-3_11'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2022). Abstract monitors
for quantitative specifications. In 22nd International Conference on Runtime
Verification (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature.
https://doi.org/10.1007/978-3-031-17196-3_11'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract
Monitors for Quantitative Specifications.” In 22nd International Conference
on Runtime Verification, 13498:200–220. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-17196-3_11.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for
quantitative specifications,” in 22nd International Conference on Runtime Verification,
Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative
specifications. 22nd International Conference on Runtime Verification. RV: Runtime
Verification, LNCS, vol. 13498, 200–220.'
mla: Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.”
22nd International Conference on Runtime Verification, vol. 13498, Springer
Nature, 2022, pp. 200–20, doi:10.1007/978-3-031-17196-3_11.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference
on Runtime Verification, Springer Nature, 2022, pp. 200–220.
conference:
end_date: 2022-09-30
location: Tbilisi, Georgia
name: 'RV: Runtime Verification'
start_date: 2022-09-28
corr_author: '1'
date_created: 2022-08-08T17:09:09Z
date_published: 2022-09-23T00:00:00Z
date_updated: 2026-04-07T12:02:56Z
day: '23'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-17196-3_11
ec_funded: 1
external_id:
isi:
- '000866539700011'
file:
- access_level: open_access
checksum: 05c7dcfbb9053a98f46441fb2eccb213
content_type: application/pdf
creator: dernst
date_created: 2023-01-20T07:34:50Z
date_updated: 2023-01-20T07:34:50Z
file_id: '12317'
file_name: 2022_LNCS_RV_Henzinger.pdf
file_size: 477110
relation: main_file
success: 1
file_date_updated: 2023-01-20T07:34:50Z
has_accepted_license: '1'
intvolume: ' 13498'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 200-220
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 22nd International Conference on Runtime Verification
publication_identifier:
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Abstract monitors for quantitative specifications
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13498
year: '2022'
...
---
_id: '9356'
abstract:
- lang: eng
text: 'In runtime verification, a monitor watches a trace of a system and, if possible,
decides after observing each finite prefix whether or not the unknown infinite
trace satisfies a given specification. We generalize the theory of runtime verification
to monitors that attempt to estimate numerical values of quantitative trace properties
(instead of attempting to conclude boolean values of trace specifications), such
as maximal or average response time along a trace. Quantitative monitors are approximate:
with every finite prefix, they can improve their estimate of the infinite trace''s
unknown property value. Consequently, quantitative monitors can be compared with
regard to a precision-cost trade-off: better approximations of the property value
require more monitor resources, such as states (in the case of finite-state monitors)
or registers, and additional resources yield better approximations. We introduce
a formal framework for quantitative and approximate monitoring, show how it conservatively
generalizes the classical boolean setting for monitoring, and give several precision-cost
trade-offs for monitors. For example, we prove that there are quantitative properties
for which every additional register improves monitoring precision.'
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23
(Wittgenstein Award).
article_number: '9470547'
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: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Sarac NE. Quantitative and approximate monitoring. In: Proceedings
of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute
of Electrical and Electronics Engineers; 2021. doi:10.1109/LICS52264.2021.9470547'
apa: 'Henzinger, T. A., & Sarac, N. E. (2021). Quantitative and approximate
monitoring. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
Computer Science. Online: Institute of Electrical and Electronics Engineers.
https://doi.org/10.1109/LICS52264.2021.9470547'
chicago: Henzinger, Thomas A, and Naci E Sarac. “Quantitative and Approximate Monitoring.”
In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science.
Institute of Electrical and Electronics Engineers, 2021. https://doi.org/10.1109/LICS52264.2021.9470547.
ieee: T. A. Henzinger and N. E. Sarac, “Quantitative and approximate monitoring,”
in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
Online, 2021.
ista: 'Henzinger TA, Sarac NE. 2021. Quantitative and approximate monitoring. Proceedings
of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic
in Computer Science, 9470547.'
mla: Henzinger, Thomas A., and Naci E. Sarac. “Quantitative and Approximate Monitoring.”
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
9470547, Institute of Electrical and Electronics Engineers, 2021, doi:10.1109/LICS52264.2021.9470547.
short: T.A. Henzinger, N.E. Sarac, in:, Proceedings of the 36th Annual ACM/IEEE
Symposium on Logic in Computer Science, Institute of Electrical and Electronics
Engineers, 2021.
conference:
end_date: 2021-07-02
location: Online
name: 'LICS: Logic in Computer Science'
start_date: 2021-06-29
date_created: 2021-04-30T17:30:47Z
date_published: 2021-06-29T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '29'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1109/LICS52264.2021.9470547
external_id:
arxiv:
- '2105.08353'
isi:
- '000947350400021'
file:
- access_level: open_access
checksum: 6e4cba3f72775f479c5b1b75d1a4a0c4
content_type: application/pdf
creator: esarac
date_created: 2021-06-16T08:23:54Z
date_updated: 2021-06-16T08:23:54Z
file_id: '9557'
file_name: qam.pdf
file_size: 641990
relation: main_file
success: 1
file_date_updated: 2021-06-16T08:23:54Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
Science
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Quantitative and approximate monitoring
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2021'
...
---
_id: '8912'
abstract:
- lang: eng
text: "For automata, synchronization, the problem of bringing an automaton to a
particular state regardless of its initial state, is important. It has several
applications in practice and is related to a fifty-year-old conjecture on the
length of the shortest synchronizing word. Although using shorter words increases
the effectiveness in practice, finding a shortest one (which is not necessarily
unique) is NP-hard. For this reason, there exist various heuristics in the literature.
However, high-quality heuristics such as SynchroP producing relatively shorter
sequences are very expensive and can take hours when the automaton has tens of
thousands of states. The SynchroP heuristic has been frequently used as a benchmark
to evaluate the performance of the new heuristics. In this work, we first improve
the runtime of SynchroP and its variants by using algorithmic techniques. We then
focus on adapting SynchroP for many-core architectures,\r\nand overall, we obtain
more than 1000× speedup on GPUs compared to naive sequential implementation that
has been frequently used as a benchmark to evaluate new heuristics in the literature.
We also propose two SynchroP variants and evaluate their performance."
acknowledgement: This work was supported by The Scientific and Technological Research
Council of Turkey (TUBITAK) [grant number 114E569]. This research was supported
in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).
We would like to thank the authors of (Roman & Szykula, 2015) for providing their
heuristics implementations, which we used to compare our SynchroP implementation
as given in Table 11.
article_number: '114203'
article_processing_charge: No
article_type: original
author:
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
- first_name: Ömer Faruk
full_name: Altun, Ömer Faruk
last_name: Altun
- first_name: Kamil Tolga
full_name: Atam, Kamil Tolga
last_name: Atam
- first_name: Sertac
full_name: Karahoda, Sertac
last_name: Karahoda
- first_name: Kamer
full_name: Kaya, Kamer
last_name: Kaya
- first_name: Hüsnü
full_name: Yenigün, Hüsnü
last_name: Yenigün
citation:
ama: Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. Boosting expensive
synchronizing heuristics. Expert Systems with Applications. 2021;167(4).
doi:10.1016/j.eswa.2020.114203
apa: Sarac, N. E., Altun, Ö. F., Atam, K. T., Karahoda, S., Kaya, K., & Yenigün,
H. (2021). Boosting expensive synchronizing heuristics. Expert Systems with
Applications. Elsevier. https://doi.org/10.1016/j.eswa.2020.114203
chicago: Sarac, Naci E, Ömer Faruk Altun, Kamil Tolga Atam, Sertac Karahoda, Kamer
Kaya, and Hüsnü Yenigün. “Boosting Expensive Synchronizing Heuristics.” Expert
Systems with Applications. Elsevier, 2021. https://doi.org/10.1016/j.eswa.2020.114203.
ieee: N. E. Sarac, Ö. F. Altun, K. T. Atam, S. Karahoda, K. Kaya, and H. Yenigün,
“Boosting expensive synchronizing heuristics,” Expert Systems with Applications,
vol. 167, no. 4. Elsevier, 2021.
ista: Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. 2021. Boosting
expensive synchronizing heuristics. Expert Systems with Applications. 167(4),
114203.
mla: Sarac, Naci E., et al. “Boosting Expensive Synchronizing Heuristics.” Expert
Systems with Applications, vol. 167, no. 4, 114203, Elsevier, 2021, doi:10.1016/j.eswa.2020.114203.
short: N.E. Sarac, Ö.F. Altun, K.T. Atam, S. Karahoda, K. Kaya, H. Yenigün, Expert
Systems with Applications 167 (2021).
corr_author: '1'
date_created: 2020-12-02T13:34:25Z
date_published: 2021-04-01T00:00:00Z
date_updated: 2026-04-16T09:15:47Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.eswa.2020.114203
external_id:
isi:
- '000640531100038'
file:
- access_level: open_access
checksum: 600c2f81bc898a725bcfa7cf26ff4fed
content_type: application/pdf
creator: esarac
date_created: 2020-12-02T13:33:51Z
date_updated: 2020-12-02T13:33:51Z
file_id: '8913'
file_name: synchroPaperRevised.pdf
file_size: 634967
relation: main_file
file_date_updated: 2020-12-02T13:33:51Z
has_accepted_license: '1'
intvolume: ' 167'
isi: 1
issue: '4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Expert Systems with Applications
publication_identifier:
eissn:
- 1873-6793
issn:
- 0957-4174
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Boosting expensive synchronizing heuristics
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 167
year: '2021'
...
---
_id: '8623'
abstract:
- lang: eng
text: We introduce the monitoring of trace properties under assumptions. An assumption
limits the space of possible traces that the monitor may encounter. An assumption
may result from knowledge about the system that is being monitored, about the
environment, or about another, connected monitor. We define monitorability under
assumptions and study its theoretical properties. In particular, we show that
for every assumption A, the boolean combinations of properties that are safe or
co-safe relative to A are monitorable under A. We give several examples and constructions
on how an assumption can make a non-monitorable property monitorable, and how
an assumption can make a monitorable property monitorable with fewer resources,
such as integer registers.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
article_processing_charge: No
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: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Sarac NE. Monitorability under assumptions. In: Runtime Verification.
Vol 12399. Springer Nature; 2020:3-18. doi:10.1007/978-3-030-60508-7_1'
apa: 'Henzinger, T. A., & Sarac, N. E. (2020). Monitorability under assumptions.
In Runtime Verification (Vol. 12399, pp. 3–18). Los Angeles, CA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-60508-7_1'
chicago: Henzinger, Thomas A, and Naci E Sarac. “Monitorability under Assumptions.”
In Runtime Verification, 12399:3–18. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-60508-7_1.
ieee: T. A. Henzinger and N. E. Sarac, “Monitorability under assumptions,” in Runtime
Verification, Los Angeles, CA, United States, 2020, vol. 12399, pp. 3–18.
ista: 'Henzinger TA, Sarac NE. 2020. Monitorability under assumptions. Runtime Verification.
RV: Runtime Verification, LNCS, vol. 12399, 3–18.'
mla: Henzinger, Thomas A., and Naci E. Sarac. “Monitorability under Assumptions.”
Runtime Verification, vol. 12399, Springer Nature, 2020, pp. 3–18, doi:10.1007/978-3-030-60508-7_1.
short: T.A. Henzinger, N.E. Sarac, in:, Runtime Verification, Springer Nature, 2020,
pp. 3–18.
conference:
end_date: 2020-10-09
location: Los Angeles, CA, United States
name: 'RV: Runtime Verification'
start_date: 2020-10-06
date_created: 2020-10-07T15:05:37Z
date_published: 2020-10-02T00:00:00Z
date_updated: 2026-04-16T10:22:01Z
day: '02'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-60508-7_1
external_id:
isi:
- '000728160600001'
file:
- access_level: open_access
checksum: 00661f9b7034f52e18bf24fa552b8194
content_type: application/pdf
creator: esarac
date_created: 2020-10-15T14:28:06Z
date_updated: 2020-10-15T14:28:06Z
file_id: '8665'
file_name: monitorability.pdf
file_size: 478148
relation: main_file
success: 1
file_date_updated: 2020-10-15T14:28:06Z
has_accepted_license: '1'
intvolume: ' 12399'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 3-18
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Runtime Verification
publication_identifier:
eisbn:
- '9783030605087'
eissn:
- 1611-3349
isbn:
- '9783030605070'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitorability under assumptions
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 12399
year: '2020'
...