[{"arxiv":1,"conference":{"name":"GD: Graph Drawing and Network Visualization","location":"Isola delle Femmine, Palermo, Italy","start_date":"2023-09-20","end_date":"2023-09-22"},"page":"18-33","acknowledgement":"This work was initiated at the 16th European Research Week on Geometric Graphs in Strobl in 2019. A.W. is supported by the Austrian Science Fund (FWF): W1230. S.T. has been funded by the Vienna Science and Technology Fund (WWTF) [10.47379/ICT19035]. A preliminary version of this work has been presented at the 38th European Workshop on Computational Geometry (EuroCG 2022) in Perugia [9]. A full version of this paper, which includes appendices but is otherwise identical, is available as a technical report [10].","scopus_import":"1","month":"01","department":[{"_id":"UlWa"},{"_id":"HeEd"}],"publisher":"Springer Nature","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2202.12175"}],"type":"conference","volume":14466,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2024-01-06T00:00:00Z","doi":"10.1007/978-3-031-49275-4_2","status":"public","language":[{"iso":"eng"}],"intvolume":" 14466","alternative_title":["LNCS"],"date_created":"2024-01-28T23:01:43Z","_id":"14888","year":"2024","publication_status":"published","abstract":[{"lang":"eng","text":"A face in a curve arrangement is called popular if it is bounded by the same curve multiple times. Motivated by the automatic generation of curved nonogram puzzles, we investigate possibilities to eliminate the popular faces in an arrangement by inserting a single additional curve. This turns out to be NP-hard; however, it becomes tractable when the number of popular faces is small: We present a probabilistic FPT-approach in the number of popular faces."}],"quality_controlled":"1","article_processing_charge":"No","oa_version":"Preprint","citation":{"short":"P. De Nooijer, S. Terziadis, A. Weinberger, Z. Masárová, T. Mchedlidze, M. Löffler, G. Rote, in:, 31st International Symposium on Graph Drawing and Network Visualization, Springer Nature, 2024, pp. 18–33.","chicago":"De Nooijer, Phoebe, Soeren Terziadis, Alexandra Weinberger, Zuzana Masárová, Tamara Mchedlidze, Maarten Löffler, and Günter Rote. “Removing Popular Faces in Curve Arrangements.” In 31st International Symposium on Graph Drawing and Network Visualization, 14466:18–33. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-49275-4_2.","ista":"De Nooijer P, Terziadis S, Weinberger A, Masárová Z, Mchedlidze T, Löffler M, Rote G. 2024. Removing popular faces in curve arrangements. 31st International Symposium on Graph Drawing and Network Visualization. GD: Graph Drawing and Network Visualization, LNCS, vol. 14466, 18–33.","mla":"De Nooijer, Phoebe, et al. “Removing Popular Faces in Curve Arrangements.” 31st International Symposium on Graph Drawing and Network Visualization, vol. 14466, Springer Nature, 2024, pp. 18–33, doi:10.1007/978-3-031-49275-4_2.","apa":"De Nooijer, P., Terziadis, S., Weinberger, A., Masárová, Z., Mchedlidze, T., Löffler, M., & Rote, G. (2024). Removing popular faces in curve arrangements. In 31st International Symposium on Graph Drawing and Network Visualization (Vol. 14466, pp. 18–33). Isola delle Femmine, Palermo, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-49275-4_2","ama":"De Nooijer P, Terziadis S, Weinberger A, et al. Removing popular faces in curve arrangements. In: 31st International Symposium on Graph Drawing and Network Visualization. Vol 14466. Springer Nature; 2024:18-33. doi:10.1007/978-3-031-49275-4_2","ieee":"P. De Nooijer et al., “Removing popular faces in curve arrangements,” in 31st International Symposium on Graph Drawing and Network Visualization, Isola delle Femmine, Palermo, Italy, 2024, vol. 14466, pp. 18–33."},"author":[{"last_name":"De Nooijer","first_name":"Phoebe","full_name":"De Nooijer, Phoebe"},{"first_name":"Soeren","last_name":"Terziadis","full_name":"Terziadis, Soeren"},{"last_name":"Weinberger","first_name":"Alexandra","full_name":"Weinberger, Alexandra"},{"last_name":"Masárová","first_name":"Zuzana","full_name":"Masárová, Zuzana","id":"45CFE238-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6660-1322"},{"full_name":"Mchedlidze, Tamara","last_name":"Mchedlidze","first_name":"Tamara"},{"first_name":"Maarten","last_name":"Löffler","full_name":"Löffler, Maarten"},{"full_name":"Rote, Günter","last_name":"Rote","first_name":"Günter"}],"date_updated":"2025-07-21T07:28:03Z","day":"06","oa":1,"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031492747"],"eissn":["1611-3349"]},"publication":"31st International Symposium on Graph Drawing and Network Visualization","external_id":{"arxiv":["2202.12175"]},"title":"Removing popular faces in curve arrangements","project":[{"_id":"bdb2a702-d553-11ed-ba76-f12e3e5a3bc6","grant_number":"101087907","name":"A quantum hybrid of atoms and milligram-scale pendulums: towards gravitational quantum mechanics"}]},{"arxiv":1,"page":"349-370","conference":{"start_date":"2023-04-22","location":"Paris, France","name":"FOSSACS: Foundations of Software Science and Computation Structures","end_date":"2023-04-27"},"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","scopus_import":"1","publisher":"Springer Nature","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"month":"04","type":"conference","volume":13992,"file_date_updated":"2023-06-19T10:28:09Z","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","doi":"10.1007/978-3-031-30829-1_17","date_published":"2023-04-21T00:00:00Z","language":[{"iso":"eng"}],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"intvolume":" 13992","alternative_title":["LNCS"],"ddc":["000"],"ec_funded":1,"date_created":"2023-01-31T07:23:56Z","year":"2023","_id":"12467","publication_status":"published","file":[{"file_name":"qsl.pdf","file_id":"12468","date_created":"2023-01-31T07:22:21Z","relation":"main_file","success":1,"date_updated":"2023-01-31T07:22:21Z","checksum":"981025aed580b6b27c426cb8856cf63e","content_type":"application/pdf","file_size":449027,"access_level":"open_access","creator":"esarac"},{"date_updated":"2023-06-19T10:28:09Z","file_name":"2023_LNCS_HenzingerT.pdf","file_id":"13153","date_created":"2023-06-19T10:28:09Z","relation":"main_file","success":1,"access_level":"open_access","creator":"dernst","checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","content_type":"application/pdf","file_size":1048171}],"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."}],"quality_controlled":"1","oa_version":"Published Version","article_processing_charge":"No","author":[{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Mazzocchi","first_name":"Nicolas Adrien","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac"}],"citation":{"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.","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","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.","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","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."},"date_updated":"2023-07-14T11:20:27Z","day":"21","publication":"26th International Conference Foundations of Software Science and Computation Structures","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308284"]},"oa":1,"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"title":"Quantitative safety and liveness","external_id":{"arxiv":["2301.11175"]},"has_accepted_license":"1"},{"has_accepted_license":"1","title":"Bubaak: Runtime monitoring of program verifiers","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"oa":1,"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308192"],"eisbn":["9783031308208"],"issn":["0302-9743"]},"publication":"Tools and Algorithms for the Construction and Analysis of Systems","day":"20","citation":{"mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.","apa":"Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32","ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 535–540.","ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In Tools and Algorithms for the Construction and Analysis of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.","ista":"Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540."},"author":[{"first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"}],"date_updated":"2023-04-25T07:02:43Z","article_processing_charge":"No","oa_version":"Published Version","quality_controlled":"1","abstract":[{"text":"The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.","lang":"eng"}],"file":[{"content_type":"application/pdf","file_size":16096413,"checksum":"120d2c2a38384058ad0630fdf8288312","creator":"dernst","access_level":"open_access","success":1,"date_created":"2023-04-25T06:58:36Z","relation":"main_file","file_id":"12864","file_name":"2023_LNCS_Chalupa.pdf","date_updated":"2023-04-25T06:58:36Z"}],"publication_status":"published","_id":"12854","year":"2023","ec_funded":1,"date_created":"2023-04-20T08:22:53Z","alternative_title":["LNCS"],"intvolume":" 13994","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","language":[{"iso":"eng"}],"date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30820-8_32","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2023-04-25T06:58:36Z","volume":13994,"type":"conference","month":"04","department":[{"_id":"ToHe"}],"publisher":"Springer Nature","acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","conference":{"end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22","location":"Paris, France"},"page":"535-540"},{"day":"20","publication_identifier":{"isbn":["9783031308253"],"eisbn":["9783031308260"],"eissn":["1611-3349"],"issn":["0302-9743"]},"publication":"Fundamental Approaches to Software Engineering","oa":1,"citation":{"mla":"Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in Fundamental Approaches to Software Engineering, Paris, France, 2023, vol. 13991, pp. 260–281.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30826-0_15","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: Fundamental Approaches to Software Engineering. Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15.","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware for best-effort third-party monitoring. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281."},"author":[{"last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek"},{"last_name":"Mühlböck","first_name":"Fabian","full_name":"Mühlböck, Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177"},{"last_name":"Muroya Lei","first_name":"Stefanie","full_name":"Muroya Lei, Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"}],"date_updated":"2023-04-25T07:19:07Z","has_accepted_license":"1","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"title":"Vamos: Middleware for best-effort third-party monitoring","ec_funded":1,"date_created":"2023-04-20T08:29:42Z","year":"2023","_id":"12856","quality_controlled":"1","oa_version":"Published Version","article_processing_charge":"No","publication_status":"published","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"12407"}]},"file":[{"date_updated":"2023-04-25T07:16:36Z","file_name":"2023_LNCS_ChalupaM.pdf","file_id":"12865","date_created":"2023-04-25T07:16:36Z","success":1,"relation":"main_file","access_level":"open_access","creator":"dernst","checksum":"17a7c8e08be609cf2408d37ea55e322c","file_size":580828,"content_type":"application/pdf"}],"abstract":[{"lang":"eng","text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch."}],"file_date_updated":"2023-04-25T07:16:36Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","volume":13991,"alternative_title":["LNCS"],"intvolume":" 13991","ddc":["000"],"doi":"10.1007/978-3-031-30826-0_15","date_published":"2023-04-20T00:00:00Z","language":[{"iso":"eng"}],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","page":"260-281","conference":{"end_date":"2023-04-27","location":"Paris, France","start_date":"2023-04-22","name":"FASE: Fundamental Approaches to Software Engineering"},"department":[{"_id":"ToHe"}],"publisher":"Springer Nature","month":"04"},{"year":"2023","_id":"13139","date_created":"2023-06-18T22:00:46Z","file":[{"date_updated":"2023-06-19T07:18:40Z","file_id":"13148","relation":"main_file","success":1,"date_created":"2023-06-19T07:18:40Z","file_name":"2023_LNCS_Meggendorfer.pdf","access_level":"open_access","creator":"dernst","content_type":"application/pdf","file_size":521951,"checksum":"59f707a3949c03793251b0d04c62542a"}],"abstract":[{"text":"A classical problem for Markov chains is determining their stationary (or steady-state) distribution. This problem has an equally classical solution based on eigenvectors and linear equation systems. However, this approach does not scale to large instances, and iterative solutions are desirable. It turns out that a naive approach, as used by current model checkers, may yield completely wrong results. We present a new approach, which utilizes recent advances in partial exploration and mean payoff computation to obtain a correct, converging approximation.","lang":"eng"}],"related_material":{"record":[{"relation":"research_data","id":"14990","status":"public"}]},"publication_status":"published","oa_version":"Published Version","article_processing_charge":"No","quality_controlled":"1","author":[{"last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"}],"citation":{"mla":"Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.” TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13993, Springer Nature, 2023, pp. 489–507, doi:10.1007/978-3-031-30823-9_25.","ama":"Meggendorfer T. Correct approximation of stationary distributions. In: TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13993. Springer Nature; 2023:489-507. doi:10.1007/978-3-031-30823-9_25","ieee":"T. Meggendorfer, “Correct approximation of stationary distributions,” in TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13993, pp. 489–507.","apa":"Meggendorfer, T. (2023). Correct approximation of stationary distributions. In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13993, pp. 489–507). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_25","chicago":"Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.” In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, 13993:489–507. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_25.","ista":"Meggendorfer T. 2023. Correct approximation of stationary distributions. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 489–507.","short":"T. Meggendorfer, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 489–507."},"date_updated":"2024-02-27T07:19:33Z","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308222"],"issn":["0302-9743"]},"oa":1,"day":"22","external_id":{"arxiv":["2301.08137"]},"title":"Correct approximation of stationary distributions","has_accepted_license":"1","conference":{"location":"Paris, France","start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27"},"page":"489-507","arxiv":1,"scopus_import":"1","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"month":"04","volume":13993,"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2023-06-19T07:18:40Z","language":[{"iso":"eng"}],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"doi":"10.1007/978-3-031-30823-9_25","date_published":"2023-04-22T00:00:00Z","alternative_title":["LNCS"],"ddc":["000"],"intvolume":" 13993"},{"month":"04","publisher":"Springer Nature","department":[{"_id":"ToHe"}],"scopus_import":"1","page":"211-228","conference":{"end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22","location":"Paris, France"},"alternative_title":["LNCS"],"intvolume":" 13994","ddc":["000"],"date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30820-8_15","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"language":[{"iso":"eng"}],"file_date_updated":"2023-06-19T08:43:21Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","volume":13994,"quality_controlled":"1","article_processing_charge":"No","oa_version":"Published Version","publication_status":"published","abstract":[{"lang":"eng","text":"We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω\r\n-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive."}],"file":[{"date_created":"2023-06-19T08:43:21Z","success":1,"relation":"main_file","file_id":"13151","file_name":"2023_LNCS_Anand.pdf","date_updated":"2023-06-19T08:43:21Z","content_type":"application/pdf","file_size":521425,"checksum":"60dcafc1b4f6f070be43bad3fe877974","creator":"dernst","access_level":"open_access"}],"date_created":"2023-06-18T22:00:47Z","_id":"13141","year":"2023","has_accepted_license":"1","title":"Computing adequately permissive assumptions for synthesis","day":"20","oa":1,"publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308192"],"eissn":["1611-3349"]},"author":[{"full_name":"Anand, Ashwani","first_name":"Ashwani","last_name":"Anand"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik"},{"last_name":"Nayak","first_name":"Satya Prakash","full_name":"Nayak, Satya Prakash"},{"full_name":"Schmuck, Anne Kathrin","first_name":"Anne Kathrin","last_name":"Schmuck"}],"date_updated":"2023-06-19T08:49:46Z","citation":{"short":"A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 211–228.","chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15.","ista":"Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 211–228.","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.","ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 211–228.","apa":"Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15"}},{"abstract":[{"text":"Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.","lang":"eng"}],"file":[{"creator":"dernst","access_level":"open_access","checksum":"3d8a8bb24d211bc83360dfc2fd744307","file_size":528455,"content_type":"application/pdf","date_updated":"2023-06-19T08:29:30Z","file_name":"2023_LNCS_Chatterjee.pdf","relation":"main_file","date_created":"2023-06-19T08:29:30Z","success":1,"file_id":"13150"}],"publication_status":"published","article_processing_charge":"No","oa_version":"Published Version","quality_controlled":"1","_id":"13142","year":"2023","ec_funded":1,"date_created":"2023-06-18T22:00:47Z","title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"has_accepted_license":"1","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"}],"date_updated":"2025-07-14T09:09:52Z","citation":{"short":"K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.","ama":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: Tools and Algorithms for the Construction and Analysis of Systems . Vol 13993. Springer Nature; 2023:3-25. doi:10.1007/978-3-031-30823-9_1","ieee":"K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier framework for neural network controllers and certificates of stochastic systems,” in Tools and Algorithms for the Construction and Analysis of Systems , Paris, France, 2023, vol. 13993, pp. 3–25.","apa":"Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_1","mla":"Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” Tools and Algorithms for the Construction and Analysis of Systems , vol. 13993, Springer Nature, 2023, pp. 3–25, doi:10.1007/978-3-031-30823-9_1.","ista":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” In Tools and Algorithms for the Construction and Analysis of Systems , 13993:3–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_1."},"oa":1,"publication":"Tools and Algorithms for the Construction and Analysis of Systems ","publication_identifier":{"isbn":["9783031308222"],"eissn":["1611-3349"],"issn":["0302-9743"]},"day":"22","month":"04","publisher":"Springer Nature","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"conference":{"location":"Paris, France","start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27"},"page":"3-25","scopus_import":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"language":[{"iso":"eng"}],"date_published":"2023-04-22T00:00:00Z","doi":"10.1007/978-3-031-30823-9_1","alternative_title":["LNCS"],"intvolume":" 13993","ddc":["000"],"volume":13993,"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2023-06-19T08:29:30Z"},{"title":"Certifying giant nonprimes","day":"02","oa":1,"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031313677"],"issn":["0302-9743"]},"publication":"Public-Key Cryptography - PKC 2023","author":[{"id":"0f78d746-dc7d-11ea-9b2f-83f92091afe7","full_name":"Hoffmann, Charlotte","last_name":"Hoffmann","first_name":"Charlotte"},{"full_name":"Hubáček, Pavel","first_name":"Pavel","last_name":"Hubáček"},{"first_name":"Chethan","last_name":"Kamath","full_name":"Kamath, Chethan"},{"orcid":"0000-0002-9139-1654","full_name":"Pietrzak, Krzysztof Z","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z","last_name":"Pietrzak"}],"date_updated":"2023-06-19T08:03:37Z","citation":{"short":"C. Hoffmann, P. Hubáček, C. Kamath, K.Z. Pietrzak, in:, Public-Key Cryptography - PKC 2023, Springer Nature, 2023, pp. 530–553.","chicago":"Hoffmann, Charlotte, Pavel Hubáček, Chethan Kamath, and Krzysztof Z Pietrzak. “Certifying Giant Nonprimes.” In Public-Key Cryptography - PKC 2023, 13940:530–53. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-31368-4_19.","ista":"Hoffmann C, Hubáček P, Kamath C, Pietrzak KZ. 2023. Certifying giant nonprimes. Public-Key Cryptography - PKC 2023. PKC: Public-Key Cryptography, LNCS, vol. 13940, 530–553.","mla":"Hoffmann, Charlotte, et al. “Certifying Giant Nonprimes.” Public-Key Cryptography - PKC 2023, vol. 13940, Springer Nature, 2023, pp. 530–53, doi:10.1007/978-3-031-31368-4_19.","apa":"Hoffmann, C., Hubáček, P., Kamath, C., & Pietrzak, K. Z. (2023). Certifying giant nonprimes. In Public-Key Cryptography - PKC 2023 (Vol. 13940, pp. 530–553). Atlanta, GA, United States: Springer Nature. https://doi.org/10.1007/978-3-031-31368-4_19","ama":"Hoffmann C, Hubáček P, Kamath C, Pietrzak KZ. Certifying giant nonprimes. In: Public-Key Cryptography - PKC 2023. Vol 13940. Springer Nature; 2023:530-553. doi:10.1007/978-3-031-31368-4_19","ieee":"C. Hoffmann, P. Hubáček, C. Kamath, and K. Z. Pietrzak, “Certifying giant nonprimes,” in Public-Key Cryptography - PKC 2023, Atlanta, GA, United States, 2023, vol. 13940, pp. 530–553."},"quality_controlled":"1","article_processing_charge":"No","oa_version":"Submitted Version","publication_status":"published","abstract":[{"text":"GIMPS and PrimeGrid are large-scale distributed projects dedicated to searching giant prime numbers, usually of special forms like Mersenne and Proth primes. The numbers in the current search-space are millions of digits large and the participating volunteers need to run resource-consuming primality tests. Once a candidate prime N has been found, the only way for another party to independently verify the primality of N used to be by repeating the expensive primality test. To avoid the need for second recomputation of each primality test, these projects have recently adopted certifying mechanisms that enable efficient verification of performed tests. However, the mechanisms presently in place only detect benign errors and there is no guarantee against adversarial behavior: a malicious volunteer can mislead the project to reject a giant prime as being non-prime.\r\nIn this paper, we propose a practical, cryptographically-sound mechanism for certifying the non-primality of Proth numbers. That is, a volunteer can – parallel to running the primality test for N – generate an efficiently verifiable proof at a little extra cost certifying that N is not prime. The interactive protocol has statistical soundness and can be made non-interactive using the Fiat-Shamir heuristic.\r\nOur approach is based on a cryptographic primitive called Proof of Exponentiation (PoE) which, for a group G, certifies that a tuple (x,y,T)∈G2×N satisfies x2T=y (Pietrzak, ITCS 2019 and Wesolowski, J. Cryptol. 2020). In particular, we show how to adapt Pietrzak’s PoE at a moderate additional cost to make it a cryptographically-sound certificate of non-primality.","lang":"eng"}],"date_created":"2023-06-18T22:00:47Z","_id":"13143","year":"2023","intvolume":" 13940","alternative_title":["LNCS"],"date_published":"2023-05-02T00:00:00Z","doi":"10.1007/978-3-031-31368-4_19","status":"public","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","volume":13940,"main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2023/238"}],"month":"05","department":[{"_id":"KrPi"}],"publisher":"Springer Nature","acknowledgement":"We are grateful to Pavel Atnashev for clarifying via e-mail several aspects of the primality tests implementated in the PrimeGrid project. Pavel Hubáček is supported by the Czech Academy of Sciences (RVO 67985840), the Grant Agency of the Czech Republic under the grant agreement no. 19-27871X, and by the Charles University project UNCE/SCI/004. Chethan Kamath is supported by Azrieli International Postdoctoral Fellowship, ISF grants 484/18 and 1789/19, and ERC StG project SPP: Secrecy Preserving Proofs.","scopus_import":"1","page":"530-553","conference":{"location":"Atlanta, GA, United States","name":"PKC: Public-Key Cryptography","start_date":"2023-05-07","end_date":"2023-05-10"}},{"day":"22","publication":"International Conference on Integer Programming and Combinatorial Optimization","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031327254"]},"oa":1,"date_updated":"2023-07-18T07:08:51Z","author":[{"full_name":"Zheng, Da Wei","first_name":"Da Wei","last_name":"Zheng"},{"last_name":"Henzinger","first_name":"Monika H","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"}],"citation":{"chicago":"Zheng, Da Wei, and Monika H Henzinger. “Multiplicative Auction Algorithm for Approximate Maximum Weight Bipartite Matching.” In International Conference on Integer Programming and Combinatorial Optimization, 13904:453–65. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-32726-1_32.","ista":"Zheng DW, Henzinger MH. 2023. Multiplicative auction algorithm for approximate maximum weight bipartite matching. International Conference on Integer Programming and Combinatorial Optimization. IPCO: Integer Programming and Combinatorial Optimization, LNCS, vol. 13904, 453–465.","mla":"Zheng, Da Wei, and Monika H. Henzinger. “Multiplicative Auction Algorithm for Approximate Maximum Weight Bipartite Matching.” International Conference on Integer Programming and Combinatorial Optimization, vol. 13904, Springer Nature, 2023, pp. 453–65, doi:10.1007/978-3-031-32726-1_32.","apa":"Zheng, D. W., & Henzinger, M. H. (2023). Multiplicative auction algorithm for approximate maximum weight bipartite matching. In International Conference on Integer Programming and Combinatorial Optimization (Vol. 13904, pp. 453–465). Madison, WI, United States: Springer Nature. https://doi.org/10.1007/978-3-031-32726-1_32","ieee":"D. W. Zheng and M. H. Henzinger, “Multiplicative auction algorithm for approximate maximum weight bipartite matching,” in International Conference on Integer Programming and Combinatorial Optimization, Madison, WI, United States, 2023, vol. 13904, pp. 453–465.","ama":"Zheng DW, Henzinger MH. Multiplicative auction algorithm for approximate maximum weight bipartite matching. In: International Conference on Integer Programming and Combinatorial Optimization. Vol 13904. Springer Nature; 2023:453-465. doi:10.1007/978-3-031-32726-1_32","short":"D.W. Zheng, M.H. Henzinger, in:, International Conference on Integer Programming and Combinatorial Optimization, Springer Nature, 2023, pp. 453–465."},"project":[{"call_identifier":"H2020","_id":"bd9ca328-d553-11ed-ba76-dc4f890cfe62","grant_number":"101019564","name":"The design and evaluation of modern fully dynamic data structures"},{"name":"Fast Algorithms for a Reactive Network Layer","grant_number":"P33775 ","_id":"bd9e3a2e-d553-11ed-ba76-8aa684ce17fe"}],"external_id":{"arxiv":["2301.09217"]},"title":"Multiplicative auction algorithm for approximate maximum weight bipartite matching","date_created":"2023-07-16T22:01:11Z","ec_funded":1,"year":"2023","_id":"13236","quality_controlled":"1","oa_version":"Preprint","article_processing_charge":"No","publication_status":"published","abstract":[{"text":"We present an auction algorithm using multiplicative instead of constant weight updates to compute a (1−ε)-approximate maximum weight matching (MWM) in a bipartite graph with n vertices and m edges in time O(mε−1log(ε−1)), matching the running time of the linear-time approximation algorithm of Duan and Pettie [JACM ’14]. Our algorithm is very simple and it can be extended to give a dynamic data structure that maintains a (1−ε)-approximate maximum weight matching under (1) one-sided vertex deletions (with incident edges) and (2) one-sided vertex insertions (with incident edges sorted by weight) to the other side. The total time time used is O(mε−1log(ε−1)), where m is the sum of the number of initially existing and inserted edges.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","volume":13904,"alternative_title":["LNCS"],"intvolume":" 13904","doi":"10.1007/978-3-031-32726-1_32","date_published":"2023-05-22T00:00:00Z","language":[{"iso":"eng"}],"status":"public","acknowledgement":"The first author thanks to Chandra Chekuri for useful discussions about this paper. This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 101019564 “The Design of Modern Fully Dynamic Data Structures (MoDynStruct)” and from the Austrian Science Fund (FWF) project “Fast Algorithms for a Reactive Network Layer (ReactNet)”, P 33775-N, with additional funding from the netidee SCIENCE Stiftung, 2020–2024.","scopus_import":"1","arxiv":1,"conference":{"end_date":"2023-06-23","start_date":"2023-06-21","name":"IPCO: Integer Programming and Combinatorial Optimization","location":"Madison, WI, United States"},"page":"453-465","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2301.09217","open_access":"1"}],"department":[{"_id":"MoHe"}],"publisher":"Springer Nature","month":"05"},{"arxiv":1,"conference":{"end_date":"2023-06-09","location":"Alcala de Henares, Spain","name":"SIROCCO: Structural Information and Communication Complexity","start_date":"2023-06-06"},"page":"576-594","acknowledgement":"We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful discussions about different variants of the problem. This work is supported by the European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025, the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant 470029389 (FlexNets), 2021–2024.","scopus_import":"1","department":[{"_id":"KrPi"},{"_id":"KrCh"}],"publisher":"Springer Nature","month":"05","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2204.13459"}],"type":"conference","volume":13892,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-031-32733-9_26","date_published":"2023-05-25T00:00:00Z","language":[{"iso":"eng"}],"status":"public","intvolume":" 13892","alternative_title":["LNCS"],"date_created":"2023-07-16T22:01:12Z","ec_funded":1,"year":"2023","_id":"13238","publication_status":"published","related_material":{"record":[{"status":"public","id":"14506","relation":"dissertation_contains"}]},"abstract":[{"lang":"eng","text":"We consider a natural problem dealing with weighted packet selection across a rechargeable link, which e.g., finds applications in cryptocurrency networks. The capacity of a link (u, v) is determined by how much nodes u and v allocate for this link. Specifically, the input is a finite ordered sequence of packets that arrive in both directions along a link. Given (u, v) and a packet of weight x going from u to v, node u can either accept or reject the packet. If u accepts the packet, the capacity on link (u, v) decreases by x. Correspondingly, v’s capacity on (u, v) increases by x. If a node rejects the packet, this will entail a cost affinely linear in the weight of the packet. A link is “rechargeable” in the sense that the total capacity of the link has to remain constant, but the allocation of capacity at the ends of the link can depend arbitrarily on the nodes’ decisions. The goal is to minimise the sum of the capacity injected into the link and the cost of rejecting packets. We show that the problem is NP-hard, but can be approximated efficiently with a ratio of (1+ε)⋅(1+3–√) for some arbitrary ε>0.\r\n."}],"quality_controlled":"1","oa_version":"Preprint","article_processing_charge":"No","author":[{"full_name":"Schmid, Stefan","last_name":"Schmid","first_name":"Stefan"},{"last_name":"Svoboda","first_name":"Jakub","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267"},{"first_name":"Michelle X","last_name":"Yeo","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","full_name":"Yeo, Michelle X","orcid":"0009-0001-3676-4809"}],"date_updated":"2025-07-14T09:09:53Z","citation":{"ieee":"S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation,” in SIROCCO 2023: Structural Information and Communication Complexity , Alcala de Henares, Spain, 2023, vol. 13892, pp. 576–594.","ama":"Schmid S, Svoboda J, Yeo MX. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In: SIROCCO 2023: Structural Information and Communication Complexity . Vol 13892. Springer Nature; 2023:576-594. doi:10.1007/978-3-031-32733-9_26","apa":"Schmid, S., Svoboda, J., & Yeo, M. X. (2023). Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In SIROCCO 2023: Structural Information and Communication Complexity (Vol. 13892, pp. 576–594). Alcala de Henares, Spain: Springer Nature. https://doi.org/10.1007/978-3-031-32733-9_26","mla":"Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” SIROCCO 2023: Structural Information and Communication Complexity , vol. 13892, Springer Nature, 2023, pp. 576–94, doi:10.1007/978-3-031-32733-9_26.","ista":"Schmid S, Svoboda J, Yeo MX. 2023. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. SIROCCO 2023: Structural Information and Communication Complexity . SIROCCO: Structural Information and Communication Complexity, LNCS, vol. 13892, 576–594.","chicago":"Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” In SIROCCO 2023: Structural Information and Communication Complexity , 13892:576–94. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-32733-9_26.","short":"S. Schmid, J. Svoboda, M.X. Yeo, in:, SIROCCO 2023: Structural Information and Communication Complexity , Springer Nature, 2023, pp. 576–594."},"day":"25","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031327322"]},"publication":"SIROCCO 2023: Structural Information and Communication Complexity ","oa":1,"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"}],"title":"Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation","external_id":{"arxiv":["2204.13459"]}},{"arxiv":1,"conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","location":"Paris, France","end_date":"2023-07-22"},"page":"358–382","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG101020093.","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"Springer Nature","month":"07","type":"conference","volume":13965,"file_date_updated":"2023-07-31T08:11:20Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","doi":"10.1007/978-3-031-37703-7_17","date_published":"2023-07-18T00:00:00Z","language":[{"iso":"eng"}],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"alternative_title":["LNCS"],"intvolume":" 13965","ddc":["000"],"ec_funded":1,"date_created":"2023-07-25T18:32:40Z","year":"2023","_id":"13310","publication_status":"published","file":[{"date_updated":"2023-07-31T08:11:20Z","file_name":"2023_LNCS_CAV_HenzingerT.pdf","relation":"main_file","date_created":"2023-07-31T08:11:20Z","success":1,"file_id":"13327","creator":"dernst","access_level":"open_access","checksum":"ccaf94bf7d658ba012c016e11869b54c","content_type":"application/pdf","file_size":647760}],"abstract":[{"lang":"eng","text":"Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian monitors compute estimates that are correct subject to a given prior belief about the system’s model. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation."}],"quality_controlled":"1","oa_version":"Published Version","article_processing_charge":"Yes (in subscription journal)","citation":{"short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification, Springer Nature, 2023, pp. 358–382.","ista":"Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13965, 358–382.","chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness.” In Computer Aided Verification, 13965:358–382. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37703-7_17.","apa":"Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic fairness. In Computer Aided Verification (Vol. 13965, pp. 358–382). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37703-7_17","ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness,” in Computer Aided Verification, Paris, France, 2023, vol. 13965, pp. 358–382.","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness. In: Computer Aided Verification. Vol 13965. Springer Nature; 2023:358–382. doi:10.1007/978-3-031-37703-7_17","mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” Computer Aided Verification, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:10.1007/978-3-031-37703-7_17."},"date_updated":"2023-09-05T15:14:00Z","author":[{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Karimi","first_name":"Mahyar","orcid":"0009-0005-0820-1696","id":"f1dedef5-2f78-11ee-989a-c4c97bccf506","full_name":"Karimi, Mahyar"},{"first_name":"Konstantin","last_name":"Kueffner","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"},{"first_name":"Kaushik","last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475"}],"day":"18","publication_identifier":{"isbn":["9783031377020"],"eissn":["1611-3349"],"eisbn":["9783031377037"],"issn":["0302-9743"]},"publication":"Computer Aided Verification","oa":1,"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"title":"Monitoring algorithmic fairness","external_id":{"arxiv":["2305.15979"]},"has_accepted_license":"1"},{"quality_controlled":"1","article_processing_charge":"Yes (in subscription journal)","oa_version":"Published Version","publication_status":"published","abstract":[{"text":"We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.","lang":"eng"}],"file":[{"date_updated":"2023-09-06T08:25:50Z","file_name":"2023_LNCS_CAV_Kretinsky.pdf","file_id":"14276","success":1,"date_created":"2023-09-06T08:25:50Z","relation":"main_file","access_level":"open_access","creator":"dernst","checksum":"ed66278b61bb869e1baba3d9b9081271","content_type":"application/pdf","file_size":428354}],"date_created":"2023-09-03T22:01:16Z","_id":"14259","year":"2023","has_accepted_license":"1","title":"Guessing winning policies in LTL synthesis by semantic learning","day":"17","oa":1,"publication":"35th International Conference on Computer Aided Verification ","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031377051"],"eissn":["1611-3349"]},"date_updated":"2023-09-06T08:27:33Z","citation":{"short":"J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.","ista":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies in LTL synthesis by semantic learning. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In 35th International Conference on Computer Aided Verification , 13964:390–414. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_20.","ama":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies in LTL synthesis by semantic learning. In: 35th International Conference on Computer Aided Verification . Vol 13964. Springer Nature; 2023:390-414. doi:10.1007/978-3-031-37706-8_20","ieee":"J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning policies in LTL synthesis by semantic learning,” in 35th International Conference on Computer Aided Verification , Paris, France, 2023, vol. 13964, pp. 390–414.","apa":"Kretinsky, J., Meggendorfer, T., Prokop, M., & Rieder, S. (2023). Guessing winning policies in LTL synthesis by semantic learning. In 35th International Conference on Computer Aided Verification (Vol. 13964, pp. 390–414). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_20","mla":"Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” 35th International Conference on Computer Aided Verification , vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20."},"author":[{"orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"},{"first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"},{"first_name":"Maximilian","last_name":"Prokop","full_name":"Prokop, Maximilian"},{"full_name":"Rieder, Sabine","last_name":"Rieder","first_name":"Sabine"}],"month":"07","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).","scopus_import":"1","conference":{"start_date":"2023-07-17","location":"Paris, France","name":"CAV: Computer Aided Verification","end_date":"2023-07-22"},"page":"390-414","ddc":["000"],"alternative_title":["LNCS"],"intvolume":" 13964","date_published":"2023-07-17T00:00:00Z","doi":"10.1007/978-3-031-37706-8_20","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","language":[{"iso":"eng"}],"file_date_updated":"2023-09-06T08:25:50Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","volume":13964},{"doi":"10.1007/978-3-031-37706-8_8","date_published":"2023-07-17T00:00:00Z","language":[{"iso":"eng"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","intvolume":" 13964","alternative_title":["LNCS"],"ddc":["000"],"type":"conference","volume":13964,"file_date_updated":"2023-09-06T08:16:25Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","department":[{"_id":"DaAl"},{"_id":"GradSch"}],"month":"07","conference":{"name":"CAV: Computer Aided Verification","location":"Paris, France","start_date":"2023-07-17","end_date":"2023-07-22"},"page":"156-169","scopus_import":"1","title":"Lincheck: A practical framework for testing concurrent data structures on JVM","has_accepted_license":"1","date_updated":"2024-02-27T07:46:52Z","citation":{"short":"N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, D.-A. Alistarh, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 156–169.","ista":"Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. 2023. Lincheck: A practical framework for testing concurrent data structures on JVM. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 156–169.","chicago":"Koval, Nikita, Alexander Fedorov, Maria Sokolova, Dmitry Tsitelov, and Dan-Adrian Alistarh. “Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM.” In 35th International Conference on Computer Aided Verification , 13964:156–69. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_8.","apa":"Koval, N., Fedorov, A., Sokolova, M., Tsitelov, D., & Alistarh, D.-A. (2023). Lincheck: A practical framework for testing concurrent data structures on JVM. In 35th International Conference on Computer Aided Verification (Vol. 13964, pp. 156–169). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_8","ieee":"N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, and D.-A. Alistarh, “Lincheck: A practical framework for testing concurrent data structures on JVM,” in 35th International Conference on Computer Aided Verification , Paris, France, 2023, vol. 13964, pp. 156–169.","ama":"Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. Lincheck: A practical framework for testing concurrent data structures on JVM. In: 35th International Conference on Computer Aided Verification . Vol 13964. Springer Nature; 2023:156-169. doi:10.1007/978-3-031-37706-8_8","mla":"Koval, Nikita, et al. “Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM.” 35th International Conference on Computer Aided Verification , vol. 13964, Springer Nature, 2023, pp. 156–69, doi:10.1007/978-3-031-37706-8_8."},"author":[{"last_name":"Koval","first_name":"Nikita","full_name":"Koval, Nikita","id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87"},{"id":"2e711909-896a-11ed-bdf8-eb0f5a2984c6","full_name":"Fedorov, Alexander","last_name":"Fedorov","first_name":"Alexander"},{"full_name":"Sokolova, Maria","last_name":"Sokolova","first_name":"Maria"},{"full_name":"Tsitelov, Dmitry","last_name":"Tsitelov","first_name":"Dmitry"},{"first_name":"Dan-Adrian","last_name":"Alistarh","orcid":"0000-0003-3650-940X","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","full_name":"Alistarh, Dan-Adrian"}],"day":"17","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031377051"],"eissn":["1611-3349"]},"publication":"35th International Conference on Computer Aided Verification ","oa":1,"publication_status":"published","related_material":{"record":[{"relation":"research_data","id":"14995","status":"public"}]},"file":[{"date_updated":"2023-09-06T08:16:25Z","file_name":"2023_LNCS_Koval.pdf","file_id":"14275","date_created":"2023-09-06T08:16:25Z","relation":"main_file","success":1,"access_level":"open_access","creator":"dernst","checksum":"c346016393123a0a2338ad4d976f61bc","file_size":421408,"content_type":"application/pdf"}],"abstract":[{"lang":"eng","text":"This paper presents Lincheck, a new practical and user-friendly framework for testing concurrent algorithms on the Java Virtual Machine (JVM). Lincheck provides a simple and declarative way to write concurrent tests: instead of describing how to perform the test, users specify what to test by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with Lincheck are concise and easy to understand. The framework automatically generates a set of concurrent scenarios, examines them using stress-testing or bounded model checking, and verifies that the results of each invocation are correct. Notably, if an error is detected via model checking, Lincheck provides an easy-to-follow trace to reproduce it, significantly simplifying the bug investigation.\r\n\r\nTo the best of our knowledge, Lincheck is the first production-ready tool on the JVM that offers such a simple way of writing concurrent tests, without requiring special skills or expertise. We successfully integrated Lincheck in the development process of several large projects, such as Kotlin Coroutines, and identified new bugs in popular concurrency libraries, such as a race in Java’s standard ConcurrentLinkedDeque and a liveliness bug in Java’s AbstractQueuedSynchronizer framework, which is used in most of the synchronization primitives. We believe that Lincheck can significantly improve the quality and productivity of concurrent algorithms research and development and become the state-of-the-art tool for checking their correctness."}],"quality_controlled":"1","oa_version":"Published Version","article_processing_charge":"Yes (in subscription journal)","date_created":"2023-09-03T22:01:16Z","year":"2023","_id":"14260"},{"abstract":[{"text":"Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.\r\nIn light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples.","lang":"eng"}],"file":[{"file_id":"14349","date_created":"2023-09-20T08:46:43Z","success":1,"relation":"main_file","file_name":"2023_LNCS_Akshay.pdf","date_updated":"2023-09-20T08:46:43Z","content_type":"application/pdf","file_size":531745,"checksum":"f143c8eedf609f20f2aad2eeb496d53f","access_level":"open_access","creator":"dernst"}],"publication_status":"published","article_processing_charge":"Yes (in subscription journal)","oa_version":"Published Version","quality_controlled":"1","_id":"14317","year":"2023","ec_funded":1,"date_created":"2023-09-10T22:01:12Z","title":"MDPs as distribution transformers: Affine invariant synthesis for safety objectives","project":[{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"has_accepted_license":"1","date_updated":"2025-07-14T09:09:56Z","author":[{"first_name":"S.","last_name":"Akshay","full_name":"Akshay, S."},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","first_name":"Tobias"},{"first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"citation":{"chicago":"Akshay, S., Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” In International Conference on Computer Aided Verification, 13966:86–112. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_5.","ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 86–112.","mla":"Akshay, S., et al. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” International Conference on Computer Aided Verification, vol. 13966, Springer Nature, 2023, pp. 86–112, doi:10.1007/978-3-031-37709-9_5.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In: International Conference on Computer Aided Verification. Vol 13966. Springer Nature; 2023:86-112. doi:10.1007/978-3-031-37709-9_5","apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., & Zikelic, D. (2023). MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In International Conference on Computer Aided Verification (Vol. 13966, pp. 86–112). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_5","ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “MDPs as distribution transformers: Affine invariant synthesis for safety objectives,” in International Conference on Computer Aided Verification, Paris, France, 2023, vol. 13966, pp. 86–112.","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112."},"oa":1,"publication":"International Conference on Computer Aided Verification","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031377082"],"eissn":["1611-3349"]},"day":"17","month":"07","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"page":"86-112","conference":{"end_date":"2023-07-22","start_date":"2023-07-17","location":"Paris, France","name":"CAV: Computer Aided Verification"},"scopus_import":"1","acknowledgement":"This work was supported in part by the ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385 as well as DST/CEFIPRA/INRIA project EQuaVE and SERB Matrices grant MTR/2018/00074.","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","language":[{"iso":"eng"}],"date_published":"2023-07-17T00:00:00Z","doi":"10.1007/978-3-031-37709-9_5","intvolume":" 13966","alternative_title":["LNCS"],"ddc":["000"],"volume":13966,"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2023-09-20T08:46:43Z"},{"volume":13966,"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2023-09-20T08:24:47Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","language":[{"iso":"eng"}],"date_published":"2023-07-17T00:00:00Z","doi":"10.1007/978-3-031-37709-9_2","ddc":["000"],"alternative_title":["LNCS"],"intvolume":" 13966","conference":{"end_date":"2023-07-22","start_date":"2023-07-17","name":"CAV: Computer Aided Verification","location":"Paris, France"},"page":"16-39","scopus_import":"1","acknowledgement":"We thank Prof. Bican Xia for valuable information on the exponential theory of reals. The work is partially supported by the National Natural Science Foundation of China (NSFC) with Grant No. 62172271, ERC CoG 863818 (ForM-SMArt), the Hong Kong Research Grants Council ECS Project Number 26208122, the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055 and the HKUST Startup Grant R9272.","month":"07","department":[{"_id":"KrCh"}],"publisher":"Springer Nature","date_updated":"2025-07-14T09:09:57Z","citation":{"apa":"Sun, Y., Fu, H., Chatterjee, K., & Goharshady, A. K. (2023). Automated tail bound analysis for probabilistic recurrence relations. In Computer Aided Verification (Vol. 13966, pp. 16–39). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_2","ama":"Sun Y, Fu H, Chatterjee K, Goharshady AK. Automated tail bound analysis for probabilistic recurrence relations. In: Computer Aided Verification. Vol 13966. Springer Nature; 2023:16-39. doi:10.1007/978-3-031-37709-9_2","ieee":"Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Automated tail bound analysis for probabilistic recurrence relations,” in Computer Aided Verification, Paris, France, 2023, vol. 13966, pp. 16–39.","mla":"Sun, Yican, et al. “Automated Tail Bound Analysis for Probabilistic Recurrence Relations.” Computer Aided Verification, vol. 13966, Springer Nature, 2023, pp. 16–39, doi:10.1007/978-3-031-37709-9_2.","ista":"Sun Y, Fu H, Chatterjee K, Goharshady AK. 2023. Automated tail bound analysis for probabilistic recurrence relations. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 16–39.","chicago":"Sun, Yican, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Automated Tail Bound Analysis for Probabilistic Recurrence Relations.” In Computer Aided Verification, 13966:16–39. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_2.","short":"Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Computer Aided Verification, Springer Nature, 2023, pp. 16–39."},"author":[{"full_name":"Sun, Yican","first_name":"Yican","last_name":"Sun"},{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584"}],"oa":1,"publication":"Computer Aided Verification","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031377082"],"eissn":["1611-3349"]},"day":"17","title":"Automated tail bound analysis for probabilistic recurrence relations","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"}],"has_accepted_license":"1","_id":"14318","year":"2023","date_created":"2023-09-10T22:01:12Z","ec_funded":1,"abstract":[{"text":"Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit κ, we consider the tail probability Pr[T≥κ], i.e., the probability that the randomized runtime T of the PRR exceeds κ. Our focus is the formal analysis of tail bounds that aims at finding a tight asymptotic upper bound u≥Pr[T≥κ]. To address this problem, the classical and most well-known approach is the cookbook method by Karp (JACM 1994), while other approaches are mostly limited to deriving tail bounds of specific PRRs via involved custom analysis.\r\nIn this work, we propose a novel approach for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing time and random passed sizes observe discrete or (piecewise) uniform distribution and whose recursive call is either a single procedure call or a divide-and-conquer. We first establish a theoretical approach via Markov’s inequality, and then instantiate the theoretical approach with a template-based algorithmic approach via a refined treatment of exponentiation. Experimental evaluation shows that our algorithmic approach is capable of deriving tail bounds that are (i) asymptotically tighter than Karp’s method, (ii) match the best-known manually-derived asymptotic tail bound for QuickSelect, and (iii) is only slightly worse (with a loglogn factor) than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover, our algorithmic approach handles all examples (including realistic PRRs such as QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 s, showing that our approach is efficient in practice.","lang":"eng"}],"file":[{"date_updated":"2023-09-20T08:24:47Z","file_name":"2023_LNCS_Sun.pdf","relation":"main_file","success":1,"date_created":"2023-09-20T08:24:47Z","file_id":"14348","creator":"dernst","access_level":"open_access","checksum":"42917e086f8c7699f3bccf84f74fe000","file_size":624647,"content_type":"application/pdf"}],"publication_status":"published","related_material":{"link":[{"relation":"software","url":"https://github.com/boyvolcano/PRR"}]},"article_processing_charge":"Yes (in subscription journal)","oa_version":"Published Version","quality_controlled":"1"},{"date_created":"2023-10-08T22:01:18Z","year":"2023","scopus_import":"1","_id":"14410","conference":{"name":"RRPR: Reproducible Research in Pattern Recognition","start_date":"2022-08-21","location":"Montreal, Canada","end_date":"2022-08-21"},"page":"67-73","quality_controlled":"1","oa_version":"None","article_processing_charge":"No","department":[{"_id":"ChLa"}],"publisher":"Springer Nature","publication_status":"published","month":"08","abstract":[{"text":"This paper focuses on the implementation details of the baseline methods and a recent lightweight conditional model extrapolation algorithm LIMES [5] for streaming data under class-prior shift. LIMES achieves superior performance over the baseline methods, especially concerning the minimum-across-day accuracy, which is important for the users of the system. In this work, the key measures to facilitate reproducibility and enhance the credibility of the results are described.","lang":"eng"}],"day":"20","publication":"International Workshop on Reproducible Research in Pattern Recognition","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031407727"],"issn":["0302-9743"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","date_updated":"2023-10-09T06:48:02Z","citation":{"short":"P. Tomaszewska, C. Lampert, in:, International Workshop on Reproducible Research in Pattern Recognition, Springer Nature, 2023, pp. 67–73.","ieee":"P. Tomaszewska and C. Lampert, “On the implementation of baselines and lightweight conditional model extrapolation (LIMES) under class-prior shift,” in International Workshop on Reproducible Research in Pattern Recognition, Montreal, Canada, 2023, vol. 14068, pp. 67–73.","apa":"Tomaszewska, P., & Lampert, C. (2023). On the implementation of baselines and lightweight conditional model extrapolation (LIMES) under class-prior shift. In International Workshop on Reproducible Research in Pattern Recognition (Vol. 14068, pp. 67–73). Montreal, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-40773-4_6","ama":"Tomaszewska P, Lampert C. On the implementation of baselines and lightweight conditional model extrapolation (LIMES) under class-prior shift. In: International Workshop on Reproducible Research in Pattern Recognition. Vol 14068. Springer Nature; 2023:67-73. doi:10.1007/978-3-031-40773-4_6","mla":"Tomaszewska, Paulina, and Christoph Lampert. “On the Implementation of Baselines and Lightweight Conditional Model Extrapolation (LIMES) under Class-Prior Shift.” International Workshop on Reproducible Research in Pattern Recognition, vol. 14068, Springer Nature, 2023, pp. 67–73, doi:10.1007/978-3-031-40773-4_6.","ista":"Tomaszewska P, Lampert C. 2023. On the implementation of baselines and lightweight conditional model extrapolation (LIMES) under class-prior shift. International Workshop on Reproducible Research in Pattern Recognition. RRPR: Reproducible Research in Pattern Recognition, LNCS, vol. 14068, 67–73.","chicago":"Tomaszewska, Paulina, and Christoph Lampert. “On the Implementation of Baselines and Lightweight Conditional Model Extrapolation (LIMES) under Class-Prior Shift.” In International Workshop on Reproducible Research in Pattern Recognition, 14068:67–73. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-40773-4_6."},"author":[{"full_name":"Tomaszewska, Paulina","last_name":"Tomaszewska","first_name":"Paulina"},{"first_name":"Christoph","last_name":"Lampert","full_name":"Lampert, Christoph","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8622-7887"}],"volume":14068,"intvolume":" 14068","alternative_title":["LNCS"],"doi":"10.1007/978-3-031-40773-4_6","date_published":"2023-08-20T00:00:00Z","language":[{"iso":"eng"}],"title":"On the implementation of baselines and lightweight conditional model extrapolation (LIMES) under class-prior shift","status":"public"},{"publisher":"Springer Nature","department":[{"_id":"ToHe"}],"month":"09","conference":{"start_date":"2023-09-13","location":"Luxembourg City, Luxembourg","name":"CMSB: Computational Methods in Systems Biology","end_date":"2023-09-15"},"page":"18-35","acknowledgement":"This work was supported by the Czech Foundation grant No. GA22-10845S, Grant Agency of Masaryk University grant No. MUNI/G/1771/2020, and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413.","scopus_import":"1","doi":"10.1007/978-3-031-42697-1_2","date_published":"2023-09-09T00:00:00Z","language":[{"iso":"eng"}],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"intvolume":" 14137","alternative_title":["LNBI"],"ddc":["000"],"type":"conference","volume":14137,"file_date_updated":"2024-02-16T08:26:32Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","file":[{"access_level":"open_access","creator":"spastva","content_type":"application/pdf","file_size":691582,"checksum":"6f71bdaedb770b52380222fd9f4d7937","date_updated":"2024-02-16T08:26:32Z","file_id":"14997","success":1,"relation":"main_file","date_created":"2024-02-16T08:26:32Z","file_name":"cmsb2023.pdf"}],"abstract":[{"lang":"eng","text":"Partially specified Boolean networks (PSBNs) represent a promising framework for the qualitative modelling of biological systems in which the logic of interactions is not completely known. Phenotype control aims to stabilise the network in states exhibiting specific traits.\r\nIn this paper, we define the phenotype control problem in the context of asynchronous PSBNs and propose a novel semi-symbolic algorithm for solving this problem with permanent variable perturbations."}],"quality_controlled":"1","oa_version":"Submitted Version","article_processing_charge":"No","ec_funded":1,"date_created":"2023-10-08T22:01:18Z","year":"2023","_id":"14411","project":[{"name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"}],"title":"Phenotype control of partially specified boolean networks","has_accepted_license":"1","date_updated":"2024-02-20T09:02:04Z","author":[{"full_name":"Beneš, Nikola","last_name":"Beneš","first_name":"Nikola"},{"first_name":"Luboš","last_name":"Brim","full_name":"Brim, Luboš"},{"orcid":"0000-0003-1993-0331","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","full_name":"Pastva, Samuel","first_name":"Samuel","last_name":"Pastva"},{"last_name":"Šafránek","first_name":"David","full_name":"Šafránek, David"},{"full_name":"Šmijáková, Eva","first_name":"Eva","last_name":"Šmijáková"}],"citation":{"ista":"Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. 2023. Phenotype control of partially specified boolean networks. 21st International Conference on Computational Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNBI, vol. 14137, 18–35.","chicago":"Beneš, Nikola, Luboš Brim, Samuel Pastva, David Šafránek, and Eva Šmijáková. “Phenotype Control of Partially Specified Boolean Networks.” In 21st International Conference on Computational Methods in Systems Biology, 14137:18–35. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-42697-1_2.","apa":"Beneš, N., Brim, L., Pastva, S., Šafránek, D., & Šmijáková, E. (2023). Phenotype control of partially specified boolean networks. In 21st International Conference on Computational Methods in Systems Biology (Vol. 14137, pp. 18–35). Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-42697-1_2","ieee":"N. Beneš, L. Brim, S. Pastva, D. Šafránek, and E. Šmijáková, “Phenotype control of partially specified boolean networks,” in 21st International Conference on Computational Methods in Systems Biology, Luxembourg City, Luxembourg, 2023, vol. 14137, pp. 18–35.","ama":"Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially specified boolean networks. In: 21st International Conference on Computational Methods in Systems Biology. Vol 14137. Springer Nature; 2023:18-35. doi:10.1007/978-3-031-42697-1_2","mla":"Beneš, Nikola, et al. “Phenotype Control of Partially Specified Boolean Networks.” 21st International Conference on Computational Methods in Systems Biology, vol. 14137, Springer Nature, 2023, pp. 18–35, doi:10.1007/978-3-031-42697-1_2.","short":"N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková, in:, 21st International Conference on Computational Methods in Systems Biology, Springer Nature, 2023, pp. 18–35."},"day":"09","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031426964"],"eissn":["1611-3349"]},"publication":"21st International Conference on Computational Methods in Systems Biology","oa":1},{"language":[{"iso":"eng"}],"status":"public","doi":"10.1007/978-3-031-38545-2_17","date_published":"2023-08-09T00:00:00Z","alternative_title":["LNCS"],"intvolume":" 14082","volume":14082,"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","department":[{"_id":"KrPi"}],"month":"08","main_file_link":[{"url":"https://eprint.iacr.org/2023/1041","open_access":"1"}],"conference":{"start_date":"2023-08-20","name":"CRYPTO: Advances in Cryptology","location":"Santa Barbara, CA, United States","end_date":"2023-08-24"},"page":"514-546","scopus_import":"1","title":"Random oracle combiners: Breaking the concatenation barrier for collision-resistance","author":[{"last_name":"Dodis","first_name":"Yevgeniy","full_name":"Dodis, Yevgeniy"},{"last_name":"Ferguson","first_name":"Niels","full_name":"Ferguson, Niels"},{"full_name":"Goldin, Eli","first_name":"Eli","last_name":"Goldin"},{"full_name":"Hall, Peter","last_name":"Hall","first_name":"Peter"},{"orcid":"0000-0002-9139-1654","full_name":"Pietrzak, Krzysztof Z","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z","last_name":"Pietrzak"}],"date_updated":"2023-10-16T08:02:11Z","citation":{"mla":"Dodis, Yevgeniy, et al. “Random Oracle Combiners: Breaking the Concatenation Barrier for Collision-Resistance.” 43rd Annual International Cryptology Conference, vol. 14082, Springer Nature, 2023, pp. 514–46, doi:10.1007/978-3-031-38545-2_17.","ieee":"Y. Dodis, N. Ferguson, E. Goldin, P. Hall, and K. Z. Pietrzak, “Random oracle combiners: Breaking the concatenation barrier for collision-resistance,” in 43rd Annual International Cryptology Conference, Santa Barbara, CA, United States, 2023, vol. 14082, pp. 514–546.","ama":"Dodis Y, Ferguson N, Goldin E, Hall P, Pietrzak KZ. Random oracle combiners: Breaking the concatenation barrier for collision-resistance. In: 43rd Annual International Cryptology Conference. Vol 14082. Springer Nature; 2023:514-546. doi:10.1007/978-3-031-38545-2_17","apa":"Dodis, Y., Ferguson, N., Goldin, E., Hall, P., & Pietrzak, K. Z. (2023). Random oracle combiners: Breaking the concatenation barrier for collision-resistance. In 43rd Annual International Cryptology Conference (Vol. 14082, pp. 514–546). Santa Barbara, CA, United States: Springer Nature. https://doi.org/10.1007/978-3-031-38545-2_17","chicago":"Dodis, Yevgeniy, Niels Ferguson, Eli Goldin, Peter Hall, and Krzysztof Z Pietrzak. “Random Oracle Combiners: Breaking the Concatenation Barrier for Collision-Resistance.” In 43rd Annual International Cryptology Conference, 14082:514–46. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-38545-2_17.","ista":"Dodis Y, Ferguson N, Goldin E, Hall P, Pietrzak KZ. 2023. Random oracle combiners: Breaking the concatenation barrier for collision-resistance. 43rd Annual International Cryptology Conference. CRYPTO: Advances in Cryptology, LNCS, vol. 14082, 514–546.","short":"Y. Dodis, N. Ferguson, E. Goldin, P. Hall, K.Z. Pietrzak, in:, 43rd Annual International Cryptology Conference, Springer Nature, 2023, pp. 514–546."},"publication":"43rd Annual International Cryptology Conference","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031385445"],"issn":["0302-9743"]},"oa":1,"day":"09","abstract":[{"text":"Suppose we have two hash functions h1 and h2, but we trust the security of only one of them. To mitigate this worry, we wish to build a hash combiner Ch1,h2 which is secure so long as one of the underlying hash functions is. This question has been well-studied in the regime of collision resistance. In this case, concatenating the two hash function outputs clearly works. Unfortunately, a long series of works (Boneh and Boyen, CRYPTO’06; Pietrzak, Eurocrypt’07; Pietrzak, CRYPTO’08) showed no (noticeably) shorter combiner for collision resistance is possible.\r\nIn this work, we revisit this pessimistic state of affairs, motivated by the observation that collision-resistance is insufficient for many interesting applications of cryptographic hash functions anyway. We argue the right formulation of the “hash combiner” is to build what we call random oracle (RO) combiners, utilizing stronger assumptions for stronger constructions.\r\nIndeed, we circumvent the previous lower bounds for collision resistance by constructing a simple length-preserving RO combiner C˜h1,h2Z1,Z2(M)=h1(M,Z1)⊕h2(M,Z2),where Z1,Z2\r\n are random salts of appropriate length. We show that this extra randomness is necessary for RO combiners, and indeed our construction is somewhat tight with this lower bound.\r\nOn the negative side, we show that one cannot generically apply the composition theorem to further replace “monolithic” hash functions h1 and h2 by some simpler indifferentiable construction (such as the Merkle-Damgård transformation) from smaller components, such as fixed-length compression functions. Finally, despite this issue, we directly prove collision resistance of the Merkle-Damgård variant of our combiner, where h1 and h2 are replaced by iterative Merkle-Damgård hashes applied to a fixed-length compression function. Thus, we can still subvert the concatenation barrier for collision-resistance combiners while utilizing practically small fixed-length components underneath.","lang":"eng"}],"publication_status":"published","oa_version":"Preprint","article_processing_charge":"No","quality_controlled":"1","year":"2023","_id":"14428","date_created":"2023-10-15T22:01:11Z"},{"alternative_title":["LNCS"],"intvolume":" 14245","language":[{"iso":"eng"}],"status":"public","doi":"10.1007/978-3-031-44267-4_15","date_published":"2023-10-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":14245,"type":"conference","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2308.00341"}],"publisher":"Springer Nature","department":[{"_id":"ToHe"}],"month":"10","scopus_import":"1","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","page":"291-311","conference":{"end_date":"2023-10-06","start_date":"2023-10-03","name":"RV: Conference on Runtime Verification","location":"Thessaloniki, Greece"},"arxiv":1,"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"external_id":{"arxiv":["2308.00341"]},"title":"Monitoring algorithmic fairness under partial observations","publication":"23rd International Conference on Runtime Verification","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031442667"]},"oa":1,"day":"01","author":[{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin","last_name":"Kueffner"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik"}],"date_updated":"2023-10-31T11:48:20Z","citation":{"mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial Observations.” 23rd International Conference on Runtime Verification, vol. 14245, Springer Nature, 2023, pp. 291–311, doi:10.1007/978-3-031-44267-4_15.","ieee":"T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness under partial observations,” in 23rd International Conference on Runtime Verification, Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311.","apa":"Henzinger, T. A., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic fairness under partial observations. In 23rd International Conference on Runtime Verification (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature. https://doi.org/10.1007/978-3-031-44267-4_15","ama":"Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under partial observations. In: 23rd International Conference on Runtime Verification. Vol 14245. Springer Nature; 2023:291-311. doi:10.1007/978-3-031-44267-4_15","chicago":"Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness under Partial Observations.” In 23rd International Conference on Runtime Verification, 14245:291–311. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_15.","ista":"Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness under partial observations. 23rd International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.","short":"T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference on Runtime Verification, Springer Nature, 2023, pp. 291–311."},"oa_version":"Preprint","article_processing_charge":"No","quality_controlled":"1","abstract":[{"text":"As AI and machine-learned software are used increasingly for making decisions that affect humans, it is imperative that they remain fair and unbiased in their decisions. To complement design-time bias mitigation measures, runtime verification techniques have been introduced recently to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of the states of the (unknown) monitored system. Moreover, they can monitor only fairness properties that are specified as arithmetic expressions over the probabilities of different events. In this work, we extend fairness monitoring to systems modeled as partially observed Markov chains (POMC), and to specifications containing arithmetic expressions over the expected values of numerical functions on event sequences. The only assumptions we make are that the underlying POMC is aperiodic and starts in the stationary distribution, with a bound on its mixing time being known. These assumptions enable us to estimate a given property for the entire distribution of possible executions of the monitored POMC, by observing only a single execution. Our monitors observe a long run of the system and, after each new observation, output updated PAC-estimates of how fair or biased the system is. The monitors are computationally lightweight and, using a prototype implementation, we demonstrate their effectiveness on several real-world examples.","lang":"eng"}],"publication_status":"published","year":"2023","_id":"14454","date_created":"2023-10-29T23:01:15Z","ec_funded":1},{"month":"09","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2307.10847"}],"arxiv":1,"page":"333-347","conference":{"start_date":"2023-09-18","name":"FCT: Fundamentals of Computation Theory","location":"Trier, Germany","end_date":"2023-09-21"},"scopus_import":"1","date_published":"2023-09-21T00:00:00Z","doi":"10.1007/978-3-031-43587-4_24","status":"public","language":[{"iso":"eng"}],"intvolume":" 14292","alternative_title":["LNCS"],"type":"conference","volume":14292,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"link":[{"url":"https://doi.org/10.1007/978-3-031-43587-4_31","relation":"erratum"}]},"publication_status":"published","abstract":[{"lang":"eng","text":"In this paper, we present novel algorithms that efficiently compute a shortest reconfiguration sequence between two given dominating sets in trees and interval graphs under the TOKEN SLIDING model. In this problem, a graph is provided along with its two dominating sets, which can be imagined as tokens placed on vertices. The objective is to find a shortest sequence of dominating sets that transforms one set into the other, with each set in the sequence resulting from sliding a single token in the previous set. While identifying any sequence has been well studied, our work presents the first polynomial algorithms for this optimization variant in the context of dominating sets."}],"quality_controlled":"1","article_processing_charge":"No","oa_version":"Preprint","date_created":"2023-10-29T23:01:16Z","_id":"14456","year":"2023","external_id":{"arxiv":["2307.10847"]},"title":"Shortest dominating set reconfiguration under token sliding","date_updated":"2024-01-22T08:10:49Z","citation":{"ista":"Křišťan JM, Svoboda J. 2023. Shortest dominating set reconfiguration under token sliding. 24th International Symposium on Fundamentals of Computation Theory. FCT: Fundamentals of Computation Theory, LNCS, vol. 14292, 333–347.","chicago":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Shortest Dominating Set Reconfiguration under Token Sliding.” In 24th International Symposium on Fundamentals of Computation Theory, 14292:333–47. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-43587-4_24.","ieee":"J. M. Křišťan and J. Svoboda, “Shortest dominating set reconfiguration under token sliding,” in 24th International Symposium on Fundamentals of Computation Theory, Trier, Germany, 2023, vol. 14292, pp. 333–347.","ama":"Křišťan JM, Svoboda J. Shortest dominating set reconfiguration under token sliding. In: 24th International Symposium on Fundamentals of Computation Theory. Vol 14292. Springer Nature; 2023:333-347. doi:10.1007/978-3-031-43587-4_24","apa":"Křišťan, J. M., & Svoboda, J. (2023). Shortest dominating set reconfiguration under token sliding. In 24th International Symposium on Fundamentals of Computation Theory (Vol. 14292, pp. 333–347). Trier, Germany: Springer Nature. https://doi.org/10.1007/978-3-031-43587-4_24","mla":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Shortest Dominating Set Reconfiguration under Token Sliding.” 24th International Symposium on Fundamentals of Computation Theory, vol. 14292, Springer Nature, 2023, pp. 333–47, doi:10.1007/978-3-031-43587-4_24.","short":"J.M. Křišťan, J. Svoboda, in:, 24th International Symposium on Fundamentals of Computation Theory, Springer Nature, 2023, pp. 333–347."},"author":[{"last_name":"Křišťan","first_name":"Jan Matyáš","full_name":"Křišťan, Jan Matyáš"},{"last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub"}],"day":"21","oa":1,"publication_identifier":{"isbn":["9783031435867"],"eissn":["1611-3349"],"issn":["0302-9743"]},"publication":"24th International Symposium on Fundamentals of Computation Theory"}]