[{"type":"conference","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8","conference":{"start_date":"2024-09-09","end_date":"2024-09-13","name":"CONCUR: Conference on Concurrency Theory","location":"Calgary, Canada"},"year":"2024","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","license":"https://creativecommons.org/licenses/by/4.0/","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","corr_author":"1","acknowledgement":"This work was supported in part by the ERC projects ERC-2020-AdG 101020093 and CoG 863818 (ForM-SMArt) and by ISF grant no. 1679/21.","ddc":["000"],"has_accepted_license":"1","day":"01","volume":311,"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773393"]},"scopus_import":"1","abstract":[{"lang":"eng","text":"Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite path (aka play) traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent monetary rewards, aka the \"charges.\" Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. For example, a reachability objective may require multiple detours to vertices with high charges to earn additional budget. We show that, nonetheless, the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?"}],"month":"09","external_id":{"arxiv":["2407.06288"],"isi":["001556847400008"]},"publication":"35th International Conference on Concurrency Theory","oa":1,"article_processing_charge":"Yes","arxiv":1,"file":[{"file_id":"18083","access_level":"open_access","file_name":"2024_LIPICS_Avni.pdf","date_created":"2024-09-17T09:35:03Z","success":1,"creator":"dernst","date_updated":"2024-09-17T09:35:03Z","checksum":"cb6f2254b84922cd7bf224f550b73f4a","relation":"main_file","content_type":"application/pdf","file_size":854430}],"publication_status":"published","date_published":"2024-09-01T00:00:00Z","author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","last_name":"Avni","first_name":"Guy"},{"last_name":"Goharshady","first_name":"Ehsan Kafshdar","full_name":"Goharshady, Ehsan Kafshdar"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mallik, Kaushik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","last_name":"Mallik"}],"isi":1,"file_date_updated":"2024-09-17T09:35:03Z","title":"Bidding games with charging","das_tickbox":"0","doi":"10.4230/LIPIcs.CONCUR.2024.8","alternative_title":["LIPIcs"],"article_number":"8","quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T12:17:18Z","_id":"18066","intvolume":"       311","date_created":"2024-09-15T22:01:39Z","researchdata_availability":"no","language":[{"iso":"eng"}],"ec_funded":1,"oa_version":"Published Version","status":"public","department":[{"_id":"ToHe"}],"citation":{"ieee":"G. Avni, E. K. Goharshady, T. A. Henzinger, and K. Mallik, “Bidding games with charging,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311.","ista":"Avni G, Goharshady EK, Henzinger TA, Mallik K. 2024. Bidding games with charging. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 8.","ama":"Avni G, Goharshady EK, Henzinger TA, Mallik K. Bidding games with charging. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">10.4230/LIPIcs.CONCUR.2024.8</a>","mla":"Avni, Guy, et al. “Bidding Games with Charging.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">10.4230/LIPIcs.CONCUR.2024.8</a>.","short":"G. Avni, E.K. Goharshady, T.A. Henzinger, K. Mallik, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","chicago":"Avni, Guy, Ehsan Kafshdar Goharshady, Thomas A Henzinger, and Kaushik Mallik. “Bidding Games with Charging.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.8</a>.","apa":"Avni, G., Goharshady, E. K., Henzinger, T. A., &#38; Mallik, K. (2024). Bidding games with charging. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.8</a>"}},{"type":"conference","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"conference":{"location":"Calgary, Canada","name":"CONCUR: Conference on Concurrency Theory","end_date":"2024-09-13","start_date":"2024-09-09"},"year":"2024","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","acknowledgement":"Udi Boker: Israel Science Foundation grant 2410/22\r\nThomas A. Henzinger: ERC-2020-AdG 101020093 (VAMOS)\r\nKaroliina Lehtinen: ANR QUASY 23-CE48-0008-01\r\nAditya Prakash: Chancellors’ International Scholarship from the University of Warwick and Centre for Discrete Mathematics and Its Applications (DIMAP)","has_accepted_license":"1","ddc":["000"],"corr_author":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773393"]},"scopus_import":"1","abstract":[{"text":"An automaton 𝒜 is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted particular attention for its applications in synthesis problems. An automaton 𝒜 is guidable with respect to a class C of automata if it can fairly simulate every automaton in C, whose language is contained in that of 𝒜. In other words, guidable automata are those for which inclusion and simulation coincide, making them particularly interesting for model-checking. We study the connection between these two notions, and specifically the question of when they coincide. For classes of automata on which they do, deciding guidability, an otherwise challenging decision problem, reduces to deciding history-determinism, a problem that is starting to be well-understood for many classes. We provide a selection of sufficient criteria for a class of automata to guarantee the coincidence of the notions, and use them to show that the notions coincide for the most common automata classes, among which are ω-regular automata and many infinite-state automata with safety and reachability acceptance conditions, including vector addition systems with states, one-counter nets, pushdown-, Parikh-, and timed-automata. We also demonstrate that history-determinism and guidability do not always coincide, for example, for the classes of timed automata with a fixed number of clocks.","lang":"eng"}],"day":"01","volume":311,"month":"09","oa":1,"article_processing_charge":"No","arxiv":1,"publication":"35th International Conference on Concurrency Theory","external_id":{"isi":["001556847400012"],"arxiv":["2407.08620"]},"date_published":"2024-09-01T00:00:00Z","author":[{"last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","full_name":"Boker, Udi"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Lehtinen, Karoliina","first_name":"Karoliina","last_name":"Lehtinen"},{"full_name":"Prakash, Aditya","first_name":"Aditya","last_name":"Prakash"}],"publication_status":"published","file":[{"file_name":"2024_LIPICS_Boker.pdf","file_id":"18080","access_level":"open_access","file_size":766902,"content_type":"application/pdf","creator":"dernst","date_created":"2024-09-17T07:31:18Z","success":1,"relation":"main_file","checksum":"66db11ef8e600a434079c278050c3f09","date_updated":"2024-09-17T07:31:18Z"}],"file_date_updated":"2024-09-17T07:31:18Z","das_tickbox":"0","isi":1,"title":"History-determinism vs fair simulation","doi":"10.4230/LIPIcs.CONCUR.2024.12","alternative_title":["LIPIcs"],"intvolume":"       311","researchdata_availability":"no","date_created":"2024-09-15T22:01:40Z","article_number":"12","quality_controlled":"1","_id":"18067","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T12:17:34Z","ec_funded":1,"oa_version":"Published Version","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"citation":{"apa":"Boker, U., Henzinger, T. A., Lehtinen, K., &#38; Prakash, A. (2024). History-determinism vs fair simulation. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a>","chicago":"Boker, Udi, Thomas A Henzinger, Karoliina Lehtinen, and Aditya Prakash. “History-Determinism vs Fair Simulation.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a>.","short":"U. Boker, T.A. Henzinger, K. Lehtinen, A. Prakash, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","mla":"Boker, Udi, et al. “History-Determinism vs Fair Simulation.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">10.4230/LIPIcs.CONCUR.2024.12</a>.","ama":"Boker U, Henzinger TA, Lehtinen K, Prakash A. History-determinism vs fair simulation. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">10.4230/LIPIcs.CONCUR.2024.12</a>","ista":"Boker U, Henzinger TA, Lehtinen K, Prakash A. 2024. History-determinism vs fair simulation. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 12.","ieee":"U. Boker, T. A. Henzinger, K. Lehtinen, and A. Prakash, “History-determinism vs fair simulation,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311."},"status":"public"},{"alternative_title":["LNCS"],"intvolume":"     14572","date_created":"2024-05-12T22:01:02Z","researchdata_availability":"no","quality_controlled":"1","date_updated":"2026-10-21T12:16:28Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"_id":"15376","ec_funded":1,"oa_version":"Published Version","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"citation":{"mla":"Avni, Guy, et al. “Auction-Based Scheduling.” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 153–72, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>.","ista":"Avni G, Mallik K, Sadhukhan S. 2024. Auction-based scheduling. 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 14572, 153–172.","ama":"Avni G, Mallik K, Sadhukhan S. Auction-based scheduling. In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:153-172. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>","ieee":"G. Avni, K. Mallik, and S. Sadhukhan, “Auction-based scheduling,” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 153–172.","chicago":"Avni, Guy, Kaushik Mallik, and Suman Sadhukhan. “Auction-Based Scheduling.” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:153–72. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>.","apa":"Avni, G., Mallik, K., &#38; Sadhukhan, S. (2024). Auction-based scheduling. In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 153–172). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>","short":"G. Avni, K. Mallik, S. Sadhukhan, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 153–172."},"status":"public","file":[{"file_id":"15414","access_level":"open_access","file_name":"2024_LNCS_Avni.pdf","creator":"dernst","success":1,"date_created":"2024-05-22T07:09:24Z","relation":"main_file","checksum":"dbeb123510997886d11925aedbf9c400","date_updated":"2024-05-22T07:09:24Z","file_size":508191,"content_type":"application/pdf"}],"publication_status":"published","date_published":"2024-04-05T00:00:00Z","author":[{"first_name":"Guy","last_name":"Avni","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik"},{"first_name":"Suman","last_name":"Sadhukhan","full_name":"Sadhukhan, Suman"}],"page":"153-172","title":"Auction-based scheduling","file_date_updated":"2024-05-22T07:09:24Z","isi":1,"das_tickbox":"0","doi":"10.1007/978-3-031-57256-2_8","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and by ISF grant no. 1679/21.","ddc":["000"],"has_accepted_license":"1","corr_author":"1","publisher":"Springer Nature","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031572555"]},"abstract":[{"text":"Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a single policy fulfills all objectives. We present auction-based scheduling, a decentralized framework for multi-objective sequential decision making. Each objective is fulfilled using a separate and independent policy. Composition of policies is performed at runtime, where at each step, the policies simultaneously bid from pre-allocated budgets for the privilege of choosing the next action. The framework allows policies to be independently created, modified, and replaced. We study path planning problems on finite graphs with two temporal objectives and present algorithms to synthesize policies together with bidding policies in a decentralized manner. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other. We identify a class of assumptions called assume-admissible for which synthesis is always possible for graphs whose every vertex has at most two outgoing edges.","lang":"eng"}],"scopus_import":"1","day":"05","volume":14572,"month":"04","oa":1,"arxiv":1,"article_processing_charge":"Yes (in subscription journal)","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","external_id":{"arxiv":["2310.11798"],"isi":["001284187100008"]},"type":"conference","fulldoi":"https://doi.org/10.1007/978-3-031-57256-2_8","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"conference":{"start_date":"2024-04-06","location":"Luxembourg City, Luxembourg","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2024-04-11"},"year":"2024","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"intvolume":"     14739","researchdata_availability":"no","date_created":"2024-08-11T22:01:13Z","quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T12:03:11Z","_id":"17413","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"citation":{"short":"N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.","chicago":"Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying Phase Abstraction.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 14739:284–303. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">https://doi.org/10.1007/978-3-031-63498-7_17</a>.","apa":"Froleyks, N., Yu, E., Biere, A., &#38; Heljanko, K. (2024). Certifying phase abstraction. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 14739, pp. 284–303). Nancy, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">https://doi.org/10.1007/978-3-031-63498-7_17</a>","ieee":"N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Nancy, France, 2024, vol. 14739, pp. 284–303.","ista":"Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.","ama":"Froleyks N, Yu E, Biere A, Heljanko K. Certifying phase abstraction. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 14739. Springer Nature; 2024:284-303. doi:<a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">10.1007/978-3-031-63498-7_17</a>","mla":"Froleyks, Nils, et al. “Certifying Phase Abstraction.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 14739, Springer Nature, 2024, pp. 284–303, doi:<a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">10.1007/978-3-031-63498-7_17</a>."},"status":"public","ec_funded":1,"oa_version":"Published Version","language":[{"iso":"eng"}],"file_date_updated":"2024-08-12T06:53:39Z","isi":1,"das_tickbox":"0","title":"Certifying phase abstraction","doi":"10.1007/978-3-031-63498-7_17","file":[{"file_name":"2024_LNCS_Froleyks.pdf","file_id":"17414","access_level":"open_access","file_size":556902,"content_type":"application/pdf","creator":"dernst","success":1,"date_created":"2024-08-12T06:53:39Z","relation":"main_file","date_updated":"2024-08-12T06:53:39Z","checksum":"7d7839fc8c5c680ea3ac09f40a66e55d"}],"author":[{"full_name":"Froleyks, Nils","last_name":"Froleyks","first_name":"Nils"},{"full_name":"Yu, Zhengqi","last_name":"Yu","orcid":"0000-0002-4993-773X","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi"},{"last_name":"Biere","first_name":"Armin","full_name":"Biere, Armin"},{"first_name":"Keijo","last_name":"Heljanko","full_name":"Heljanko, Keijo"}],"publication_status":"published","date_published":"2024-07-01T00:00:00Z","page":"284-303","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031634970"]},"scopus_import":"1","abstract":[{"lang":"eng","text":"Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time."}],"day":"01","volume":14739,"acknowledgement":"This work is supported by the Austrian Science Fund (FWF) under the project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG 101020093, the Academy of Finland under the project 336092 and by a gift from Intel Corporation.","has_accepted_license":"1","ddc":["000"],"publisher":"Springer Nature","oa":1,"article_processing_charge":"Yes (in subscription journal)","arxiv":1,"external_id":{"isi":["001273489700017"],"arxiv":["2405.04297"]},"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","month":"07","type":"conference","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.1007/978-3-031-63498-7_17","conference":{"end_date":"2024-07-06","location":"Nancy, France","name":"IJCAR: International Joint Conference on Automated Reasoning","start_date":"2024-07-03"},"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"year":"2024"},{"citation":{"mla":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 353–358, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>.","ama":"Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition contribution). In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:353–358. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>","ista":"Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition contribution). 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 14572, 353–358.","ieee":"M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition contribution),” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 353–358.","chicago":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:353–358. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>.","apa":"Chalupa, M., &#38; Richter, C. (2024). Bubaak-SpLit: Split what you cannot verify (Competition contribution). In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 353–358). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>","short":"M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358."},"department":[{"_id":"ToHe"}],"status":"public","oa_version":"Published Version","ec_funded":1,"language":[{"iso":"eng"}],"researchdata_availability":"yes","date_created":"2024-04-20T18:14:06Z","intvolume":"     14572","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T12:12:16Z","_id":"15333","quality_controlled":"1","alternative_title":["LNCS"],"doi":"10.1007/978-3-031-57256-2_20","isi":1,"file_date_updated":"2024-04-26T11:27:26Z","das_tickbox":"1","title":"Bubaak-SpLit: Split what you cannot verify (Competition contribution)","page":"353–358","date_published":"2024-04-05T00:00:00Z","publication_status":"published","file":[{"file_name":"2024_LNCS_Chalupa.pdf","access_level":"open_access","file_id":"15347","content_type":"application/pdf","file_size":577128,"relation":"main_file","date_updated":"2024-04-26T11:27:26Z","checksum":"208c855c60824bec936b8d01d0396474","creator":"cchlebak","success":1,"date_created":"2024-04-26T11:27:26Z"}],"author":[{"last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek"},{"full_name":"Richter, Cedric","first_name":"Cedric","last_name":"Richter"}],"article_processing_charge":"Yes (in subscription journal)","oa":1,"external_id":{"isi":["001284187100020"]},"publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","month":"04","related_material":{"record":[{"id":"23183","status":"public","relation":"research_data"}]},"scopus_import":"1","abstract":[{"text":"BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed for running combinations of verifiers in parallel. In contrast to BUBAAK, that directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting the input program into multiple modified versions called program splits. During the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number of hard-to-verify program splits is generated or a splitting limit is reached. During the main verification phase, we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining unsolved parts of the verification task.","lang":"eng"}],"publication_identifier":{"eisbn":["9783031572562"],"isbn":["9783031572555"],"issn":["0302-9743"],"eissn":["1611-3349"]},"volume":14572,"day":"05","has_accepted_license":"1","ddc":["000"],"acknowledgement":"This work was partially supported by the ERC-2020-AdG 10102009 grant.","corr_author":"1","publisher":"Springer Nature","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","year":"2024","fulldoi":"https://doi.org/10.1007/978-3-031-57256-2_20","conference":{"end_date":"2024-04-11","location":"Luxembourg City, Luxembourg","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2024-04-06"},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"type":"conference","dataavailabilitystatement":"The submitted version of our tool contribution is archived and available at Zenodo [2] https://zenodo.org/records/10202207. The source code is also available on GitLab [3] https://gitlab.com/mchalupa/bubaak"},{"volume":14572,"day":"06","abstract":[{"text":"We provide an algorithmto solve Rabin and Streett games over graphs\r\nwith n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and\r\nO(nk logk logn) space, where ˜O hides poly-logarithmic factors. Our algorithm\r\nis an improvement by a super quadratic dependence on k! from the currently\r\nbest known run time of O³mn2(k!)2+o(1)´, obtained by converting a Rabin\r\ngameinto a parity game,while simultaneously improving its exponential space\r\nrequirement.\r\nOur main technical ingredient is a characterisation of progress measures for\r\nRabin games using colourful trees and a combinatorial construction of succinctlyrepresented,\r\nuniversal colourful trees. Colourful universal trees are generalisations\r\nof universal trees used by Jurdzi´nski and Lazi´c (2017) to solve parity\r\ngames, as well as of Rabin progress measures of Klarlund and Kozen (1991).\r\nOur algorithm for Rabin games is a progress measure lifting algorithm where\r\nthe lifting is performed on succinct, colourful, universal trees.","lang":"eng"}],"scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031572555"]},"corr_author":"1","publisher":"Springer Nature","ddc":["000"],"has_accepted_license":"1","acknowledgement":"This work is a part of the project VAMOS that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreements No 101020093. Rupak Majumdar was partially supported by the DFG project 389792660 TRR 248-CPEC.","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","external_id":{"isi":["001284187100011"],"arxiv":["2401.07548"]},"arxiv":1,"article_processing_charge":"Yes (in subscription journal)","oa":1,"month":"04","type":"conference","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","year":"2024","fulldoi":"https://doi.org/10.1007/978-3-031-57256-2_11","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"_id":"15377","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T12:16:56Z","quality_controlled":"1","researchdata_availability":"no","date_created":"2024-05-12T22:01:02Z","intvolume":"     14572","alternative_title":["LNCS"],"status":"public","citation":{"mla":"Majumdar, Rupak, et al. “Rabin Games and Colourful Universal Trees.” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 213–31, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">10.1007/978-3-031-57256-2_11</a>.","ama":"Majumdar R, Sağlam I, Thejaswini KS. Rabin games and colourful universal trees. In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:213-231. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">10.1007/978-3-031-57256-2_11</a>","ista":"Majumdar R, Sağlam I, Thejaswini KS. 2024. Rabin games and colourful universal trees. 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 14572, 213–231.","ieee":"R. Majumdar, I. Sağlam, and K. S. Thejaswini, “Rabin games and colourful universal trees,” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2024, vol. 14572, pp. 213–231.","chicago":"Majumdar, Rupak, Irmak Sağlam, and K. S. Thejaswini. “Rabin Games and Colourful Universal Trees.” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:213–31. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">https://doi.org/10.1007/978-3-031-57256-2_11</a>.","apa":"Majumdar, R., Sağlam, I., &#38; Thejaswini, K. S. (2024). Rabin games and colourful universal trees. In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 213–231). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">https://doi.org/10.1007/978-3-031-57256-2_11</a>","short":"R. Majumdar, I. Sağlam, K.S. Thejaswini, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 213–231."},"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"oa_version":"Published Version","ec_funded":1,"doi":"10.1007/978-3-031-57256-2_11","file_date_updated":"2024-05-22T07:24:45Z","das_tickbox":"0","isi":1,"title":"Rabin games and colourful universal trees","page":"213-231","publication_status":"published","date_published":"2024-04-06T00:00:00Z","author":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"first_name":"Irmak","last_name":"Sağlam","full_name":"Sağlam, Irmak"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","last_name":"Thejaswini","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753"}],"file":[{"file_id":"15415","access_level":"open_access","file_name":"2024_LNCS_Majumdar.pdf","success":1,"date_created":"2024-05-22T07:24:45Z","creator":"dernst","date_updated":"2024-05-22T07:24:45Z","checksum":"492be74f69cd6ea42d38681082d0b521","relation":"main_file","content_type":"application/pdf","file_size":462173}]},{"quality_controlled":"1","date_updated":"2026-10-21T12:03:35Z","_id":"17898","date_created":"2024-09-08T22:01:13Z","researchdata_availability":"no","status":"public","department":[{"_id":"ToHe"}],"citation":{"short":"M. Lechner, R. Hasani, A. Amini, T.H. Wang, T.A. Henzinger, D. Rus, in:, Proceedings of the 2024 IEEE International Conference on Robotics and Automation, IEEE, 2024, pp. 2774–2782.","apa":"Lechner, M., Hasani, R., Amini, A., Wang, T. H., Henzinger, T. A., &#38; Rus, D. (2024). Overparametrization helps offline-to-online generalization of closed-loop control from pixels. In <i>Proceedings of the 2024 IEEE International Conference on Robotics and Automation</i> (pp. 2774–2782). Yokohama, Japan: IEEE. <a href=\"https://doi.org/10.1109/ICRA57147.2024.10610284\">https://doi.org/10.1109/ICRA57147.2024.10610284</a>","chicago":"Lechner, Mathias, Ramin Hasani, Alexander Amini, Tsun Hsuan Wang, Thomas A Henzinger, and Daniela Rus. “Overparametrization Helps Offline-to-Online Generalization of Closed-Loop Control from Pixels.” In <i>Proceedings of the 2024 IEEE International Conference on Robotics and Automation</i>, 2774–82. IEEE, 2024. <a href=\"https://doi.org/10.1109/ICRA57147.2024.10610284\">https://doi.org/10.1109/ICRA57147.2024.10610284</a>.","ieee":"M. Lechner, R. Hasani, A. Amini, T. H. Wang, T. A. Henzinger, and D. Rus, “Overparametrization helps offline-to-online generalization of closed-loop control from pixels,” in <i>Proceedings of the 2024 IEEE International Conference on Robotics and Automation</i>, Yokohama, Japan, 2024, pp. 2774–2782.","ama":"Lechner M, Hasani R, Amini A, Wang TH, Henzinger TA, Rus D. Overparametrization helps offline-to-online generalization of closed-loop control from pixels. In: <i>Proceedings of the 2024 IEEE International Conference on Robotics and Automation</i>. IEEE; 2024:2774-2782. doi:<a href=\"https://doi.org/10.1109/ICRA57147.2024.10610284\">10.1109/ICRA57147.2024.10610284</a>","ista":"Lechner M, Hasani R, Amini A, Wang TH, Henzinger TA, Rus D. 2024. Overparametrization helps offline-to-online generalization of closed-loop control from pixels. Proceedings of the 2024 IEEE International Conference on Robotics and Automation. ICRA: International Conference on Robotics and Automation, 2774–2782.","mla":"Lechner, Mathias, et al. “Overparametrization Helps Offline-to-Online Generalization of Closed-Loop Control from Pixels.” <i>Proceedings of the 2024 IEEE International Conference on Robotics and Automation</i>, IEEE, 2024, pp. 2774–82, doi:<a href=\"https://doi.org/10.1109/ICRA57147.2024.10610284\">10.1109/ICRA57147.2024.10610284</a>."},"language":[{"iso":"eng"}],"ec_funded":1,"oa_version":"None","das_tickbox":"0","isi":1,"title":"Overparametrization helps offline-to-online generalization of closed-loop control from pixels","doi":"10.1109/ICRA57147.2024.10610284","author":[{"full_name":"Lechner, Mathias","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner"},{"first_name":"Ramin","last_name":"Hasani","full_name":"Hasani, Ramin"},{"full_name":"Amini, Alexander","last_name":"Amini","first_name":"Alexander"},{"last_name":"Wang","first_name":"Tsun Hsuan","full_name":"Wang, Tsun Hsuan"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"}],"date_published":"2024-08-08T00:00:00Z","publication_status":"published","page":"2774-2782","day":"08","publication_identifier":{"issn":["1050-4729"],"isbn":["9798350384574"]},"scopus_import":"1","abstract":[{"lang":"eng","text":"There is an ever-growing zoo of modern neural network models that can efficiently learn end-to-end control from visual observations. These advanced deep models, ranging from convolutional to Vision Transformers, from small to gigantic networks, have been extensively tested on offline image classification tasks. In this paper, we study these vision models with respect to the open-loop training to closed-loop generalization abilities, i.e., deployment realizes a causal feedback loop that is not present during training. This causality gap typically emerges in robotics applications such as autonomous driving, where a network is trained to imitate the control commands of a human. In this setting, two situations arise: 1) Closed-loop testing in-distribution, where the test environment shares properties with those of offline training data. 2) Closed-loop testing under distribution shifts and out-of-distribution. Contrary to recently reported results, we show that under proper training guidelines, all vision architectures perform indistinguishably well on in-distribution deployment, resolving the causality gap. In situation 2, We observe that scale is the strongest factor in improving closed-loop generalization regardless of the choice of the model architecture. Our results predict the trend that in the future we will see larger and larger models being used in offline-training-online-deployment imitation learning tasks in robotic applications."}],"publisher":"IEEE","acknowledgement":"This work was partially supported in parts by the ERC-2020-AdG 101020093. Additionally, it was partially sponsored by the United States Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under Cooperative Agreement Number FA8750-19-2-1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation herein. This work was further supported by The Boeing Company and the Office of Naval Research (ONR) Grant N00014-18-1-2830.","external_id":{"isi":["001294576202044"]},"publication":"Proceedings of the 2024 IEEE International Conference on Robotics and Automation","article_processing_charge":"No","month":"08","type":"conference","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.1109/ICRA57147.2024.10610284","conference":{"start_date":"2024-05-13","end_date":"2024-05-17","location":"Yokohama, Japan","name":"ICRA: International Conference on Robotics and Automation"},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"year":"2024"},{"page":"10714-10722","publication_status":"published","author":[{"full_name":"Trinh, Giang","last_name":"Trinh","first_name":"Giang"},{"full_name":"Benhamou, Belaid","first_name":"Belaid","last_name":"Benhamou"},{"first_name":"Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","orcid":"0000-0003-1993-0331","last_name":"Pastva","full_name":"Pastva, Samuel"},{"full_name":"Soliman, Sylvain","last_name":"Soliman","first_name":"Sylvain"}],"date_published":"2024-03-25T00:00:00Z","doi":"10.1609/aaai.v38i9.28943","das_tickbox":"0","title":"Scalable enumeration of trap spaces in boolean networks via answer set programming","language":[{"iso":"eng"}],"oa_version":"Published Version","ec_funded":1,"status":"public","citation":{"ieee":"G. Trinh, B. Benhamou, S. Pastva, and S. Soliman, “Scalable enumeration of trap spaces in boolean networks via answer set programming,” in <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>, 2024, vol. 38, no. 9, pp. 10714–10722.","ista":"Trinh G, Benhamou B, Pastva S, Soliman S. 2024. Scalable enumeration of trap spaces in boolean networks via answer set programming. Proceedings of the 38th AAAI Conference on Artificial Intelligence. vol. 38, 10714–10722.","ama":"Trinh G, Benhamou B, Pastva S, Soliman S. Scalable enumeration of trap spaces in boolean networks via answer set programming. In: <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>. Vol 38. Association for the Advancement of Artificial Intelligence; 2024:10714-10722. doi:<a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">10.1609/aaai.v38i9.28943</a>","mla":"Trinh, Giang, et al. “Scalable Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming.” <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>, vol. 38, no. 9, Association for the Advancement of Artificial Intelligence, 2024, pp. 10714–22, doi:<a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">10.1609/aaai.v38i9.28943</a>.","short":"G. Trinh, B. Benhamou, S. Pastva, S. Soliman, in:, Proceedings of the 38th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2024, pp. 10714–10722.","chicago":"Trinh, Giang, Belaid Benhamou, Samuel Pastva, and Sylvain Soliman. “Scalable Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming.” In <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i>, 38:10714–22. Association for the Advancement of Artificial Intelligence, 2024. <a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">https://doi.org/10.1609/aaai.v38i9.28943</a>.","apa":"Trinh, G., Benhamou, B., Pastva, S., &#38; Soliman, S. (2024). Scalable enumeration of trap spaces in boolean networks via answer set programming. In <i>Proceedings of the 38th AAAI Conference on Artificial Intelligence</i> (Vol. 38, pp. 10714–10722). Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v38i9.28943\">https://doi.org/10.1609/aaai.v38i9.28943</a>"},"main_file_link":[{"open_access":"1","url":"https://amu.hal.science/hal-04523118/"}],"department":[{"_id":"ToHe"}],"_id":"15321","date_updated":"2026-10-21T12:04:20Z","quality_controlled":"1","researchdata_availability":"yes (supplementary data)","date_created":"2024-04-14T22:01:02Z","intvolume":"        38","year":"2024","fulldoi":"https://doi.org/10.1609/aaai.v38i9.28943","project":[{"grant_number":"101034413","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","issue":"9","supplementarymaterial":"yes","type":"conference","month":"03","publication":"Proceedings of the 38th AAAI Conference on Artificial Intelligence","article_processing_charge":"No","oa":1,"publisher":"Association for the Advancement of Artificial Intelligence","ddc":["000"],"acknowledgement":"This work was supported by Institut Carnot STAR, Marseille, France and by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413.","volume":38,"day":"25","scopus_import":"1","abstract":[{"text":"Boolean Networks (BNs) are widely used as a modeling formalism in several domains, notably systems biology and computer science. A fundamental problem in BN analysis is the enumeration of trap spaces, which are hypercubes in the state space that cannot be escaped once entered. Several methods have been proposed for enumerating trap spaces, however they often suffer from scalability and efficiency issues, particularly for large and complex models. To our knowledge, the most efficient and recent methods for the trap space enumeration all rely on Answer Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated by these considerations, our work proposes a new method for enumerating trap spaces in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+ randomly generated BNs, showing that it enables analysis of models beyond the capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn).","lang":"eng"}],"publication_identifier":{"isbn":["1577358872"],"issn":["2159-5399"],"eissn":["2374-3468"]}},{"department":[{"_id":"ToHe"},{"_id":"GradSch"}],"citation":{"ieee":"B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy,” in <i>24th International Conference on Runtime Verification</i>, Istanbul, Turkey, 2024, vol. 15191, pp. 282–301.","mla":"Bonakdarpour, Borzoo, et al. “Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed &#38; Accuracy.” <i>24th International Conference on Runtime Verification</i>, vol. 15191, Springer Nature, 2024, pp. 282–301, doi:<a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">10.1007/978-3-031-74234-7_18</a>.","ista":"Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. 2024. Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. 24th International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 15191, 282–301.","ama":"Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. In: <i>24th International Conference on Runtime Verification</i>. Vol 15191. Springer Nature; 2024:282-301. doi:<a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">10.1007/978-3-031-74234-7_18</a>","short":"B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301.","apa":"Bonakdarpour, B., Momtaz, A., Nickovic, D., &#38; Sarac, N. E. (2024). Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. In <i>24th International Conference on Runtime Verification</i> (Vol. 15191, pp. 282–301). Istanbul, Turkey: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">https://doi.org/10.1007/978-3-031-74234-7_18</a>","chicago":"Bonakdarpour, Borzoo, Anik Momtaz, Dejan Nickovic, and Naci E Sarac. “Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed &#38; Accuracy.” In <i>24th International Conference on Runtime Verification</i>, 15191:282–301. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">https://doi.org/10.1007/978-3-031-74234-7_18</a>."},"status":"public","ec_funded":1,"oa_version":"Published Version","language":[{"iso":"eng"}],"intvolume":"     15191","date_created":"2024-11-10T23:01:58Z","researchdata_availability":"no","quality_controlled":"1","_id":"18521","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T13:14:54Z","alternative_title":["LNCS"],"OA_type":"hybrid","das_tickbox":"0","isi":1,"title":"Approximate distributed monitoring under partial synchrony: Balancing speed & accuracy","file_date_updated":"2024-11-11T09:42:28Z","doi":"10.1007/978-3-031-74234-7_18","date_published":"2024-10-12T00:00:00Z","author":[{"last_name":"Bonakdarpour","first_name":"Borzoo","full_name":"Bonakdarpour, Borzoo"},{"full_name":"Momtaz, Anik","last_name":"Momtaz","first_name":"Anik"},{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","last_name":"Sarac","first_name":"Naci E"}],"publication_status":"published","file":[{"success":1,"date_created":"2024-11-11T09:42:28Z","creator":"dernst","checksum":"7b8ca21b8c19ab796fa445b0e54003ca","date_updated":"2024-11-11T09:42:28Z","relation":"main_file","file_size":1897101,"content_type":"application/pdf","file_id":"18539","access_level":"open_access","file_name":"2024_LNCS_Bonakdarpour.pdf"}],"page":"282-301","oa":1,"article_processing_charge":"Yes (in subscription journal)","arxiv":1,"publication":"24th International Conference on Runtime Verification","OA_place":"publisher","external_id":{"arxiv":["2408.05033"],"isi":["001420093700018"]},"month":"10","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031742330"]},"scopus_import":"1","abstract":[{"lang":"eng","text":"In distributed systems with processes that do not share a global clock, partial synchrony is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an approximate distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples."}],"day":"12","volume":15191,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. This work is sponsored in part by the United States NSF CCF-2118356 award. This research was partially funded by A-IQ Ready (Chips JU, grant agreement No. 101096658).","has_accepted_license":"1","ddc":["000"],"corr_author":"1","publisher":"Springer Nature","APC_amount":"2748 EUR","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"name":"RV: Conference on Runtime Verification","location":"Istanbul, Turkey","end_date":"2024-10-17","start_date":"2024-10-15"},"fulldoi":"https://doi.org/10.1007/978-3-031-74234-7_18","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"year":"2024","type":"conference"},{"isi":1,"file_date_updated":"2024-09-17T07:48:56Z","title":"Strategic dominance: A new preorder for nondeterministic processes","das_tickbox":"0","doi":"10.4230/LIPIcs.CONCUR.2024.29","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"full_name":"Sarac, Naci E","last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E"}],"publication_status":"published","file":[{"relation":"main_file","checksum":"555bd343e1fb38adeab8fc465ff4fad8","date_updated":"2024-09-17T07:48:56Z","creator":"dernst","success":1,"date_created":"2024-09-17T07:48:56Z","file_size":964124,"content_type":"application/pdf","access_level":"open_access","file_id":"18081","file_name":"2024_LIPICS_Henzinger.pdf"}],"date_published":"2024-09-01T00:00:00Z","OA_type":"gold","quality_controlled":"1","article_number":"29","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T13:15:11Z","_id":"18068","intvolume":"       311","date_created":"2024-09-15T22:01:40Z","researchdata_availability":"no","alternative_title":["LIPIcs"],"status":"public","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"citation":{"chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>.","apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2024). Strategic dominance: A new preorder for nondeterministic processes. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","mla":"Henzinger, Thomas A., et al. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">10.4230/LIPIcs.CONCUR.2024.29</a>.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2024. Strategic dominance: A new preorder for nondeterministic processes. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 29.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder for nondeterministic processes. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">10.4230/LIPIcs.CONCUR.2024.29</a>","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance: A new preorder for nondeterministic processes,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311."},"language":[{"iso":"eng"}],"ec_funded":1,"oa_version":"Published Version","type":"conference","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"start_date":"2024-09-09","name":"CONCUR: Conference on Concurrency Theory","location":"Calgary, Canada","end_date":"2024-09-13"},"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"year":"2024","day":"01","volume":311,"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773393"]},"abstract":[{"lang":"eng","text":"We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as \"strategy inclusion\" between 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata."}],"scopus_import":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","corr_author":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. N. Mazzocchi was affiliated with ISTA when this work was submitted for publication.","ddc":["000"],"has_accepted_license":"1","OA_place":"publisher","external_id":{"arxiv":["2407.10473"],"isi":["001556847400029"]},"publication":"35th International Conference on Concurrency Theory","oa":1,"arxiv":1,"article_processing_charge":"Yes","month":"09"},{"alternative_title":["LIPIcs"],"intvolume":"       313","researchdata_availability":"no","date_created":"2024-10-06T22:01:12Z","quality_controlled":"1","article_number":"27","date_updated":"2026-10-21T13:11:58Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"_id":"18175","oa_version":"Published Version","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"citation":{"chicago":"Maj, Petr, Stefanie Muroya Lei, Konrad Siek, Luca Di Grazia, and Jan Vitek. “The Fault in Our Stars: Designing Reproducible Large-Scale Code Analysis Experiments.” In <i>38th European Conference on Object-Oriented Programming</i>, Vol. 313. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.ECOOP.2024.27\">https://doi.org/10.4230/LIPIcs.ECOOP.2024.27</a>.","apa":"Maj, P., Muroya Lei, S., Siek, K., Di Grazia, L., &#38; Vitek, J. (2024). The fault in our stars: Designing reproducible large-scale code analysis experiments. In <i>38th European Conference on Object-Oriented Programming</i> (Vol. 313). Vienna, Austria: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ECOOP.2024.27\">https://doi.org/10.4230/LIPIcs.ECOOP.2024.27</a>","short":"P. Maj, S. Muroya Lei, K. Siek, L. Di Grazia, J. Vitek, in:, 38th European Conference on Object-Oriented Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","ama":"Maj P, Muroya Lei S, Siek K, Di Grazia L, Vitek J. The fault in our stars: Designing reproducible large-scale code analysis experiments. In: <i>38th European Conference on Object-Oriented Programming</i>. Vol 313. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ECOOP.2024.27\">10.4230/LIPIcs.ECOOP.2024.27</a>","ista":"Maj P, Muroya Lei S, Siek K, Di Grazia L, Vitek J. 2024. The fault in our stars: Designing reproducible large-scale code analysis experiments. 38th European Conference on Object-Oriented Programming. ECOOP: European Conference on Object-Oriented Programming, LIPIcs, vol. 313, 27.","mla":"Maj, Petr, et al. “The Fault in Our Stars: Designing Reproducible Large-Scale Code Analysis Experiments.” <i>38th European Conference on Object-Oriented Programming</i>, vol. 313, 27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ECOOP.2024.27\">10.4230/LIPIcs.ECOOP.2024.27</a>.","ieee":"P. Maj, S. Muroya Lei, K. Siek, L. Di Grazia, and J. Vitek, “The fault in our stars: Designing reproducible large-scale code analysis experiments,” in <i>38th European Conference on Object-Oriented Programming</i>, Vienna, Austria, 2024, vol. 313."},"status":"public","author":[{"full_name":"Maj, Petr","first_name":"Petr","last_name":"Maj"},{"first_name":"Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","last_name":"Muroya Lei","full_name":"Muroya Lei, Stefanie"},{"full_name":"Siek, Konrad","last_name":"Siek","first_name":"Konrad"},{"first_name":"Luca","last_name":"Di Grazia","full_name":"Di Grazia, Luca"},{"full_name":"Vitek, Jan","last_name":"Vitek","first_name":"Jan"}],"publication_status":"published","date_published":"2024-09-01T00:00:00Z","file":[{"content_type":"application/pdf","file_size":1764222,"relation":"main_file","date_updated":"2024-10-07T11:10:55Z","checksum":"2e75d305a8c817d76a0c7f136ce34f86","creator":"dernst","success":1,"date_created":"2024-10-07T11:10:55Z","file_name":"2024_LIPICs_Maj.pdf","access_level":"open_access","file_id":"18184"}],"das_tickbox":"0","isi":1,"title":"The fault in our stars: Designing reproducible large-scale code analysis experiments","file_date_updated":"2024-10-07T11:10:55Z","doi":"10.4230/LIPIcs.ECOOP.2024.27","acknowledgement":"This work was supported by the Czech Ministry of Education, Youth and Sports under\r\nprogram ERC-CZ, grant agreement LL2325, BigCode (reg. no. CZ.02.1.01/0.0/0.0/15_003/0000421). NSF grants CCF-1910850, CNS-1925644, and CCF-2139612, as well as the GACR EXPRO grant 23-07580X. We would like to thank Digital Ocean for their involuntary contribution of computational resources during the early data gathering phase of our research. We acknoweldge the reviewers of ICSE’22, and thank the reviewers of ECOOP’23 for their encouragments and for sticking around until 2024.","ddc":["000"],"has_accepted_license":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773416"]},"abstract":[{"text":"Large-scale software repositories are a source of insights for software engineering. They offer an unmatched window into the software development process at scale. Their sheer number and size holds the promise of broadly applicable results. At the same time, that very size presents practical challenges for scaling tools and algorithms to millions of projects. A reasonable approach is to limit studies to representative samples of the population of interest. Broadly applicable conclusions can then be obtained by generalizing to the entire population. The contribution of this paper is a standardized experimental design methodology for choosing the inputs of studies working with large-scale repositories. We advocate for a methodology that clearly lays out what the population of interest is, how to sample it, and that fosters reproducibility. Along the way, we discourage researchers from using extrinsic attributes of projects such as stars, that measure some unclear notion of popularity.","lang":"eng"}],"scopus_import":"1","day":"01","volume":313,"month":"09","oa":1,"article_processing_charge":"No","external_id":{"isi":["001533999700027"]},"publication":"38th European Conference on Object-Oriented Programming","type":"conference","fulldoi":"https://doi.org/10.4230/LIPIcs.ECOOP.2024.27","conference":{"name":"ECOOP: European Conference on Object-Oriented Programming","location":"Vienna, Austria","end_date":"2024-09-20","start_date":"2024-09-16"},"year":"2024","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"date_published":"2024-10-02T00:00:00Z","file":[{"relation":"main_file","date_updated":"2024-11-11T08:32:02Z","checksum":"26826786a960039b9501cfc5cb4f3fe6","creator":"dernst","success":1,"date_created":"2024-11-11T08:32:02Z","content_type":"application/pdf","file_size":563394,"access_level":"open_access","file_id":"18532","file_name":"2024_LMCS_Bose.pdf"}],"publication_status":"published","author":[{"full_name":"Bose, Sougata","last_name":"Bose","first_name":"Sougata"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Lehtinen, Karoliina","first_name":"Karoliina","last_name":"Lehtinen"},{"first_name":"Sven","last_name":"Schewe","full_name":"Schewe, Sven"},{"full_name":"Totzke, Patrick","first_name":"Patrick","last_name":"Totzke"}],"page":"1-28","isi":1,"file_date_updated":"2024-11-11T08:32:02Z","title":"History-deterministic timed automata","das_tickbox":"0","doi":"10.46298/lmcs-20(4:1)2024","OA_type":"gold","intvolume":"        20","researchdata_availability":"no","date_created":"2024-11-10T23:02:01Z","quality_controlled":"1","date_updated":"2026-10-21T13:12:37Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"_id":"18530","ec_funded":1,"oa_version":"Published Version","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"citation":{"ieee":"S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic timed automata,” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4. EPI Sciences, pp. 1–28, 2024.","mla":"Bose, Sougata, et al. “History-Deterministic Timed Automata.” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4, EPI Sciences, 2024, pp. 1–28, doi:<a href=\"https://doi.org/10.46298/lmcs-20(4:1)2024\">10.46298/lmcs-20(4:1)2024</a>.","ista":"Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2024. History-deterministic timed automata. Logical Methods in Computer Science. 20(4), 1–28.","ama":"Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic timed automata. <i>Logical Methods in Computer Science</i>. 2024;20(4):1-28. doi:<a href=\"https://doi.org/10.46298/lmcs-20(4:1)2024\">10.46298/lmcs-20(4:1)2024</a>","short":"S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, Logical Methods in Computer Science 20 (2024) 1–28.","chicago":"Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. “History-Deterministic Timed Automata.” <i>Logical Methods in Computer Science</i>. EPI Sciences, 2024. <a href=\"https://doi.org/10.46298/lmcs-20(4:1)2024\">https://doi.org/10.46298/lmcs-20(4:1)2024</a>.","apa":"Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., &#38; Totzke, P. (2024). History-deterministic timed automata. <i>Logical Methods in Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/lmcs-20(4:1)2024\">https://doi.org/10.46298/lmcs-20(4:1)2024</a>"},"status":"public","article_type":"original","type":"journal_article","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"fulldoi":"https://doi.org/10.46298/lmcs-20(4:1)2024","year":"2024","supplementarymaterial":"no","issue":"4","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","acknowledgement":"This work has in parts been presented at the 33rd International Conference on Concurrency Theory (CONCUR’22) [HLT22] and at the 16th International Workshop on Reachability Problems (RP’22) [BHL+22]. This work was supported by the EU (ERC-2020-AdG 101020093); the EPSRC (EP/V025848/1, EP/X042596/1, EP/X017796/1 and EP/X03688X/1); and the ANR (QUASY 23-CE48-0008-01).","ddc":["000"],"has_accepted_license":"1","corr_author":"1","publisher":"EPI Sciences","publication_identifier":{"eissn":["1860-5974"]},"abstract":[{"text":"We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step. We show that the class of timed ω\r\n-languages recognized by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA. For non-deterministic timed automata it is known that universality is already undecidable for safety/reachability TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete. For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automaton states.","lang":"eng"}],"scopus_import":"1","day":"02","volume":20,"related_material":{"record":[{"id":"12508","relation":"earlier_version","status":"public"}]},"month":"10","DOAJ_listed":"1","oa":1,"article_processing_charge":"No","arxiv":1,"OA_place":"publisher","external_id":{"isi":["001332466900002"],"arxiv":["2304.03183"]},"publication":"Logical Methods in Computer Science"},{"supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.1137/1.9781611977936.16","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"conference":{"location":"Alexandria, VA, United States","name":"SOSA: Symposium on Simplicity in Algorithms","end_date":"2024-01-10","start_date":"2024-01-08"},"year":"2024","type":"conference","publication":"2024 Symposium on Simplicity in Algorithms","OA_place":"repository","external_id":{"arxiv":["2310.20433"]},"oa":1,"arxiv":1,"article_processing_charge":"No","month":"01","day":"01","publication_identifier":{"isbn":["9781611977936"]},"abstract":[{"lang":"eng","text":"We give a simple proof that assuming the Exponential Time Hypothesis (ETH), determining the winner of a Rabin game cannot be done in time 2o(k log k) · nO(1), where k is the number of pairs of vertex subsets involved in the winning condition and n is the vertex count of the game graph. While this result follows from the lower bounds provided by Calude et al [SIAM J. Comp. 2022], our reduction is considerably simpler and arguably provides more insight into the complexity of the problem. In fact, the analogous lower bounds discussed by Calude et al, for solving Muller games and multidimensional parity games, follow as simple corollaries of our approach. Our reduction also highlights the usefulness of a certain pivot problem — Permutation SAT — which may be of independent interest."}],"scopus_import":"1","publisher":"Society for Industrial and Applied Mathematics","acknowledgement":"This work is a part of projects CUTACOMBS (Ma. Pilipczuk), BOBR (Mi. Pilipczuk), and VAMOS (K. S. Thejaswini) that have received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme, grant agreements No 714704, 948057, and 101020093, respectively. Ma. Pilipczuk is also partially supported by Polish National Science Centre SONATA BIS-12 grant number 2022/46/E/ST6/00143.","OA_type":"green","title":"Simple and tight complexity lower bounds for solving Rabin games","das_tickbox":"0","doi":"10.1137/1.9781611977936.16","publication_status":"published","author":[{"full_name":"Casares, Antonio","first_name":"Antonio","last_name":"Casares"},{"full_name":"Pilipczuk, Marcin","last_name":"Pilipczuk","first_name":"Marcin"},{"full_name":"Pilipczuk, Michał","last_name":"Pilipczuk","first_name":"Michał"},{"full_name":"Souza, Uéverton S.","last_name":"Souza","first_name":"Uéverton S."},{"id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","last_name":"Thejaswini","first_name":"K. S.","full_name":"Thejaswini, K. S."}],"date_published":"2024-01-01T00:00:00Z","page":"160-167","status":"public","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2310.20433"}],"department":[{"_id":"ToHe"}],"citation":{"chicago":"Casares, Antonio, Marcin Pilipczuk, Michał Pilipczuk, Uéverton S. Souza, and K. S. Thejaswini. “Simple and Tight Complexity Lower Bounds for Solving Rabin Games.” In <i>2024 Symposium on Simplicity in Algorithms</i>, 160–67. Society for Industrial and Applied Mathematics, 2024. <a href=\"https://doi.org/10.1137/1.9781611977936.16\">https://doi.org/10.1137/1.9781611977936.16</a>.","apa":"Casares, A., Pilipczuk, M., Pilipczuk, M., Souza, U. S., &#38; Thejaswini, K. S. (2024). Simple and tight complexity lower bounds for solving Rabin games. In <i>2024 Symposium on Simplicity in Algorithms</i> (pp. 160–167). Alexandria, VA, United States: Society for Industrial and Applied Mathematics. <a href=\"https://doi.org/10.1137/1.9781611977936.16\">https://doi.org/10.1137/1.9781611977936.16</a>","short":"A. Casares, M. Pilipczuk, M. Pilipczuk, U.S. Souza, K.S. Thejaswini, in:, 2024 Symposium on Simplicity in Algorithms, Society for Industrial and Applied Mathematics, 2024, pp. 160–167.","mla":"Casares, Antonio, et al. “Simple and Tight Complexity Lower Bounds for Solving Rabin Games.” <i>2024 Symposium on Simplicity in Algorithms</i>, Society for Industrial and Applied Mathematics, 2024, pp. 160–67, doi:<a href=\"https://doi.org/10.1137/1.9781611977936.16\">10.1137/1.9781611977936.16</a>.","ista":"Casares A, Pilipczuk M, Pilipczuk M, Souza US, Thejaswini KS. 2024. Simple and tight complexity lower bounds for solving Rabin games. 2024 Symposium on Simplicity in Algorithms. SOSA: Symposium on Simplicity in Algorithms, 160–167.","ama":"Casares A, Pilipczuk M, Pilipczuk M, Souza US, Thejaswini KS. Simple and tight complexity lower bounds for solving Rabin games. In: <i>2024 Symposium on Simplicity in Algorithms</i>. Society for Industrial and Applied Mathematics; 2024:160-167. doi:<a href=\"https://doi.org/10.1137/1.9781611977936.16\">10.1137/1.9781611977936.16</a>","ieee":"A. Casares, M. Pilipczuk, M. Pilipczuk, U. S. Souza, and K. S. Thejaswini, “Simple and tight complexity lower bounds for solving Rabin games,” in <i>2024 Symposium on Simplicity in Algorithms</i>, Alexandria, VA, United States, 2024, pp. 160–167."},"language":[{"iso":"eng"}],"ec_funded":1,"oa_version":"Preprint","quality_controlled":"1","_id":"18955","date_updated":"2026-10-21T13:13:33Z","date_created":"2025-01-29T11:55:50Z","researchdata_availability":"no"},{"external_id":{"isi":["001416640500009"]},"publication":"Integrated Formal Methods","article_processing_charge":"No","month":"11","volume":15234,"day":"13","abstract":[{"lang":"eng","text":"Hypernode logic can reason about the prefix relation on stutter-reduced finite traces through the stutter-reduced prefix predicate. We increase the expressiveness of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate into an explicit stutter-reduction operator and the classical prefix predicate on words. This change gives hypernode logic the ability to combine synchronous and asynchronous reasoning by explicitly stating which parts of traces can stutter. Second, we allow the use of regular expressions in formulas to reason about the structure of traces. This change enables hypernode logic to describe a mixture of trace properties and hyperproperties.\r\n\r\nWe show how to translate extended hypernode logic formulas into multi-track automata, which are automata that read multiple input words. Then we describe a fully online monitoring algorithm for monitoring k-safety hyperproperties specified in the logic. We have implemented the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous versions of observational determinism, and on checking the privacy preservation by compiler optimizations."}],"scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031765537"]},"publisher":"Springer Nature","corr_author":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, and by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","year":"2024","fulldoi":"https://doi.org/10.1007/978-3-031-76554-4_9","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"type":"conference","status":"public","citation":{"apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. (2024). Monitoring extended hypernode logic. In <i>Integrated Formal Methods</i> (Vol. 15234, pp. 151–171). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">https://doi.org/10.1007/978-3-031-76554-4_9</a>","chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana Oliveira da Costa. “Monitoring Extended Hypernode Logic.” In <i>Integrated Formal Methods</i>, 15234:151–71. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">https://doi.org/10.1007/978-3-031-76554-4_9</a>.","short":"M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal Methods, Springer Nature, 2024, pp. 151–171.","mla":"Chalupa, Marek, et al. “Monitoring Extended Hypernode Logic.” <i>Integrated Formal Methods</i>, vol. 15234, Springer Nature, 2024, pp. 151–71, doi:<a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">10.1007/978-3-031-76554-4_9</a>.","ista":"Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171.","ama":"Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode logic. In: <i>Integrated Formal Methods</i>. Vol 15234. Springer Nature; 2024:151-171. doi:<a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">10.1007/978-3-031-76554-4_9</a>","ieee":"M. Chalupa, T. A. Henzinger, and A. Oliveira da Costa, “Monitoring extended hypernode logic,” in <i>Integrated Formal Methods</i>, 2024, vol. 15234, pp. 151–171."},"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"oa_version":"None","ec_funded":1,"date_updated":"2026-10-21T13:13:13Z","_id":"18599","quality_controlled":"1","date_created":"2024-12-01T23:01:52Z","researchdata_availability":"no","intvolume":"     15234","alternative_title":["LNCS"],"OA_type":"closed access","doi":"10.1007/978-3-031-76554-4_9","title":"Monitoring extended hypernode logic","isi":1,"das_tickbox":"0","page":"151-171","author":[{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ana","orcid":"0000-0002-8741-5799","last_name":"Oliveira da Costa","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","full_name":"Oliveira da Costa, Ana"}],"publication_status":"published","date_published":"2024-11-13T00:00:00Z"},{"oa_version":"None","ec_funded":1,"language":[{"iso":"eng"}],"citation":{"short":"N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, in:, Computational Methods in Systems Biology, Springer Nature, 2024, pp. 19–26.","apa":"Beneš, N., Brim, L., Huvar, O., Pastva, S., &#38; Šafránek, D. (2024). BNClassifier: Classifying boolean models by dynamic properties. In <i>Computational Methods in Systems Biology</i> (Vol. 14971, pp. 19–26). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">https://doi.org/10.1007/978-3-031-71671-3_2</a>","chicago":"Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek. “BNClassifier: Classifying Boolean Models by Dynamic Properties.” In <i>Computational Methods in Systems Biology</i>, 14971:19–26. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">https://doi.org/10.1007/978-3-031-71671-3_2</a>.","ieee":"N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “BNClassifier: Classifying boolean models by dynamic properties,” in <i>Computational Methods in Systems Biology</i>, 2024, vol. 14971, pp. 19–26.","ama":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. BNClassifier: Classifying boolean models by dynamic properties. In: <i>Computational Methods in Systems Biology</i>. Vol 14971. Springer Nature; 2024:19-26. doi:<a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">10.1007/978-3-031-71671-3_2</a>","ista":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2024. BNClassifier: Classifying boolean models by dynamic properties. Computational Methods in Systems Biology. , LNBI, vol. 14971, 19–26.","mla":"Beneš, Nikola, et al. “BNClassifier: Classifying Boolean Models by Dynamic Properties.” <i>Computational Methods in Systems Biology</i>, vol. 14971, Springer Nature, 2024, pp. 19–26, doi:<a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">10.1007/978-3-031-71671-3_2</a>."},"department":[{"_id":"ToHe"}],"status":"public","alternative_title":["LNBI"],"date_created":"2024-10-06T22:01:12Z","researchdata_availability":"no","intvolume":"     14971","_id":"18177","date_updated":"2026-10-21T13:12:17Z","quality_controlled":"1","page":"19-26","author":[{"first_name":"Nikola","last_name":"Beneš","full_name":"Beneš, Nikola"},{"last_name":"Brim","first_name":"Luboš","full_name":"Brim, Luboš"},{"first_name":"Ondřej","last_name":"Huvar","full_name":"Huvar, Ondřej"},{"full_name":"Pastva, Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","last_name":"Pastva","orcid":"0000-0003-1993-0331","first_name":"Samuel"},{"first_name":"David","last_name":"Šafránek","full_name":"Šafránek, David"}],"date_published":"2024-09-19T00:00:00Z","publication_status":"published","doi":"10.1007/978-3-031-71671-3_2","title":"BNClassifier: Classifying boolean models by dynamic properties","das_tickbox":"0","isi":1,"month":"09","article_processing_charge":"No","publication":"Computational Methods in Systems Biology","external_id":{"isi":["001333144400002"]},"acknowledgement":"The work has been supported by the Czech Science Foundation grant No. GA22-10845S. This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement No. 101034413.","publisher":"Springer Nature","scopus_import":"1","abstract":[{"text":"Partially Specified Boolean Networks (PSBNs) represent a family of Boolean models resulting from possible interpretations of unknown update logics. Hybrid extension of CTL (HCTL) has the power to express complex dynamical phenomena, such as oscillations or stability. We present BNClassifier to classify Boolean Networks corresponding to a given PSBN according to criteria specified in HCTL. The implementation of the tool is fully symbolic (based on BDDs). The results are visualised using the machine-learning-based technology of decision trees.","lang":"eng"}],"publication_identifier":{"isbn":["9783031716706"],"issn":["0302-9743"],"eissn":["1611-3349"]},"volume":14971,"day":"19","year":"2024","fulldoi":"https://doi.org/10.1007/978-3-031-71671-3_2","project":[{"name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","grant_number":"101034413"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","type":"conference"},{"OA_type":"closed access","series_title":"LNCS","doi":"10.1007/978-3-031-73751-0_12","das_tickbox":"0","title":"Reminiscences of a Real-Time Researcher","page":"154-164","publication_status":"published","date_published":"2024-10-23T00:00:00Z","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"status":"public","citation":{"mla":"Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” <i>Real Time and Such</i>, edited by Susanne Graf et al., vol. 15230, Springer Nature, 2024, pp. 154–64, doi:<a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">10.1007/978-3-031-73751-0_12</a>.","ista":"Henzinger TA. 2024.Reminiscences of a Real-Time Researcher. In: Real Time and Such. LNCS, vol. 15230, 154–164.","ama":"Henzinger TA. Reminiscences of a Real-Time Researcher. In: Graf S, Pettersson P, Steffen B, eds. <i>Real Time and Such</i>. Vol 15230. LNCS. Cham: Springer Nature; 2024:154-164. doi:<a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">10.1007/978-3-031-73751-0_12</a>","ieee":"T. A. Henzinger, “Reminiscences of a Real-Time Researcher,” in <i>Real Time and Such</i>, vol. 15230, S. Graf, P. Pettersson, and B. Steffen, Eds. Cham: Springer Nature, 2024, pp. 154–164.","apa":"Henzinger, T. A. (2024). Reminiscences of a Real-Time Researcher. In S. Graf, P. Pettersson, &#38; B. Steffen (Eds.), <i>Real Time and Such</i> (Vol. 15230, pp. 154–164). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">https://doi.org/10.1007/978-3-031-73751-0_12</a>","chicago":"Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” In <i>Real Time and Such</i>, edited by Susanne Graf, Paul Pettersson, and Bernhard Steffen, 15230:154–64. LNCS. Cham: Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">https://doi.org/10.1007/978-3-031-73751-0_12</a>.","short":"T.A. Henzinger, in:, S. Graf, P. Pettersson, B. Steffen (Eds.), Real Time and Such, Springer Nature, Cham, 2024, pp. 154–164."},"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"editor":[{"full_name":"Graf, Susanne","last_name":"Graf","first_name":"Susanne"},{"last_name":"Pettersson","first_name":"Paul","full_name":"Pettersson, Paul"},{"first_name":"Bernhard","last_name":"Steffen","full_name":"Steffen, Bernhard"}],"oa_version":"None","_id":"18563","date_updated":"2026-10-21T13:12:56Z","quality_controlled":"1","date_created":"2024-11-18T09:10:06Z","researchdata_availability":"no","intvolume":"     15230","alternative_title":["LNCS"],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","year":"2024","fulldoi":"https://doi.org/10.1007/978-3-031-73751-0_12","type":"book_chapter","place":"Cham","publication":"Real Time and Such","article_processing_charge":"No","month":"10","volume":15230,"day":"23","abstract":[{"lang":"eng","text":"I give a personal account about the wave of new research activities that rose in the 1990s on the specification, verification, and control of real-time systems."}],"scopus_import":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031737503"],"eisbn":["9783031737510"]},"corr_author":"1","publisher":"Springer Nature","acknowledgement":"I thank all my collaborators over the years. None of the mentioned contributions would have been possible without them. I also apologize for all omissions. The selection of contributions in this essay reflects primarily my personal involvement rather than any measure of importance."},{"year":"2024","fulldoi":"https://doi.org/10.4230/LIPIcs.STACS.2024.34","conference":{"location":"Clermont-Ferrand, France","name":"STACS: Symposium on Theoretical Aspects of Computer Science","end_date":"2024-03-14","start_date":"2024-03-12"},"project":[{"name":"Algorithms for Embeddings and Homotopy Theory","_id":"26611F5C-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P31312"},{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"yes","type":"conference","month":"03","related_material":{"record":[{"id":"22247","relation":"later_version","status":"public"},{"id":"20339","relation":"dissertation_contains","status":"public"}]},"arxiv":1,"article_processing_charge":"No","oa":1,"external_id":{"arxiv":["2312.12981"],"isi":["001300393400034"]},"publication":"41st International Symposium on Theoretical Aspects of Computer Science","ddc":["510"],"has_accepted_license":"1","acknowledgement":"Marek Filakovský: This research was supported by Charles University (project PRIMUS/\r\n21/SCI/014), the Austrian Science Fund (FWF project P31312-N35), and MSCAfellow5_MUNI\r\n(CZ.02.01.01/00/22_010/0003229). Tamio-Vesa Nakajima: This research was funded by UKRI EP/X024431/1 and by a Clarendon Fund Scholarship. All data is provided in full in the results section of this paper. Jakub Opršal: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No 101034413. Uli Wagner: This research was supported by the Austrian Science Fund (FWF project P31312-N35).","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","corr_author":"1","abstract":[{"lang":"eng","text":"A linearly ordered (LO) k-colouring of a hypergraph is a colouring of its vertices with colours 1, … , k such that each edge contains a unique maximal colour. Deciding whether an input hypergraph admits LO k-colouring with a fixed number of colours is NP-complete (and in the special case of graphs, LO colouring coincides with the usual graph colouring). Here, we investigate the complexity of approximating the \"linearly ordered chromatic number\" of a hypergraph. We prove that the following promise problem is NP-complete: Given a 3-uniform hypergraph, distinguish between the case that it is LO 3-colourable, and the case that it is not even LO 4-colourable. We prove this result by a combination of algebraic, topological, and combinatorial methods, building on and extending a topological approach for studying approximate graph colouring introduced by Krokhin, Opršal, Wrochna, and Živný (2023)."}],"scopus_import":"1","publication_identifier":{"isbn":["9783959773119"],"eissn":["1868-8969"]},"volume":289,"day":"01","date_published":"2024-03-01T00:00:00Z","publication_status":"published","file":[{"file_size":927290,"content_type":"application/pdf","relation":"main_file","checksum":"0524d4189fd1ed08989546511343edf3","date_updated":"2024-03-25T07:44:30Z","creator":"dernst","date_created":"2024-03-25T07:44:30Z","success":1,"file_name":"2024_LIPICs_Filakovsky.pdf","access_level":"open_access","file_id":"15175"}],"author":[{"full_name":"Filakovský, Marek","id":"3E8AF77E-F248-11E8-B48F-1D18A9856A87","last_name":"Filakovský","first_name":"Marek"},{"full_name":"Nakajima, Tamio Vesa","last_name":"Nakajima","first_name":"Tamio Vesa"},{"full_name":"Opršal, Jakub","first_name":"Jakub","orcid":"0000-0003-1245-3456","last_name":"Opršal","id":"ec596741-c539-11ec-b829-c79322a91242"},{"full_name":"Tasinato, Gianluca","last_name":"Tasinato","id":"0433290C-AF8F-11E9-A4C7-F729E6697425","first_name":"Gianluca"},{"id":"36690CA2-F248-11E8-B48F-1D18A9856A87","last_name":"Wagner","orcid":"0000-0002-1494-0568","first_name":"Uli","full_name":"Wagner, Uli"}],"doi":"10.4230/LIPIcs.STACS.2024.34","file_date_updated":"2024-03-25T07:44:30Z","isi":1,"title":"Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs","das_tickbox":"0","oa_version":"Published Version","ec_funded":1,"language":[{"iso":"eng"}],"citation":{"ieee":"M. Filakovský, T. V. Nakajima, J. Opršal, G. Tasinato, and U. Wagner, “Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs,” in <i>41st International Symposium on Theoretical Aspects of Computer Science</i>, Clermont-Ferrand, France, 2024, vol. 289.","mla":"Filakovský, Marek, et al. “Hardness of Linearly Ordered 4-Colouring of 3-Colourable 3-Uniform Hypergraphs.” <i>41st International Symposium on Theoretical Aspects of Computer Science</i>, vol. 289, 34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.STACS.2024.34\">10.4230/LIPIcs.STACS.2024.34</a>.","ama":"Filakovský M, Nakajima TV, Opršal J, Tasinato G, Wagner U. Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs. In: <i>41st International Symposium on Theoretical Aspects of Computer Science</i>. Vol 289. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.STACS.2024.34\">10.4230/LIPIcs.STACS.2024.34</a>","ista":"Filakovský M, Nakajima TV, Opršal J, Tasinato G, Wagner U. 2024. Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs. 41st International Symposium on Theoretical Aspects of Computer Science. STACS: Symposium on Theoretical Aspects of Computer Science, LIPIcs, vol. 289, 34.","short":"M. Filakovský, T.V. Nakajima, J. Opršal, G. Tasinato, U. Wagner, in:, 41st International Symposium on Theoretical Aspects of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","chicago":"Filakovský, Marek, Tamio Vesa Nakajima, Jakub Opršal, Gianluca Tasinato, and Uli Wagner. “Hardness of Linearly Ordered 4-Colouring of 3-Colourable 3-Uniform Hypergraphs.” In <i>41st International Symposium on Theoretical Aspects of Computer Science</i>, Vol. 289. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.STACS.2024.34\">https://doi.org/10.4230/LIPIcs.STACS.2024.34</a>.","apa":"Filakovský, M., Nakajima, T. V., Opršal, J., Tasinato, G., &#38; Wagner, U. (2024). Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs. In <i>41st International Symposium on Theoretical Aspects of Computer Science</i> (Vol. 289). Clermont-Ferrand, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.STACS.2024.34\">https://doi.org/10.4230/LIPIcs.STACS.2024.34</a>"},"department":[{"_id":"UlWa"}],"status":"public","alternative_title":["LIPIcs"],"researchdata_availability":"yes","date_created":"2024-03-24T23:00:59Z","intvolume":"       289","date_updated":"2026-10-21T13:23:55Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"_id":"15168","article_number":"34","quality_controlled":"1"},{"date_created":"2021-07-14T07:01:27Z","researchdata_availability":"not applicable","intvolume":"       218","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"_id":"9651","date_updated":"2026-10-21T13:22:57Z","quality_controlled":"1","article_number":"15","oa_version":"Published Version","language":[{"iso":"eng"}],"citation":{"ieee":"M. Dymond and V. Kaluza, “Divergence of separated nets with respect to displacement equivalence,” <i>Geometriae Dedicata</i>, vol. 218. Springer Nature, 2024.","ama":"Dymond M, Kaluza V. Divergence of separated nets with respect to displacement equivalence. <i>Geometriae Dedicata</i>. 2024;218. doi:<a href=\"https://doi.org/10.1007/s10711-023-00862-3\">10.1007/s10711-023-00862-3</a>","ista":"Dymond M, Kaluza V. 2024. Divergence of separated nets with respect to displacement equivalence. Geometriae Dedicata. 218, 15.","mla":"Dymond, Michael, and Vojtech Kaluza. “Divergence of Separated Nets with Respect to Displacement Equivalence.” <i>Geometriae Dedicata</i>, vol. 218, 15, Springer Nature, 2024, doi:<a href=\"https://doi.org/10.1007/s10711-023-00862-3\">10.1007/s10711-023-00862-3</a>.","short":"M. Dymond, V. Kaluza, Geometriae Dedicata 218 (2024).","apa":"Dymond, M., &#38; Kaluza, V. (2024). Divergence of separated nets with respect to displacement equivalence. <i>Geometriae Dedicata</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10711-023-00862-3\">https://doi.org/10.1007/s10711-023-00862-3</a>","chicago":"Dymond, Michael, and Vojtech Kaluza. “Divergence of Separated Nets with Respect to Displacement Equivalence.” <i>Geometriae Dedicata</i>. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/s10711-023-00862-3\">https://doi.org/10.1007/s10711-023-00862-3</a>."},"department":[{"_id":"UlWa"}],"status":"public","file":[{"file_name":"2024_GeometriaeDedicata_Dymond.pdf","access_level":"open_access","file_id":"17257","content_type":"application/pdf","file_size":540981,"relation":"main_file","date_updated":"2024-07-16T10:14:13Z","checksum":"9418534ac2f3d6f1f091a8b8ccaed01e","creator":"dernst","date_created":"2024-07-16T10:14:13Z","success":1}],"publication_status":"published","pmid":1,"author":[{"first_name":"Michael","last_name":"Dymond","full_name":"Dymond, Michael"},{"id":"21AE5134-9EAC-11EA-BEA2-D7BD3DDC885E","orcid":"0000-0002-2512-8698","last_name":"Kaluza","first_name":"Vojtech","full_name":"Kaluza, Vojtech"}],"date_published":"2024-02-01T00:00:00Z","doi":"10.1007/s10711-023-00862-3","isi":1,"title":"Divergence of separated nets with respect to displacement equivalence","file_date_updated":"2024-07-16T10:14:13Z","das_tickbox":"1","OA_type":"hybrid","has_accepted_license":"1","ddc":["510"],"acknowledgement":"Open access funding provided by Institute of Science and Technology (IST Austria). This work was started while both authors were employed at the University of Innsbruck and enjoyed the full support of Austrian Science Fund (FWF): P 30902-N35. It was continued when the first named author was employed at University of Leipzig and the second named author was employed at Institute of Science and Technology of Austria, where he was supported by an IST Fellowship.","publisher":"Springer Nature","corr_author":"1","scopus_import":"1","abstract":[{"lang":"eng","text":"We introduce a hierachy of equivalence relations on the set of separated nets of a given Euclidean space, indexed by concave increasing functions ϕ:(0,∞)→(0,∞). Two separated nets are called ϕ-displacement equivalent if, roughly speaking, there is a bijection between them which, for large radii R, displaces points of norm at most R by something of order at most ϕ(R). We show that the spectrum of ϕ-displacement equivalence spans from the established notion of bounded displacement equivalence, which corresponds to bounded ϕ, to the indiscrete equivalence relation, coresponding to ϕ(R)∈Ω(R), in which all separated nets are equivalent. In between the two ends of this spectrum, the notions of ϕ-displacement equivalence are shown to be pairwise distinct with respect to the asymptotic classes of ϕ(R) for R→∞. We further undertake a comparison of our notion of ϕ-displacement equivalence with previously studied relations on separated nets. Particular attention is given to the interaction of the notions of ϕ-displacement equivalence with that of bilipschitz equivalence."}],"publication_identifier":{"issn":["0046-5755"],"eissn":["1572-9168"]},"volume":218,"day":"01","month":"02","article_processing_charge":"Yes (via OA deal)","arxiv":1,"oa":1,"external_id":{"arxiv":["2102.13046"],"isi":["001105681500001"],"pmid":["38021107"]},"OA_place":"publisher","publication":"Geometriae Dedicata","dataavailabilitystatement":"Data sharing not applicable to this article as no datasets were generated or analysed during the current study.","article_type":"original","type":"journal_article","year":"2024","fulldoi":"https://doi.org/10.1007/s10711-023-00862-3","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no"},{"publication":"Bulletin of the London Mathematical Society","external_id":{"arxiv":["2212.04308"],"isi":["001113277100001"]},"oa":1,"arxiv":1,"article_processing_charge":"Yes (via OA deal)","month":"02","day":"01","volume":56,"publication_identifier":{"eissn":["1469-2120"],"issn":["0024-6093"]},"scopus_import":"1","abstract":[{"lang":"eng","text":"The classical Steinitz theorem states that if the origin belongs to the interior of the convex hull of a set 𝑆⊂ℝ𝑑, then there are at most 2𝑑 points of 𝑆 whose convex hull contains the origin in the interior. Bárány, Katchalski,and Pach proved the following quantitative version of Steinitz’s theorem. Let 𝑄 be a convex polytope in ℝ𝑑 containing the standard Euclidean unit ball 𝐁𝑑. Then there exist at most 2𝑑 vertices of 𝑄 whose convex hull 𝑄′ satisfies 𝑟𝐁𝑑⊂𝑄′ with 𝑟⩾𝑑−2𝑑. They conjectured that 𝑟⩾𝑐𝑑−1∕2 holds with a universal constant 𝑐>0. We prove 𝑟⩾15𝑑2, the first polynomial lower bound on 𝑟. Furthermore, we show that 𝑟 is not greater than 2/√𝑑."}],"publisher":"London Mathematical Society","corr_author":"1","acknowledgement":"M.N. was supported by the János Bolyai Scholarship of the Hungarian Academy of Sciences aswell as the National Research, Development and Innovation Fund (NRDI) grants K119670 andK131529, and the ÚNKP-22-5 New National Excellence Program of the Ministry for Innovationand Technology from the source of the NRDI as well as the ELTE TKP 2021-NKTA-62 fundingscheme","has_accepted_license":"1","ddc":["510"],"supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","issue":"2","fulldoi":"https://doi.org/10.1112/blms.12965","year":"2024","type":"journal_article","article_type":"original","status":"public","department":[{"_id":"UlWa"}],"citation":{"chicago":"Ivanov, Grigory, and Márton Naszódi. “Quantitative Steinitz Theorem: A Polynomial Bound.” <i>Bulletin of the London Mathematical Society</i>. London Mathematical Society, 2024. <a href=\"https://doi.org/10.1112/blms.12965\">https://doi.org/10.1112/blms.12965</a>.","apa":"Ivanov, G., &#38; Naszódi, M. (2024). Quantitative Steinitz theorem: A polynomial bound. <i>Bulletin of the London Mathematical Society</i>. London Mathematical Society. <a href=\"https://doi.org/10.1112/blms.12965\">https://doi.org/10.1112/blms.12965</a>","short":"G. Ivanov, M. Naszódi, Bulletin of the London Mathematical Society 56 (2024) 796–802.","mla":"Ivanov, Grigory, and Márton Naszódi. “Quantitative Steinitz Theorem: A Polynomial Bound.” <i>Bulletin of the London Mathematical Society</i>, vol. 56, no. 2, London Mathematical Society, 2024, pp. 796–802, doi:<a href=\"https://doi.org/10.1112/blms.12965\">10.1112/blms.12965</a>.","ama":"Ivanov G, Naszódi M. Quantitative Steinitz theorem: A polynomial bound. <i>Bulletin of the London Mathematical Society</i>. 2024;56(2):796-802. doi:<a href=\"https://doi.org/10.1112/blms.12965\">10.1112/blms.12965</a>","ista":"Ivanov G, Naszódi M. 2024. Quantitative Steinitz theorem: A polynomial bound. Bulletin of the London Mathematical Society. 56(2), 796–802.","ieee":"G. Ivanov and M. Naszódi, “Quantitative Steinitz theorem: A polynomial bound,” <i>Bulletin of the London Mathematical Society</i>, vol. 56, no. 2. London Mathematical Society, pp. 796–802, 2024."},"language":[{"iso":"eng"}],"oa_version":"Published Version","quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T13:23:20Z","_id":"14660","intvolume":"        56","researchdata_availability":"no","date_created":"2023-12-10T23:00:58Z","isi":1,"file_date_updated":"2024-07-16T10:35:10Z","title":"Quantitative Steinitz theorem: A polynomial bound","das_tickbox":"0","doi":"10.1112/blms.12965","publication_status":"published","date_published":"2024-02-01T00:00:00Z","file":[{"creator":"dernst","success":1,"date_created":"2024-07-16T10:35:10Z","relation":"main_file","checksum":"30ea0694757bc668cf7cd15ae357b35e","date_updated":"2024-07-16T10:35:10Z","file_size":111756,"content_type":"application/pdf","file_id":"17259","access_level":"open_access","file_name":"2024_BulletinLondonMathSoc_Ivanov.pdf"}],"author":[{"full_name":"Ivanov, Grigory","first_name":"Grigory","id":"87744F66-5C6F-11EA-AFE0-D16B3DDC885E","last_name":"Ivanov","orcid":"0000-0002-5021-3982"},{"full_name":"Naszódi, Márton","last_name":"Naszódi","first_name":"Márton"}],"page":"796-802"},{"OA_type":"hybrid","publication_status":"published","date_published":"2024-08-01T00:00:00Z","author":[{"full_name":"Beďatš, Daniel","first_name":"Daniel","id":"78ea3cc9-31e7-11ee-aa02-a6169bbfe1f1","orcid":"0009-0004-1828-0044","last_name":"Beďatš"}],"file":[{"creator":"dernst","success":1,"date_created":"2024-12-09T13:56:26Z","relation":"main_file","checksum":"7b01c89128ba16d5334dfab389a03878","date_updated":"2024-12-09T13:56:26Z","file_size":486969,"content_type":"application/pdf","file_id":"18638","access_level":"open_access","file_name":"2024_JourAlgebra_Bedats.pdf"}],"page":"281-304","das_tickbox":"1","title":"Separation of variables for scalar-valued polynomials in the non-stable range","isi":1,"file_date_updated":"2024-12-09T13:56:26Z","doi":"10.1016/j.jalgebra.2024.04.013","language":[{"iso":"eng"}],"oa_version":"Published Version","status":"public","department":[{"_id":"UlWa"}],"citation":{"chicago":"Beďatš, Daniel. “Separation of Variables for Scalar-Valued Polynomials in the Non-Stable Range.” <i>Journal of Algebra</i>. Elsevier, 2024. <a href=\"https://doi.org/10.1016/j.jalgebra.2024.04.013\">https://doi.org/10.1016/j.jalgebra.2024.04.013</a>.","apa":"Beďatš, D. (2024). Separation of variables for scalar-valued polynomials in the non-stable range. <i>Journal of Algebra</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jalgebra.2024.04.013\">https://doi.org/10.1016/j.jalgebra.2024.04.013</a>","short":"D. Beďatš, Journal of Algebra 651 (2024) 281–304.","ama":"Beďatš D. Separation of variables for scalar-valued polynomials in the non-stable range. <i>Journal of Algebra</i>. 2024;651:281-304. doi:<a href=\"https://doi.org/10.1016/j.jalgebra.2024.04.013\">10.1016/j.jalgebra.2024.04.013</a>","ista":"Beďatš D. 2024. Separation of variables for scalar-valued polynomials in the non-stable range. Journal of Algebra. 651, 281–304.","mla":"Beďatš, Daniel. “Separation of Variables for Scalar-Valued Polynomials in the Non-Stable Range.” <i>Journal of Algebra</i>, vol. 651, Elsevier, 2024, pp. 281–304, doi:<a href=\"https://doi.org/10.1016/j.jalgebra.2024.04.013\">10.1016/j.jalgebra.2024.04.013</a>.","ieee":"D. Beďatš, “Separation of variables for scalar-valued polynomials in the non-stable range,” <i>Journal of Algebra</i>, vol. 651. Elsevier, pp. 281–304, 2024."},"quality_controlled":"1","_id":"18617","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"date_updated":"2026-10-21T13:24:58Z","intvolume":"       651","researchdata_availability":"not applicable","date_created":"2024-12-04T07:58:45Z","fulldoi":"https://doi.org/10.1016/j.jalgebra.2024.04.013","year":"2024","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_type":"original","dataavailabilitystatement":"No data was used for the research described in the article.\r\n","type":"journal_article","month":"08","OA_place":"publisher","publication":"Journal of Algebra","external_id":{"arxiv":["2309.11154"],"isi":["001232775600001"]},"oa":1,"arxiv":1,"article_processing_charge":"Yes (via OA deal)","publisher":"Elsevier","corr_author":"1","acknowledgement":"The author is sincerely grateful for guidance, advice and valuable feedback from Roman Lávička.","ddc":["510"],"has_accepted_license":"1","day":"01","volume":651,"publication_identifier":{"issn":["0021-8693"]},"scopus_import":"1","abstract":[{"lang":"eng","text":"Any complex-valued polynomial on (Rn)k decomposes into an algebraic combination of O(n)-invariant polynomials and harmonic polynomials. This decomposition, separation of variables, is granted to be unique if n≥2k−1. We prove that the condition n≥2k−1 is not only sufficient, but also necessary for uniqueness of the separation. Moreover, we describe the structure of non-uniqueness of the separation in the boundary cases when n=2k−2 and n=2k−3.\r\nFormally, we study the kernel of a multiplication map ϕ carrying out separation of variables. We devise a general algorithmic procedure for describing Ker ϕ in the restricted non-stable range k≤n<2k−1. In the full non-stable range n<2k−1, we give formulas for highest weights of generators of the kernel as well as formulas for its Hilbert series. Using the developed methods, we obtain a list of highest weight vectors generating Ker ϕ."}]}]