[{"ddc":["000"],"date_updated":"2023-07-14T11:20:27Z","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2023-06-19T10:28:09Z","_id":"12467","status":"public","conference":{"name":"FOSSACS: Foundations of Software Science and Computation Structures","start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","success":1,"checksum":"981025aed580b6b27c426cb8856cf63e","file_id":"12468","file_size":449027,"date_updated":"2023-01-31T07:22:21Z","creator":"esarac","file_name":"qsl.pdf","date_created":"2023-01-31T07:22:21Z"},{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","file_id":"13153","success":1,"date_updated":"2023-06-19T10:28:09Z","file_size":1048171,"creator":"dernst","date_created":"2023-06-19T10:28:09Z","file_name":"2023_LNCS_HenzingerT.pdf"}],"publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308284"],"issn":["0302-9743"]},"license":"https://creativecommons.org/licenses/by/4.0/","ec_funded":1,"volume":13992,"oa_version":"Published Version","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."}],"intvolume":" 13992","month":"04","alternative_title":["LNCS"],"scopus_import":"1","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"mla":"Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International Conference Foundations of Software Science and Computation Structures, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: 26th International Conference Foundations of Software Science and Computation Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17","apa":"Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative safety and liveness. In 26th International Conference Foundations of Software Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in 26th International Conference Foundations of Software Science and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.","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.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In 26th International Conference Foundations of Software Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17.","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."},"title":"Quantitative safety and liveness","external_id":{"arxiv":["2301.11175"]},"article_processing_charge":"No","author":[{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"full_name":"Sarac, Naci E","last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"publication":"26th International Conference Foundations of Software Science and Computation Structures","day":"21","year":"2023","has_accepted_license":"1","date_created":"2023-01-31T07:23:56Z","doi":"10.1007/978-3-031-30829-1_17","date_published":"2023-04-21T00:00:00Z","page":"349-370","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","oa":1,"quality_controlled":"1","publisher":"Springer Nature"},{"ec_funded":1,"volume":261,"publication_status":"published","publication_identifier":{"isbn":["9783959772785"],"eissn":["1868-8969"]},"language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"5d4c8932ef3450615a53b9bb15d92eb2","file_id":"13293","success":1,"date_updated":"2023-07-24T15:11:05Z","file_size":859379,"creator":"esarac","date_created":"2023-07-24T15:11:05Z","file_name":"icalp23.pdf"}],"alternative_title":["LIPIcs"],"intvolume":" 261","month":"07","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."}],"oa_version":"Published Version","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2023-07-24T15:11:05Z","date_updated":"2023-07-31T08:38:38Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2023-07-10","location":"Paderborn, Germany","end_date":"2023-07-14","name":"ICALP: International Colloquium on Automata, Languages, and Programming"},"type":"conference","status":"public","_id":"13292","page":"129:1--129:20","date_created":"2023-07-24T15:11:41Z","doi":"10.4230/LIPIcs.ICALP.2023.129","date_published":"2023-07-05T00:00:00Z","year":"2023","has_accepted_license":"1","publication":"50th International Colloquium on Automata, Languages, and Programming","day":"05","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","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","external_id":{"arxiv":["2305.03447"]},"article_processing_charge":"Yes","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Kebis, Pavol","last_name":"Kebis","first_name":"Pavol"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"last_name":"Sarac","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E"}],"title":"Regular methods for operator precedence languages","citation":{"mla":"Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.” 50th International Colloquium on Automata, Languages, and Programming, vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20, doi:10.4230/LIPIcs.ICALP.2023.129.","ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: 50th International Colloquium on Automata, Languages, and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1--129:20. doi:10.4230/LIPIcs.ICALP.2023.129","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2023). Regular methods for operator precedence languages. In 50th International Colloquium on Automata, Languages, and Programming (Vol. 261, p. 129:1--129:20). Paderborn, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.129","ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods for operator precedence languages,” in 50th International Colloquium on Automata, Languages, and Programming, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.","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.","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Regular Methods for Operator Precedence Languages.” In 50th International Colloquium on Automata, Languages, and Programming, 261:129:1--129:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.129.","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: International Colloquium on Automata, Languages, and Programming, LIPIcs, vol. 261, 129:1--129:20."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}]},{"article_number":"17","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Safety and Liveness of Quantitative Automata.” In 34th International Conference on Concurrency Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17.","ista":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness of quantitative automata. 34th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17.","mla":"Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” 34th International Conference on Concurrency Theory, vol. 279, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.17.","apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Safety and liveness of quantitative automata. In 34th International Conference on Concurrency Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17","ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: 34th International Conference on Concurrency Theory. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.17","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.","ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness of quantitative automata,” in 34th International Conference on Concurrency Theory, Antwerp, Belgium, 2023, vol. 279."},"title":"Safety and liveness of quantitative automata","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","full_name":"Boker, Udi","last_name":"Boker"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E"}],"external_id":{"arxiv":["2307.06016"]},"article_processing_charge":"No","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.","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","oa":1,"day":"01","publication":"34th International Conference on Concurrency Theory","has_accepted_license":"1","year":"2023","doi":"10.4230/LIPIcs.CONCUR.2023.17","date_published":"2023-09-01T00:00:00Z","date_created":"2023-07-14T10:00:15Z","_id":"13221","status":"public","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2023-09-18","end_date":"2023-09-23","location":"Antwerp, Belgium","name":"CONCUR: Conference on Concurrency Theory"},"ddc":["000"],"date_updated":"2023-10-09T07:14:03Z","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2023-07-14T12:03:48Z","oa_version":"Published Version","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"}],"month":"09","intvolume":" 279","alternative_title":["LIPIcs"],"file":[{"success":1,"file_id":"13224","checksum":"d40e57a04448ea5c77d7e1cfb9590a81","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"CONCUR23.pdf","date_created":"2023-07-14T12:03:48Z","creator":"esarac","file_size":755529,"date_updated":"2023-07-14T12:03:48Z"}],"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959772990"]},"publication_status":"published","volume":279,"ec_funded":1},{"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2023-01-20T07:34:50Z","date_updated":"2023-08-03T13:38:46Z","ddc":["000"],"type":"conference","conference":{"location":"Tbilisi, Georgia","end_date":"2022-09-30","start_date":"2022-09-28","name":"RV: Runtime Verification"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","_id":"11775","volume":13498,"ec_funded":1,"publication_identifier":{"issn":["0302-9743"]},"publication_status":"published","file":[{"creator":"dernst","date_updated":"2023-01-20T07:34:50Z","file_size":477110,"date_created":"2023-01-20T07:34:50Z","file_name":"2022_LNCS_RV_Henzinger.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"12317","checksum":"05c7dcfbb9053a98f46441fb2eccb213","success":1}],"language":[{"iso":"eng"}],"alternative_title":["LNCS"],"scopus_import":"1","month":"09","intvolume":" 13498","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"}],"oa_version":"Published Version","author":[{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","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","last_name":"Sarac","full_name":"Sarac, Naci E"}],"external_id":{"isi":["000866539700011"]},"article_processing_charge":"Yes","title":"Abstract monitors for quantitative specifications","citation":{"chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract Monitors for Quantitative Specifications.” In 22nd International Conference on Runtime Verification, 13498:200–220. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-17196-3_11.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative specifications. 22nd International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 13498, 200–220.","mla":"Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.” 22nd International Conference on Runtime Verification, vol. 13498, Springer Nature, 2022, pp. 200–20, doi:10.1007/978-3-031-17196-3_11.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for quantitative specifications,” in 22nd International Conference on Runtime Verification, Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference on Runtime Verification, Springer Nature, 2022, pp. 200–220.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications. In: 22nd International Conference on Runtime Verification. Vol 13498. Springer Nature; 2022:200-220. doi:10.1007/978-3-031-17196-3_11","apa":"Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2022). Abstract monitors for quantitative specifications. In 22nd International Conference on Runtime Verification (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature. https://doi.org/10.1007/978-3-031-17196-3_11"},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"page":"200-220","date_published":"2022-09-23T00:00:00Z","doi":"10.1007/978-3-031-17196-3_11","date_created":"2022-08-08T17:09:09Z","isi":1,"has_accepted_license":"1","year":"2022","day":"23","publication":"22nd International Conference on Runtime Verification","quality_controlled":"1","publisher":"Springer Nature","oa":1,"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093."},{"volume":13372,"ec_funded":1,"file":[{"file_name":"2022_LNCS_Doveri.pdf","date_created":"2023-01-30T12:51:02Z","creator":"dernst","file_size":497682,"date_updated":"2023-01-30T12:51:02Z","success":1,"file_id":"12465","checksum":"edc363b1be5447a09063e115c247918a","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"publication_identifier":{"eisbn":["9783031131882"],"issn":["0302-9743"],"isbn":["9783031131875"],"eissn":["1611-3349"]},"publication_status":"published","month":"08","intvolume":" 13372","scopus_import":"1","alternative_title":["LNCS"],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign. The resulting implementation, called FORKLIFT, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870"}],"file_date_updated":"2023-01-30T12:51:02Z","department":[{"_id":"ToHe"}],"ddc":["000"],"date_updated":"2023-09-05T15:13:36Z","status":"public","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2022-08-07","location":"Haifa, Israel","end_date":"2022-08-10","name":"CAV: Computer Aided Verification"},"_id":"12302","date_published":"2022-08-06T00:00:00Z","doi":"10.1007/978-3-031-13188-2_6","date_created":"2023-01-16T10:06:31Z","page":"109-129","day":"06","publication":"Computer Aided Verification","has_accepted_license":"1","isi":1,"year":"2022","quality_controlled":"1","publisher":"Springer Nature","oa":1,"acknowledgement":"This work was partially funded by the ESF Investing in your future, the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00 BOSCO, the Ramón y Cajal fellowship RYC-2016-20281, and the ERC grant PR1001ERC02.","title":"FORQ-based language inclusion formal testing","author":[{"first_name":"Kyveli","full_name":"Doveri, Kyveli","last_name":"Doveri"},{"full_name":"Ganty, Pierre","last_name":"Ganty","first_name":"Pierre"},{"first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"}],"external_id":{"arxiv":["2207.13549"],"isi":["000870310500006"]},"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"short":"K. Doveri, P. Ganty, N.A. Mazzocchi, in:, Computer Aided Verification, Springer Nature, 2022, pp. 109–129.","ieee":"K. Doveri, P. Ganty, and N. A. Mazzocchi, “FORQ-based language inclusion formal testing,” in Computer Aided Verification, Haifa, Israel, 2022, vol. 13372, pp. 109–129.","apa":"Doveri, K., Ganty, P., & Mazzocchi, N. A. (2022). FORQ-based language inclusion formal testing. In Computer Aided Verification (Vol. 13372, pp. 109–129). Haifa, Israel: Springer Nature. https://doi.org/10.1007/978-3-031-13188-2_6","ama":"Doveri K, Ganty P, Mazzocchi NA. FORQ-based language inclusion formal testing. In: Computer Aided Verification. Vol 13372. Springer Nature; 2022:109-129. doi:10.1007/978-3-031-13188-2_6","mla":"Doveri, Kyveli, et al. “FORQ-Based Language Inclusion Formal Testing.” Computer Aided Verification, vol. 13372, Springer Nature, 2022, pp. 109–29, doi:10.1007/978-3-031-13188-2_6.","ista":"Doveri K, Ganty P, Mazzocchi NA. 2022. FORQ-based language inclusion formal testing. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13372, 109–129.","chicago":"Doveri, Kyveli, Pierre Ganty, and Nicolas Adrien Mazzocchi. “FORQ-Based Language Inclusion Formal Testing.” In Computer Aided Verification, 13372:109–29. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-13188-2_6."},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}]}]