QuAK: Quantitative Automata Kit

Chalupa, Marek; Henzinger, Thomas A; Mazzocchi, Nicolas Adrien; Sarac, Naci E

QuAK: Quantitative Automata Kit

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, , 3–20.

Download

isola24.pdf 847.42 KB [Published Version]

2024_LNCS_Chalupa.pdf 1.36 MB

DOI

10.48550/arXiv.2409.03569

Conference Paper | Published | English

Scopus indexed

Author

Chalupa, Marek^ISTA; Henzinger, Thomas A^ISTA ; Mazzocchi, Nicolas A^ISTA; Saraç, N. Ege^ISTA

Corresponding author has ISTA affiliation

Department

Graduate School
Henzinger_Thomas Group

Grant

Vigilant Algorithmic Monitoring of Software

Series Title

LNCS

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

2024

Date Published

2024-10-26

Proceedings Title

12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

Publisher

Springer Nature

Acknowledgement

This work was supported in part by the ERC-2020-AdG 101020093. N. Mazzocchi was affiliated with ISTA when his collaboration started.

Page

3-20

Conference

ISoLA: International Symposium on Leveraging Applications

Conference Location

Crete, Greece

Conference Date

2024-10-27 – 2024-10-31

ISBN

9783031753862

ISSN

0302-9743

eISSN

1611-3349

IST-REx-ID

17634

Cite this

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. Springer Nature; 2024:3-20. doi:10.48550/arXiv.2409.03569

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 (pp. 3–20). Crete, Greece: Springer Nature. https://doi.org/10.48550/arXiv.2409.03569

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, 3–20. Springer Nature, 2024. https://doi.org/10.48550/arXiv.2409.03569.

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, pp. 3–20.

Chalupa, Marek, et al. “QuAK: Quantitative Automata Kit.” 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Springer Nature, 2024, pp. 3–20, 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):