Document Open Access Logo

Quantitative Language Automata

Authors Thomas A. Henzinger , Pavol Kebis , Nicolas Mazzocchi , N. Ege Saraç

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.21.pdf
  • Filesize: 1.19 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Quantitative automata
Keywords
  • Quantitative hyperproperties
  • quantitative automata
  • automata-based verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 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 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 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 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 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.

Cite As Get BibTex

Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative Language Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.21

Author Details

Thomas A. Henzinger
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria
Pavol Kebis
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria
Nicolas Mazzocchi
  • Slovak University of Technology in Bratislava, Slovakia
N. Ege Saraç
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria

Funding

This work was supported in part by the ERC-2020-AdG 101020093.

References

  1. Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata? Inf. Comput., 282:104651, 2022. URL: https://doi.org/10.1016/J.IC.2020.104651.
  2. Bowen Alpern and Fred B. Schneider. Defining liveness. Inf. Process. Lett., 21(4):181-185, 1985. URL: https://doi.org/10.1016/0020-0190(85)90056-0.
  3. Daniel Andersson. An improved algorithm for discounted payoff games. In Janneke Huitink and Sophia Katrenko, editors, Proceedings of the 11th ESSLLI Student Session, pages 91-98, August 2006. Google Scholar
  4. Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Safety and liveness of quantitative automata. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 17:1-17:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.17.
  5. Udi Boker, Thomas A Henzinger, Nicolas Mazzocchi, and N Ege Saraç. Safety and liveness of quantitative properties and automata. Logical Methods in Computer Science, 21, 2025. Google Scholar
  6. Udi Boker, Thomas A. Henzinger, and Jan Otop. The target discounted-sum problem. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 750-761. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.74.
  7. Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Quak: Quantitative automata kit. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies - 12th International Symposium, ISoLA 2024, Crete, Greece, October 27-31, 2024, Proceedings, Part IV, volume 15222 of Lecture Notes in Computer Science, pages 3-20. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-75387-9_1.
  8. Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Automating the analysis of quantitative automata with quak. In Arie Gurfinkel and Marijn Heule, editors, Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I, volume 15696 of Lecture Notes in Computer Science, pages 303-312. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90643-5_16.
  9. Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner, Thomas A. Henzinger, and Philippe Rannou. Mean-payoff automaton expressions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 269-283. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_19.
  10. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Alternating weighted automata. In Miroslaw Kutylowski, Witold Charatonik, and Maciej Gebala, editors, Fundamentals of Computation Theory, 17th International Symposium, FCT 2009, Wroclaw, Poland, September 2-4, 2009. Proceedings, volume 5699 of Lecture Notes in Computer Science, pages 3-13. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03409-1_2.
  11. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Expressiveness and closure properties for quantitative languages. Log. Methods Comput. Sci., 6(3), 2010. URL: http://arxiv.org/abs/1007.4018.
  12. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 11(4):23:1-23:38, 2010. URL: https://doi.org/10.1145/1805950.1805953.
  13. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  14. Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Torunczyk. Energy and mean-payoff games with imperfect information. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 260-274. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_22.
  15. Emmanuel Filiot, Nicolas Mazzocchi, and Jean-François Raskin. A pattern logic for automata with outputs. In Mizuho Hoshi and Shinnosuke Seki, editors, Developments in Language Theory - 22nd International Conference, DLT 2018, Tokyo, Japan, September 10-14, 2018, Proceedings, volume 11088 of Lecture Notes in Computer Science, pages 304-317. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98654-8_25.
  16. Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah. Model checking quantitative hyperproperties. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 144-163. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_8.
  17. Vojtech Havlena, Ondrej Lengál, and Barbora Smahlíková. Complementing Büchi automata with ranker. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 188-201. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_10.
  18. Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative safety and liveness. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 349-370. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_17.
  19. Thomas A. Henzinger and Jan Otop. From model checking to model measuring. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 273-287. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_20.
  20. Paul Hunter, Arno Pauly, Guillermo A. Pérez, and Jean-François Raskin. Mean-payoff games with partial observation. Theor. Comput. Sci., 735:82-110, 2018. URL: https://doi.org/10.1016/J.TCS.2017.03.038.
  21. Narendra Karmarkar. A new polynomial-time algorithm for linear programming. Comb., 4(4):373-396, 1984. URL: https://doi.org/10.1007/BF02579150.
  22. Richard M. Karp. A characterization of the minimum cycle mean in a digraph. Discret. Math., 23(3):309-311, 1978. URL: https://doi.org/10.1016/0012-365X(78)90011-0.
  23. Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. Algebra Comput., 4(3):405-426, 1994. URL: https://doi.org/10.1142/S0218196794000063.
  24. Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng., 3(2):125-143, 1977. URL: https://doi.org/10.1109/TSE.1977.229904.
  25. Christof Löding and Anton Pirogov. On finitely ambiguous Büchi automata. In Mizuho Hoshi and Shinnosuke Seki, editors, Developments in Language Theory - 22nd International Conference, DLT 2018, Tokyo, Japan, September 10-14, 2018, Proceedings, volume 11088 of Lecture Notes in Computer Science, pages 503-515. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98654-8_41.
  26. Omid Madani, Steve Hanks, and Anne Condon. On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell., 147(1-2):5-34, 2003. URL: https://doi.org/10.1016/S0004-3702(02)00378-8.
  27. Jakub Michaliszyn and Jan Otop. Non-deterministic weighted automata evaluated over Markov chains. J. Comput. Syst. Sci., 108:118-136, 2020. URL: https://doi.org/10.1016/J.JCSS.2019.10.001.
  28. Shubham Sahai, Pramod Subramanyan, and Rohit Sinha. Verification of quantitative hyperproperties using trace enumeration relations. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 201-224. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_11.
  29. Sven Schewe. Büchi complementation made tight. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 of LIPIcs, pages 661-672. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009. URL: https://doi.org/10.4230/LIPICS.STACS.2009.1854.
  30. Andreas Weber and Helmut Seidl. On the degree of ambiguity of finite automata. Theor. Comput. Sci., 88(2):325-349, 1991. URL: https://doi.org/10.1016/0304-3975(91)90381-B.
  31. Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, and Alexandra Silva. Quantitative weakest hyper pre: Unifying correctness and incorrectness hyperproperties via predicate transformers. CoRR, abs/2404.05097, 2024. URL: https://doi.org/10.48550/arXiv.2404.05097.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact