QuAK: Quantitative Automata Kit

Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata Kit. arXiv, 2409.03569.

Download
OA isola24.pdf 847.42 KB [Preprint]
Download (ext.)

Preprint | Submitted | English

Corresponding author has ISTA affiliation

Abstract
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.
Publishing Year
Date Published
2024-09-05
Journal Title
arXiv
Acknowledgement
This work was supported in part by the ERC-2020-AdG 101020093.
Article Number
2409.03569
IST-REx-ID

Cite this

Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata Kit. arXiv. doi:10.48550/arXiv.2409.03569
Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (n.d.). QuAK: Quantitative Automata Kit. arXiv. https://doi.org/10.48550/arXiv.2409.03569
Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “QuAK: Quantitative Automata Kit.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2409.03569.
M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “QuAK: Quantitative Automata Kit,” arXiv. .
Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata Kit. arXiv, 2409.03569.
Chalupa, Marek, et al. “QuAK: Quantitative Automata Kit.” ArXiv, 2409.03569, doi:10.48550/arXiv.2409.03569.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
isola24.pdf 847.42 KB
Access Level
OA Open Access
Date Uploaded
2024-09-05
MD5 Checksum
43e432f82be376434b358f3dd7a94b71


Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data ISTA Research Explorer

Sources

arXiv 2409.03569

Search this title in

Google Scholar