[{"volume":51,"acknowledgement":"We thank Daniel Hausmann and Nir Piterman for their valuable comments on an earlier version of the manuscript of our other paper [22] where we present, among other things, the parity fixpoint for 2 1/2-player games (for a slightly more general class of games) with a different and indirect proof of correctness. Based on their comments we observed that, unlike the other fixpoints that we present in [22], the parity fixpoint does not follow the exact same structure as its counterpart for 2-player games, which we also use int his paper.\r\nWe also thank Thejaswini Raghavan for observing that our symbolic parity fixpoint algorithm can be solved in quasi-polynomial time using recent improved algorithms for solving \r\n-calculus expressions. This significantly improved the complexity bounds of our algorithm in this paper.\r\nThe work of R. Majumdar and A.-K. Schmuck are partially supported by DFG, Germany project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG, Germany project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","day":"27","doi":"10.1016/j.nahs.2023.101430","arxiv":1,"abstract":[{"lang":"eng","text":"We consider the problem of computing the maximal probability of satisfying an \r\n-regular specification for stochastic, continuous-state, nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almost surely, and (II) computing the maximal probability of reaching this qualitative winning region.\r\nThe heart of our approach is a technique to symbolically compute the under-approximation of the qualitative winning region in step (I) via a finite-state abstraction of the original system as a \r\n-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We prove that the winning set in the abstract -player game induces an under-approximation of the qualitative winning region in the original synthesis problem, along with a policy to solve it. By combining these contributions with (a) a symbolic fixpoint algorithm to solve \r\n-player games and (b) existing techniques for reachability policy synthesis in stochastic nonlinear systems, we get an abstraction-based algorithm for finding a lower bound on the maximal satisfaction probability.\r\nWe have implemented the abstraction-based algorithm in Mascot-SDS, where we combined the outlined abstraction step with our tool Genie (Majumdar et al., 2023) that solves \r\n-player parity games (through a reduction to Rabin games) more efficiently than existing algorithms. We evaluated our implementation on the nonlinear model of a perturbed bistable switch from the literature. We show empirically that the lower bound on the winning region computed by our approach is precise, by comparing against an over-approximation of the qualitative winning region. Moreover, our implementation outperforms a recently proposed tool for solving this problem by a large margin."}],"year":"2023","citation":{"ieee":"R. Majumdar, K. Mallik, A. K. Schmuck, and S. Soudjani, “Symbolic control for stochastic systems via finite parity games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51. Elsevier, 2023.","chicago":"Majumdar, Rupak, Kaushik Mallik, Anne Kathrin Schmuck, and Sadegh Soudjani. “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2023. <a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">https://doi.org/10.1016/j.nahs.2023.101430</a>.","apa":"Majumdar, R., Mallik, K., Schmuck, A. K., &#38; Soudjani, S. (2023). Symbolic control for stochastic systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">https://doi.org/10.1016/j.nahs.2023.101430</a>","ama":"Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2023;51. doi:<a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">10.1016/j.nahs.2023.101430</a>","ista":"Majumdar R, Mallik K, Schmuck AK, Soudjani S. 2023. Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 51, 101430.","short":"R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid Systems 51 (2023).","mla":"Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51, 101430, Elsevier, 2023, doi:<a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">10.1016/j.nahs.2023.101430</a>."},"date_updated":"2023-12-13T12:58:56Z","external_id":{"arxiv":["2101.00834"],"isi":["001093188100001"]},"isi":1,"publisher":"Elsevier","article_type":"original","quality_controlled":"1","ec_funded":1,"department":[{"_id":"ToHe"}],"date_created":"2023-10-08T22:01:15Z","article_processing_charge":"No","publication_status":"epub_ahead","intvolume":"        51","title":"Symbolic control for stochastic systems via finite parity games","scopus_import":"1","_id":"14400","author":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"first_name":"Anne Kathrin","last_name":"Schmuck","full_name":"Schmuck, Anne Kathrin"},{"last_name":"Soudjani","first_name":"Sadegh","full_name":"Soudjani, Sadegh"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.nahs.2023.101430"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["1751-570X"]},"oa":1,"type":"journal_article","date_published":"2023-09-27T00:00:00Z","language":[{"iso":"eng"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"oa_version":"Published Version","article_number":"101430","month":"09","publication":"Nonlinear Analysis: Hybrid Systems"},{"external_id":{"arxiv":["2305.02836"]},"date_updated":"2023-10-09T07:43:44Z","year":"2023","citation":{"short":"E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, 34th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.","mla":"Bartocci, Ezio, et al. “Hypernode Automata.” <i>34th International Conference on Concurrency Theory</i>, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">10.4230/LIPIcs.CONCUR.2023.21</a>.","ista":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2023. Hypernode automata. 34th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 21.","ama":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. In: <i>34th International Conference on Concurrency Theory</i>. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">10.4230/LIPIcs.CONCUR.2023.21</a>","apa":"Bartocci, E., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2023). Hypernode automata. In <i>34th International Conference on Concurrency Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.21</a>","chicago":"Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” In <i>34th International Conference on Concurrency Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.21</a>.","ieee":"E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” in <i>34th International Conference on Concurrency Theory</i>, Antwerp, Belgium, 2023, vol. 279."},"abstract":[{"text":"We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automata. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs.","lang":"eng"}],"doi":"10.4230/LIPIcs.CONCUR.2023.21","arxiv":1,"day":"01","ddc":["000"],"acknowledgement":"This work was supported in part by the Austrian Science Fund (FWF) SFB project\r\nSpyCoDe F8502, by the FWF projects ZK-35 and W1255-N23, and by the ERC Advanced Grant\r\nVAMOS 101020093.","volume":279,"author":[{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"},{"id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","last_name":"Oliveira da Costa","first_name":"Ana","full_name":"Oliveira da Costa, Ana","orcid":"0000-0002-8741-5799"}],"_id":"14405","scopus_import":"1","alternative_title":["LIPIcs"],"title":"Hypernode automata","intvolume":"       279","publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"Yes","date_created":"2023-10-08T22:01:16Z","file_date_updated":"2023-10-09T07:42:45Z","quality_controlled":"1","ec_funded":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2023-09-01T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783959772990"],"issn":["18688969"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"file_name":"2023_LIPcs_Bartocci.pdf","content_type":"application/pdf","date_updated":"2023-10-09T07:42:45Z","file_size":795790,"checksum":"215765e40454d806174ac0a223e8d6fa","date_created":"2023-10-09T07:42:45Z","creator":"dernst","file_id":"14413","success":1,"relation":"main_file","access_level":"open_access"}],"publication":"34th International Conference on Concurrency Theory","has_accepted_license":"1","month":"09","article_number":"21","oa_version":"Published Version","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"language":[{"iso":"eng"}],"conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2023-09-19","end_date":"2023-09-22","location":"Antwerp, Belgium"}},{"volume":14137,"acknowledgement":"This work was supported by the Czech Foundation grant No. GA22-10845S, Grant Agency of Masaryk University grant No. MUNI/G/1771/2020, and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413.","ddc":["000"],"day":"09","doi":"10.1007/978-3-031-42697-1_2","abstract":[{"lang":"eng","text":"Partially specified Boolean networks (PSBNs) represent a promising framework for the qualitative modelling of biological systems in which the logic of interactions is not completely known. Phenotype control aims to stabilise the network in states exhibiting specific traits.\r\nIn this paper, we define the phenotype control problem in the context of asynchronous PSBNs and propose a novel semi-symbolic algorithm for solving this problem with permanent variable perturbations."}],"year":"2023","citation":{"mla":"Beneš, Nikola, et al. “Phenotype Control of Partially Specified Boolean Networks.” <i>21st International Conference on Computational Methods in Systems Biology</i>, vol. 14137, Springer Nature, 2023, pp. 18–35, doi:<a href=\"https://doi.org/10.1007/978-3-031-42697-1_2\">10.1007/978-3-031-42697-1_2</a>.","short":"N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková, in:, 21st International Conference on Computational Methods in Systems Biology, Springer Nature, 2023, pp. 18–35.","ista":"Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. 2023. Phenotype control of partially specified boolean networks. 21st International Conference on Computational Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNBI, vol. 14137, 18–35.","ama":"Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially specified boolean networks. In: <i>21st International Conference on Computational Methods in Systems Biology</i>. Vol 14137. Springer Nature; 2023:18-35. doi:<a href=\"https://doi.org/10.1007/978-3-031-42697-1_2\">10.1007/978-3-031-42697-1_2</a>","apa":"Beneš, N., Brim, L., Pastva, S., Šafránek, D., &#38; Šmijáková, E. (2023). Phenotype control of partially specified boolean networks. In <i>21st International Conference on Computational Methods in Systems Biology</i> (Vol. 14137, pp. 18–35). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-42697-1_2\">https://doi.org/10.1007/978-3-031-42697-1_2</a>","chicago":"Beneš, Nikola, Luboš Brim, Samuel Pastva, David Šafránek, and Eva Šmijáková. “Phenotype Control of Partially Specified Boolean Networks.” In <i>21st International Conference on Computational Methods in Systems Biology</i>, 14137:18–35. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-42697-1_2\">https://doi.org/10.1007/978-3-031-42697-1_2</a>.","ieee":"N. Beneš, L. Brim, S. Pastva, D. Šafránek, and E. Šmijáková, “Phenotype control of partially specified boolean networks,” in <i>21st International Conference on Computational Methods in Systems Biology</i>, Luxembourg City, Luxembourg, 2023, vol. 14137, pp. 18–35."},"date_updated":"2024-02-20T09:02:04Z","publisher":"Springer Nature","ec_funded":1,"quality_controlled":"1","page":"18-35","file_date_updated":"2024-02-16T08:26:32Z","date_created":"2023-10-08T22:01:18Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","intvolume":"     14137","alternative_title":["LNBI"],"title":"Phenotype control of partially specified boolean networks","scopus_import":"1","_id":"14411","author":[{"first_name":"Nikola","last_name":"Beneš","full_name":"Beneš, Nikola"},{"full_name":"Brim, Luboš","first_name":"Luboš","last_name":"Brim"},{"first_name":"Samuel","last_name":"Pastva","orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b"},{"full_name":"Šafránek, David","first_name":"David","last_name":"Šafránek"},{"last_name":"Šmijáková","first_name":"Eva","full_name":"Šmijáková, Eva"}],"file":[{"creator":"spastva","file_id":"14997","access_level":"open_access","success":1,"relation":"main_file","content_type":"application/pdf","file_name":"cmsb2023.pdf","date_updated":"2024-02-16T08:26:32Z","file_size":691582,"checksum":"6f71bdaedb770b52380222fd9f4d7937","date_created":"2024-02-16T08:26:32Z"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031426964"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2023-09-09T00:00:00Z","conference":{"start_date":"2023-09-13","name":"CMSB: Computational Methods in Systems Biology","end_date":"2023-09-15","location":"Luxembourg City, Luxembourg"},"language":[{"iso":"eng"}],"project":[{"grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"oa_version":"Submitted Version","month":"09","has_accepted_license":"1","publication":"21st International Conference on Computational Methods in Systems Biology"},{"acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","volume":14245,"day":"01","arxiv":1,"doi":"10.1007/978-3-031-44267-4_15","abstract":[{"text":"As AI and machine-learned software are used increasingly for making decisions that affect humans, it is imperative that they remain fair and unbiased in their decisions. To complement design-time bias mitigation measures, runtime verification techniques have been introduced recently to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of the states of the (unknown) monitored system. Moreover, they can monitor only fairness properties that are specified as arithmetic expressions over the probabilities of different events. In this work, we extend fairness monitoring to systems modeled as partially observed Markov chains (POMC), and to specifications containing arithmetic expressions over the expected values of numerical functions on event sequences. The only assumptions we make are that the underlying POMC is aperiodic and starts in the stationary distribution, with a bound on its mixing time being known. These assumptions enable us to estimate a given property for the entire distribution of possible executions of the monitored POMC, by observing only a single execution. Our monitors observe a long run of the system and, after each new observation, output updated PAC-estimates of how fair or biased the system is. The monitors are computationally lightweight and, using a prototype implementation, we demonstrate their effectiveness on several real-world examples.","lang":"eng"}],"year":"2023","citation":{"ista":"Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness under partial observations. 23rd International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.","short":"T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference on Runtime Verification, Springer Nature, 2023, pp. 291–311.","mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial Observations.” <i>23rd International Conference on Runtime Verification</i>, vol. 14245, Springer Nature, 2023, pp. 291–311, doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">10.1007/978-3-031-44267-4_15</a>.","chicago":"Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness under Partial Observations.” In <i>23rd International Conference on Runtime Verification</i>, 14245:291–311. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">https://doi.org/10.1007/978-3-031-44267-4_15</a>.","ieee":"T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness under partial observations,” in <i>23rd International Conference on Runtime Verification</i>, Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311.","apa":"Henzinger, T. A., Kueffner, K., &#38; Mallik, K. (2023). Monitoring algorithmic fairness under partial observations. In <i>23rd International Conference on Runtime Verification</i> (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">https://doi.org/10.1007/978-3-031-44267-4_15</a>","ama":"Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under partial observations. In: <i>23rd International Conference on Runtime Verification</i>. Vol 14245. Springer Nature; 2023:291-311. doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">10.1007/978-3-031-44267-4_15</a>"},"date_updated":"2023-10-31T11:48:20Z","external_id":{"arxiv":["2308.00341"]},"publisher":"Springer Nature","quality_controlled":"1","ec_funded":1,"page":"291-311","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2023-10-29T23:01:15Z","publication_status":"published","intvolume":"     14245","alternative_title":["LNCS"],"title":"Monitoring algorithmic fairness under partial observations","scopus_import":"1","_id":"14454","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","first_name":"Konstantin","last_name":"Kueffner"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2308.00341","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","publication_identifier":{"isbn":["9783031442667"],"issn":["0302-9743"],"eissn":["1611-3349"]},"oa":1,"type":"conference","date_published":"2023-10-01T00:00:00Z","conference":{"end_date":"2023-10-06","location":"Thessaloniki, Greece","name":"RV: Conference on Runtime Verification","start_date":"2023-10-03"},"language":[{"iso":"eng"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"oa_version":"Preprint","month":"10","publication":"23rd International Conference on Runtime Verification"},{"language":[{"iso":"eng"}],"conference":{"name":"ECAI: European Conference on Artificial Intelligence","start_date":"2023-09-30","end_date":"2023-10-04","location":"Krakow, Poland"},"publication":"Frontiers in Artificial Intelligence and Applications","has_accepted_license":"1","month":"09","oa_version":"Published Version","project":[{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"file_id":"14529","creator":"dernst","relation":"main_file","success":1,"access_level":"open_access","date_updated":"2023-11-13T10:16:10Z","file_name":"2023_FAIA_Avni.pdf","content_type":"application/pdf","date_created":"2023-11-13T10:16:10Z","checksum":"1390ca38480fa4cf286b0f1a42e8c12f","file_size":501011}],"date_published":"2023-09-28T00:00:00Z","type":"conference","tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode"},"oa":1,"publication_identifier":{"issn":["0922-6389"],"isbn":["9781643684369"]},"file_date_updated":"2023-11-13T10:16:10Z","page":"141-148","ec_funded":1,"quality_controlled":"1","publisher":"IOS Press","author":[{"first_name":"Guy","last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"},{"full_name":"Sadhukhan, Suman","last_name":"Sadhukhan","first_name":"Suman"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","first_name":"Josef"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699"}],"_id":"14518","scopus_import":"1","license":"https://creativecommons.org/licenses/by-nc/4.0/","title":"Reachability poorman discrete-bidding games","intvolume":"       372","publication_status":"published","article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2023-11-12T23:00:56Z","ddc":["000"],"acknowledgement":"This research was supported in part by ISF grant no. 1679/21, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie Grant Agreement No. 665385.","volume":372,"external_id":{"arxiv":["2307.15218"]},"date_updated":"2025-07-14T09:09:57Z","year":"2023","citation":{"mla":"Avni, Guy, et al. “Reachability Poorman Discrete-Bidding Games.” <i>Frontiers in Artificial Intelligence and Applications</i>, vol. 372, IOS Press, 2023, pp. 141–48, doi:<a href=\"https://doi.org/10.3233/FAIA230264\">10.3233/FAIA230264</a>.","short":"G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, D. Zikelic, in:, Frontiers in Artificial Intelligence and Applications, IOS Press, 2023, pp. 141–148.","ista":"Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications. ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.","ama":"Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. Reachability poorman discrete-bidding games. In: <i>Frontiers in Artificial Intelligence and Applications</i>. Vol 372. IOS Press; 2023:141-148. doi:<a href=\"https://doi.org/10.3233/FAIA230264\">10.3233/FAIA230264</a>","apa":"Avni, G., Meggendorfer, T., Sadhukhan, S., Tkadlec, J., &#38; Zikelic, D. (2023). Reachability poorman discrete-bidding games. In <i>Frontiers in Artificial Intelligence and Applications</i> (Vol. 372, pp. 141–148). Krakow, Poland: IOS Press. <a href=\"https://doi.org/10.3233/FAIA230264\">https://doi.org/10.3233/FAIA230264</a>","chicago":"Avni, Guy, Tobias Meggendorfer, Suman Sadhukhan, Josef Tkadlec, and Dorde Zikelic. “Reachability Poorman Discrete-Bidding Games.” In <i>Frontiers in Artificial Intelligence and Applications</i>, 372:141–48. IOS Press, 2023. <a href=\"https://doi.org/10.3233/FAIA230264\">https://doi.org/10.3233/FAIA230264</a>.","ieee":"G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, and D. Zikelic, “Reachability poorman discrete-bidding games,” in <i>Frontiers in Artificial Intelligence and Applications</i>, Krakow, Poland, 2023, vol. 372, pp. 141–148."},"abstract":[{"lang":"eng","text":"We consider bidding games, a class of two-player zero-sum graph games. The game proceeds as follows. Both players have bounded budgets. A token is placed on a vertex of a graph, in each turn the players simultaneously submit bids, and the higher bidder moves the token, where we break bidding ties in favor of Player 1. Player 1 wins the game iff the token visits a designated target vertex. We consider, for the first time, poorman discrete-bidding in which the granularity of the bids is restricted and the higher bid is paid to the bank. Previous work either did not impose granularity restrictions or considered Richman bidding (bids are paid to the opponent). While the latter mechanisms are technically more accessible, the former is more appealing from a practical standpoint. Our study focuses on threshold budgets, which is the necessary and sufficient initial budget required for Player 1 to ensure winning against a given Player 2 budget. We first show existence of thresholds. In DAGs, we show that threshold budgets can be approximated with error bounds by thresholds under continuous-bidding and that they exhibit a periodic behavior. We identify closed-form solutions in special cases. We implement and experiment with an algorithm to find threshold budgets."}],"doi":"10.3233/FAIA230264","arxiv":1,"day":"28"},{"intvolume":"     14215","title":"Learning provably stabilizing neural controllers for discrete-time stochastic systems","alternative_title":["LNCS"],"date_created":"2023-11-19T23:00:56Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","publication_status":"published","author":[{"full_name":"Ansaripour, Matin","last_name":"Ansaripour","first_name":"Matin"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic"}],"scopus_import":"1","_id":"14559","publisher":"Springer Nature","ec_funded":1,"quality_controlled":"1","page":"357-379","abstract":[{"lang":"eng","text":"We consider the problem of learning control policies in discrete-time stochastic systems which guarantee that the system stabilizes within some specified stabilization region with probability 1. Our approach is based on the novel notion of stabilizing ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome the limitation of methods proposed in previous works whose applicability is restricted to systems in which the stabilizing region cannot be left once entered under any control policy. We present a learning procedure that learns a control policy together with an sRSM that formally certifies probability 1 stability, both learned as neural networks. We show that this procedure can also be adapted to formally verifying that, under a given Lipschitz continuous control policy, the stochastic system stabilizes within some stabilizing region with probability 1. Our experimental evaluation shows that our learning procedure can successfully learn provably stabilizing policies in practice."}],"day":"22","doi":"10.1007/978-3-031-45329-8_17","year":"2023","citation":{"ista":"Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning provably stabilizing neural controllers for discrete-time stochastic systems. 21st International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.","short":"M. Ansaripour, K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, 21st International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2023, pp. 357–379.","mla":"Ansaripour, Matin, et al. “Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems.” <i>21st International Symposium on Automated Technology for Verification and Analysis</i>, vol. 14215, Springer Nature, 2023, pp. 357–79, doi:<a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">10.1007/978-3-031-45329-8_17</a>.","ieee":"M. Ansaripour, K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “Learning provably stabilizing neural controllers for discrete-time stochastic systems,” in <i>21st International Symposium on Automated Technology for Verification and Analysis</i>, Singapore, Singapore, 2023, vol. 14215, pp. 357–379.","chicago":"Ansaripour, Matin, Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems.” In <i>21st International Symposium on Automated Technology for Verification and Analysis</i>, 14215:357–79. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">https://doi.org/10.1007/978-3-031-45329-8_17</a>.","ama":"Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. Learning provably stabilizing neural controllers for discrete-time stochastic systems. In: <i>21st International Symposium on Automated Technology for Verification and Analysis</i>. Vol 14215. Springer Nature; 2023:357-379. doi:<a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">10.1007/978-3-031-45329-8_17</a>","apa":"Ansaripour, M., Chatterjee, K., Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2023). Learning provably stabilizing neural controllers for discrete-time stochastic systems. In <i>21st International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 14215, pp. 357–379). Singapore, Singapore: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">https://doi.org/10.1007/978-3-031-45329-8_17</a>"},"date_updated":"2025-07-14T09:09:59Z","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","volume":14215,"month":"10","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"oa_version":"None","publication":"21st International Symposium on Automated Technology for Verification and Analysis","conference":{"location":"Singapore, Singapore","end_date":"2023-10-27","start_date":"2023-10-24","name":"ATVA: Automated Technology for Verification and Analysis"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031453281"]},"type":"conference","date_published":"2023-10-22T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public"},{"author":[{"id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","first_name":"Samuel","last_name":"Pastva","orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","_id":"14718","title":"Binary decision diagrams on modern hardware","date_created":"2023-12-31T23:01:03Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","file_date_updated":"2024-01-02T08:14:23Z","ec_funded":1,"quality_controlled":"1","page":"122-131","publisher":"TU Vienna Academic Press","year":"2023","citation":{"ieee":"S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,” in <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>, Ames, IA, United States, 2023, pp. 122–131.","chicago":"Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern Hardware.” In <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>, 122–31. TU Vienna Academic Press, 2023. <a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20</a>.","apa":"Pastva, S., &#38; Henzinger, T. A. (2023). Binary decision diagrams on modern hardware. In <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i> (pp. 122–131). Ames, IA, United States: TU Vienna Academic Press. <a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20</a>","ama":"Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>. TU Vienna Academic Press; 2023:122-131. doi:<a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">10.34727/2023/isbn.978-3-85448-060-0_20</a>","ista":"Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware. Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. FMCAD: Conference on Formal Methods in Computer-aided design, 122–131.","short":"S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–131.","mla":"Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern Hardware.” <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>, TU Vienna Academic Press, 2023, pp. 122–31, doi:<a href=\"https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20\">10.34727/2023/isbn.978-3-85448-060-0_20</a>."},"date_updated":"2024-01-02T08:16:28Z","abstract":[{"text":"Binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores. ","lang":"eng"}],"day":"01","doi":"10.34727/2023/isbn.978-3-85448-060-0_20","ddc":["000"],"acknowledgement":"This work was supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413 and the\r\n“VAMOS” grant ERC-2020-AdG 101020093.","has_accepted_license":"1","publication":"Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design","month":"10","project":[{"name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"start_date":"2023-10-25","name":"FMCAD: Conference on Formal Methods in Computer-aided design","location":"Ames, IA, United States","end_date":"2023-10-27"},"type":"conference","date_published":"2023-10-01T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783854480600"]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"success":1,"relation":"main_file","access_level":"open_access","creator":"dernst","file_id":"14721","file_size":524321,"checksum":"818d6e13dd508f3a04f0941081022e5d","date_created":"2024-01-02T08:14:23Z","file_name":"2023_FMCAD_Pastva.pdf","content_type":"application/pdf","date_updated":"2024-01-02T08:14:23Z"}]},{"file":[{"checksum":"1a361d83db0244fd32c03b544c294b5a","file_size":405147,"date_created":"2024-01-09T10:01:07Z","file_name":"2023_LNCSCAV_Majumdar.pdf","content_type":"application/pdf","date_updated":"2024-01-09T10:01:07Z","success":1,"relation":"main_file","access_level":"open_access","creator":"dernst","file_id":"14765"}],"status":"public","related_material":{"record":[{"relation":"research_data","id":"14994","status":"public"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2023-07-16T00:00:00Z","type":"conference","publication_identifier":{"eisbn":["9783031377099"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031377082"]},"oa":1,"language":[{"iso":"eng"}],"conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","end_date":"2023-07-22","location":"Paris, France"},"publication":"35th International Conference on Computer Aided Verification","has_accepted_license":"1","oa_version":"Published Version","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"month":"07","acknowledgement":"Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","volume":13966,"ddc":["000"],"date_updated":"2024-02-27T07:39:51Z","citation":{"chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” In <i>35th International Conference on Computer Aided Verification</i>, 13966:3–15. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>.","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties,” in <i>35th International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 3–15.","ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: <i>35th International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:3-15. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>","apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In <i>35th International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 3–15). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 3–15.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 3–15.","mla":"Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” <i>35th International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>."},"year":"2023","doi":"10.1007/978-3-031-37709-9_1","day":"16","abstract":[{"lang":"eng","text":"We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings."}],"page":"3-15","quality_controlled":"1","ec_funded":1,"file_date_updated":"2024-01-09T10:01:07Z","publisher":"Springer Nature","_id":"14758","scopus_import":"1","author":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"first_name":"Mateusz","last_name":"Rychlicki","full_name":"Rychlicki, Mateusz"},{"full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck","first_name":"Anne-Kathrin"},{"full_name":"Soudjani, Sadegh","last_name":"Soudjani","first_name":"Sadegh"}],"publication_status":"published","article_processing_charge":"Yes (in subscription journal)","date_created":"2024-01-08T13:18:00Z","department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","intvolume":"     13966"},{"publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","month":"06","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program","grant_number":"665385"}],"oa_version":"Preprint","keyword":["General Medicine"],"language":[{"iso":"eng"}],"conference":{"end_date":"2023-02-14","location":"Washington, DC, United States","name":"AAAI: Conference on Artificial Intelligence","start_date":"2023-02-07"},"type":"conference","date_published":"2023-06-26T00:00:00Z","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"related_material":{"record":[{"id":"14600","relation":"earlier_version","status":"public"}]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"10","author":[{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"}],"_id":"14830","intvolume":"        37","title":"Learning control policies for stochastic systems with reach-avoid guarantees","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2024-01-18T07:44:31Z","article_processing_charge":"No","publication_status":"published","ec_funded":1,"quality_controlled":"1","page":"11926-11935","publisher":"Association for the Advancement of Artificial Intelligence","external_id":{"arxiv":["2210.05308"]},"citation":{"chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>.","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935.","apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935.","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>."},"year":"2023","date_updated":"2025-07-14T09:10:02Z","abstract":[{"text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.","lang":"eng"}],"day":"26","arxiv":1,"doi":"10.1609/aaai.v37i10.26407","volume":37,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385."},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"journal_article","date_published":"2023-02-24T00:00:00Z","publication_identifier":{"issn":["2751-4838"]},"oa":1,"file":[{"file_id":"14940","creator":"dernst","relation":"main_file","access_level":"open_access","success":1,"date_updated":"2024-02-05T10:19:35Z","content_type":"application/pdf","file_name":"2023_TheoretiCS_Banerjee.pdf","date_created":"2024-02-05T10:19:35Z","file_size":917076,"checksum":"2972d531122a6f15727b396110fb3f5c"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","has_accepted_license":"1","publication":"TheoretiCS","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"oa_version":"Published Version","article_number":"4","month":"02","language":[{"iso":"eng"}],"citation":{"ista":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic algorithms for mega-regular games under strong transition fairness. TheoretiCS. 2, 4.","short":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS 2 (2023).","mla":"Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>, vol. 2, 4, EPI Sciences, 2023, doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>.","chicago":"Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>. EPI Sciences, 2023. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>.","ieee":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast symbolic algorithms for mega-regular games under strong transition fairness,” <i>TheoretiCS</i>, vol. 2. EPI Sciences, 2023.","ama":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. 2023;2. doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>","apa":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., &#38; Soudjani, S. (2023). Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>"},"year":"2023","date_updated":"2024-02-05T10:21:51Z","external_id":{"arxiv":["2202.07480"]},"day":"24","arxiv":1,"doi":"10.46298/theoretics.23.4","abstract":[{"lang":"eng","text":"We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the\r\nsource vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude."}],"acknowledgement":"A previous version of this paper has appeared in TACAS 2022. Authors ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research was conducted. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093.","volume":2,"ddc":["000"],"_id":"14920","author":[{"first_name":"Tamajit","last_name":"Banerjee","full_name":"Banerjee, Tamajit"},{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"first_name":"Anne-Kathrin","last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin"},{"first_name":"Sadegh","last_name":"Soudjani","full_name":"Soudjani, Sadegh"}],"date_created":"2024-01-31T13:40:49Z","department":[{"_id":"ToHe"}],"article_processing_charge":"Yes","publication_status":"published","intvolume":"         2","title":"Fast symbolic algorithms for mega-regular games under strong transition fairness","ec_funded":1,"quality_controlled":"1","file_date_updated":"2024-02-05T10:19:35Z","publisher":"EPI Sciences","article_type":"original"},{"type":"research_data_reference","date_published":"2023-04-28T00:00:00Z","year":"2023","citation":{"ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023).","mla":"Majumdar, Rupak, et al. <i>A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>.","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>.","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties.” Zenodo, 2023.","apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>","ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_updated":"2024-02-27T07:39:51Z","oa":1,"abstract":[{"lang":"eng","text":"This resource contains the artifacts for reproducing the experimental results presented in the paper titled \"A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties\" that has been submitted in CAV 2023."}],"day":"28","doi":"10.5281/ZENODO.7877790","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"14758","relation":"used_in_publication"}]},"ddc":["000"],"status":"public","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.7877790"}],"author":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik"},{"last_name":"Rychlicki","first_name":"Mateusz","full_name":"Rychlicki, Mateusz"},{"full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck","first_name":"Anne-Kathrin"},{"first_name":"Sadegh","last_name":"Soudjani","full_name":"Soudjani, Sadegh"}],"has_accepted_license":"1","_id":"14994","month":"04","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","department":[{"_id":"ToHe"}],"date_created":"2024-02-14T15:13:00Z","article_processing_charge":"No","oa_version":"Published Version","publisher":"Zenodo"},{"oa_version":"Preprint","publication_status":"epub_ahead","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"article_processing_charge":"No","date_created":"2024-02-25T09:23:24Z","month":"12","title":"Compositional policy learning in stochastic control systems with formal guarantees","publication":"37th Conference on Neural Information Processing Systems","_id":"15023","author":[{"first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner"},{"id":"a235593c-d7fa-11eb-a0c5-b22ca3c66ee6","full_name":"Verma, Abhinav","first_name":"Abhinav","last_name":"Verma"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"conference":{"end_date":"2023-12-16","location":"New Orleans, LO, United States","name":"NeurIPS: Neural Information Processing Systems","start_date":"2023-12-10"},"ec_funded":1,"quality_controlled":"1","language":[{"iso":"eng"}],"arxiv":1,"day":"15","abstract":[{"text":"Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.","lang":"eng"}],"oa":1,"date_updated":"2025-07-14T09:10:04Z","citation":{"ieee":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in <i>37th Conference on Neural Information Processing Systems</i>, New Orleans, LO, United States, 2023.","chicago":"Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In <i>37th Conference on Neural Information Processing Systems</i>, 2023.","apa":"Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., &#38; Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In <i>37th Conference on Neural Information Processing Systems</i>. New Orleans, LO, United States.","ama":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: <i>37th Conference on Neural Information Processing Systems</i>. ; 2023.","ista":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems.","short":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023.","mla":"Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” <i>37th Conference on Neural Information Processing Systems</i>, 2023."},"year":"2023","date_published":"2023-12-15T00:00:00Z","type":"conference","external_id":{"arxiv":["2312.01456"]},"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt).","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.01456"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public"},{"has_accepted_license":"1","_id":"15035","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","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"}],"article_processing_charge":"No","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"department":[{"_id":"ToHe"}],"date_created":"2024-02-28T07:34:34Z","oa_version":"Published Version","title":"Monitoring hyperproperties with prefix transducers","month":"07","ec_funded":1,"publisher":"Zenodo","citation":{"apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>","ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>.","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.” Zenodo, 2023.","short":"M. Chalupa, T.A. Henzinger, (2023).","mla":"Chalupa, Marek, and Thomas A. Henzinger. <i>Monitoring Hyperproperties with Prefix Transducers</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>.","ista":"Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>."},"year":"2023","date_updated":"2024-02-28T12:33:09Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"research_data_reference","date_published":"2023-07-28T00:00:00Z","day":"28","doi":"10.5281/ZENODO.8191723","oa":1,"abstract":[{"lang":"eng","text":"This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties With Prefix Transducers accepted at RV'23, and give further pointers to implementation of prefix transducers.\r\nIt has two parts: a pre-compiled docker image and sources that one can use to compile (locally or in docker) the software and run the experiments."}],"main_file_link":[{"url":"https://doi.org/10.5281/zenodo.8191722","open_access":"1"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"related_material":{"record":[{"relation":"used_in_publication","id":"14076","status":"public"}]}},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"date_created":"2023-06-19T08:43:21Z","file_size":521425,"checksum":"60dcafc1b4f6f070be43bad3fe877974","date_updated":"2023-06-19T08:43:21Z","file_name":"2023_LNCS_Anand.pdf","content_type":"application/pdf","success":1,"relation":"main_file","access_level":"open_access","file_id":"13151","creator":"dernst"}],"oa":1,"publication_identifier":{"isbn":["9783031308192"],"issn":["0302-9743"],"eissn":["1611-3349"]},"type":"conference","date_published":"2023-04-20T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"conference":{"location":"Paris, France","end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22"},"language":[{"iso":"eng"}],"month":"04","oa_version":"Published Version","has_accepted_license":"1","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","ddc":["000"],"volume":13994,"abstract":[{"lang":"eng","text":"We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω\r\n-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive."}],"day":"20","doi":"10.1007/978-3-031-30820-8_15","citation":{"short":"A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 211–228.","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>.","ista":"Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 211–228.","apa":"Anand, A., Mallik, K., Nayak, S. P., &#38; Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>","ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:211-228. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 211–228.","chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:211–28. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>."},"year":"2023","date_updated":"2023-06-19T08:49:46Z","publisher":"Springer Nature","file_date_updated":"2023-06-19T08:43:21Z","quality_controlled":"1","page":"211-228","intvolume":"     13994","title":"Computing adequately permissive assumptions for synthesis","alternative_title":["LNCS"],"date_created":"2023-06-18T22:00:47Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","author":[{"full_name":"Anand, Ashwani","first_name":"Ashwani","last_name":"Anand"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475"},{"last_name":"Nayak","first_name":"Satya Prakash","full_name":"Nayak, Satya Prakash"},{"full_name":"Schmuck, Anne Kathrin","last_name":"Schmuck","first_name":"Anne Kathrin"}],"scopus_import":"1","_id":"13141"},{"file_date_updated":"2023-06-19T08:29:30Z","page":"3-25","quality_controlled":"1","ec_funded":1,"publisher":"Springer Nature","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"_id":"13142","scopus_import":"1","title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","alternative_title":["LNCS"],"intvolume":"     13993","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2023-06-18T22:00:47Z","ddc":["000"],"volume":13993,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","date_updated":"2025-07-14T09:09:52Z","year":"2023","citation":{"ista":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.","mla":"Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, vol. 13993, Springer Nature, 2023, pp. 3–25, doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>.","short":"K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” In <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, 13993:3–25. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>.","ieee":"K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier framework for neural network controllers and certificates of stochastic systems,” in <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, Paris, France, 2023, vol. 13993, pp. 3–25.","apa":"Chatterjee, K., Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In <i>Tools and Algorithms for the Construction and Analysis of Systems </i> (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>","ama":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: <i>Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 13993. Springer Nature; 2023:3-25. doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>"},"abstract":[{"lang":"eng","text":"Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions."}],"doi":"10.1007/978-3-031-30823-9_1","day":"22","language":[{"iso":"eng"}],"conference":{"start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27","location":"Paris, France"},"publication":"Tools and Algorithms for the Construction and Analysis of Systems ","has_accepted_license":"1","month":"04","oa_version":"Published Version","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"665385","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2023-06-19T08:29:30Z","file_size":528455,"checksum":"3d8a8bb24d211bc83360dfc2fd744307","date_updated":"2023-06-19T08:29:30Z","content_type":"application/pdf","file_name":"2023_LNCS_Chatterjee.pdf","access_level":"open_access","success":1,"relation":"main_file","file_id":"13150","creator":"dernst"}],"date_published":"2023-04-22T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783031308222"],"eissn":["1611-3349"],"issn":["0302-9743"]}},{"ddc":["000"],"acknowledgement":"We thank Christof Löding for pointing us to some results on PSpace-hardess of universality problems and the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science Foundation grant 2410/22.","volume":279,"abstract":[{"lang":"eng","text":"The safety-liveness dichotomy is a fundamental concept in formal languages which plays a key role in verification. Recently, this dichotomy has been lifted to quantitative properties, which are arbitrary functions from infinite words to partially-ordered domains. We look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totallyordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpace-complete checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications."}],"day":"01","doi":"10.4230/LIPIcs.CONCUR.2023.17","arxiv":1,"external_id":{"arxiv":["2307.06016"]},"citation":{"chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Safety and Liveness of Quantitative Automata.” In <i>34th International Conference on Concurrency Theory</i>, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>.","ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness of quantitative automata,” in <i>34th International Conference on Concurrency Theory</i>, Antwerp, Belgium, 2023, vol. 279.","apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Safety and liveness of quantitative automata. In <i>34th International Conference on Concurrency Theory</i> (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">https://doi.org/10.4230/LIPIcs.CONCUR.2023.17</a>","ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: <i>34th International Conference on Concurrency Theory</i>. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>","ista":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness of quantitative automata. 34th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17.","mla":"Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” <i>34th International Conference on Concurrency Theory</i>, vol. 279, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2023.17\">10.4230/LIPIcs.CONCUR.2023.17</a>.","short":"U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 34th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023."},"year":"2023","date_updated":"2023-10-09T07:14:03Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2023-07-14T12:03:48Z","quality_controlled":"1","ec_funded":1,"intvolume":"       279","title":"Safety and liveness of quantitative automata","alternative_title":["LIPIcs"],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2023-07-14T10:00:15Z","publication_status":"published","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi","full_name":"Boker, Udi"},{"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":"Mazzocchi","first_name":"Nicolas Adrien","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","first_name":"Naci E","last_name":"Sarac"}],"_id":"13221","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_id":"13224","creator":"esarac","relation":"main_file","access_level":"open_access","success":1,"date_updated":"2023-07-14T12:03:48Z","content_type":"application/pdf","file_name":"CONCUR23.pdf","date_created":"2023-07-14T12:03:48Z","file_size":755529,"checksum":"d40e57a04448ea5c77d7e1cfb9590a81"}],"oa":1,"publication_identifier":{"isbn":["9783959772990"],"eissn":["1868-8969"]},"type":"conference","date_published":"2023-09-01T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"conference":{"end_date":"2023-09-23","location":"Antwerp, Belgium","name":"CONCUR: Conference on Concurrency Theory","start_date":"2023-09-18"},"language":[{"iso":"eng"}],"article_number":"17","month":"09","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"34th International Conference on Concurrency Theory"},{"language":[{"iso":"eng"}],"conference":{"start_date":"2023-06-12","name":"FAccT: Conference on Fairness, Accountability and Transparency","end_date":"2023-06-15","location":"Chicago, IL, United States"},"has_accepted_license":"1","publication":"FAccT '23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency","month":"06","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"oa_version":"Published Version","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"content_type":"application/pdf","file_name":"2023_ACM_HenzingerT.pdf","date_updated":"2023-07-18T07:43:10Z","file_size":4100596,"checksum":"96c759db9cdf94b81e37871a66a6ff48","date_created":"2023-07-18T07:43:10Z","creator":"dernst","file_id":"13245","relation":"main_file","access_level":"open_access","success":1}],"type":"conference","date_published":"2023-06-12T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9781450372527"]},"file_date_updated":"2023-07-18T07:43:10Z","ec_funded":1,"quality_controlled":"1","page":"604-614","publisher":"Association for Computing Machinery","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Karimi, Mahyar","first_name":"Mahyar","last_name":"Karimi"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner","first_name":"Konstantin"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik"}],"scopus_import":"1","_id":"13228","title":"Runtime monitoring of dynamic fairness properties","date_created":"2023-07-16T22:01:09Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","ddc":["000"],"acknowledgement":"The authors would like to thank the anonymous reviewers for their valuable comments and helpful suggestions. This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","external_id":{"arxiv":["2305.04699"],"isi":["001062819300057"]},"isi":1,"year":"2023","citation":{"apa":"Henzinger, T. A., Karimi, M., Kueffner, K., &#38; Mallik, K. (2023). Runtime monitoring of dynamic fairness properties. In <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i> (pp. 604–614). Chicago, IL, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3593013.3594028\">https://doi.org/10.1145/3593013.3594028</a>","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Runtime monitoring of dynamic fairness properties. In: <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>. Association for Computing Machinery; 2023:604-614. doi:<a href=\"https://doi.org/10.1145/3593013.3594028\">10.1145/3593013.3594028</a>","chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Runtime Monitoring of Dynamic Fairness Properties.” In <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, 604–14. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3593013.3594028\">https://doi.org/10.1145/3593013.3594028</a>.","ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Runtime monitoring of dynamic fairness properties,” in <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, Chicago, IL, United States, 2023, pp. 604–614.","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, Association for Computing Machinery, 2023, pp. 604–614.","mla":"Henzinger, Thomas A., et al. “Runtime Monitoring of Dynamic Fairness Properties.” <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, Association for Computing Machinery, 2023, pp. 604–14, doi:<a href=\"https://doi.org/10.1145/3593013.3594028\">10.1145/3593013.3594028</a>.","ista":"Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Runtime monitoring of dynamic fairness properties. FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency. FAccT: Conference on Fairness, Accountability and Transparency, 604–614."},"date_updated":"2023-12-13T11:30:31Z","abstract":[{"text":"A machine-learned system that is fair in static decision-making tasks may have biased societal impacts in the long-run. This may happen when the system interacts with humans and feedback patterns emerge, reinforcing old biases in the system and creating new biases. While existing works try to identify and mitigate long-run biases through smart system design, we introduce techniques for monitoring fairness in real time. Our goal is to build and deploy a monitor that will continuously observe a long sequence of events generated by the system in the wild, and will output, with each event, a verdict on how fair the system is at the current point in time. The advantages of monitoring are two-fold. Firstly, fairness is evaluated at run-time, which is important because unfair behaviors may not be eliminated a priori, at design-time, due to partial knowledge about the system and the environment, as well as uncertainties and dynamic changes in the system and the environment, such as the unpredictability of human behavior. Secondly, monitors are by design oblivious to how the monitored system is constructed, which makes them suitable to be used as trusted third-party fairness watchdogs. They function as computationally lightweight statistical estimators, and their correctness proofs rely on the rigorous analysis of the stochastic process that models the assumptions about the underlying dynamics of the system. We show, both in theory and experiments, how monitors can warn us (1) if a bank’s credit policy over time has created an unfair distribution of credit scores among the population, and (2) if a resource allocator’s allocation policy over time has made unfair allocations. Our experiments demonstrate that the monitors introduce very low overhead. We believe that runtime monitoring is an important and mathematically rigorous new addition to the fairness toolbox.","lang":"eng"}],"day":"12","arxiv":1,"doi":"10.1145/3593013.3594028"},{"language":[{"iso":"eng"}],"publication":"International Journal on Software Tools for Technology Transfer","has_accepted_license":"1","month":"08","oa_version":"Published Version","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"status":"public","related_material":{"record":[{"id":"10206","relation":"shorter_version","status":"public"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_id":"14903","creator":"dernst","success":1,"access_level":"open_access","relation":"main_file","date_updated":"2024-01-30T12:06:07Z","file_name":"2023_JourSoftwareTools_Kueffner.pdf","content_type":"application/pdf","date_created":"2024-01-30T12:06:07Z","file_size":13387667,"checksum":"3c4b347f39412a76872f9a6f30101f94"}],"date_published":"2023-08-01T00:00:00Z","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"file_date_updated":"2024-01-30T12:06:07Z","page":"575-592","ec_funded":1,"quality_controlled":"1","article_type":"original","publisher":"Springer Nature","author":[{"first_name":"Konstantin","last_name":"Kueffner","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"},{"last_name":"Lukina","first_name":"Anna","full_name":"Lukina, Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","first_name":"Christian"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A"}],"_id":"13234","scopus_import":"1","title":"Into the unknown: Active monitoring of neural networks (extended version)","intvolume":"        25","publication_status":"published","date_created":"2023-07-16T22:01:11Z","article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"ToHe"}],"ddc":["000"],"volume":25,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.","isi":1,"external_id":{"arxiv":["2009.06429"],"isi":["001020160000001"]},"date_updated":"2024-01-30T12:06:57Z","citation":{"ama":"Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. 2023;25:575-592. doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>","apa":"Kueffner, K., Lukina, A., Schilling, C., &#38; Henzinger, T. A. (2023). Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>","chicago":"Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>.","ieee":"K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: Active monitoring of neural networks (extended version),” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25. Springer Nature, pp. 575–592, 2023.","short":"K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 25 (2023) 575–592.","mla":"Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25, Springer Nature, 2023, pp. 575–92, doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>.","ista":"Kueffner K, Lukina A, Schilling C, Henzinger TA. 2023. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 25, 575–592."},"year":"2023","abstract":[{"lang":"eng","text":"Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. We consider the problem of monitoring the classification decisions of neural networks in the presence of novel classes. For this purpose, we generalize our recently proposed abstraction-based monitor from binary output to real-valued quantitative output. This quantitative output enables new applications, two of which we investigate in the paper. As our first application, we introduce an algorithmic framework for active monitoring of a neural network, which allows us to learn new classes dynamically and yet maintain high monitoring performance. As our second application, we present an offline procedure to retrain the neural network to improve the monitor’s detection performance without deteriorating the network’s classification accuracy. Our experimental evaluation demonstrates both the benefits of our active monitoring framework in dynamic scenarios and the effectiveness of the retraining procedure."}],"arxiv":1,"doi":"10.1007/s10009-023-00711-4","day":"01"},{"ddc":["000"],"acknowledgement":"This work was supported by L’Institut Carnot STAR, Marseille, France, and by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. [101034413].","volume":39,"external_id":{"isi":["001027457000060"],"pmid":["37387165"]},"isi":1,"year":"2023","citation":{"ieee":"V. G. Trinh, B. Benhamou, T. A. Henzinger, and S. Pastva, “Trap spaces of multi-valued networks: Definition, computation, and applications,” <i>Bioinformatics</i>, vol. 39, no. Supplement_1. Oxford Academic, pp. i513–i522, 2023.","chicago":"Trinh, Van Giang, Belaid Benhamou, Thomas A Henzinger, and Samuel Pastva. “Trap Spaces of Multi-Valued Networks: Definition, Computation, and Applications.” <i>Bioinformatics</i>. Oxford Academic, 2023. <a href=\"https://doi.org/10.1093/bioinformatics/btad262\">https://doi.org/10.1093/bioinformatics/btad262</a>.","ama":"Trinh VG, Benhamou B, Henzinger TA, Pastva S. Trap spaces of multi-valued networks: Definition, computation, and applications. <i>Bioinformatics</i>. 2023;39(Supplement_1):i513-i522. doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad262\">10.1093/bioinformatics/btad262</a>","apa":"Trinh, V. G., Benhamou, B., Henzinger, T. A., &#38; Pastva, S. (2023). Trap spaces of multi-valued networks: Definition, computation, and applications. <i>Bioinformatics</i>. Oxford Academic. <a href=\"https://doi.org/10.1093/bioinformatics/btad262\">https://doi.org/10.1093/bioinformatics/btad262</a>","ista":"Trinh VG, Benhamou B, Henzinger TA, Pastva S. 2023. Trap spaces of multi-valued networks: Definition, computation, and applications. Bioinformatics. 39(Supplement_1), i513–i522.","mla":"Trinh, Van Giang, et al. “Trap Spaces of Multi-Valued Networks: Definition, Computation, and Applications.” <i>Bioinformatics</i>, vol. 39, no. Supplement_1, Oxford Academic, 2023, pp. i513–22, doi:<a href=\"https://doi.org/10.1093/bioinformatics/btad262\">10.1093/bioinformatics/btad262</a>.","short":"V.G. Trinh, B. Benhamou, T.A. Henzinger, S. Pastva, Bioinformatics 39 (2023) i513–i522."},"date_updated":"2023-12-13T11:41:52Z","abstract":[{"lang":"eng","text":"Motivation: Boolean networks are simple but efficient mathematical formalism for modelling complex biological systems. However, having only two levels of activation is sometimes not enough to fully capture the dynamics of real-world biological systems. Hence, the need for multi-valued networks (MVNs), a generalization of Boolean networks. Despite the importance of MVNs for modelling biological systems, only limited progress has been made on developing theories, analysis methods, and tools that can support them. In particular, the recent use of trap spaces in Boolean networks made a great impact on the field of systems biology, but there has been no similar concept defined and studied for MVNs to date.\r\n\r\nResults: In this work, we generalize the concept of trap spaces in Boolean networks to that in MVNs. We then develop the theory and the analysis methods for trap spaces in MVNs. In particular, we implement all proposed methods in a Python package called trapmvn. Not only showing the applicability of our approach via a realistic case study, we also evaluate the time efficiency of the method on a large collection of real-world models. The experimental results confirm the time efficiency, which we believe enables more accurate analysis on larger and more complex multi-valued models."}],"day":"30","doi":"10.1093/bioinformatics/btad262","file_date_updated":"2023-07-31T11:09:05Z","quality_controlled":"1","ec_funded":1,"page":"i513-i522","article_type":"original","publisher":"Oxford Academic","issue":"Supplement_1","author":[{"full_name":"Trinh, Van Giang","first_name":"Van Giang","last_name":"Trinh"},{"full_name":"Benhamou, Belaid","last_name":"Benhamou","first_name":"Belaid"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Samuel","last_name":"Pastva","orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b"}],"scopus_import":"1","pmid":1,"_id":"13263","intvolume":"        39","title":"Trap spaces of multi-valued networks: Definition, computation, and applications","article_processing_charge":"Yes","department":[{"_id":"ToHe"}],"date_created":"2023-07-23T22:01:12Z","publication_status":"published","status":"public","related_material":{"link":[{"url":"https://github.com/giang-trinh/trap-mvn","relation":"software"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_updated":"2023-07-31T11:09:05Z","file_name":"2023_Bioinformatics_Trinh.pdf","content_type":"application/pdf","date_created":"2023-07-31T11:09:05Z","checksum":"ba3abe1171df1958413b7c7f957f5486","file_size":641736,"file_id":"13335","creator":"dernst","access_level":"open_access","success":1,"relation":"main_file"}],"type":"journal_article","date_published":"2023-06-30T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"issn":["1367-4803"],"eissn":["1367-4811"]},"language":[{"iso":"eng"}],"has_accepted_license":"1","publication":"Bioinformatics","month":"06","project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"oa_version":"Published Version"},{"external_id":{"arxiv":["2305.03447"]},"year":"2023","citation":{"ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods for operator precedence languages,” in <i>50th International Colloquium on Automata, Languages, and Programming</i>, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Regular Methods for Operator Precedence Languages.” In <i>50th International Colloquium on Automata, Languages, and Programming</i>, 261:129:1--129:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>.","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Regular methods for operator precedence languages. In <i>50th International Colloquium on Automata, Languages, and Programming</i> (Vol. 261, p. 129:1--129:20). Paderborn, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">https://doi.org/10.4230/LIPIcs.ICALP.2023.129</a>","ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: <i>50th International Colloquium on Automata, Languages, and Programming</i>. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1--129:20. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">10.4230/LIPIcs.ICALP.2023.129</a>","ista":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for operator precedence languages. 50th International Colloquium on Automata, Languages, and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LIPIcs, vol. 261, 129:1--129:20.","short":"T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20.","mla":"Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.” <i>50th International Colloquium on Automata, Languages, and Programming</i>, vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2023.129\">10.4230/LIPIcs.ICALP.2023.129</a>."},"date_updated":"2023-07-31T08:38:38Z","abstract":[{"text":"The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time.","lang":"eng"}],"day":"05","doi":"10.4230/LIPIcs.ICALP.2023.129","arxiv":1,"ddc":["000"],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful comments.\r\n","volume":261,"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Pavol","last_name":"Kebis","full_name":"Kebis, Pavol"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","last_name":"Mazzocchi","first_name":"Nicolas Adrien","full_name":"Mazzocchi, Nicolas Adrien"},{"first_name":"Naci E","last_name":"Sarac","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"_id":"13292","intvolume":"       261","title":"Regular methods for operator precedence languages","alternative_title":["LIPIcs"],"article_processing_charge":"Yes","date_created":"2023-07-24T15:11:41Z","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publication_status":"published","file_date_updated":"2023-07-24T15:11:05Z","quality_controlled":"1","ec_funded":1,"page":"129:1--129:20","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","type":"conference","date_published":"2023-07-05T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783959772785"],"eissn":["1868-8969"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"relation":"main_file","success":1,"access_level":"open_access","file_id":"13293","creator":"esarac","date_created":"2023-07-24T15:11:05Z","file_size":859379,"checksum":"5d4c8932ef3450615a53b9bb15d92eb2","date_updated":"2023-07-24T15:11:05Z","file_name":"icalp23.pdf","content_type":"application/pdf"}],"has_accepted_license":"1","publication":"50th International Colloquium on Automata, Languages, and Programming","month":"07","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"start_date":"2023-07-10","name":"ICALP: International Colloquium on Automata, Languages, and Programming","end_date":"2023-07-14","location":"Paderborn, Germany"}}]