[{"month":"07","quality_controlled":"1","has_accepted_license":"1","article_processing_charge":"Yes","publication_identifier":{"issn":["0010-440X"],"eissn":["1532-8384"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","publication_status":"published","pmid":1,"abstract":[{"lang":"eng","text":"Background: Benzodiazepines and antidepressants are effective agents for the treatment of generalized anxiety disorder (GAD), with the HAM-A frequently used as a primary outcome measure. The GAD literature is inconsistent regarding which medications are more effective for somatic versus psychic symptoms of GAD, and treatment guidelines do not advocate for prescribing based on subtype. This meta-analysis aimed to determine whether benzodiazepines and antidepressants have a differential impact on the somatic versus psychic subscales of the HAM-A in GAD.\r\n\r\nMethods: An electronic search was undertaken for randomized controlled trials of either benzodiazepines or antidepressants for GAD that reported treatment response using the HAM-A subscales. Data were extracted by independent reviewers. A random effects assessment of weighted mean difference with 95% confidence intervals and subgroup difference was applied. All analysis was done on SPSS 26. An assessment of bias, and of quality of evidence was performed.\r\n\r\nResults: 24 randomized controlled trials met the inclusion criteria: 18 antidepressant trials, 5 benzodiazepine trials and 1 of both. 14 studies were assessed as having between some and high risk of bias, while 10 were assessed as having low risk of bias. Benzodiazepines (WMD of 1.81 [CI 1.03, 2.58]) were significantly more effective than antidepressants (WMD of 0.83 [CI 0.64, 1.02]) for reducing somatic symptoms of GAD (Chi2 = 5.81, p = 0.02), and were also more effective (WMD of 2.46 [CI 1.83, 3.09]) in reducing psychic symptoms than antidepressants (WMD of 1.83 [CI 1.55, 2.10]), although this comparison did not reach statistical significance (Chi2 = 3.31, p = 0.07).\r\n\r\nConclusion: The finding that benzodiazepines were significantly more effective than antidepressants for somatic symptoms needs to be weighed up against potential benefits of antidepressants over benzodiazepines. It may be useful for future treatment guidelines for GAD to explicitly consider symptom subtype."}],"das_tickbox":"0","oa_version":"Published Version","doi":"10.1016/j.comppsych.2024.152479","day":"01","volume":132,"file_date_updated":"2025-01-13T10:47:20Z","publication":"Comprehensive Psychiatry","title":"Meta-analysis of the comparative efficacy of benzodiazepines and antidepressants for psychic versus somatic symptoms of generalized anxiety disorder","scopus_import":"1","OA_type":"gold","type":"journal_article","status":"public","date_published":"2024-07-01T00:00:00Z","article_number":"152479","_id":"15295","file":[{"creator":"dernst","access_level":"open_access","file_size":2874425,"date_updated":"2025-01-13T10:47:20Z","file_id":"18839","checksum":"aadb57448b5f170761ed72cbcc31ba16","file_name":"2024_ComprehensivePsychiatry_Beyer.pdf","relation":"main_file","success":1,"date_created":"2025-01-13T10:47:20Z","content_type":"application/pdf"}],"year":"2024","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"date_created":"2024-04-07T22:00:55Z","DOAJ_listed":"1","publisher":"Elsevier","external_id":{"pmid":["38564872"],"isi":["001221136000001"]},"citation":{"apa":"Beyer, C., Currin, C., Williams, T., &#38; Stein, D. J. (2024). Meta-analysis of the comparative efficacy of benzodiazepines and antidepressants for psychic versus somatic symptoms of generalized anxiety disorder. <i>Comprehensive Psychiatry</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.comppsych.2024.152479\">https://doi.org/10.1016/j.comppsych.2024.152479</a>","ama":"Beyer C, Currin C, Williams T, Stein DJ. Meta-analysis of the comparative efficacy of benzodiazepines and antidepressants for psychic versus somatic symptoms of generalized anxiety disorder. <i>Comprehensive Psychiatry</i>. 2024;132. doi:<a href=\"https://doi.org/10.1016/j.comppsych.2024.152479\">10.1016/j.comppsych.2024.152479</a>","ieee":"C. Beyer, C. Currin, T. Williams, and D. J. Stein, “Meta-analysis of the comparative efficacy of benzodiazepines and antidepressants for psychic versus somatic symptoms of generalized anxiety disorder,” <i>Comprehensive Psychiatry</i>, vol. 132. Elsevier, 2024.","ista":"Beyer C, Currin C, Williams T, Stein DJ. 2024. Meta-analysis of the comparative efficacy of benzodiazepines and antidepressants for psychic versus somatic symptoms of generalized anxiety disorder. Comprehensive Psychiatry. 132, 152479.","mla":"Beyer, Chad, et al. “Meta-Analysis of the Comparative Efficacy of Benzodiazepines and Antidepressants for Psychic versus Somatic Symptoms of Generalized Anxiety Disorder.” <i>Comprehensive Psychiatry</i>, vol. 132, 152479, Elsevier, 2024, doi:<a href=\"https://doi.org/10.1016/j.comppsych.2024.152479\">10.1016/j.comppsych.2024.152479</a>.","short":"C. Beyer, C. Currin, T. Williams, D.J. Stein, Comprehensive Psychiatry 132 (2024).","chicago":"Beyer, Chad, Christopher Currin, Taryn Williams, and Dan J. Stein. “Meta-Analysis of the Comparative Efficacy of Benzodiazepines and Antidepressants for Psychic versus Somatic Symptoms of Generalized Anxiety Disorder.” <i>Comprehensive Psychiatry</i>. Elsevier, 2024. <a href=\"https://doi.org/10.1016/j.comppsych.2024.152479\">https://doi.org/10.1016/j.comppsych.2024.152479</a>."},"fulldoi":"https://doi.org/10.1016/j.comppsych.2024.152479","article_type":"original","isi":1,"intvolume":"       132","author":[{"last_name":"Beyer","full_name":"Beyer, Chad","first_name":"Chad"},{"id":"e8321fc5-3091-11eb-8a53-83f309a11ac9","first_name":"Christopher","full_name":"Currin, Christopher","orcid":"0000-0002-4809-5059","last_name":"Currin"},{"last_name":"Williams","full_name":"Williams, Taryn","first_name":"Taryn"},{"first_name":"Dan J.","full_name":"Stein, Dan J.","last_name":"Stein"}],"ddc":["570"],"oa":1,"language":[{"iso":"eng"}],"researchdata_availability":"no","department":[{"_id":"TiVo"}],"date_updated":"2026-10-21T12:00:08Z"},{"author":[{"last_name":"Froleyks","full_name":"Froleyks, Nils","first_name":"Nils"},{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","orcid":"0000-0002-4993-773X","first_name":"Zhengqi","full_name":"Yu, Zhengqi","last_name":"Yu"},{"last_name":"Biere","full_name":"Biere, Armin","first_name":"Armin"}],"oa":1,"ec_funded":1,"language":[{"iso":"eng"}],"date_updated":"2026-10-21T12:01:13Z","department":[{"_id":"ToHe"}],"researchdata_availability":"unclear","publisher":"VDE Verlag","date_created":"2024-05-26T22:00:58Z","citation":{"apa":"Froleyks, N., Yu, E., &#38; Biere, A. (2024). Ternary simulation as abstract interpretation (Work in Progress). In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i> (pp. 148–151). Kaiserslautern, Germany: VDE Verlag.","ama":"Froleyks N, Yu E, Biere A. Ternary simulation as abstract interpretation (Work in Progress). In: <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>. VDE Verlag; 2024:148-151.","ieee":"N. Froleyks, E. Yu, and A. Biere, “Ternary simulation as abstract interpretation (Work in Progress),” in <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, Kaiserslautern, Germany, 2024, pp. 148–151.","ista":"Froleyks N, Yu E, Biere A. 2024. Ternary simulation as abstract interpretation (Work in Progress). 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems, 148–151.","mla":"Froleyks, Nils, et al. “Ternary Simulation as Abstract Interpretation (Work in Progress).” <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, VDE Verlag, 2024, pp. 148–51.","chicago":"Froleyks, Nils, Emily Yu, and Armin Biere. “Ternary Simulation as Abstract Interpretation (Work in Progress).” In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, 148–51. VDE Verlag, 2024.","short":"N. Froleyks, E. Yu, A. Biere, in:, 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems, VDE Verlag, 2024, pp. 148–151."},"page":"148-151","scopus_import":"1","title":"Ternary simulation as abstract interpretation (Work in Progress)","OA_place":"repository","OA_type":"green","date_published":"2024-02-01T00:00:00Z","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 and by a gift from Intel Corporation.","conference":{"start_date":"2024-02-14","end_date":"2024-02-15","name":"MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems","location":"Kaiserslautern, Germany"},"type":"conference","status":"public","_id":"17053","year":"2024","main_file_link":[{"url":"https://cca.informatik.uni-freiburg.de/papers/FroleyksYuBiere-MBMV24.pdf","open_access":"1"}],"article_processing_charge":"No","publication_identifier":{"isbn":["9783800762682"]},"month":"02","quality_controlled":"1","supplementarymaterial":"unclear","publication_status":"published","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","das_tickbox":"1","oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking."}],"publication":"27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems","day":"01"},{"article_processing_charge":"No","month":"05","publisher":"Figshare","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2026-10-21T11:57:04Z","oa_version":"None","fulldoi":"https://doi.org/10.6084/m9.figshare.24527848","citation":{"ista":"Zendrikov D, Paraskevov A. 2024. Supplementary Material for the article entitled ‘The vitals for steady nucleation maps of spontaneous spiking coherence in autonomous two-dimensional neuronal networks’, Figshare, <a href=\"https://doi.org/10.6084/m9.figshare.24527848\">10.6084/m9.figshare.24527848</a>.","ieee":"D. Zendrikov and A. Paraskevov, “Supplementary Material for the article entitled ‘The vitals for steady nucleation maps of spontaneous spiking coherence in autonomous two-dimensional neuronal networks.’” Figshare, 2024.","apa":"Zendrikov, D., &#38; Paraskevov, A. (2024). Supplementary Material for the article entitled “The vitals for steady nucleation maps of spontaneous spiking coherence in autonomous two-dimensional neuronal networks.” Figshare. <a href=\"https://doi.org/10.6084/m9.figshare.24527848\">https://doi.org/10.6084/m9.figshare.24527848</a>","ama":"Zendrikov D, Paraskevov A. Supplementary Material for the article entitled “The vitals for steady nucleation maps of spontaneous spiking coherence in autonomous two-dimensional neuronal networks.” 2024. doi:<a href=\"https://doi.org/10.6084/m9.figshare.24527848\">10.6084/m9.figshare.24527848</a>","chicago":"Zendrikov, Dmitrii, and Alexander Paraskevov. “Supplementary Material for the Article Entitled ‘The Vitals for Steady Nucleation Maps of Spontaneous Spiking Coherence in Autonomous Two-Dimensional Neuronal Networks.’” Figshare, 2024. <a href=\"https://doi.org/10.6084/m9.figshare.24527848\">https://doi.org/10.6084/m9.figshare.24527848</a>.","short":"D. Zendrikov, A. Paraskevov, (2024).","mla":"Zendrikov, Dmitrii, and Alexander Paraskevov. <i>Supplementary Material for the Article Entitled “The Vitals for Steady Nucleation Maps of Spontaneous Spiking Coherence in Autonomous Two-Dimensional Neuronal Networks.”</i> Figshare, 2024, doi:<a href=\"https://doi.org/10.6084/m9.figshare.24527848\">10.6084/m9.figshare.24527848</a>."},"abstract":[{"lang":"eng","text":"This online resource contains the simulation data and program codes required for reproducing all results of the study described in the article, and Supplementary Figures and Videos."}],"day":"01","doi":"10.6084/m9.figshare.24527848","ddc":["570"],"author":[{"last_name":"Zendrikov","full_name":"Zendrikov, Dmitrii","first_name":"Dmitrii"},{"full_name":"Paraskevov, Alexander","first_name":"Alexander","last_name":"Paraskevov"}],"OA_place":"repository","title":"Supplementary Material for the article entitled \"The vitals for steady nucleation maps of spontaneous spiking coherence in autonomous two-dimensional neuronal networks\"","oa":1,"OA_type":"green","date_published":"2024-05-01T00:00:00Z","status":"public","type":"research_data_reference","related_material":{"record":[{"status":"public","id":"17886","relation":"used_in_publication"}]},"year":"2024","_id":"23182","main_file_link":[{"open_access":"1","url":"https://doi.org/10.6084/m9.figshare.24527848"}],"department":[{"_id":"TiVo"}],"date_updated":"2026-10-21T11:57:09Z"},{"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8","citation":{"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>.","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>.","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.","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.","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>","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>"},"external_id":{"arxiv":["2407.06288"],"isi":["001556847400008"]},"corr_author":"1","intvolume":"       311","isi":1,"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"alternative_title":["LIPIcs"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2024-09-15T22:01:39Z","date_updated":"2026-10-21T12:17:18Z","language":[{"iso":"eng"}],"researchdata_availability":"no","department":[{"_id":"ToHe"}],"ddc":["000"],"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni"},{"last_name":"Goharshady","first_name":"Ehsan Kafshdar","full_name":"Goharshady, Ehsan Kafshdar"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","last_name":"Mallik"}],"oa":1,"arxiv":1,"ec_funded":1,"oa_version":"Published Version","das_tickbox":"0","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?"}],"publication":"35th International Conference on Concurrency Theory","file_date_updated":"2024-09-17T09:35:03Z","volume":311,"day":"01","doi":"10.4230/LIPIcs.CONCUR.2024.8","publication_identifier":{"isbn":["9783959773393"],"issn":["1868-8969"]},"article_processing_charge":"Yes","has_accepted_license":"1","quality_controlled":"1","month":"09","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"}],"publication_status":"published","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"end_date":"2024-09-13","name":"CONCUR: Conference on Concurrency Theory","location":"Calgary, Canada","start_date":"2024-09-09"},"date_published":"2024-09-01T00:00:00Z","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.","status":"public","type":"conference","file":[{"content_type":"application/pdf","date_created":"2024-09-17T09:35:03Z","success":1,"relation":"main_file","file_id":"18083","date_updated":"2024-09-17T09:35:03Z","checksum":"cb6f2254b84922cd7bf224f550b73f4a","file_name":"2024_LIPICS_Avni.pdf","file_size":854430,"access_level":"open_access","creator":"dernst"}],"year":"2024","_id":"18066","article_number":"8","scopus_import":"1","title":"Bidding games with charging"},{"alternative_title":["LIPIcs"],"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2024-09-15T22:01:40Z","citation":{"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>.","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.","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.","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>","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>"},"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12","corr_author":"1","external_id":{"arxiv":["2407.08620"],"isi":["001556847400012"]},"intvolume":"       311","isi":1,"ddc":["000"],"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi","first_name":"Udi","last_name":"Boker"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Lehtinen","full_name":"Lehtinen, Karoliina","first_name":"Karoliina"},{"last_name":"Prakash","first_name":"Aditya","full_name":"Prakash, Aditya"}],"arxiv":1,"oa":1,"ec_funded":1,"researchdata_availability":"no","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"date_updated":"2026-10-21T12:17:34Z","article_processing_charge":"No","has_accepted_license":"1","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773393"]},"month":"09","quality_controlled":"1","supplementarymaterial":"no","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","das_tickbox":"0","oa_version":"Published Version","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"}],"file_date_updated":"2024-09-17T07:31:18Z","volume":311,"publication":"35th International Conference on Concurrency Theory","doi":"10.4230/LIPIcs.CONCUR.2024.12","day":"01","scopus_import":"1","title":"History-determinism vs fair simulation","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)","date_published":"2024-09-01T00:00:00Z","conference":{"start_date":"2024-09-09","name":"CONCUR: Conference on Concurrency Theory","location":"Calgary, Canada","end_date":"2024-09-13"},"type":"conference","status":"public","_id":"18067","article_number":"12","year":"2024","file":[{"success":1,"relation":"main_file","date_created":"2024-09-17T07:31:18Z","content_type":"application/pdf","creator":"dernst","file_size":766902,"date_updated":"2024-09-17T07:31:18Z","checksum":"66db11ef8e600a434079c278050c3f09","file_name":"2024_LIPICS_Boker.pdf","file_id":"18080","access_level":"open_access"}]},{"file_date_updated":"2024-05-22T07:09:24Z","volume":14572,"publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","doi":"10.1007/978-3-031-57256-2_8","day":"05","das_tickbox":"0","oa_version":"Published Version","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"}],"supplementarymaterial":"no","publication_status":"published","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","has_accepted_license":"1","article_processing_charge":"Yes (in subscription journal)","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031572555"]},"month":"04","quality_controlled":"1","_id":"15376","year":"2024","file":[{"file_name":"2024_LNCS_Avni.pdf","file_id":"15414","checksum":"dbeb123510997886d11925aedbf9c400","date_updated":"2024-05-22T07:09:24Z","file_size":508191,"access_level":"open_access","creator":"dernst","content_type":"application/pdf","date_created":"2024-05-22T07:09:24Z","success":1,"relation":"main_file"}],"acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and by ISF grant no. 1679/21.","date_published":"2024-04-05T00:00:00Z","conference":{"start_date":"2024-04-06","end_date":"2024-04-11","location":"Luxembourg City, Luxembourg","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","status":"public","scopus_import":"1","title":"Auction-based scheduling","intvolume":"     14572","isi":1,"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>.","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.","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>.","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>","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>","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.","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."},"fulldoi":"https://doi.org/10.1007/978-3-031-57256-2_8","page":"153-172","external_id":{"arxiv":["2310.11798"],"isi":["001284187100008"]},"corr_author":"1","publisher":"Springer Nature","date_created":"2024-05-12T22:01:02Z","alternative_title":["LNCS"],"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"date_updated":"2026-10-21T12:16:28Z","language":[{"iso":"eng"}],"researchdata_availability":"no","department":[{"_id":"ToHe"}],"arxiv":1,"oa":1,"ec_funded":1,"ddc":["000"],"author":[{"orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni"},{"last_name":"Mallik","full_name":"Mallik, Kaushik","first_name":"Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"first_name":"Suman","full_name":"Sadhukhan, Suman","last_name":"Sadhukhan"}]},{"citation":{"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>.","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>.","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>","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."},"fulldoi":"https://doi.org/10.1007/978-3-031-63498-7_17","external_id":{"isi":["001273489700017"],"arxiv":["2405.04297"]},"page":"284-303","intvolume":"     14739","isi":1,"alternative_title":["LNCS"],"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publisher":"Springer Nature","date_created":"2024-08-11T22:01:13Z","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"researchdata_availability":"no","date_updated":"2026-10-21T12:03:11Z","ddc":["000"],"author":[{"full_name":"Froleyks, Nils","first_name":"Nils","last_name":"Froleyks"},{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi","first_name":"Zhengqi","orcid":"0000-0002-4993-773X","last_name":"Yu"},{"last_name":"Biere","full_name":"Biere, Armin","first_name":"Armin"},{"first_name":"Keijo","full_name":"Heljanko, Keijo","last_name":"Heljanko"}],"oa":1,"arxiv":1,"ec_funded":1,"das_tickbox":"0","oa_version":"Published Version","abstract":[{"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.","lang":"eng"}],"file_date_updated":"2024-08-12T06:53:39Z","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","volume":14739,"day":"01","doi":"10.1007/978-3-031-63498-7_17","has_accepted_license":"1","article_processing_charge":"Yes (in subscription journal)","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031634970"],"issn":["0302-9743"]},"month":"07","quality_controlled":"1","supplementarymaterial":"no","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","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.","date_published":"2024-07-01T00:00:00Z","conference":{"name":"IJCAR: International Joint Conference on Automated Reasoning","location":"Nancy, France","end_date":"2024-07-06","start_date":"2024-07-03"},"type":"conference","status":"public","_id":"17413","year":"2024","file":[{"success":1,"relation":"main_file","content_type":"application/pdf","date_created":"2024-08-12T06:53:39Z","creator":"dernst","file_name":"2024_LNCS_Froleyks.pdf","date_updated":"2024-08-12T06:53:39Z","checksum":"7d7839fc8c5c680ea3ac09f40a66e55d","file_id":"17414","file_size":556902,"access_level":"open_access"}],"scopus_import":"1","title":"Certifying phase abstraction"},{"quality_controlled":"1","month":"04","publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783031572562"],"isbn":["9783031572555"],"issn":["0302-9743"]},"has_accepted_license":"1","article_processing_charge":"Yes (in subscription journal)","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","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","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"publication_status":"published","supplementarymaterial":"no","abstract":[{"lang":"eng","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."}],"oa_version":"Published Version","das_tickbox":"1","doi":"10.1007/978-3-031-57256-2_20","day":"05","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","file_date_updated":"2024-04-26T11:27:26Z","volume":14572,"title":"Bubaak-SpLit: Split what you cannot verify (Competition contribution)","scopus_import":"1","status":"public","related_material":{"record":[{"relation":"research_data","id":"23183","status":"public"}]},"type":"conference","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Luxembourg City, Luxembourg","end_date":"2024-04-11","start_date":"2024-04-06"},"date_published":"2024-04-05T00:00:00Z","acknowledgement":"This work was partially supported by the ERC-2020-AdG 10102009 grant.","year":"2024","file":[{"relation":"main_file","success":1,"content_type":"application/pdf","date_created":"2024-04-26T11:27:26Z","creator":"cchlebak","access_level":"open_access","date_updated":"2024-04-26T11:27:26Z","file_name":"2024_LNCS_Chalupa.pdf","checksum":"208c855c60824bec936b8d01d0396474","file_id":"15347","file_size":577128}],"_id":"15333","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"alternative_title":["LNCS"],"date_created":"2024-04-20T18:14:06Z","publisher":"Springer Nature","external_id":{"isi":["001284187100020"]},"corr_author":"1","page":"353–358","fulldoi":"https://doi.org/10.1007/978-3-031-57256-2_20","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>.","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.","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>.","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>","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>","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.","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."},"isi":1,"intvolume":"     14572","author":[{"last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","first_name":"Marek"},{"last_name":"Richter","full_name":"Richter, Cedric","first_name":"Cedric"}],"ddc":["000"],"ec_funded":1,"oa":1,"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"researchdata_availability":"yes","date_updated":"2026-10-21T12:12:16Z"},{"ec_funded":1,"oa":1,"arxiv":1,"author":[{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"},{"last_name":"Sağlam","first_name":"Irmak","full_name":"Sağlam, Irmak"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","last_name":"Thejaswini"}],"ddc":["000"],"researchdata_availability":"no","department":[{"_id":"ToHe"}],"date_updated":"2026-10-21T12:16:56Z","language":[{"iso":"eng"}],"date_created":"2024-05-12T22:01:02Z","publisher":"Springer Nature","alternative_title":["LNCS"],"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"isi":1,"intvolume":"     14572","page":"213-231","external_id":{"isi":["001284187100011"],"arxiv":["2401.07548"]},"corr_author":"1","citation":{"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>.","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.","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>.","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.","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>","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>"},"fulldoi":"https://doi.org/10.1007/978-3-031-57256-2_11","title":"Rabin games and colourful universal trees","scopus_import":"1","_id":"15377","file":[{"creator":"dernst","file_size":462173,"file_name":"2024_LNCS_Majumdar.pdf","checksum":"492be74f69cd6ea42d38681082d0b521","date_updated":"2024-05-22T07:24:45Z","file_id":"15415","access_level":"open_access","success":1,"relation":"main_file","date_created":"2024-05-22T07:24:45Z","content_type":"application/pdf"}],"year":"2024","type":"conference","status":"public","date_published":"2024-04-06T00:00:00Z","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.","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","publication_status":"published","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"month":"04","quality_controlled":"1","article_processing_charge":"Yes (in subscription journal)","has_accepted_license":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031572555"],"eissn":["1611-3349"]},"day":"06","doi":"10.1007/978-3-031-57256-2_11","volume":14572,"file_date_updated":"2024-05-22T07:24:45Z","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","abstract":[{"lang":"eng","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."}],"das_tickbox":"0","oa_version":"Published Version"},{"year":"2024","_id":"17898","status":"public","type":"conference","conference":{"start_date":"2024-05-13","location":"Yokohama, Japan","name":"ICRA: International Conference on Robotics and Automation","end_date":"2024-05-17"},"date_published":"2024-08-08T00:00:00Z","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.","title":"Overparametrization helps offline-to-online generalization of closed-loop control from pixels","scopus_import":"1","day":"08","doi":"10.1109/ICRA57147.2024.10610284","publication":"Proceedings of the 2024 IEEE International Conference on Robotics and Automation","abstract":[{"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.","lang":"eng"}],"oa_version":"None","das_tickbox":"0","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_status":"published","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"supplementarymaterial":"no","quality_controlled":"1","month":"08","publication_identifier":{"issn":["1050-4729"],"isbn":["9798350384574"]},"article_processing_charge":"No","date_updated":"2026-10-21T12:03:35Z","researchdata_availability":"no","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"ec_funded":1,"author":[{"last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","first_name":"Mathias"},{"full_name":"Hasani, Ramin","first_name":"Ramin","last_name":"Hasani"},{"full_name":"Amini, Alexander","first_name":"Alexander","last_name":"Amini"},{"last_name":"Wang","first_name":"Tsun Hsuan","full_name":"Wang, Tsun Hsuan"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Rus","first_name":"Daniela","full_name":"Rus, Daniela"}],"isi":1,"page":"2774-2782","external_id":{"isi":["001294576202044"]},"fulldoi":"https://doi.org/10.1109/ICRA57147.2024.10610284","citation":{"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.","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>","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>","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.","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>.","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>."},"date_created":"2024-09-08T22:01:13Z","publisher":"IEEE"},{"oa_version":"Published Version","das_tickbox":"0","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"}],"volume":38,"publication":"Proceedings of the 38th AAAI Conference on Artificial Intelligence","issue":"9","doi":"10.1609/aaai.v38i9.28943","day":"25","publication_identifier":{"isbn":["1577358872"],"issn":["2159-5399"],"eissn":["2374-3468"]},"article_processing_charge":"No","quality_controlled":"1","month":"03","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","grant_number":"101034413"}],"publication_status":"published","supplementarymaterial":"yes","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","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.","date_published":"2024-03-25T00:00:00Z","status":"public","type":"conference","year":"2024","_id":"15321","main_file_link":[{"open_access":"1","url":"https://amu.hal.science/hal-04523118/"}],"scopus_import":"1","title":"Scalable enumeration of trap spaces in boolean networks via answer set programming","fulldoi":"https://doi.org/10.1609/aaai.v38i9.28943","citation":{"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>.","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>.","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.","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.","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>","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>"},"page":"10714-10722","intvolume":"        38","publisher":"Association for the Advancement of Artificial Intelligence","date_created":"2024-04-14T22:01:02Z","language":[{"iso":"eng"}],"researchdata_availability":"yes (supplementary data)","department":[{"_id":"ToHe"}],"date_updated":"2026-10-21T12:04:20Z","ddc":["000"],"author":[{"last_name":"Trinh","full_name":"Trinh, Giang","first_name":"Giang"},{"first_name":"Belaid","full_name":"Benhamou, Belaid","last_name":"Benhamou"},{"orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel","first_name":"Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","last_name":"Pastva"},{"full_name":"Soliman, Sylvain","first_name":"Sylvain","last_name":"Soliman"}],"oa":1,"ec_funded":1},{"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"alternative_title":["LNCS"],"publisher":"Springer Nature","date_created":"2024-11-10T23:01:58Z","fulldoi":"https://doi.org/10.1007/978-3-031-74234-7_18","citation":{"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>","ama":"Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. In: <i>24th International Conference on Runtime Verification</i>. Vol 15191. Springer Nature; 2024:282-301. doi:<a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">10.1007/978-3-031-74234-7_18</a>","ieee":"B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy,” in <i>24th International Conference on Runtime Verification</i>, Istanbul, Turkey, 2024, vol. 15191, pp. 282–301.","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.","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>.","short":"B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301.","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>."},"corr_author":"1","external_id":{"arxiv":["2408.05033"],"isi":["001420093700018"]},"page":"282-301","intvolume":"     15191","isi":1,"ddc":["000"],"author":[{"first_name":"Borzoo","full_name":"Bonakdarpour, Borzoo","last_name":"Bonakdarpour"},{"full_name":"Momtaz, Anik","first_name":"Anik","last_name":"Momtaz"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic"},{"last_name":"Sarac","full_name":"Sarac, Naci E","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"arxiv":1,"oa":1,"ec_funded":1,"department":[{"_id":"ToHe"},{"_id":"GradSch"}],"date_updated":"2026-10-21T13:14:54Z","researchdata_availability":"no","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783031742330"],"issn":["0302-9743"],"eissn":["1611-3349"]},"has_accepted_license":"1","article_processing_charge":"Yes (in subscription journal)","quality_controlled":"1","month":"10","publication_status":"published","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"Published Version","das_tickbox":"0","APC_amount":"2748 EUR","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."}],"publication":"24th International Conference on Runtime Verification","volume":15191,"file_date_updated":"2024-11-11T09:42:28Z","day":"12","doi":"10.1007/978-3-031-74234-7_18","scopus_import":"1","OA_place":"publisher","title":"Approximate distributed monitoring under partial synchrony: Balancing speed & accuracy","OA_type":"hybrid","conference":{"name":"RV: Conference on Runtime Verification","location":"Istanbul, Turkey","end_date":"2024-10-17","start_date":"2024-10-15"},"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).","date_published":"2024-10-12T00:00:00Z","status":"public","type":"conference","file":[{"date_created":"2024-11-11T09:42:28Z","content_type":"application/pdf","success":1,"relation":"main_file","file_size":1897101,"file_id":"18539","file_name":"2024_LNCS_Bonakdarpour.pdf","checksum":"7b8ca21b8c19ab796fa445b0e54003ca","date_updated":"2024-11-11T09:42:28Z","access_level":"open_access","creator":"dernst"}],"year":"2024","_id":"18521"},{"language":[{"iso":"eng"}],"department":[{"_id":"ToHe"},{"_id":"GradSch"}],"researchdata_availability":"no","date_updated":"2026-10-21T13:15:11Z","ec_funded":1,"oa":1,"arxiv":1,"author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"last_name":"Sarac","full_name":"Sarac, Naci E","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"ddc":["000"],"isi":1,"intvolume":"       311","external_id":{"arxiv":["2407.10473"],"isi":["001556847400029"]},"corr_author":"1","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29","citation":{"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.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance: A new preorder for nondeterministic processes,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder for nondeterministic processes. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">10.4230/LIPIcs.CONCUR.2024.29</a>","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.","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>.","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>."},"date_created":"2024-09-15T22:01:40Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"alternative_title":["LIPIcs"],"year":"2024","file":[{"access_level":"open_access","file_name":"2024_LIPICS_Henzinger.pdf","checksum":"555bd343e1fb38adeab8fc465ff4fad8","date_updated":"2024-09-17T07:48:56Z","file_id":"18081","file_size":964124,"creator":"dernst","content_type":"application/pdf","date_created":"2024-09-17T07:48:56Z","relation":"main_file","success":1}],"article_number":"29","_id":"18068","status":"public","type":"conference","conference":{"end_date":"2024-09-13","name":"CONCUR: Conference on Concurrency Theory","location":"Calgary, Canada","start_date":"2024-09-09"},"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.","date_published":"2024-09-01T00:00:00Z","OA_type":"gold","OA_place":"publisher","title":"Strategic dominance: A new preorder for nondeterministic processes","scopus_import":"1","doi":"10.4230/LIPIcs.CONCUR.2024.29","day":"01","volume":311,"file_date_updated":"2024-09-17T07:48:56Z","publication":"35th International Conference on Concurrency Theory","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."}],"oa_version":"Published Version","das_tickbox":"0","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_status":"published","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"supplementarymaterial":"no","quality_controlled":"1","month":"09","publication_identifier":{"isbn":["9783959773393"],"issn":["1868-8969"]},"has_accepted_license":"1","article_processing_charge":"Yes"},{"year":"2024","file":[{"file_size":1764222,"file_id":"18184","file_name":"2024_LIPICs_Maj.pdf","checksum":"2e75d305a8c817d76a0c7f136ce34f86","date_updated":"2024-10-07T11:10:55Z","access_level":"open_access","creator":"dernst","date_created":"2024-10-07T11:10:55Z","content_type":"application/pdf","success":1,"relation":"main_file"}],"article_number":"27","_id":"18175","conference":{"start_date":"2024-09-16","end_date":"2024-09-20","name":"ECOOP: European Conference on Object-Oriented Programming","location":"Vienna, Austria"},"date_published":"2024-09-01T00:00:00Z","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.","status":"public","type":"conference","scopus_import":"1","title":"The fault in our stars: Designing reproducible large-scale code analysis experiments","file_date_updated":"2024-10-07T11:10:55Z","publication":"38th European Conference on Object-Oriented Programming","volume":313,"doi":"10.4230/LIPIcs.ECOOP.2024.27","day":"01","oa_version":"Published Version","das_tickbox":"0","abstract":[{"lang":"eng","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."}],"publication_status":"published","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_identifier":{"isbn":["9783959773416"],"issn":["1868-8969"]},"has_accepted_license":"1","article_processing_charge":"No","quality_controlled":"1","month":"09","language":[{"iso":"eng"}],"date_updated":"2026-10-21T13:11:58Z","department":[{"_id":"ToHe"}],"researchdata_availability":"no","oa":1,"ddc":["000"],"author":[{"last_name":"Maj","first_name":"Petr","full_name":"Maj, Petr"},{"last_name":"Muroya Lei","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie","first_name":"Stefanie"},{"first_name":"Konrad","full_name":"Siek, Konrad","last_name":"Siek"},{"full_name":"Di Grazia, Luca","first_name":"Luca","last_name":"Di Grazia"},{"last_name":"Vitek","first_name":"Jan","full_name":"Vitek, Jan"}],"intvolume":"       313","isi":1,"fulldoi":"https://doi.org/10.4230/LIPIcs.ECOOP.2024.27","citation":{"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.","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.","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>","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>","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.","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>.","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>."},"external_id":{"isi":["001533999700027"]},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2024-10-06T22:01:12Z","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"alternative_title":["LIPIcs"]},{"article_processing_charge":"No","has_accepted_license":"1","publication_identifier":{"eissn":["1860-5974"]},"month":"10","quality_controlled":"1","supplementarymaterial":"no","project":[{"call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","das_tickbox":"0","oa_version":"Published Version","abstract":[{"lang":"eng","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."}],"issue":"4","file_date_updated":"2024-11-11T08:32:02Z","volume":20,"publication":"Logical Methods in Computer Science","doi":"10.46298/lmcs-20(4:1)2024","day":"02","scopus_import":"1","title":"History-deterministic timed automata","OA_place":"publisher","OA_type":"gold","date_published":"2024-10-02T00:00:00Z","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).","type":"journal_article","related_material":{"record":[{"status":"public","id":"12508","relation":"earlier_version"}]},"status":"public","_id":"18530","file":[{"file_name":"2024_LMCS_Bose.pdf","date_updated":"2024-11-11T08:32:02Z","checksum":"26826786a960039b9501cfc5cb4f3fe6","file_id":"18532","file_size":563394,"access_level":"open_access","creator":"dernst","content_type":"application/pdf","date_created":"2024-11-11T08:32:02Z","success":1,"relation":"main_file"}],"year":"2024","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publisher":"EPI Sciences","DOAJ_listed":"1","date_created":"2024-11-10T23:02:01Z","citation":{"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.","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.","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>","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>","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>.","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>."},"fulldoi":"https://doi.org/10.46298/lmcs-20(4:1)2024","page":"1-28","corr_author":"1","external_id":{"isi":["001332466900002"],"arxiv":["2304.03183"]},"intvolume":"        20","article_type":"original","isi":1,"ddc":["000"],"author":[{"last_name":"Bose","first_name":"Sougata","full_name":"Bose, Sougata"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Lehtinen","first_name":"Karoliina","full_name":"Lehtinen, Karoliina"},{"last_name":"Schewe","first_name":"Sven","full_name":"Schewe, Sven"},{"first_name":"Patrick","full_name":"Totzke, Patrick","last_name":"Totzke"}],"arxiv":1,"oa":1,"ec_funded":1,"language":[{"iso":"eng"}],"researchdata_availability":"no","date_updated":"2026-10-21T13:12:37Z","department":[{"_id":"ToHe"}]},{"date_created":"2025-01-29T11:55:50Z","publisher":"Society for Industrial and Applied Mathematics","page":"160-167","external_id":{"arxiv":["2310.20433"]},"fulldoi":"https://doi.org/10.1137/1.9781611977936.16","citation":{"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>","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>","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.","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.","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>.","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>.","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."},"author":[{"full_name":"Casares, Antonio","first_name":"Antonio","last_name":"Casares"},{"full_name":"Pilipczuk, Marcin","first_name":"Marcin","last_name":"Pilipczuk"},{"first_name":"Michał","full_name":"Pilipczuk, Michał","last_name":"Pilipczuk"},{"full_name":"Souza, Uéverton S.","first_name":"Uéverton S.","last_name":"Souza"},{"id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","full_name":"Thejaswini, K. S.","first_name":"K. S.","last_name":"Thejaswini"}],"ec_funded":1,"oa":1,"arxiv":1,"date_updated":"2026-10-21T13:13:33Z","language":[{"iso":"eng"}],"researchdata_availability":"no","department":[{"_id":"ToHe"}],"quality_controlled":"1","month":"01","publication_identifier":{"isbn":["9781611977936"]},"article_processing_charge":"No","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_status":"published","project":[{"call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"supplementarymaterial":"no","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."}],"oa_version":"Preprint","das_tickbox":"0","day":"01","doi":"10.1137/1.9781611977936.16","publication":"2024 Symposium on Simplicity in Algorithms","OA_place":"repository","title":"Simple and tight complexity lower bounds for solving Rabin games","scopus_import":"1","OA_type":"green","status":"public","type":"conference","conference":{"start_date":"2024-01-08","location":"Alexandria, VA, United States","name":"SOSA: Symposium on Simplicity in Algorithms","end_date":"2024-01-10"},"date_published":"2024-01-01T00:00:00Z","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.","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2310.20433","open_access":"1"}],"year":"2024","_id":"18955"},{"_id":"18599","year":"2024","type":"conference","status":"public","date_published":"2024-11-13T00:00:00Z","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, and by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.","OA_type":"closed access","title":"Monitoring extended hypernode logic","scopus_import":"1","day":"13","doi":"10.1007/978-3-031-76554-4_9","volume":15234,"publication":"Integrated Formal Methods","abstract":[{"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.","lang":"eng"}],"das_tickbox":"0","oa_version":"None","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","publication_status":"published","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"month":"11","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"isbn":["9783031765537"],"issn":["0302-9743"],"eissn":["1611-3349"]},"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"researchdata_availability":"no","date_updated":"2026-10-21T13:13:13Z","ec_funded":1,"author":[{"last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","orcid":"0000-0002-8741-5799","full_name":"Oliveira da Costa, Ana","first_name":"Ana","last_name":"Oliveira da Costa"}],"isi":1,"intvolume":"     15234","page":"151-171","external_id":{"isi":["001416640500009"]},"corr_author":"1","citation":{"short":"M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal Methods, Springer Nature, 2024, pp. 151–171.","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>.","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.","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.","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>","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>"},"fulldoi":"https://doi.org/10.1007/978-3-031-76554-4_9","date_created":"2024-12-01T23:01:52Z","publisher":"Springer Nature","alternative_title":["LNCS"]},{"author":[{"last_name":"Beneš","first_name":"Nikola","full_name":"Beneš, Nikola"},{"first_name":"Luboš","full_name":"Brim, Luboš","last_name":"Brim"},{"last_name":"Huvar","full_name":"Huvar, Ondřej","first_name":"Ondřej"},{"orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel","first_name":"Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","last_name":"Pastva"},{"first_name":"David","full_name":"Šafránek, David","last_name":"Šafránek"}],"ec_funded":1,"researchdata_availability":"no","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"date_updated":"2026-10-21T13:12:17Z","alternative_title":["LNBI"],"date_created":"2024-10-06T22:01:12Z","publisher":"Springer Nature","page":"19-26","external_id":{"isi":["001333144400002"]},"citation":{"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>","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>","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.","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.","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>.","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>.","short":"N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, in:, Computational Methods in Systems Biology, Springer Nature, 2024, pp. 19–26."},"fulldoi":"https://doi.org/10.1007/978-3-031-71671-3_2","isi":1,"intvolume":"     14971","title":"BNClassifier: Classifying boolean models by dynamic properties","scopus_import":"1","type":"conference","status":"public","date_published":"2024-09-19T00:00:00Z","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.","_id":"18177","year":"2024","month":"09","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031716706"],"eissn":["1611-3349"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","project":[{"name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","call_identifier":"H2020"}],"publication_status":"published","abstract":[{"lang":"eng","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."}],"das_tickbox":"0","oa_version":"None","day":"19","doi":"10.1007/978-3-031-71671-3_2","volume":14971,"publication":"Computational Methods in Systems Biology"},{"doi":"10.1007/978-3-031-73751-0_12","day":"23","publication":"Real Time and Such","volume":15230,"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."}],"das_tickbox":"0","oa_version":"None","series_title":"LNCS","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","publication_status":"published","month":"10","quality_controlled":"1","article_processing_charge":"No","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031737503"],"eissn":["1611-3349"],"eisbn":["9783031737510"]},"_id":"18563","year":"2024","type":"book_chapter","status":"public","date_published":"2024-10-23T00:00:00Z","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.","place":"Cham","OA_type":"closed access","title":"Reminiscences of a Real-Time Researcher","scopus_import":"1","intvolume":"     15230","corr_author":"1","page":"154-164","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>.","short":"T.A. Henzinger, in:, S. Graf, P. Pettersson, B. Steffen (Eds.), Real Time and Such, Springer Nature, Cham, 2024, pp. 154–164.","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>.","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>","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>","ista":"Henzinger TA. 2024.Reminiscences of a Real-Time Researcher. In: Real Time and Such. LNCS, vol. 15230, 154–164.","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."},"fulldoi":"https://doi.org/10.1007/978-3-031-73751-0_12","date_created":"2024-11-18T09:10:06Z","publisher":"Springer Nature","alternative_title":["LNCS"],"date_updated":"2026-10-21T13:12:56Z","language":[{"iso":"eng"}],"researchdata_availability":"no","department":[{"_id":"ToHe"}],"author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"editor":[{"last_name":"Graf","full_name":"Graf, Susanne","first_name":"Susanne"},{"first_name":"Paul","full_name":"Pettersson, Paul","last_name":"Pettersson"},{"last_name":"Steffen","first_name":"Bernhard","full_name":"Steffen, Bernhard"}]},{"scopus_import":"1","title":"Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs","conference":{"start_date":"2024-03-12","name":"STACS: Symposium on Theoretical Aspects of Computer Science","location":"Clermont-Ferrand, France","end_date":"2024-03-14"},"date_published":"2024-03-01T00:00:00Z","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).","status":"public","related_material":{"record":[{"relation":"later_version","status":"public","id":"22247"},{"relation":"dissertation_contains","status":"public","id":"20339"}]},"type":"conference","file":[{"access_level":"open_access","file_size":927290,"checksum":"0524d4189fd1ed08989546511343edf3","file_id":"15175","date_updated":"2024-03-25T07:44:30Z","file_name":"2024_LIPICs_Filakovsky.pdf","creator":"dernst","date_created":"2024-03-25T07:44:30Z","content_type":"application/pdf","relation":"main_file","success":1}],"year":"2024","_id":"15168","article_number":"34","publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959773119"]},"article_processing_charge":"No","has_accepted_license":"1","quality_controlled":"1","month":"03","publication_status":"published","project":[{"_id":"26611F5C-B435-11E9-9278-68D0E5697425","name":"Algorithms for Embeddings and Homotopy Theory","call_identifier":"FWF","grant_number":"P31312"},{"grant_number":"101034413","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"supplementarymaterial":"yes","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"Published Version","das_tickbox":"0","abstract":[{"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).","lang":"eng"}],"publication":"41st International Symposium on Theoretical Aspects of Computer Science","file_date_updated":"2024-03-25T07:44:30Z","volume":289,"day":"01","doi":"10.4230/LIPIcs.STACS.2024.34","ddc":["510"],"author":[{"first_name":"Marek","full_name":"Filakovský, Marek","id":"3E8AF77E-F248-11E8-B48F-1D18A9856A87","last_name":"Filakovský"},{"full_name":"Nakajima, Tamio Vesa","first_name":"Tamio Vesa","last_name":"Nakajima"},{"orcid":"0000-0003-1245-3456","first_name":"Jakub","full_name":"Opršal, Jakub","id":"ec596741-c539-11ec-b829-c79322a91242","last_name":"Opršal"},{"last_name":"Tasinato","full_name":"Tasinato, Gianluca","first_name":"Gianluca","id":"0433290C-AF8F-11E9-A4C7-F729E6697425"},{"last_name":"Wagner","orcid":"0000-0002-1494-0568","first_name":"Uli","full_name":"Wagner, Uli","id":"36690CA2-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"arxiv":1,"ec_funded":1,"language":[{"iso":"eng"}],"researchdata_availability":"yes","department":[{"_id":"UlWa"}],"date_updated":"2026-10-21T13:23:55Z","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"alternative_title":["LIPIcs"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2024-03-24T23:00:59Z","fulldoi":"https://doi.org/10.4230/LIPIcs.STACS.2024.34","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.","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.","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>","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>","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>.","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.","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>."},"external_id":{"isi":["001300393400034"],"arxiv":["2312.12981"]},"corr_author":"1","intvolume":"       289","isi":1}]