[{"license":"https://creativecommons.org/licenses/by/4.0/","year":"2025","language":[{"iso":"eng"}],"OA_type":"gold","department":[{"_id":"ToHe"}],"article_processing_charge":"No","has_accepted_license":"1","day":"18","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":348,"date_created":"2025-08-31T22:01:32Z","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Kebis, Pavol","last_name":"Kebis","first_name":"Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a"},{"last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","last_name":"Sarac"}],"intvolume":"       348","doi":"10.4230/LIPIcs.CONCUR.2025.21","scopus_import":"1","article_number":"21","_id":"20253","ddc":["000"],"file_date_updated":"2025-09-03T10:01:53Z","status":"public","oa_version":"Published Version","month":"08","oa":1,"publication":"36th International Conference on Concurrency Theory","citation":{"ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Quantitative language automata,” in <i>36th International Conference on Concurrency Theory</i>, Aarhus, Denmark, 2025, vol. 348.","ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Quantitative language automata. In: <i>36th International Conference on Concurrency Theory</i>. Vol 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">10.4230/LIPIcs.CONCUR.2025.21</a>","mla":"Henzinger, Thomas A., et al. “Quantitative Language Automata.” <i>36th International Conference on Concurrency Theory</i>, vol. 348, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">10.4230/LIPIcs.CONCUR.2025.21</a>.","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.","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., &#38; Sarac, N. E. (2025). Quantitative language automata. In <i>36th International Conference on Concurrency Theory</i> (Vol. 348). Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2025.21</a>","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Language Automata.” In <i>36th International Conference on Concurrency Theory</i>, Vol. 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2025.21</a>.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2025-08-26","location":"Aarhus, Denmark","end_date":"2025-08-29"},"OA_place":"publisher","type":"conference","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.","alternative_title":["LIPIcs"],"file":[{"success":1,"date_updated":"2025-09-03T10:01:53Z","creator":"dernst","access_level":"open_access","file_name":"2025_CONCUR_HenzingerT.pdf","date_created":"2025-09-03T10:01:53Z","relation":"main_file","content_type":"application/pdf","checksum":"9d4054058757a73477e6015b10ed6996","file_size":1257397,"file_id":"20282"}],"quality_controlled":"1","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 𝒜 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."}],"date_published":"2025-08-18T00:00:00Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"isi":1,"external_id":{"isi":["001570540800021"],"arxiv":["2506.0515"]},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"title":"Quantitative language automata","publication_status":"published","date_updated":"2025-12-01T12:36:52Z","ec_funded":1,"arxiv":1,"corr_author":"1","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773898"]}},{"status":"public","oa_version":"Published Version","_id":"20147","ddc":["000"],"file_date_updated":"2025-09-10T08:19:51Z","month":"08","oa":1,"date_created":"2025-08-07T15:57:57Z","related_material":{"record":[{"relation":"part_of_dissertation","id":"11775","status":"public"},{"status":"deleted","id":"13140","relation":"part_of_dissertation"},{"status":"public","id":"19741","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"9356","status":"public"},{"relation":"part_of_dissertation","id":"19643","status":"deleted"},{"status":"public","relation":"part_of_dissertation","id":"17634"},{"status":"public","relation":"part_of_dissertation","id":"20342"},{"status":"public","relation":"part_of_dissertation","id":"13221"}]},"author":[{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"doi":"10.15479/AT-ISTA-20147","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"has_accepted_license":"1","article_processing_charge":"No","day":"07","publisher":"Institute of Science and Technology Austria","page":"149","language":[{"iso":"eng"}],"year":"2025","ec_funded":1,"publication_identifier":{"issn":["2663-337X"]},"corr_author":"1","degree_awarded":"PhD","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"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"date_published":"2025-08-07T00:00:00Z","date_updated":"2026-04-07T12:02:57Z","project":[{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"publication_status":"published","title":"A monitoring-oriented theory and classification of quantitative specifications","type":"dissertation","supervisor":[{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"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","OA_place":"publisher","alternative_title":["ISTA Thesis"],"file":[{"file_size":8884801,"file_id":"20200","checksum":"0f3015f1db36576a23d8d669afb60b41","relation":"source_file","content_type":"application/x-zip-compressed","file_name":"2025_Sarac_NaciEge_Thesis.zip","date_created":"2025-08-21T09:40:28Z","access_level":"closed","creator":"esarac","date_updated":"2025-09-10T08:19:51Z"},{"creator":"esarac","access_level":"open_access","date_updated":"2025-08-21T09:40:34Z","success":1,"date_created":"2025-08-21T09:40:34Z","file_name":"2025_Sarac_NaciEge_Thesis.pdf","checksum":"332ed2fe61f580641664ec3f05d30f14","content_type":"application/pdf","relation":"main_file","file_size":2955584,"file_id":"20201"}],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","citation":{"short":"N.E. Sarac, A Monitoring-Oriented Theory and Classification of Quantitative Specifications, Institute of Science and Technology Austria, 2025.","apa":"Sarac, N. E. (2025). <i>A monitoring-oriented theory and classification of quantitative specifications</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-20147\">https://doi.org/10.15479/AT-ISTA-20147</a>","chicago":"Sarac, Naci E. “A Monitoring-Oriented Theory and Classification of Quantitative Specifications.” Institute of Science and Technology Austria, 2025. <a href=\"https://doi.org/10.15479/AT-ISTA-20147\">https://doi.org/10.15479/AT-ISTA-20147</a>.","ista":"Sarac NE. 2025. A monitoring-oriented theory and classification of quantitative specifications. Institute of Science and Technology Austria.","mla":"Sarac, Naci E. <i>A Monitoring-Oriented Theory and Classification of Quantitative Specifications</i>. Institute of Science and Technology Austria, 2025, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-20147\">10.15479/AT-ISTA-20147</a>.","ama":"Sarac NE. A monitoring-oriented theory and classification of quantitative specifications. 2025. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-20147\">10.15479/AT-ISTA-20147</a>","ieee":"N. E. Sarac, “A monitoring-oriented theory and classification of quantitative specifications,” Institute of Science and Technology Austria, 2025."}},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"isi":1,"external_id":{"arxiv":["2307.06016"],"isi":["001468887900001"]},"date_published":"2025-04-08T00:00:00Z","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"publication_status":"published","title":" Safety and liveness of quantitative properties and automata","date_updated":"2026-04-07T12:02:57Z","DOAJ_listed":"1","abstract":[{"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.","lang":"eng"}],"quality_controlled":"1","PlanS_conform":"1","corr_author":"1","publication_identifier":{"eissn":["1860-5974"]},"ec_funded":1,"arxiv":1,"citation":{"ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “ Safety and liveness of quantitative properties and automata,” <i>Logical Methods in Computer Science</i>, vol. 21, no. 2. EPI Sciences, 2025.","ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE.  Safety and liveness of quantitative properties and automata. <i>Logical Methods in Computer Science</i>. 2025;21(2). doi:<a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">10.46298/lmcs-21(2:2)2025</a>","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.” <i>Logical Methods in Computer Science</i>, vol. 21, no. 2, 13149, EPI Sciences, 2025, doi:<a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">10.46298/lmcs-21(2:2)2025</a>.","chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “ Safety and Liveness of Quantitative Properties and Automata.” <i>Logical Methods in Computer Science</i>. EPI Sciences, 2025. <a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">https://doi.org/10.46298/lmcs-21(2:2)2025</a>.","apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2025).  Safety and liveness of quantitative properties and automata. <i>Logical Methods in Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/lmcs-21(2:2)2025\">https://doi.org/10.46298/lmcs-21(2:2)2025</a>","short":"U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, Logical Methods in Computer Science 21 (2025)."},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication":"Logical Methods in Computer Science","file":[{"file_size":709584,"file_id":"20343","checksum":"0b4d477bd981379724c35a4de2c176e5","content_type":"application/pdf","relation":"main_file","date_created":"2025-09-11T12:17:12Z","file_name":"2307.06016.pdf","creator":"esarac","access_level":"open_access","date_updated":"2025-09-11T12:17:12Z","success":1}],"OA_place":"publisher","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.","type":"journal_article","intvolume":"        21","doi":"10.46298/lmcs-21(2:2)2025","scopus_import":"1","volume":21,"related_material":{"record":[{"id":"13221","relation":"earlier_version","status":"public"},{"id":"20147","relation":"dissertation_contains","status":"public"}]},"date_created":"2025-09-11T12:17:52Z","author":[{"last_name":"Boker","full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi"},{"full_name":"Sarac, Naci E","last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E"}],"month":"04","oa":1,"article_number":"13149","_id":"20342","file_date_updated":"2025-09-11T12:17:12Z","ddc":["000"],"status":"public","oa_version":"Published Version","year":"2025","language":[{"iso":"eng"}],"OA_type":"gold","day":"08","issue":"2","publisher":"EPI Sciences","article_type":"original","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"Yes","has_accepted_license":"1"},{"oa":1,"month":"05","file_date_updated":"2025-06-02T08:13:11Z","_id":"19741","ddc":["000"],"status":"public","oa_version":"Published Version","doi":"10.1007/978-3-031-90643-5_16","scopus_import":"1","intvolume":"     15696","author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi"},{"last_name":"Sarac","full_name":"Sarac, Naci E","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"volume":15696,"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"20147"}]},"date_created":"2025-05-25T22:17:07Z","publisher":"Springer Nature","day":"01","article_processing_charge":"No","has_accepted_license":"1","department":[{"_id":"ToHe"}],"OA_type":"hybrid","year":"2025","language":[{"iso":"eng"}],"page":"303-312","corr_author":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031906428"]},"ec_funded":1,"arxiv":1,"publication_status":"published","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"title":"Automating the analysis of quantitative automata with QuAK","date_updated":"2026-04-07T12:02:57Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["2501.16088"]},"date_published":"2025-05-01T00:00:00Z","quality_controlled":"1","abstract":[{"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.","lang":"eng"}],"file":[{"content_type":"application/pdf","relation":"main_file","checksum":"a27fa245be8d83421e9127b48a09c8af","file_size":420669,"file_id":"19768","date_updated":"2025-06-02T08:13:11Z","success":1,"access_level":"open_access","creator":"dernst","date_created":"2025-06-02T08:13:11Z","file_name":"2025_TACAS_ChalupaMarek.pdf"}],"alternative_title":["LNCS"],"OA_place":"publisher","type":"conference","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.","citation":{"chicago":"Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:303–12. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>.","apa":"Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2025). Automating the analysis of quantitative automata with QuAK. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 303–312). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>","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.","ieee":"M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating the analysis of quantitative automata with QuAK,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2025, vol. 15696, pp. 303–312.","ama":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of quantitative automata with QuAK. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:303-312. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>","mla":"Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with QuAK.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"corr_author":"1","publication_identifier":{"isbn":["9783959773393"],"issn":["1868-8969"]},"ec_funded":1,"arxiv":1,"date_published":"2024-09-01T00:00:00Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["001556847400029"],"arxiv":["2407.10473"]},"isi":1,"publication_status":"published","title":"Strategic dominance: A new preorder for nondeterministic processes","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"date_updated":"2025-12-02T13:45:38Z","abstract":[{"text":"We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 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 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 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.","lang":"eng"}],"quality_controlled":"1","alternative_title":["LIPIcs"],"file":[{"checksum":"555bd343e1fb38adeab8fc465ff4fad8","relation":"main_file","content_type":"application/pdf","file_id":"18081","file_size":964124,"access_level":"open_access","creator":"dernst","success":1,"date_updated":"2024-09-17T07:48:56Z","file_name":"2024_LIPICS_Henzinger.pdf","date_created":"2024-09-17T07:48:56Z"}],"conference":{"start_date":"2024-09-09","location":"Calgary, Canada","end_date":"2024-09-13","name":"CONCUR: Conference on Concurrency Theory"},"OA_place":"publisher","type":"conference","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.","citation":{"apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2024). Strategic dominance: A new preorder for nondeterministic processes. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>.","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.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance: A new preorder for nondeterministic processes,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder for nondeterministic processes. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">10.4230/LIPIcs.CONCUR.2024.29</a>","mla":"Henzinger, Thomas A., et al. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">10.4230/LIPIcs.CONCUR.2024.29</a>.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"35th International Conference on Concurrency Theory","month":"09","oa":1,"article_number":"29","file_date_updated":"2024-09-17T07:48:56Z","_id":"18068","ddc":["000"],"oa_version":"Published Version","status":"public","intvolume":"       311","doi":"10.4230/LIPIcs.CONCUR.2024.29","scopus_import":"1","volume":311,"date_created":"2024-09-15T22:01:40Z","author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","last_name":"Sarac"}],"day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"article_processing_charge":"Yes","has_accepted_license":"1","year":"2024","language":[{"iso":"eng"}],"OA_type":"gold"},{"date_updated":"2026-04-07T12:02:57Z","APC_amount":"2748 EUR","title":"QuAK: Quantitative Automata Kit","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"isi":1,"date_published":"2024-10-26T00:00:00Z","external_id":{"isi":["001419008700001"],"arxiv":["2409.03569"]},"abstract":[{"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.","lang":"eng"}],"quality_controlled":"1","publication_identifier":{"isbn":["9783031753862"],"issn":["0302-9743"],"eissn":["1611-3349"]},"corr_author":"1","ec_funded":1,"arxiv":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"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.","apa":"Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2024). QuAK: Quantitative Automata Kit. In <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i> (Vol. 15222, pp. 3–20). Crete, Greece: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">https://doi.org/10.1007/978-3-031-75387-9_1</a>","chicago":"Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “QuAK: Quantitative Automata Kit.” In <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>, 15222:3–20. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">https://doi.org/10.1007/978-3-031-75387-9_1</a>.","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.” <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>, vol. 15222, Springer Nature, 2024, pp. 3–20, doi:<a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">10.1007/978-3-031-75387-9_1</a>.","ieee":"M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “QuAK: Quantitative Automata Kit,” in <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>, Crete, Greece, 2024, vol. 15222, pp. 3–20.","ama":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata Kit. In: <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>. Vol 15222. Springer Nature; 2024:3-20. doi:<a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">10.1007/978-3-031-75387-9_1</a>"},"publication":"12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","file":[{"content_type":"application/pdf","relation":"main_file","checksum":"43e432f82be376434b358f3dd7a94b71","file_id":"17635","file_size":847422,"success":1,"date_updated":"2024-09-05T14:26:02Z","access_level":"open_access","creator":"esarac","date_created":"2024-09-05T14:26:02Z","file_name":"isola24.pdf"},{"date_updated":"2025-01-21T14:39:49Z","success":1,"access_level":"open_access","creator":"dernst","file_name":"2024_LNCS_Chalupa.pdf","date_created":"2025-01-21T14:39:49Z","relation":"main_file","content_type":"application/pdf","checksum":"6bc04f07bb5612c0e7ea00ac121a69b6","file_id":"18865","file_size":1358706}],"alternative_title":["LNCS"],"type":"conference","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. N. Mazzocchi was affiliated with ISTA when his collaboration started.","OA_place":"publisher","conference":{"start_date":"2024-10-27","location":"Crete, Greece","end_date":"2024-10-31","name":"ISoLA: International Symposium on Leveraging Applications"},"scopus_import":"1","doi":"10.1007/978-3-031-75387-9_1","intvolume":"     15222","author":[{"first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","last_name":"Sarac","full_name":"Sarac, Naci E"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"20147","status":"public"}]},"date_created":"2024-09-05T14:27:08Z","volume":15222,"oa":1,"month":"10","status":"public","oa_version":"Published Version","_id":"17634","file_date_updated":"2025-01-21T14:39:49Z","ddc":["000"],"OA_type":"hybrid","language":[{"iso":"eng"}],"year":"2024","page":"3-20","publisher":"Springer Nature","day":"26","has_accepted_license":"1","article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"GradSch"},{"_id":"ToHe"}]},{"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031742330"],"eissn":["1611-3349"]},"corr_author":"1","arxiv":1,"ec_funded":1,"date_updated":"2026-05-20T08:43:20Z","title":"Approximate distributed monitoring under partial synchrony: Balancing speed & accuracy","APC_amount":"2748 EUR","publication_status":"published","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"date_published":"2024-10-12T00:00:00Z","external_id":{"isi":["001420093700018"],"arxiv":["2408.05033"]},"isi":1,"abstract":[{"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.","lang":"eng"}],"quality_controlled":"1","file":[{"file_size":1897101,"file_id":"18539","checksum":"7b8ca21b8c19ab796fa445b0e54003ca","relation":"main_file","content_type":"application/pdf","file_name":"2024_LNCS_Bonakdarpour.pdf","date_created":"2024-11-11T09:42:28Z","creator":"dernst","access_level":"open_access","success":1,"date_updated":"2024-11-11T09:42:28Z"}],"alternative_title":["LNCS"],"type":"conference","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).","OA_place":"publisher","conference":{"name":"RV: Conference on Runtime Verification","start_date":"2024-10-15","location":"Istanbul, Turkey","end_date":"2024-10-17"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. In: <i>24th International Conference on Runtime Verification</i>. Vol 15191. Springer Nature; 2024:282-301. doi:<a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">10.1007/978-3-031-74234-7_18</a>","ieee":"B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy,” in <i>24th International Conference on Runtime Verification</i>, Istanbul, Turkey, 2024, vol. 15191, pp. 282–301.","mla":"Bonakdarpour, Borzoo, et al. “Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed &#38; Accuracy.” <i>24th International Conference on Runtime Verification</i>, vol. 15191, Springer Nature, 2024, pp. 282–301, doi:<a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">10.1007/978-3-031-74234-7_18</a>.","ista":"Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. 2024. Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. 24th International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 15191, 282–301.","apa":"Bonakdarpour, B., Momtaz, A., Nickovic, D., &#38; Sarac, N. E. (2024). Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. In <i>24th International Conference on Runtime Verification</i> (Vol. 15191, pp. 282–301). Istanbul, Turkey: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">https://doi.org/10.1007/978-3-031-74234-7_18</a>","chicago":"Bonakdarpour, Borzoo, Anik Momtaz, Dejan Nickovic, and Naci E Sarac. “Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed &#38; Accuracy.” In <i>24th International Conference on Runtime Verification</i>, 15191:282–301. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">https://doi.org/10.1007/978-3-031-74234-7_18</a>.","short":"B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301."},"publication":"24th International Conference on Runtime Verification","oa":1,"month":"10","oa_version":"Published Version","status":"public","ddc":["000"],"_id":"18521","file_date_updated":"2024-11-11T09:42:28Z","scopus_import":"1","doi":"10.1007/978-3-031-74234-7_18","intvolume":"     15191","author":[{"first_name":"Borzoo","full_name":"Bonakdarpour, Borzoo","last_name":"Bonakdarpour"},{"first_name":"Anik","full_name":"Momtaz, Anik","last_name":"Momtaz"},{"first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","full_name":"Nickovic, Dejan"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","full_name":"Sarac, Naci E","last_name":"Sarac"}],"date_created":"2024-11-10T23:01:58Z","volume":15191,"publisher":"Springer Nature","day":"12","has_accepted_license":"1","article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"OA_type":"hybrid","language":[{"iso":"eng"}],"year":"2024","page":"282-301"},{"alternative_title":["LNCS"],"file":[{"checksum":"981025aed580b6b27c426cb8856cf63e","content_type":"application/pdf","relation":"main_file","file_size":449027,"file_id":"12468","creator":"esarac","access_level":"open_access","date_updated":"2023-01-31T07:22:21Z","success":1,"date_created":"2023-01-31T07:22:21Z","file_name":"qsl.pdf"},{"file_id":"13153","file_size":1048171,"content_type":"application/pdf","relation":"main_file","checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","date_created":"2023-06-19T10:28:09Z","file_name":"2023_LNCS_HenzingerT.pdf","success":1,"date_updated":"2023-06-19T10:28:09Z","access_level":"open_access","creator":"dernst"}],"conference":{"start_date":"2023-04-22","location":"Paris, France","end_date":"2023-04-27","name":"FOSSACS: Foundations of Software Science and Computation Structures"},"type":"conference","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","citation":{"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.","apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Quantitative safety and liveness. In <i>26th International Conference Foundations of Software Science and Computation Structures</i> (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In <i>26th International Conference Foundations of Software Science and Computation Structures</i>, 13992:349–70. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>.","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.” <i>26th International Conference Foundations of Software Science and Computation Structures</i>, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: <i>26th International Conference Foundations of Software Science and Computation Structures</i>. Vol 13992. Springer Nature; 2023:349-370. doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in <i>26th International Conference Foundations of Software Science and Computation Structures</i>, Paris, France, 2023, vol. 13992, pp. 349–370."},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication":"26th International Conference Foundations of Software Science and Computation Structures","corr_author":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308284"],"eissn":["1611-3349"]},"ec_funded":1,"arxiv":1,"isi":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["2301.11175"],"isi":["001288609300017"]},"date_published":"2023-04-21T00:00:00Z","title":"Quantitative safety and liveness","publication_status":"published","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"date_updated":"2025-09-09T12:21:08Z","quality_controlled":"1","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."}],"day":"21","publisher":"Springer Nature","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"No","has_accepted_license":"1","year":"2023","language":[{"iso":"eng"}],"page":"349-370","month":"04","oa":1,"ddc":["000"],"_id":"12467","file_date_updated":"2023-06-19T10:28:09Z","oa_version":"Published Version","status":"public","intvolume":"     13992","doi":"10.1007/978-3-031-30829-1_17","scopus_import":"1","volume":13992,"date_created":"2023-01-31T07:23:56Z","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","full_name":"Sarac, Naci E","last_name":"Sarac"}]},{"ec_funded":1,"arxiv":1,"publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959772785"]},"corr_author":"1","quality_controlled":"1","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."}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["2305.03447"]},"date_published":"2023-07-05T00:00:00Z","date_updated":"2025-07-10T11:50:41Z","publication_status":"published","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"title":"Regular methods for operator precedence languages","conference":{"start_date":"2023-07-10","location":"Paderborn, Germany","end_date":"2023-07-14","name":"ICALP: Automata, Languages and Programming"},"type":"conference","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"],"file":[{"success":1,"date_updated":"2023-07-24T15:11:05Z","creator":"esarac","access_level":"open_access","date_created":"2023-07-24T15:11:05Z","file_name":"icalp23.pdf","content_type":"application/pdf","relation":"main_file","checksum":"5d4c8932ef3450615a53b9bb15d92eb2","file_size":859379,"file_id":"13293"}],"publication":"50th International Colloquium on Automata, Languages, and Programming","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods for operator precedence languages,” in <i>50th International Colloquium on Automata, Languages, and Programming</i>, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.","ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: <i>50th International Colloquium on Automata, Languages, and Programming</i>. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1--129:20. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">10.4230/LIPIcs.ICALP.2023.129</a>","mla":"Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.” <i>50th International Colloquium on Automata, Languages, and Programming</i>, vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">10.4230/LIPIcs.ICALP.2023.129</a>.","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.","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Regular methods for operator precedence languages. In <i>50th International Colloquium on Automata, Languages, and Programming</i> (Vol. 261, p. 129:1--129:20). Paderborn, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Regular Methods for Operator Precedence Languages.” In <i>50th International Colloquium on Automata, Languages, and Programming</i>, 261:129:1--129:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>.","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."},"oa_version":"Published Version","status":"public","_id":"13292","file_date_updated":"2023-07-24T15:11:05Z","ddc":["000"],"month":"07","oa":1,"date_created":"2023-07-24T15:11:41Z","volume":261,"author":[{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kebis, Pavol","last_name":"Kebis","first_name":"Pavol"},{"first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","full_name":"Sarac, Naci E","last_name":"Sarac"}],"intvolume":"       261","scopus_import":"1","doi":"10.4230/LIPIcs.ICALP.2023.129","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"has_accepted_license":"1","article_processing_charge":"Yes","day":"05","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","page":"129:1--129:20","language":[{"iso":"eng"}],"year":"2023"},{"quality_controlled":"1","abstract":[{"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.","lang":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["2307.06016"],"isi":["001570542500017"]},"date_published":"2023-09-01T00:00:00Z","isi":1,"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"title":"Safety and liveness of quantitative automata","publication_status":"published","date_updated":"2026-04-07T12:02:57Z","arxiv":1,"ec_funded":1,"corr_author":"1","publication_identifier":{"isbn":["9783959772990"],"eissn":["1868-8969"]},"publication":"34th International Conference on Concurrency Theory","citation":{"ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: <i>34th International Conference on Concurrency Theory</i>. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>","ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness of quantitative automata,” in <i>34th International Conference on Concurrency Theory</i>, Antwerp, Belgium, 2023, vol. 279.","mla":"Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” <i>34th International Conference on Concurrency Theory</i>, vol. 279, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>.","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.","apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Safety and liveness of quantitative automata. In <i>34th International Conference on Concurrency Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>","chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Safety and Liveness of Quantitative Automata.” In <i>34th International Conference on Concurrency Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CONCUR: Conference on Concurrency Theory","end_date":"2023-09-23","start_date":"2023-09-18","location":"Antwerp, Belgium"},"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.","type":"conference","alternative_title":["LIPIcs"],"file":[{"file_size":755529,"file_id":"13224","checksum":"d40e57a04448ea5c77d7e1cfb9590a81","content_type":"application/pdf","relation":"main_file","date_created":"2023-07-14T12:03:48Z","file_name":"CONCUR23.pdf","creator":"esarac","access_level":"open_access","success":1,"date_updated":"2023-07-14T12:03:48Z"}],"volume":279,"related_material":{"record":[{"id":"20342","relation":"later_version","status":"public"},{"id":"20147","relation":"dissertation_contains","status":"public"}]},"date_created":"2023-07-14T10:00:15Z","author":[{"full_name":"Boker, Udi","last_name":"Boker","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","full_name":"Sarac, Naci E","last_name":"Sarac"}],"intvolume":"       279","doi":"10.4230/LIPIcs.CONCUR.2023.17","scopus_import":"1","article_number":"17","ddc":["000"],"_id":"13221","file_date_updated":"2023-07-14T12:03:48Z","status":"public","oa_version":"Published Version","month":"09","oa":1,"year":"2023","language":[{"iso":"eng"}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"No","has_accepted_license":"1","day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik"},{"ec_funded":1,"publication_identifier":{"issn":["0302-9743"]},"corr_author":"1","quality_controlled":"1","abstract":[{"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. ","lang":"eng"}],"date_updated":"2026-04-07T12:02:56Z","publication_status":"published","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"title":"Abstract monitors for quantitative specifications","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"isi":1,"external_id":{"isi":["000866539700011"]},"date_published":"2022-09-23T00:00:00Z","type":"conference","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","conference":{"end_date":"2022-09-30","start_date":"2022-09-28","location":"Tbilisi, Georgia","name":"RV: Runtime Verification"},"file":[{"relation":"main_file","content_type":"application/pdf","checksum":"05c7dcfbb9053a98f46441fb2eccb213","file_id":"12317","file_size":477110,"success":1,"date_updated":"2023-01-20T07:34:50Z","access_level":"open_access","creator":"dernst","file_name":"2022_LNCS_RV_Henzinger.pdf","date_created":"2023-01-20T07:34:50Z"}],"alternative_title":["LNCS"],"publication":"22nd International Conference on Runtime Verification","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications. In: <i>22nd International Conference on Runtime Verification</i>. Vol 13498. Springer Nature; 2022:200-220. doi:<a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">10.1007/978-3-031-17196-3_11</a>","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for quantitative specifications,” in <i>22nd International Conference on Runtime Verification</i>, Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220.","mla":"Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.” <i>22nd International Conference on Runtime Verification</i>, vol. 13498, Springer Nature, 2022, pp. 200–20, doi:<a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">10.1007/978-3-031-17196-3_11</a>.","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.","apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2022). Abstract monitors for quantitative specifications. In <i>22nd International Conference on Runtime Verification</i> (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">https://doi.org/10.1007/978-3-031-17196-3_11</a>","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract Monitors for Quantitative Specifications.” In <i>22nd International Conference on Runtime Verification</i>, 13498:200–220. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">https://doi.org/10.1007/978-3-031-17196-3_11</a>.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference on Runtime Verification, Springer Nature, 2022, pp. 200–220."},"oa_version":"Published Version","status":"public","_id":"11775","ddc":["000"],"file_date_updated":"2023-01-20T07:34:50Z","oa":1,"month":"09","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"20147"}]},"date_created":"2022-08-08T17:09:09Z","volume":13498,"scopus_import":"1","doi":"10.1007/978-3-031-17196-3_11","intvolume":"     13498","has_accepted_license":"1","article_processing_charge":"Yes","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"Springer Nature","day":"23","page":"200-220","language":[{"iso":"eng"}],"year":"2022"},{"month":"06","oa":1,"article_number":"9470547","status":"public","oa_version":"Published Version","_id":"9356","ddc":["000"],"file_date_updated":"2021-06-16T08:23:54Z","scopus_import":"1","doi":"10.1109/LICS52264.2021.9470547","date_created":"2021-04-30T17:30:47Z","related_material":{"record":[{"id":"20147","relation":"dissertation_contains","status":"public"}]},"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"last_name":"Sarac","full_name":"Sarac, Naci E","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"day":"29","publisher":"Institute of Electrical and Electronics Engineers","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"has_accepted_license":"1","article_processing_charge":"No","language":[{"iso":"eng"}],"year":"2021","arxiv":1,"date_published":"2021-06-29T00:00:00Z","isi":1,"external_id":{"arxiv":["2105.08353"],"isi":["000947350400021"]},"date_updated":"2026-04-07T12:02:57Z","publication_status":"published","title":"Quantitative and approximate monitoring","project":[{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"}],"quality_controlled":"1","abstract":[{"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.","lang":"eng"}],"file":[{"relation":"main_file","content_type":"application/pdf","checksum":"6e4cba3f72775f479c5b1b75d1a4a0c4","file_size":641990,"file_id":"9557","date_updated":"2021-06-16T08:23:54Z","success":1,"creator":"esarac","access_level":"open_access","file_name":"qam.pdf","date_created":"2021-06-16T08:23:54Z"}],"conference":{"start_date":"2021-06-29","location":"Online","end_date":"2021-07-02","name":"LICS: Logic in Computer Science"},"type":"conference","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).","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 9470547, Institute of Electrical and Electronics Engineers, 2021, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">10.1109/LICS52264.2021.9470547</a>.","ieee":"T. A. Henzinger and N. E. Sarac, “Quantitative and approximate monitoring,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Online, 2021.","ama":"Henzinger TA, Sarac NE. Quantitative and approximate monitoring. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics Engineers; 2021. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">10.1109/LICS52264.2021.9470547</a>","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.","chicago":"Henzinger, Thomas A, and Naci E Sarac. “Quantitative and Approximate Monitoring.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics Engineers, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">https://doi.org/10.1109/LICS52264.2021.9470547</a>.","apa":"Henzinger, T. A., &#38; Sarac, N. E. (2021). Quantitative and approximate monitoring. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Online: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470547\">https://doi.org/10.1109/LICS52264.2021.9470547</a>"},"publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science"},{"corr_author":"1","publication_identifier":{"issn":["0957-4174"],"eissn":["1873-6793"]},"project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"title":"Boosting expensive synchronizing heuristics","publication_status":"published","date_updated":"2026-04-16T09:15:47Z","date_published":"2021-04-01T00:00:00Z","external_id":{"isi":["000640531100038"]},"isi":1,"quality_controlled":"1","abstract":[{"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.","lang":"eng"}],"file":[{"file_name":"synchroPaperRevised.pdf","date_created":"2020-12-02T13:33:51Z","date_updated":"2020-12-02T13:33:51Z","creator":"esarac","access_level":"open_access","file_size":634967,"file_id":"8913","relation":"main_file","content_type":"application/pdf","checksum":"600c2f81bc898a725bcfa7cf26ff4fed"}],"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.","type":"journal_article","citation":{"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.” <i>Expert Systems with Applications</i>, vol. 167, no. 4, 114203, Elsevier, 2021, doi:<a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">10.1016/j.eswa.2020.114203</a>.","ieee":"N. E. Sarac, Ö. F. Altun, K. T. Atam, S. Karahoda, K. Kaya, and H. Yenigün, “Boosting expensive synchronizing heuristics,” <i>Expert Systems with Applications</i>, vol. 167, no. 4. Elsevier, 2021.","ama":"Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. Boosting expensive synchronizing heuristics. <i>Expert Systems with Applications</i>. 2021;167(4). doi:<a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">10.1016/j.eswa.2020.114203</a>","short":"N.E. Sarac, Ö.F. Altun, K.T. Atam, S. Karahoda, K. Kaya, H. Yenigün, Expert Systems with Applications 167 (2021).","chicago":"Sarac, Naci E, Ömer Faruk Altun, Kamil Tolga Atam, Sertac Karahoda, Kamer Kaya, and Hüsnü Yenigün. “Boosting Expensive Synchronizing Heuristics.” <i>Expert Systems with Applications</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">https://doi.org/10.1016/j.eswa.2020.114203</a>.","apa":"Sarac, N. E., Altun, Ö. F., Atam, K. T., Karahoda, S., Kaya, K., &#38; Yenigün, H. (2021). Boosting expensive synchronizing heuristics. <i>Expert Systems with Applications</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.eswa.2020.114203\">https://doi.org/10.1016/j.eswa.2020.114203</a>"},"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","publication":"Expert Systems with Applications","oa":1,"month":"04","_id":"8912","ddc":["000"],"file_date_updated":"2020-12-02T13:33:51Z","status":"public","oa_version":"Submitted Version","article_number":"114203","doi":"10.1016/j.eswa.2020.114203","scopus_import":"1","intvolume":"       167","author":[{"first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","last_name":"Sarac","full_name":"Sarac, Naci E"},{"full_name":"Altun, Ömer Faruk","last_name":"Altun","first_name":"Ömer Faruk"},{"full_name":"Atam, Kamil Tolga","last_name":"Atam","first_name":"Kamil Tolga"},{"first_name":"Sertac","last_name":"Karahoda","full_name":"Karahoda, Sertac"},{"first_name":"Kamer","last_name":"Kaya","full_name":"Kaya, Kamer"},{"first_name":"Hüsnü","full_name":"Yenigün, Hüsnü","last_name":"Yenigün"}],"volume":167,"date_created":"2020-12-02T13:34:25Z","article_type":"original","publisher":"Elsevier","day":"01","issue":"4","article_processing_charge":"No","has_accepted_license":"1","department":[{"_id":"ToHe"}],"year":"2021","language":[{"iso":"eng"}]},{"day":"02","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"has_accepted_license":"1","article_processing_charge":"No","language":[{"iso":"eng"}],"year":"2020","page":"3-18","month":"10","oa":1,"status":"public","oa_version":"Submitted Version","file_date_updated":"2020-10-15T14:28:06Z","_id":"8623","ddc":["000"],"intvolume":"     12399","scopus_import":"1","doi":"10.1007/978-3-030-60508-7_1","date_created":"2020-10-07T15:05:37Z","volume":12399,"author":[{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"alternative_title":["LNCS"],"file":[{"success":1,"date_updated":"2020-10-15T14:28:06Z","access_level":"open_access","creator":"esarac","date_created":"2020-10-15T14:28:06Z","file_name":"monitorability.pdf","content_type":"application/pdf","relation":"main_file","checksum":"00661f9b7034f52e18bf24fa552b8194","file_id":"8665","file_size":478148}],"conference":{"name":"RV: Runtime Verification","end_date":"2020-10-09","start_date":"2020-10-06","location":"Los Angeles, CA, United States"},"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","type":"conference","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","citation":{"mla":"Henzinger, Thomas A., and Naci E. Sarac. “Monitorability under Assumptions.” <i>Runtime Verification</i>, vol. 12399, Springer Nature, 2020, pp. 3–18, doi:<a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">10.1007/978-3-030-60508-7_1</a>.","ista":"Henzinger TA, Sarac NE. 2020. Monitorability under assumptions. Runtime Verification. RV: Runtime Verification, LNCS, vol. 12399, 3–18.","ama":"Henzinger TA, Sarac NE. Monitorability under assumptions. In: <i>Runtime Verification</i>. Vol 12399. Springer Nature; 2020:3-18. doi:<a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">10.1007/978-3-030-60508-7_1</a>","ieee":"T. A. Henzinger and N. E. Sarac, “Monitorability under assumptions,” in <i>Runtime Verification</i>, Los Angeles, CA, United States, 2020, vol. 12399, pp. 3–18.","short":"T.A. Henzinger, N.E. Sarac, in:, Runtime Verification, Springer Nature, 2020, pp. 3–18.","apa":"Henzinger, T. A., &#38; Sarac, N. E. (2020). Monitorability under assumptions. In <i>Runtime Verification</i> (Vol. 12399, pp. 3–18). Los Angeles, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">https://doi.org/10.1007/978-3-030-60508-7_1</a>","chicago":"Henzinger, Thomas A, and Naci E Sarac. “Monitorability under Assumptions.” In <i>Runtime Verification</i>, 12399:3–18. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-60508-7_1\">https://doi.org/10.1007/978-3-030-60508-7_1</a>."},"publication":"Runtime Verification","publication_identifier":{"eisbn":["9783030605087"],"issn":["0302-9743"],"isbn":["9783030605070"],"eissn":["1611-3349"]},"isi":1,"date_published":"2020-10-02T00:00:00Z","external_id":{"isi":["000728160600001"]},"date_updated":"2026-04-16T10:22:01Z","publication_status":"published","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","grant_number":"Z211"}],"title":"Monitorability under assumptions","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."}],"quality_controlled":"1"}]