[{"day":"01","page":"585-618","quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"project":[{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"has_accepted_license":"1","publisher":"Springer Nature","type":"journal_article","external_id":{"isi":["000735765500001"]},"date_published":"2022-10-01T00:00:00Z","keyword":["computer networks and communications","information systems","software"],"ddc":["000"],"language":[{"iso":"eng"}],"status":"public","isi":1,"month":"10","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","article_type":"original","scopus_import":"1","doi":"10.1007/s00236-021-00412-y","oa_version":"Published Version","article_processing_charge":"Yes (via OA deal)","file_date_updated":"2022-01-07T07:50:31Z","publication_status":"published","title":"Index appearance record with preorders","abstract":[{"lang":"eng","text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches."}],"citation":{"mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica, vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” Acta Informatica. Springer Nature, 2022. https://doi.org/10.1007/s00236-021-00412-y.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022). Index appearance record with preorders. Acta Informatica. Springer Nature. https://doi.org/10.1007/s00236-021-00412-y","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp. 585–618, 2022.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y"},"year":"2022","file":[{"file_id":"10603","creator":"cchlebak","content_type":"application/pdf","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","file_name":"2021_ActaInfor_Křetínský.pdf","access_level":"open_access","success":1,"file_size":1066082,"date_created":"2022-01-07T07:50:31Z","date_updated":"2022-01-07T07:50:31Z","relation":"main_file"}],"date_created":"2022-01-06T12:37:27Z","_id":"10602","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"first_name":"Clara","last_name":"Waldmann","full_name":"Waldmann, Clara"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"}],"volume":59,"oa":1,"intvolume":" 59","date_updated":"2023-08-02T13:49:28Z","publication":"Acta Informatica","department":[{"_id":"KrCh"}]},{"quality_controlled":"1","day":"27","issue":"1","project":[{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","type":"journal_article","external_id":{"arxiv":["2012.15155"],"isi":["000749198000039"]},"date_published":"2022-01-27T00:00:00Z","publisher":"Springer Nature","isi":1,"month":"01","status":"public","ddc":["570"],"language":[{"iso":"eng"}],"publication_status":"published","title":"Infection dynamics of COVID-19 virus under lockdown and reopening","oa_version":"Published Version","article_processing_charge":"No","file_date_updated":"2022-02-07T14:57:59Z","scopus_import":"1","doi":"10.1038/s41598-022-05333-5","publication_identifier":{"eissn":["2045-2322"]},"acknowledgement":"K.C. acknowledges support from ERC Consolidator Grant No. (863818: ForM-SMart). A.P. acknowledges support from FWF Grant No. J-4220. M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","article_type":"original","file":[{"file_name":"2022_ScientificReports_Svoboda.pdf","access_level":"open_access","success":1,"relation":"main_file","file_size":2971922,"date_created":"2022-02-07T14:57:59Z","date_updated":"2022-02-07T14:57:59Z","content_type":"application/pdf","creator":"alisjak","file_id":"10744","checksum":"247afd30c173390940f099ead35a28ed"}],"date_created":"2022-02-06T23:01:30Z","_id":"10731","citation":{"ista":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2022. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 12(1), 1526.","ieee":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Infection dynamics of COVID-19 virus under lockdown and reopening,” Scientific Reports, vol. 12, no. 1. Springer Nature, 2022.","ama":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 2022;12(1). doi:10.1038/s41598-022-05333-5","mla":"Svoboda, Jakub, et al. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” Scientific Reports, vol. 12, no. 1, 1526, Springer Nature, 2022, doi:10.1038/s41598-022-05333-5.","short":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Scientific Reports 12 (2022).","apa":"Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K., & Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. Springer Nature. https://doi.org/10.1038/s41598-022-05333-5","chicago":"Svoboda, Jakub, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” Scientific Reports. Springer Nature, 2022. https://doi.org/10.1038/s41598-022-05333-5."},"article_number":"1526","year":"2022","abstract":[{"text":"Motivated by COVID-19, we develop and analyze a simple stochastic model for the spread of disease in human population. We track how the number of infected and critically ill people develops over time in order to estimate the demand that is imposed on the hospital system. To keep this demand under control, we consider a class of simple policies for slowing down and reopening society and we compare their efficiency in mitigating the spread of the virus from several different points of view. We find that in order to avoid overwhelming of the hospital system, a policy must impose a harsh lockdown or it must react swiftly (or both). While reacting swiftly is universally beneficial, being harsh pays off only when the country is patient about reopening and when the neighboring countries coordinate their mitigation efforts. Our work highlights the importance of acting decisively when closing down and the importance of patience and coordination between neighboring countries when reopening.","lang":"eng"}],"volume":12,"oa":1,"author":[{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","first_name":"Jakub","last_name":"Svoboda"},{"first_name":"Josef","last_name":"Tkadlec","full_name":"Tkadlec, Josef"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","department":[{"_id":"KrCh"}],"ec_funded":1,"date_updated":"2025-07-14T09:10:12Z","publication":"Scientific Reports","arxiv":1,"intvolume":" 12"},{"project":[{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"}],"page":"1-21","day":"01","quality_controlled":"1","language":[{"iso":"eng"}],"month":"11","isi":1,"status":"public","publisher":"Elsevier","external_id":{"arxiv":["1802.03642"],"isi":["000805002800001"]},"date_published":"2022-11-01T00:00:00Z","type":"journal_article","year":"2022","citation":{"mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected Finite Horizon.” Journal of Computer and System Sciences, vol. 129, Elsevier, 2022, pp. 1–21, doi:10.1016/j.jcss.2022.04.003.","short":"K. Chatterjee, L. Doyen, Journal of Computer and System Sciences 129 (2022) 1–21.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected Finite Horizon.” Journal of Computer and System Sciences. Elsevier, 2022. https://doi.org/10.1016/j.jcss.2022.04.003.","apa":"Chatterjee, K., & Doyen, L. (2022). Graph planning with expected finite horizon. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2022.04.003","ama":"Chatterjee K, Doyen L. Graph planning with expected finite horizon. Journal of Computer and System Sciences. 2022;129:1-21. doi:10.1016/j.jcss.2022.04.003","ista":"Chatterjee K, Doyen L. 2022. Graph planning with expected finite horizon. Journal of Computer and System Sciences. 129, 1–21.","ieee":"K. Chatterjee and L. Doyen, “Graph planning with expected finite horizon,” Journal of Computer and System Sciences, vol. 129. Elsevier, pp. 1–21, 2022."},"abstract":[{"text":"Fixed-horizon planning considers a weighted graph and asks to construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping-time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary as the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping-time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time.","lang":"eng"}],"_id":"11402","date_created":"2022-05-22T22:01:40Z","doi":"10.1016/j.jcss.2022.04.003","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.1802.03642"}],"scopus_import":"1","article_type":"original","publication_identifier":{"eissn":["1090-2724"],"issn":["0022-0000"]},"acknowledgement":"This work was partially supported by Austrian Science Fund (FWF) NFN Grant No RiSE/SHiNE S11407 and by the grant ERC CoG 863818 (ForM-SMArt).","publication_status":"published","title":"Graph planning with expected finite horizon","article_processing_charge":"No","oa_version":"Preprint","arxiv":1,"intvolume":" 129","department":[{"_id":"KrCh"}],"publication":"Journal of Computer and System Sciences","date_updated":"2025-07-14T09:09:54Z","ec_funded":1,"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"7402"}]},"volume":129},{"citation":{"ama":"Zikelic D, Chang B-YE, Bolignano P, Raimondi F. Differential cost analysis with simultaneous potentials and anti-potentials. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2022:442-457. doi:10.1145/3519939.3523435","ieee":"D. Zikelic, B.-Y. E. Chang, P. Bolignano, and F. Raimondi, “Differential cost analysis with simultaneous potentials and anti-potentials,” in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, United States, 2022, pp. 442–457.","ista":"Zikelic D, Chang B-YE, Bolignano P, Raimondi F. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 442–457.","short":"D. Zikelic, B.-Y.E. Chang, P. Bolignano, F. Raimondi, in:, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 442–457.","chicago":"Zikelic, Dorde, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi. “Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.” In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 442–57. Association for Computing Machinery, 2022. https://doi.org/10.1145/3519939.3523435.","apa":"Zikelic, D., Chang, B.-Y. E., Bolignano, P., & Raimondi, F. (2022). Differential cost analysis with simultaneous potentials and anti-potentials. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 442–457). San Diego, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3519939.3523435","mla":"Zikelic, Dorde, et al. “Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.” Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 442–57, doi:10.1145/3519939.3523435."},"year":"2022","abstract":[{"text":"We present a novel approach to differential cost analysis that, given a program revision, attempts to statically bound the difference in resource usage, or cost, between the two program versions. Differential cost analysis is particularly interesting because of the many compelling applications for it, such as detecting resource-use regressions at code-review time or proving the absence of certain side-channel vulnerabilities. One prior approach to differential cost analysis is to apply relational reasoning that conceptually constructs a product program on which one can over-approximate the difference in costs between the two program versions. However, a significant challenge in any relational approach is effectively aligning the program versions to get precise results. In this paper, our key insight is that we can avoid the need for and the limitations of program alignment if, instead, we bound the difference of two cost-bound summaries rather than directly bounding the concrete cost difference. In particular, our method computes a threshold value for the maximal difference in cost between two program versions simultaneously using two kinds of cost-bound summaries---a potential function that evaluates to an upper bound for the cost incurred in the first program and an anti-potential function that evaluates to a lower bound for the cost incurred in the second. Our method has a number of desirable properties: it can be fully automated, it allows optimizing the threshold value on relative cost, it is suitable for programs that are not syntactically similar, and it supports non-determinism. We have evaluated an implementation of our approach on a number of program pairs collected from the literature, and we find that our method computes tight threshold values on relative cost in most examples.","lang":"eng"}],"conference":{"end_date":"2022-06-17","location":"San Diego, CA, United States","name":"PLDI: Programming Language Design and Implementation","start_date":"2022-06-13"},"date_created":"2022-06-21T09:26:15Z","file":[{"file_name":"2022_PLDI_Zikelic.pdf","access_level":"open_access","success":1,"file_size":318697,"date_updated":"2022-06-27T07:38:21Z","date_created":"2022-06-27T07:38:21Z","relation":"main_file","creator":"dernst","file_id":"11466","content_type":"application/pdf","checksum":"7eb915a2ca5b5ce4729321f33b2e16e1"}],"_id":"11459","scopus_import":"1","doi":"10.1145/3519939.3523435","publication_identifier":{"isbn":["9781450392655"]},"acknowledgement":"We thank Shaun Willows, Thomas Lugnet, and the Living Room Application Vending team for suggesting threshold\r\nbounds as a developer-friendly way to interact with a differential cost analyzer, and we thank Jim Christy, Daniel\r\nSchoepe, and the Prime Video Automated Reasoning team for their support and helpful suggestions throughout the\r\nproject. We also thank Michael Emmi for feedback on an earlier version of this paper. And finally, we thank the anonymous reviewers for their useful feedback and Aws Albarghouthi for shepherding the final version of the paper. Ðorđe Žikelić was also partially supported by ERC CoG 863818 (FoRM-SMArt).","publication_status":"published","title":"Differential cost analysis with simultaneous potentials and anti-potentials","article_processing_charge":"No","oa_version":"Published Version","file_date_updated":"2022-06-27T07:38:21Z","arxiv":1,"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"date_updated":"2025-07-14T09:09:54Z","ec_funded":1,"publication":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":[{"last_name":"Zikelic","first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chang, Bor-Yuh Evan","first_name":"Bor-Yuh Evan","last_name":"Chang"},{"last_name":"Bolignano","first_name":"Pauline","full_name":"Bolignano, Pauline"},{"full_name":"Raimondi, Franco","first_name":"Franco","last_name":"Raimondi"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa":1,"has_accepted_license":"1","tmp":{"image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"page":"442-457","day":"09","quality_controlled":"1","ddc":["000"],"language":[{"iso":"eng"}],"isi":1,"month":"06","status":"public","publisher":"Association for Computing Machinery","type":"conference","external_id":{"isi":["000850435600030"],"arxiv":["2204.00870"]},"date_published":"2022-06-09T00:00:00Z"},{"article_processing_charge":"No","oa_version":"Published Version","file_date_updated":"2022-08-22T06:42:42Z","title":"On compatible matchings","publication_status":"published","acknowledgement":"A.A. funded by the Marie Sklodowska-Curie grant agreement No 754411. Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23 (RiSE).","publication_identifier":{"issn":["1526-1719"]},"article_type":"original","scopus_import":"1","doi":"10.7155/jgaa.00591","date_created":"2022-08-21T22:01:56Z","file":[{"date_updated":"2022-08-22T06:42:42Z","file_size":694538,"date_created":"2022-08-22T06:42:42Z","relation":"main_file","file_name":"2022_JourGraphAlgorithmsApplic_Aichholzer.pdf","access_level":"open_access","success":1,"checksum":"dc6e255e3558faff924fd9e370886c11","content_type":"application/pdf","file_id":"11940","creator":"dernst"}],"_id":"11938","abstract":[{"text":"A matching is compatible to two or more labeled point sets of size n with labels {1, . . . , n} if its straight-line drawing on each of these point sets is crossing-free. We study the maximum number of edges in a matching compatible to two or more labeled point sets in general position in the plane. We show that for any two labeled sets of n points in convex position there exists a compatible matching with ⌊√2n + 1 − 1⌋ edges. More generally, for any ℓ labeled point sets we construct compatible matchings of size Ω(n1/ℓ). As a corresponding upper bound, we use probabilistic arguments to show that for any ℓ given sets of n points there exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1)) edges. Finally, we show that Θ(log n) copies of any set of n points are necessary and sufficient for the existence of labelings of these point sets such that any compatible matching consists only of a single edge.","lang":"eng"}],"citation":{"ista":"Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec J, Vogtenhuber B. 2022. On compatible matchings. Journal of Graph Algorithms and Applications. 26(2), 225–240.","ieee":"O. Aichholzer et al., “On compatible matchings,” Journal of Graph Algorithms and Applications, vol. 26, no. 2. Brown University, pp. 225–240, 2022.","ama":"Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings. Journal of Graph Algorithms and Applications. 2022;26(2):225-240. doi:10.7155/jgaa.00591","mla":"Aichholzer, Oswin, et al. “On Compatible Matchings.” Journal of Graph Algorithms and Applications, vol. 26, no. 2, Brown University, 2022, pp. 225–40, doi:10.7155/jgaa.00591.","chicago":"Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada, Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible Matchings.” Journal of Graph Algorithms and Applications. Brown University, 2022. https://doi.org/10.7155/jgaa.00591.","short":"O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz, J. Tkadlec, B. Vogtenhuber, Journal of Graph Algorithms and Applications 26 (2022) 225–240.","apa":"Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D., Pilz, A., … Vogtenhuber, B. (2022). On compatible matchings. Journal of Graph Algorithms and Applications. Brown University. https://doi.org/10.7155/jgaa.00591"},"year":"2022","volume":26,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"9296"}]},"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Oswin","last_name":"Aichholzer","full_name":"Aichholzer, Oswin"},{"last_name":"Arroyo Guevara","first_name":"Alan M","full_name":"Arroyo Guevara, Alan M","orcid":"0000-0003-2401-8670","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Masárová, Zuzana","id":"45CFE238-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6660-1322","last_name":"Masárová","first_name":"Zuzana"},{"first_name":"Irene","last_name":"Parada","full_name":"Parada, Irene"},{"last_name":"Perz","first_name":"Daniel","full_name":"Perz, Daniel"},{"last_name":"Pilz","first_name":"Alexander","full_name":"Pilz, Alexander"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","first_name":"Josef"},{"full_name":"Vogtenhuber, Birgit","first_name":"Birgit","last_name":"Vogtenhuber"}],"ec_funded":1,"date_updated":"2023-02-23T13:54:21Z","publication":"Journal of Graph Algorithms and Applications","department":[{"_id":"UlWa"},{"_id":"HeEd"},{"_id":"KrCh"}],"intvolume":" 26","arxiv":1,"quality_controlled":"1","day":"01","page":"225-240","project":[{"grant_number":"754411","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships"},{"grant_number":"Z00342","call_identifier":"FWF","_id":"268116B8-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","issue":"2","type":"journal_article","date_published":"2022-06-01T00:00:00Z","external_id":{"arxiv":["2101.03928"]},"publisher":"Brown University","status":"public","month":"06","ddc":["000"],"language":[{"iso":"eng"}]},{"publication":"Proceedings of the 34th International Conference on Computer Aided Verification","date_updated":"2025-07-14T09:09:58Z","ec_funded":1,"department":[{"_id":"KrCh"}],"intvolume":" 13371","oa":1,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"14539"}]},"volume":13371,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Goharshady","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584"},{"first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias"},{"first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"_id":"12000","date_created":"2022-08-28T22:02:02Z","file":[{"file_name":"2022_LNCS_Chatterjee.pdf","access_level":"open_access","success":1,"relation":"main_file","date_created":"2022-08-29T09:17:01Z","file_size":505094,"date_updated":"2022-08-29T09:17:01Z","content_type":"application/pdf","file_id":"12003","creator":"alisjak","checksum":"24e0f810ec52735a90ade95198bc641d"}],"conference":{"start_date":"2022-08-07","end_date":"2022-08-10","location":"Haifa, Israel","name":"CAV: Computer Aided Verification"},"abstract":[{"text":"We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p∈[0,1], we aim for certificates proving that the program terminates with probability at least 1−p. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset SI of program states such that (i) the probability of the program ever leaving SI is no more than p, and (ii) almost-surely, the program either leaves SI or terminates.\r\n\r\nWhile stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.\r\n\r\nOur prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods.","lang":"eng"}],"year":"2022","citation":{"apa":"Chatterjee, K., Goharshady, A. K., Meggendorfer, T., & Zikelic, D. (2022). Sound and complete certificates for auantitative termination analysis of probabilistic programs. In Proceedings of the 34th International Conference on Computer Aided Verification (Vol. 13371, pp. 55–78). Haifa, Israel: Springer. https://doi.org/10.1007/978-3-031-13185-1_4","short":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, in:, Proceedings of the 34th International Conference on Computer Aided Verification, Springer, 2022, pp. 55–78.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” In Proceedings of the 34th International Conference on Computer Aided Verification, 13371:55–78. Springer, 2022. https://doi.org/10.1007/978-3-031-13185-1_4.","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” Proceedings of the 34th International Conference on Computer Aided Verification, vol. 13371, Springer, 2022, pp. 55–78, doi:10.1007/978-3-031-13185-1_4.","ama":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Sound and complete certificates for auantitative termination analysis of probabilistic programs. In: Proceedings of the 34th International Conference on Computer Aided Verification. Vol 13371. Springer; 2022:55-78. doi:10.1007/978-3-031-13185-1_4","ista":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete certificates for auantitative termination analysis of probabilistic programs. Proceedings of the 34th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.","ieee":"K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Sound and complete certificates for auantitative termination analysis of probabilistic programs,” in Proceedings of the 34th International Conference on Computer Aided Verification, Haifa, Israel, 2022, vol. 13371, pp. 55–78."},"file_date_updated":"2022-08-29T09:17:01Z","article_processing_charge":"Yes (in subscription journal)","oa_version":"Published Version","title":"Sound and complete certificates for auantitative termination analysis of probabilistic programs","publication_status":"published","publication_identifier":{"isbn":["9783031131844"],"eissn":["1611-3349"],"issn":["0302-9743"]},"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055, the HKUST Startup Grant R9272 and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","doi":"10.1007/978-3-031-13185-1_4","scopus_import":"1","status":"public","month":"08","isi":1,"alternative_title":["LNCS"],"language":[{"iso":"eng"}],"ddc":["000"],"date_published":"2022-08-07T00:00:00Z","external_id":{"isi":["000870304500004"]},"type":"conference","publisher":"Springer","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020"}],"quality_controlled":"1","day":"07","page":"55-78"},{"abstract":[{"text":"Spatial games form a widely-studied class of games from biology and physics modeling the evolution of social behavior. Formally, such a game is defined by a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G represents an individual, that initially follows some strategy i ∈ {1,2,…,d}. In each round of the game, every individual plays the matrix game with each of its neighbors: An individual following strategy i meeting a neighbor following strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual updates its strategy to its neighbors' strategy with the highest sum of payoffs, and the next round starts. The basic computational problems consist of reachability between configurations and the average frequency of a strategy. For general spatial games and graphs, these problems are in PSPACE. In this paper, we examine restricted setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove that basic computational problems for spatial games with prisoner’s dilemma on a subgraph of a grid are PSPACE-hard.","lang":"eng"}],"article_number":"11:1-11:14","year":"2022","citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Complexity of spatial games. In: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:10.4230/LIPIcs.FSTTCS.2022.11","ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2022. Complexity of spatial games. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer Science vol. 250, 11:1-11:14.","ieee":"K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Complexity of spatial games,” in 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Madras, India, 2022, vol. 250.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Complexity of Spatial Games.” In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11.","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., & Svoboda, J. (2022). Complexity of spatial games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 250). Madras, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11","short":"K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","mla":"Chatterjee, Krishnendu, et al. “Complexity of Spatial Games.” 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 250, 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.FSTTCS.2022.11."},"_id":"12101","file":[{"file_name":"2022_LIPICs_Chatterjee.pdf","access_level":"open_access","success":1,"date_updated":"2023-01-20T10:19:19Z","relation":"main_file","date_created":"2023-01-20T10:19:19Z","file_size":657396,"file_id":"12323","creator":"dernst","content_type":"application/pdf","checksum":"a21e3ba2421e2c4a06aa2cb6d530ede1"}],"date_created":"2023-01-01T23:00:50Z","conference":{"location":"Madras, India","name":"FSTTC: Foundations of Software Technology and Theoretical Computer Science","end_date":"2022-12-20","start_date":"2022-12-18"},"acknowledgement":"Krishnendu Chatterjee: The research was partially supported by the ERC CoG 863818\r\n(ForM-SMArt).\r\nIsmaël Jecker: The research was partially supported by the ERC grant 950398 (INFSYS).\r\nJakub Svoboda: The research was partially supported by the ERC CoG 863818 (ForM-SMArt)","publication_identifier":{"isbn":["9783959772617"],"issn":["1868-8969"]},"doi":"10.4230/LIPIcs.FSTTCS.2022.11","scopus_import":"1","file_date_updated":"2023-01-20T10:19:19Z","article_processing_charge":"No","oa_version":"Published Version","publication_status":"published","title":"Complexity of spatial games","intvolume":" 250","publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","date_updated":"2025-07-14T09:09:55Z","ec_funded":1,"department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","full_name":"Jecker, Ismael R","first_name":"Ismael R","last_name":"Jecker"},{"first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub"}],"oa":1,"volume":250,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"has_accepted_license":"1","day":"14","quality_controlled":"1","language":[{"iso":"eng"}],"ddc":["000"],"status":"public","month":"12","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2022-12-14T00:00:00Z","type":"conference"},{"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"},{"call_identifier":"H2020","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","quality_controlled":"1","day":"14","month":"12","status":"public","language":[{"iso":"eng"}],"ddc":["000"],"date_published":"2022-12-14T00:00:00Z","type":"conference","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","conference":{"start_date":"2022-12-18","name":"FSTTC: Foundations of Software Technology and Theoretical Computer Science","location":"Madras, India","end_date":"2022-12-20"},"_id":"12102","date_created":"2023-01-01T23:00:50Z","file":[{"file_id":"12324","creator":"dernst","content_type":"application/pdf","checksum":"6660c802489013f034c9e8bd57f4d46e","success":1,"access_level":"open_access","file_name":"2022_LIPICs_Ahmadi.pdf","file_size":872534,"date_created":"2023-01-20T10:39:44Z","date_updated":"2023-01-20T10:39:44Z","relation":"main_file"}],"article_number":"29","year":"2022","citation":{"mla":"Ahmadi, Ali, et al. “Algorithms and Hardness Results for Computing Cores of Markov Chains.” 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 250, 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.FSTTCS.2022.29.","apa":"Ahmadi, A., Chatterjee, K., Goharshady, A. K., Meggendorfer, T., Safavi Hemami, R., & Zikelic, D. (2022). Algorithms and hardness results for computing cores of Markov chains. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 250). Madras, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29","chicago":"Ahmadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi Hemami, and Dorde Zikelic. “Algorithms and Hardness Results for Computing Cores of Markov Chains.” In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29.","short":"A. Ahmadi, K. Chatterjee, A.K. Goharshady, T. Meggendorfer, R. Safavi Hemami, D. Zikelic, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","ieee":"A. Ahmadi, K. Chatterjee, A. K. Goharshady, T. Meggendorfer, R. Safavi Hemami, and D. Zikelic, “Algorithms and hardness results for computing cores of Markov chains,” in 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Madras, India, 2022, vol. 250.","ista":"Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic D. 2022. Algorithms and hardness results for computing cores of Markov chains. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer Science vol. 250, 29.","ama":"Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic D. Algorithms and hardness results for computing cores of Markov chains. In: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:10.4230/LIPIcs.FSTTCS.2022.29"},"abstract":[{"lang":"eng","text":"Given a Markov chain M = (V, v_0, δ), with state space V and a starting state v_0, and a probability threshold ε, an ε-core is a subset C of states that is left with probability at most ε. More formally, C ⊆ V is an ε-core, iff ℙ[reach (V\\C)] ≤ ε. Cores have been applied in a wide variety of verification problems over Markov chains, Markov decision processes, and probabilistic programs, as a means of discarding uninteresting and low-probability parts of a probabilistic system and instead being able to focus on the states that are likely to be encountered in a real-world run. In this work, we focus on the problem of computing a minimal ε-core in a Markov chain. Our contributions include both negative and positive results: (i) We show that the decision problem on the existence of an ε-core of a given size is NP-complete. This solves an open problem posed in [Jan Kretínský and Tobias Meggendorfer, 2020]. We additionally show that the problem remains NP-complete even when limited to acyclic Markov chains with bounded maximal vertex degree; (ii) We provide a polynomial time algorithm for computing a minimal ε-core on Markov chains over control-flow graphs of structured programs. A straightforward combination of our algorithm with standard branch prediction techniques allows one to apply the idea of cores to find a subset of program lines that are left with low probability and then focus any desired static analysis on this core subset."}],"title":"Algorithms and hardness results for computing cores of Markov chains","publication_status":"published","file_date_updated":"2023-01-20T10:39:44Z","oa_version":"Published Version","article_processing_charge":"No","doi":"10.4230/LIPIcs.FSTTCS.2022.29","scopus_import":"1","acknowledgement":"The research was partially supported by the Hong Kong Research Grants Council ECS\r\nProject No. 26208122, ERC CoG 863818 (FoRM-SMArt), the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385, HKUST– Kaisa Joint Research Institute Project Grant HKJRI3A-055 and HKUST Startup Grant R9272. Ali Ahmadi and Roodabeh Safavi were interns at HKUST.","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959772617"]},"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","date_updated":"2025-07-14T09:09:55Z","ec_funded":1,"intvolume":" 250","oa":1,"volume":250,"author":[{"full_name":"Ahmadi, Ali","first_name":"Ali","last_name":"Ahmadi"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar"},{"last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"id":"72ed2640-8972-11ed-ae7b-f9c81ec75154","full_name":"Safavi Hemami, Roodabeh","first_name":"Roodabeh","last_name":"Safavi Hemami"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"citation":{"ama":"Bansal S, Chatterjee K, Vardi MY. On satisficing in quantitative games. In: 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol 12651. Springer Nature; 2021:20-37. doi:10.1007/978-3-030-72016-2","ieee":"S. Bansal, K. Chatterjee, and M. Y. Vardi, “On satisficing in quantitative games,” in 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Luxembourg City, Luxembourg, 2021, vol. 12651, pp. 20–37.","ista":"Bansal S, Chatterjee K, Vardi MY. 2021. On satisficing in quantitative games. 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 12651, 20–37.","mla":"Bansal, Suguman, et al. “On Satisficing in Quantitative Games.” 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 12651, Springer Nature, 2021, pp. 20–37, doi:10.1007/978-3-030-72016-2.","chicago":"Bansal, Suguman, Krishnendu Chatterjee, and Moshe Y. Vardi. “On Satisficing in Quantitative Games.” In 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 12651:20–37. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-72016-2.","short":"S. Bansal, K. Chatterjee, M.Y. Vardi, in:, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2021, pp. 20–37.","apa":"Bansal, S., Chatterjee, K., & Vardi, M. Y. (2021). On satisficing in quantitative games. In 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 12651, pp. 20–37). Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-030-72016-2"},"year":"2021","abstract":[{"lang":"eng","text":"Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games. Optimization is one form of analysis. We argue that in many cases it may be better to replace the optimization problem with the satisficing problem, where instead of searching for optimal solutions, the goal is to search for solutions that adhere to a given threshold bound.\r\nThis work defines and investigates the satisficing problem on a two-player graph game with the discounted-sum cost model. We show that while the satisficing problem can be solved using numerical methods just like the optimization problem, this approach does not render compelling benefits over optimization. When the discount factor is, however, an integer, we present another approach to satisficing, which is purely based on automata methods. We show that this approach is algorithmically more performant – both theoretically and empirically – and demonstrates the broader applicability of satisficing over optimization."}],"conference":{"end_date":"2021-04-01","location":"Luxembourg City, Luxembourg","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2021-03-27"},"file":[{"date_updated":"2023-03-28T11:00:33Z","relation":"main_file","file_size":747418,"date_created":"2023-03-28T11:00:33Z","success":1,"access_level":"open_access","file_name":"2021_LNCS_Bansal.pdf","checksum":"b020b78b23587ce7610b1aafb4e63438","content_type":"application/pdf","creator":"dernst","file_id":"12777"}],"date_created":"2023-03-26T22:01:09Z","_id":"12767","scopus_import":"1","doi":"10.1007/978-3-030-72016-2","acknowledgement":"We thank anonymous reviewers for valuable inputs. This work is supported in part by NSF grant 2030859 to the CRA for the CIFellows Project, NSF grants IIS-1527668, CCF-1704883, IIS-1830549, the ERC CoG 863818 (ForM-SMArt), and an award from the Maryland Procurement Office.","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030720155"],"eissn":["1611-3349"]},"title":"On satisficing in quantitative games","publication_status":"published","article_processing_charge":"No","oa_version":"Published Version","file_date_updated":"2023-03-28T11:00:33Z","arxiv":1,"intvolume":" 12651","department":[{"_id":"KrCh"}],"date_updated":"2025-07-14T09:09:51Z","ec_funded":1,"publication":"27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":[{"full_name":"Bansal, Suguman","first_name":"Suguman","last_name":"Bansal"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Vardi","first_name":"Moshe Y.","full_name":"Vardi, Moshe Y."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":12651,"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","project":[{"call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"page":"20-37","day":"21","quality_controlled":"1","ddc":["000"],"language":[{"iso":"eng"}],"alternative_title":["LNCS"],"month":"03","status":"public","publisher":"Springer Nature","type":"conference","external_id":{"arxiv":["2101.02594"]},"date_published":"2021-03-21T00:00:00Z"},{"has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"project":[{"name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"issue":"1","quality_controlled":"1","day":"31","page":"392-415","status":"public","isi":1,"month":"01","ddc":["510"],"language":[{"iso":"eng"}],"type":"journal_article","date_published":"2021-01-31T00:00:00Z","external_id":{"isi":["000596823800035"]},"publisher":"Elsevier","date_created":"2020-11-22T23:01:26Z","file":[{"checksum":"f1039ff5a2d6ca116720efdb84ee9d5e","content_type":"application/pdf","file_id":"9089","creator":"dernst","relation":"main_file","file_size":652739,"date_created":"2021-02-04T11:28:42Z","date_updated":"2021-02-04T11:28:42Z","access_level":"open_access","success":1,"file_name":"2021_DiscreteApplMath_Zeiner.pdf"}],"_id":"8793","abstract":[{"lang":"eng","text":"We study optimal election sequences for repeatedly selecting a (very) small group of leaders among a set of participants (players) with publicly known unique ids. In every time slot, every player has to select exactly one player that it considers to be the current leader, oblivious to the selection of the other players, but with the overarching goal of maximizing a given parameterized global (“social”) payoff function in the limit. We consider a quite generic model, where the local payoff achieved by a given player depends, weighted by some arbitrary but fixed real parameter, on the number of different leaders chosen in a round, the number of players that choose the given player as the leader, and whether the chosen leader has changed w.r.t. the previous round or not. The social payoff can be the maximum, average or minimum local payoff of the players. Possible applications include quite diverse examples such as rotating coordinator-based distributed algorithms and long-haul formation flying of social birds. Depending on the weights and the particular social payoff, optimal sequences can be very different, from simple round-robin where all players chose the same leader alternatingly every time slot to very exotic patterns, where a small group of leaders (at most 2) is elected in every time slot. Moreover, we study the question if and when a single player would not benefit w.r.t. its local payoff when deviating from the given optimal sequence, i.e., when our optimal sequences are Nash equilibria in the restricted strategy space of oblivious strategies. As this is the case for many parameterizations of our model, our results reveal that no punishment is needed to make it rational for the players to optimize the social payoff."}],"citation":{"mla":"Zeiner, Martin, et al. “Optimal Strategies for Selecting Coordinators.” Discrete Applied Mathematics, vol. 289, no. 1, Elsevier, 2021, pp. 392–415, doi:10.1016/j.dam.2020.10.022.","short":"M. Zeiner, U. Schmid, K. Chatterjee, Discrete Applied Mathematics 289 (2021) 392–415.","apa":"Zeiner, M., Schmid, U., & Chatterjee, K. (2021). Optimal strategies for selecting coordinators. Discrete Applied Mathematics. Elsevier. https://doi.org/10.1016/j.dam.2020.10.022","chicago":"Zeiner, Martin, Ulrich Schmid, and Krishnendu Chatterjee. “Optimal Strategies for Selecting Coordinators.” Discrete Applied Mathematics. Elsevier, 2021. https://doi.org/10.1016/j.dam.2020.10.022.","ama":"Zeiner M, Schmid U, Chatterjee K. Optimal strategies for selecting coordinators. Discrete Applied Mathematics. 2021;289(1):392-415. doi:10.1016/j.dam.2020.10.022","ista":"Zeiner M, Schmid U, Chatterjee K. 2021. Optimal strategies for selecting coordinators. Discrete Applied Mathematics. 289(1), 392–415.","ieee":"M. Zeiner, U. Schmid, and K. Chatterjee, “Optimal strategies for selecting coordinators,” Discrete Applied Mathematics, vol. 289, no. 1. Elsevier, pp. 392–415, 2021."},"year":"2021","article_processing_charge":"No","oa_version":"Published Version","file_date_updated":"2021-02-04T11:28:42Z","title":"Optimal strategies for selecting coordinators","publication_status":"published","publication_identifier":{"issn":["0166218X"]},"acknowledgement":"We are grateful to Matthias Függer and Thomas Nowak for having raised our interest in the problem studied in this paper.\r\nThis work has been supported the Austrian Science Fund (FWF) projects S11405, S11407 (RiSE), and P28182 (ADynNet).","article_type":"original","scopus_import":"1","doi":"10.1016/j.dam.2020.10.022","date_updated":"2023-08-04T11:12:41Z","publication":"Discrete Applied Mathematics","department":[{"_id":"KrCh"}],"intvolume":" 289","volume":289,"oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"full_name":"Zeiner, Martin","first_name":"Martin","last_name":"Zeiner"},{"last_name":"Schmid","first_name":"Ulrich","full_name":"Schmid, Ulrich"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"}]},{"date_published":"2021-01-01T00:00:00Z","type":"dissertation","publisher":"Institute of Science and Technology Austria","month":"01","status":"public","language":[{"iso":"eng"}],"ddc":["005"],"alternative_title":["ISTA Thesis"],"page":"278","day":"01","license":"https://creativecommons.org/publicdomain/zero/1.0/","tmp":{"name":"Creative Commons Public Domain Dedication (CC0 1.0)","image":"/images/cc_0.png","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","short":"CC0 (1.0)"},"project":[{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","oa":1,"related_material":{"record":[{"id":"1386","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","status":"public","id":"1437"},{"status":"public","relation":"part_of_dissertation","id":"639"},{"id":"6918","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"6490"},{"id":"7158","status":"public","relation":"part_of_dissertation"},{"id":"6009","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"949"},{"id":"311","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"7810"},{"relation":"part_of_dissertation","status":"public","id":"8089"},{"relation":"part_of_dissertation","status":"public","id":"8728"},{"status":"public","relation":"part_of_dissertation","id":"5977"},{"status":"public","relation":"part_of_dissertation","id":"6056"},{"id":"6175","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"6340"},{"status":"public","relation":"part_of_dissertation","id":"6378"},{"relation":"part_of_dissertation","status":"public","id":"6380"},{"status":"public","relation":"part_of_dissertation","id":"66"},{"id":"6780","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","status":"public","id":"7014"}]},"author":[{"last_name":"Goharshady","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"date_updated":"2025-06-02T08:53:47Z","degree_awarded":"PhD","publication_status":"published","title":"Parameterized and algebro-geometric advances in static program analysis","file_date_updated":"2021-12-23T23:30:04Z","oa_version":"Published Version","article_processing_charge":"No","doi":"10.15479/AT:ISTA:8934","acknowledgement":"The research was partially supported by an IBM PhD fellowship, a Facebook PhD fellowship, and DOC fellowship #24956 of the Austrian Academy of Sciences (OeAW).","publication_identifier":{"issn":["2663-337X"]},"_id":"8934","file":[{"checksum":"d1b9db3725aed34dadd81274aeb9426c","content_type":"application/pdf","file_id":"8969","creator":"akafshda","embargo":"2021-12-22","date_created":"2020-12-22T20:08:44Z","relation":"main_file","file_size":5251507,"date_updated":"2021-12-23T23:30:04Z","file_name":"Thesis-pdfa.pdf","access_level":"open_access"},{"relation":"source_file","embargo_to":"open_access","date_created":"2020-12-22T20:08:50Z","date_updated":"2021-03-04T23:30:04Z","file_size":10636756,"access_level":"closed","file_name":"source.zip","checksum":"1661df7b393e6866d2460eba3c905130","content_type":"application/zip","file_id":"8970","creator":"akafshda"}],"date_created":"2020-12-10T12:17:07Z","year":"2021","citation":{"ama":"Goharshady AK. Parameterized and algebro-geometric advances in static program analysis. 2021. doi:10.15479/AT:ISTA:8934","ieee":"A. K. Goharshady, “Parameterized and algebro-geometric advances in static program analysis,” Institute of Science and Technology Austria, 2021.","ista":"Goharshady AK. 2021. Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria.","apa":"Goharshady, A. K. (2021). Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8934","short":"A.K. Goharshady, Parameterized and Algebro-Geometric Advances in Static Program Analysis, Institute of Science and Technology Austria, 2021.","chicago":"Goharshady, Amir Kafshdar. “Parameterized and Algebro-Geometric Advances in Static Program Analysis.” Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/AT:ISTA:8934.","mla":"Goharshady, Amir Kafshdar. Parameterized and Algebro-Geometric Advances in Static Program Analysis. Institute of Science and Technology Austria, 2021, doi:10.15479/AT:ISTA:8934."},"abstract":[{"lang":"eng","text":"In this thesis, we consider several of the most classical and fundamental problems in static analysis and formal verification, including invariant generation, reachability analysis, termination analysis of probabilistic programs, data-flow analysis, quantitative analysis of Markov chains and Markov decision processes, and the problem of data packing in cache management.\r\nWe use techniques from parameterized complexity theory, polyhedral geometry, and real algebraic geometry to significantly improve the state-of-the-art, in terms of both scalability and completeness guarantees, for the mentioned problems. In some cases, our results are the first theoretical improvements for the respective problems in two or three decades."}],"supervisor":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"}]},{"issue":"8","quality_controlled":"1","day":"16","status":"public","isi":1,"month":"03","language":[{"iso":"eng"}],"type":"journal_article","date_published":"2021-03-16T00:00:00Z","external_id":{"isi":["000657537500003"],"arxiv":["1804.07031"]},"publisher":"Elsevier","date_created":"2021-03-28T22:01:40Z","_id":"9293","abstract":[{"text":"We consider planning problems for graphs, Markov Decision Processes (MDPs), and games on graphs in an explicit state space. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems with k different target sets: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in a given sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds, based on the boolean matrix multiplication (BMM) conjecture and strong exponential time hypothesis (SETH), establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs, and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) problem-separation results showing that for MDPs the coverage problem is harder than the sequential target problem.","lang":"eng"}],"citation":{"chicago":"Chatterjee, Krishnendu, Wolfgang Dvořák, Monika H Henzinger, and Alexander Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” Artificial Intelligence. Elsevier, 2021. https://doi.org/10.1016/j.artint.2021.103499.","short":"K. Chatterjee, W. Dvořák, M.H. Henzinger, A. Svozil, Artificial Intelligence 297 (2021).","apa":"Chatterjee, K., Dvořák, W., Henzinger, M. H., & Svozil, A. (2021). Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2021.103499","mla":"Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for Planning Problems.” Artificial Intelligence, vol. 297, no. 8, 103499, Elsevier, 2021, doi:10.1016/j.artint.2021.103499.","ieee":"K. Chatterjee, W. Dvořák, M. H. Henzinger, and A. Svozil, “Algorithms and conditional lower bounds for planning problems,” Artificial Intelligence, vol. 297, no. 8. Elsevier, 2021.","ista":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. 2021. Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. 297(8), 103499.","ama":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. 2021;297(8). doi:10.1016/j.artint.2021.103499"},"article_number":"103499","year":"2021","oa_version":"Preprint","article_processing_charge":"No","publication_status":"published","title":"Algorithms and conditional lower bounds for planning problems","publication_identifier":{"issn":["0004-3702"]},"article_type":"original","scopus_import":"1","doi":"10.1016/j.artint.2021.103499","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.07031"}],"date_updated":"2023-09-26T10:41:42Z","publication":"Artificial Intelligence","department":[{"_id":"KrCh"}],"intvolume":" 297","arxiv":1,"volume":297,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"35"}]},"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Dvořák, Wolfgang","last_name":"Dvořák","first_name":"Wolfgang"},{"orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger"},{"full_name":"Svozil, Alexander","last_name":"Svozil","first_name":"Alexander"}]},{"quality_controlled":"1","day":"16","page":"221-233","project":[{"call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"_id":"268116B8-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z00342"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"}],"date_published":"2021-02-16T00:00:00Z","external_id":{"arxiv":["2101.03928"]},"type":"conference","publisher":"Springer Nature","status":"public","month":"02","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"article_processing_charge":"No","oa_version":"Preprint","title":"On compatible matchings","publication_status":"published","acknowledgement":"A.A. funded by the Marie Skłodowska-Curie grant agreement No. 754411. Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23 (RiSE).","publication_identifier":{"issn":["03029743"],"eissn":["16113349"],"isbn":["9783030682101"]},"doi":"10.1007/978-3-030-68211-8_18","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2101.03928"}],"scopus_import":"1","_id":"9296","date_created":"2021-03-28T22:01:41Z","conference":{"name":"WALCOM: Algorithms and Computation","location":"Yangon, Myanmar","end_date":"2021-03-02","start_date":"2021-02-28"},"abstract":[{"text":" matching is compatible to two or more labeled point sets of size n with labels {1,…,n} if its straight-line drawing on each of these point sets is crossing-free. We study the maximum number of edges in a matching compatible to two or more labeled point sets in general position in the plane. We show that for any two labeled convex sets of n points there exists a compatible matching with ⌊2n−−√⌋ edges. More generally, for any ℓ labeled point sets we construct compatible matchings of size Ω(n1/ℓ) . As a corresponding upper bound, we use probabilistic arguments to show that for any ℓ given sets of n points there exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1)) edges. Finally, we show that Θ(logn) copies of any set of n points are necessary and sufficient for the existence of a labeling such that any compatible matching consists only of a single edge.","lang":"eng"}],"year":"2021","citation":{"ista":"Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec J, Vogtenhuber B. 2021. On compatible matchings. 15th International Conference on Algorithms and Computation. WALCOM: Algorithms and Computation, LNCS, vol. 12635, 221–233.","ieee":"O. Aichholzer et al., “On compatible matchings,” in 15th International Conference on Algorithms and Computation, Yangon, Myanmar, 2021, vol. 12635, pp. 221–233.","ama":"Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings. In: 15th International Conference on Algorithms and Computation. Vol 12635. Springer Nature; 2021:221-233. doi:10.1007/978-3-030-68211-8_18","mla":"Aichholzer, Oswin, et al. “On Compatible Matchings.” 15th International Conference on Algorithms and Computation, vol. 12635, Springer Nature, 2021, pp. 221–33, doi:10.1007/978-3-030-68211-8_18.","chicago":"Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada, Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible Matchings.” In 15th International Conference on Algorithms and Computation, 12635:221–33. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-68211-8_18.","apa":"Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D., Pilz, A., … Vogtenhuber, B. (2021). On compatible matchings. In 15th International Conference on Algorithms and Computation (Vol. 12635, pp. 221–233). Yangon, Myanmar: Springer Nature. https://doi.org/10.1007/978-3-030-68211-8_18","short":"O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz, J. Tkadlec, B. Vogtenhuber, in:, 15th International Conference on Algorithms and Computation, Springer Nature, 2021, pp. 221–233."},"oa":1,"related_material":{"record":[{"id":"11938","status":"public","relation":"later_version"}]},"volume":12635,"user_id":"D865714E-FA4E-11E9-B85B-F5C5E5697425","author":[{"first_name":"Oswin","last_name":"Aichholzer","full_name":"Aichholzer, Oswin"},{"last_name":"Arroyo Guevara","first_name":"Alan M","full_name":"Arroyo Guevara, Alan M","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2401-8670"},{"id":"45CFE238-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6660-1322","full_name":"Masárová, Zuzana","first_name":"Zuzana","last_name":"Masárová"},{"first_name":"Irene","last_name":"Parada","full_name":"Parada, Irene"},{"last_name":"Perz","first_name":"Daniel","full_name":"Perz, Daniel"},{"full_name":"Pilz, Alexander","first_name":"Alexander","last_name":"Pilz"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec"},{"full_name":"Vogtenhuber, Birgit","last_name":"Vogtenhuber","first_name":"Birgit"}],"publication":"15th International Conference on Algorithms and Computation","ec_funded":1,"date_updated":"2023-02-21T16:33:44Z","department":[{"_id":"UlWa"},{"_id":"HeEd"},{"_id":"KrCh"}],"intvolume":" 12635","arxiv":1},{"type":"journal_article","external_id":{"isi":["000639711200001"]},"date_published":"2021-04-01T00:00:00Z","publisher":"Public Library of Science","status":"public","isi":1,"month":"04","ddc":["000"],"language":[{"iso":"eng"}],"quality_controlled":"1","day":"01","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","project":[{"call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"issue":"4","volume":17,"oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"full_name":"Kleshnina, Maria","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","last_name":"Kleshnina","first_name":"Maria"},{"first_name":"Sabrina S.","last_name":"Streipert","full_name":"Streipert, Sabrina S."},{"full_name":"Filar, Jerzy A.","first_name":"Jerzy A.","last_name":"Filar"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"}],"ec_funded":1,"date_updated":"2025-07-14T09:10:04Z","publication":"PLoS Computational Biology","department":[{"_id":"KrCh"}],"intvolume":" 17","oa_version":"Published Version","article_processing_charge":"No","file_date_updated":"2021-05-11T13:50:06Z","title":"Mistakes can stabilise the dynamics of rock-paper-scissors games","publication_status":"published","acknowledgement":"Authors would like to thank Christian Hilbe and Martin Nowak for their inspiring and very helpful feedback on the manuscript.","publication_identifier":{"issn":["1553734X"],"eissn":["15537358"]},"article_type":"original","scopus_import":"1","doi":"10.1371/journal.pcbi.1008523","file":[{"content_type":"application/pdf","creator":"kschuh","file_id":"9385","checksum":"a94ebe0c4116f5047eaa6029e54d2dac","file_name":"2021_pcbi_Kleshnina.pdf","success":1,"access_level":"open_access","date_updated":"2021-05-11T13:50:06Z","file_size":1323820,"date_created":"2021-05-11T13:50:06Z","relation":"main_file"}],"date_created":"2021-05-09T22:01:38Z","_id":"9381","abstract":[{"lang":"eng","text":"A game of rock-paper-scissors is an interesting example of an interaction where none of the pure strategies strictly dominates all others, leading to a cyclic pattern. In this work, we consider an unstable version of rock-paper-scissors dynamics and allow individuals to make behavioural mistakes during the strategy execution. We show that such an assumption can break a cyclic relationship leading to a stable equilibrium emerging with only one strategy surviving. We consider two cases: completely random mistakes when individuals have no bias towards any strategy and a general form of mistakes. Then, we determine conditions for a strategy to dominate all other strategies. However, given that individuals who adopt a dominating strategy are still prone to behavioural mistakes in the observed behaviour, we may still observe extinct strategies. That is, behavioural mistakes in strategy execution stabilise evolutionary dynamics leading to an evolutionary stable and, potentially, mixed co-existence equilibrium."}],"citation":{"mla":"Kleshnina, Maria, et al. “Mistakes Can Stabilise the Dynamics of Rock-Paper-Scissors Games.” PLoS Computational Biology, vol. 17, no. 4, e1008523, Public Library of Science, 2021, doi:10.1371/journal.pcbi.1008523.","short":"M. Kleshnina, S.S. Streipert, J.A. Filar, K. Chatterjee, PLoS Computational Biology 17 (2021).","chicago":"Kleshnina, Maria, Sabrina S. Streipert, Jerzy A. Filar, and Krishnendu Chatterjee. “Mistakes Can Stabilise the Dynamics of Rock-Paper-Scissors Games.” PLoS Computational Biology. Public Library of Science, 2021. https://doi.org/10.1371/journal.pcbi.1008523.","apa":"Kleshnina, M., Streipert, S. S., Filar, J. A., & Chatterjee, K. (2021). Mistakes can stabilise the dynamics of rock-paper-scissors games. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1008523","ama":"Kleshnina M, Streipert SS, Filar JA, Chatterjee K. Mistakes can stabilise the dynamics of rock-paper-scissors games. PLoS Computational Biology. 2021;17(4). doi:10.1371/journal.pcbi.1008523","ieee":"M. Kleshnina, S. S. Streipert, J. A. Filar, and K. Chatterjee, “Mistakes can stabilise the dynamics of rock-paper-scissors games,” PLoS Computational Biology, vol. 17, no. 4. Public Library of Science, 2021.","ista":"Kleshnina M, Streipert SS, Filar JA, Chatterjee K. 2021. Mistakes can stabilise the dynamics of rock-paper-scissors games. PLoS Computational Biology. 17(4), e1008523."},"year":"2021","article_number":"e1008523"},{"publication":"Formal Methods in System Design","date_updated":"2023-10-10T11:13:20Z","ec_funded":1,"department":[{"_id":"KrCh"}],"intvolume":" 57","arxiv":1,"oa":1,"volume":57,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","first_name":"Rasmus"},{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"_id":"9393","date_created":"2021-05-16T22:01:47Z","abstract":[{"text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.","lang":"eng"}],"year":"2021","citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design. Springer, 2021. https://doi.org/10.1007/s10703-021-00373-5.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-021-00373-5","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design, vol. 57, Springer, 2021, pp. 401–28, doi:10.1007/s10703-021-00373-5.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 2021;57:401-428. doi:10.1007/s10703-021-00373-5","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 57, 401–428.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” Formal Methods in System Design, vol. 57. Springer, pp. 401–428, 2021."},"oa_version":"Preprint","article_processing_charge":"No","publication_status":"published","title":"Faster algorithms for quantitative verification in bounded treewidth graphs","article_type":"original","publication_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.07384"}],"doi":"10.1007/s10703-021-00373-5","scopus_import":"1","status":"public","month":"09","isi":1,"language":[{"iso":"eng"}],"date_published":"2021-09-01T00:00:00Z","external_id":{"isi":["000645490300001"],"arxiv":["1504.07384"]},"type":"journal_article","publisher":"Springer","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","day":"01","page":"401-428"},{"date_published":"2021-05-13T00:00:00Z","external_id":{"pmid":["33986519"],"isi":["000650304000002"]},"type":"journal_article","publisher":"Springer Nature","pmid":1,"month":"05","isi":1,"status":"public","language":[{"iso":"eng"}],"ddc":["000"],"quality_controlled":"1","page":"1292–1302","day":"13","issue":"10","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"}],"has_accepted_license":"1","oa":1,"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"10293"}],"link":[{"description":"News on IST Homepage","relation":"press_release","url":"https://ist.ac.at/en/news/the-emergence-of-cooperation/"}]},"volume":5,"author":[{"first_name":"Laura","last_name":"Schmid","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","full_name":"Schmid, Laura"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Hilbe, Christian","orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe","first_name":"Christian"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publication":"Nature Human Behaviour","date_updated":"2025-07-14T09:10:09Z","ec_funded":1,"intvolume":" 5","publication_status":"published","title":"A unified framework of direct and indirect reciprocity","file_date_updated":"2023-11-07T08:27:23Z","oa_version":"Submitted Version","article_processing_charge":"No","doi":"10.1038/s41562-021-01114-8","scopus_import":"1","article_type":"original","acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.), the European Research Council Start Grant 279307: Graph Games (to K.C.), and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.). The funders had no role in study design, data collection and analysis, decision to publish or preparation of the manuscript.","publication_identifier":{"eissn":["2397-3374"]},"_id":"9402","date_created":"2021-05-18T16:56:57Z","file":[{"access_level":"open_access","success":1,"file_name":"2021_NatureHumanBehaviour_Schmid_accepted.pdf","relation":"main_file","file_size":5232761,"date_created":"2023-11-07T08:27:23Z","date_updated":"2023-11-07T08:27:23Z","content_type":"application/pdf","creator":"dernst","file_id":"14496","checksum":"34f55e173f90dc1dab731063458ac780"}],"year":"2021","citation":{"ieee":"L. Schmid, K. Chatterjee, C. Hilbe, and M. A. Nowak, “A unified framework of direct and indirect reciprocity,” Nature Human Behaviour, vol. 5, no. 10. Springer Nature, pp. 1292–1302, 2021.","ista":"Schmid L, Chatterjee K, Hilbe C, Nowak MA. 2021. A unified framework of direct and indirect reciprocity. Nature Human Behaviour. 5(10), 1292–1302.","ama":"Schmid L, Chatterjee K, Hilbe C, Nowak MA. A unified framework of direct and indirect reciprocity. Nature Human Behaviour. 2021;5(10):1292–1302. doi:10.1038/s41562-021-01114-8","mla":"Schmid, Laura, et al. “A Unified Framework of Direct and Indirect Reciprocity.” Nature Human Behaviour, vol. 5, no. 10, Springer Nature, 2021, pp. 1292–1302, doi:10.1038/s41562-021-01114-8.","apa":"Schmid, L., Chatterjee, K., Hilbe, C., & Nowak, M. A. (2021). A unified framework of direct and indirect reciprocity. Nature Human Behaviour. Springer Nature. https://doi.org/10.1038/s41562-021-01114-8","short":"L. Schmid, K. Chatterjee, C. Hilbe, M.A. Nowak, Nature Human Behaviour 5 (2021) 1292–1302.","chicago":"Schmid, Laura, Krishnendu Chatterjee, Christian Hilbe, and Martin A. Nowak. “A Unified Framework of Direct and Indirect Reciprocity.” Nature Human Behaviour. Springer Nature, 2021. https://doi.org/10.1038/s41562-021-01114-8."},"abstract":[{"lang":"eng","text":"Direct and indirect reciprocity are key mechanisms for the evolution of cooperation. Direct reciprocity means that individuals use their own experience to decide whether to cooperate with another person. Indirect reciprocity means that they also consider the experiences of others. Although these two mechanisms are intertwined, they are typically studied in isolation. Here, we introduce a mathematical framework that allows us to explore both kinds of reciprocity simultaneously. We show that the well-known ‘generous tit-for-tat’ strategy of direct reciprocity has a natural analogue in indirect reciprocity, which we call ‘generous scoring’. Using an equilibrium analysis, we characterize under which conditions either of the two strategies can maintain cooperation. With simulations, we additionally explore which kind of reciprocity evolves when members of a population engage in social learning to adapt to their environment. Our results draw unexpected connections between direct and indirect reciprocity while highlighting important differences regarding their evolvability."}]},{"quality_controlled":"1","title":"The evolution of strategic ignorance in strategic interaction","article_processing_charge":"No","oa_version":"Published Version","page":"139-152","main_file_link":[{"open_access":"1","url":"https://esforum.de/publications/PDFs/sfr29/SFR29_09_Hilbe%20and%20Schmid.pdf"}],"day":"01","publication_identifier":{"isbn":["978-0-262-04559-9"]},"editor":[{"last_name":"Hertwig","first_name":"Ralph","full_name":"Hertwig, Ralph"},{"first_name":"Christoph","last_name":"Engel","full_name":"Engel, Christoph"}],"date_created":"2021-05-19T12:25:42Z","_id":"9403","citation":{"mla":"Schmid, Laura, and Christian Hilbe. “The Evolution of Strategic Ignorance in Strategic Interaction.” Deliberate Ignorance: Choosing Not To Know, edited by Ralph Hertwig and Christoph Engel, vol. 29, MIT Press, 2021, pp. 139–52.","short":"L. Schmid, C. Hilbe, in:, R. Hertwig, C. Engel (Eds.), Deliberate Ignorance: Choosing Not To Know, MIT Press, 2021, pp. 139–152.","chicago":"Schmid, Laura, and Christian Hilbe. “The Evolution of Strategic Ignorance in Strategic Interaction.” In Deliberate Ignorance: Choosing Not To Know, edited by Ralph Hertwig and Christoph Engel, 29:139–52. Strüngmann Forum Reports. MIT Press, 2021.","apa":"Schmid, L., & Hilbe, C. (2021). The evolution of strategic ignorance in strategic interaction. In R. Hertwig & C. Engel (Eds.), Deliberate Ignorance: Choosing Not To Know (Vol. 29, pp. 139–152). MIT Press.","ama":"Schmid L, Hilbe C. The evolution of strategic ignorance in strategic interaction. In: Hertwig R, Engel C, eds. Deliberate Ignorance: Choosing Not To Know. Vol 29. Strüngmann Forum Reports. MIT Press; 2021:139-152.","ieee":"L. Schmid and C. Hilbe, “The evolution of strategic ignorance in strategic interaction,” in Deliberate Ignorance: Choosing Not To Know, vol. 29, R. Hertwig and C. Engel, Eds. MIT Press, 2021, pp. 139–152.","ista":"Schmid L, Hilbe C. 2021.The evolution of strategic ignorance in strategic interaction. In: Deliberate Ignorance: Choosing Not To Know. vol. 29, 139–152."},"year":"2021","abstract":[{"lang":"eng","text":"Optimal decision making requires individuals to know their available options and to anticipate correctly what consequences these options have. In many social interactions, however, we refrain from gathering all relevant information, even if this information would help us make better decisions and is costless to obtain. This chapter examines several examples of “deliberate ignorance.” Two simple models are proposed to illustrate how ignorance can evolve among self-interested and payoff - maximizing individuals, and open problems are highlighted that lie ahead for future research to explore."}],"type":"book_chapter","series_title":"Strüngmann Forum Reports","date_published":"2021-03-01T00:00:00Z","volume":29,"oa":1,"author":[{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6978-7329","full_name":"Schmid, Laura","first_name":"Laura","last_name":"Schmid"},{"full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe"}],"publisher":"MIT Press","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"month":"03","date_updated":"2023-02-23T13:57:04Z","publication":"Deliberate Ignorance: Choosing Not To Know","status":"public","language":[{"iso":"eng"}],"intvolume":" 29"},{"abstract":[{"text":"We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with n vertices and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires O(n2) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(nm−−√) symbolic operations and O(m−−√) symbolic space. A main open question is whether the worst-case O(n2) bound for symbolic operations can be beaten. We present a symbolic algorithm that requires O˜(n1.5) symbolic operations and O˜(n−−√) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all 0<ϵ≤1/2 the symbolic algorithm requires O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space ( O˜ hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of ω -regular objectives for MDPs. We consider the canonical parity objectives for ω -regular objectives, and for parity objectives with d -priorities we present an algorithm that computes the almost-sure winning region with O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space, for all 0<ϵ≤1/2 .","lang":"eng"}],"year":"2021","citation":{"ieee":"K. Chatterjee, W. Dvorak, M. H. Henzinger, and A. Svozil, “Symbolic time and space tradeoffs for probabilistic verification,” in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Rome, Italy, 2021, pp. 1–13.","ista":"Chatterjee K, Dvorak W, Henzinger MH, Svozil A. 2021. Symbolic time and space tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science, 1–13.","ama":"Chatterjee K, Dvorak W, Henzinger MH, Svozil A. Symbolic time and space tradeoffs for probabilistic verification. In: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute of Electrical and Electronics Engineers; 2021:1-13. doi:10.1109/LICS52264.2021.9470739","mla":"Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13, doi:10.1109/LICS52264.2021.9470739.","short":"K. Chatterjee, W. Dvorak, M.H. Henzinger, A. Svozil, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorak, Monika H Henzinger, and Alexander Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 1–13. Institute of Electrical and Electronics Engineers, 2021. https://doi.org/10.1109/LICS52264.2021.9470739.","apa":"Chatterjee, K., Dvorak, W., Henzinger, M. H., & Svozil, A. (2021). Symbolic time and space tradeoffs for probabilistic verification. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 1–13). Rome, Italy: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LICS52264.2021.9470739"},"_id":"10002","date_created":"2021-09-12T22:01:24Z","conference":{"name":"LICS: Symposium on Logic in Computer Science","location":"Rome, Italy","end_date":"2021-07-02","start_date":"2021-06-29"},"publication_identifier":{"eisbn":["978-1-6654-4895-6"],"isbn":["978-1-6654-4896-3"],"issn":["1043-6871"]},"acknowledgement":"The authors are grateful to the anonymous referees for their valuable comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For M. H. the research leading to these results has received funding from the European Research Council under the European Unions Seventh Framework Programme (FP/2007–2013) / ERC Grant Agreement no. 340506.","doi":"10.1109/LICS52264.2021.9470739","main_file_link":[{"url":"https://arxiv.org/abs/2104.07466","open_access":"1"}],"scopus_import":"1","oa_version":"Preprint","article_processing_charge":"No","title":"Symbolic time and space tradeoffs for probabilistic verification","publication_status":"published","arxiv":1,"publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","ec_funded":1,"date_updated":"2025-07-14T09:10:07Z","department":[{"_id":"KrCh"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Dvorak, Wolfgang","last_name":"Dvorak","first_name":"Wolfgang"},{"last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530"},{"last_name":"Svozil","first_name":"Alexander","full_name":"Svozil, Alexander"}],"oa":1,"project":[{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"day":"07","page":"1-13","quality_controlled":"1","keyword":["Computer science","Computational modeling","Markov processes","Probabilistic logic","Formal verification","Game Theory"],"language":[{"iso":"eng"}],"status":"public","month":"07","isi":1,"publisher":"Institute of Electrical and Electronics Engineers","date_published":"2021-07-07T00:00:00Z","external_id":{"isi":["000947350400089"],"arxiv":["2104.07466"]},"type":"conference"},{"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"}],"quality_controlled":"1","day":"07","page":"1-13","status":"public","month":"07","isi":1,"keyword":["Computer science","Heuristic algorithms","Memory management","Automata","Markov processes","Probability distribution","Complexity theory"],"language":[{"iso":"eng"}],"external_id":{"arxiv":["2104.07278"],"isi":["000947350400036"]},"date_published":"2021-07-07T00:00:00Z","type":"conference","publisher":"Institute of Electrical and Electronics Engineers","_id":"10004","date_created":"2021-09-12T22:01:25Z","conference":{"start_date":"2021-06-29","location":"Rome, Italy","name":"LICS: Symposium on Logic in Computer Science","end_date":"2021-07-02"},"abstract":[{"text":"Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs.","lang":"eng"}],"year":"2021","citation":{"short":"K. Chatterjee, L. Doyen, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 1–13. Institute of Electrical and Electronics Engineers, 2021. https://doi.org/10.1109/LICS52264.2021.9470595.","apa":"Chatterjee, K., & Doyen, L. (2021). Stochastic processes with expected stopping time. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 1–13). Rome, Italy: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LICS52264.2021.9470595","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13, doi:10.1109/LICS52264.2021.9470595.","ama":"Chatterjee K, Doyen L. Stochastic processes with expected stopping time. In: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute of Electrical and Electronics Engineers; 2021:1-13. doi:10.1109/LICS52264.2021.9470595","ista":"Chatterjee K, Doyen L. 2021. Stochastic processes with expected stopping time. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science, 1–13.","ieee":"K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,” in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Rome, Italy, 2021, pp. 1–13."},"article_processing_charge":"No","oa_version":"Preprint","title":"Stochastic processes with expected stopping time","publication_status":"published","publication_identifier":{"issn":["1043-6871"],"eisbn":["978-1-6654-4895-6"],"isbn":["978-1-6654-4896-3"]},"acknowledgement":"We are grateful to the anonymous reviewers of LICS 2021 and of a previous version of this paper for insightful comments that helped improving the presentation. This research was partially supported by the grant ERC CoG 863818 (ForM-SMArt).","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2104.07278"}],"doi":"10.1109/LICS52264.2021.9470595","scopus_import":"1","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","date_updated":"2025-07-14T09:10:08Z","ec_funded":1,"department":[{"_id":"KrCh"}],"arxiv":1,"oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"}]},{"publisher":"Schloss Dagstuhl - Leibniz Zentrum für Informatik","external_id":{"arxiv":["2107.04683"]},"date_published":"2021-08-13T00:00:00Z","type":"conference","alternative_title":["LIPIcs"],"language":[{"iso":"eng"}],"ddc":["000"],"status":"public","month":"08","day":"13","quality_controlled":"1","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","grant_number":"754411"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","full_name":"Jecker, Ismael R","first_name":"Ismael R","last_name":"Jecker"},{"first_name":"Nicolas","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas"},{"full_name":"Wolf, Petra","last_name":"Wolf","first_name":"Petra"}],"oa":1,"volume":203,"intvolume":" 203","arxiv":1,"publication":"32nd International Conference on Concurrency Theory","ec_funded":1,"date_updated":"2022-05-13T08:12:52Z","department":[{"_id":"KrCh"}],"acknowledgement":"Ismaël Jecker: Marie Skłodowska-Curie Grant Agreement No. 754411. Nicolas Mazzocchi: BOSCO project PGC2018-102210-B-I00 (MCIU/AEI/FEDER, UE), BLOQUESCM project S2018/TCS-4339, and MINECO grant RYC-2016-20281.\r\nPetra Wolf : DFG project FE 560/9-1.\r\n","publication_identifier":{"isbn":["978-3-9597-7203-7"],"issn":["1868-8969"]},"doi":"10.4230/LIPIcs.CONCUR.2021.18","scopus_import":"1","file_date_updated":"2021-10-01T11:10:53Z","article_processing_charge":"No","oa_version":"Published Version","title":"Decomposing permutation automata","publication_status":"published","abstract":[{"text":"A deterministic finite automaton (DFA) 𝒜 is composite if its language L(𝒜) can be decomposed into an intersection ⋂_{i = 1}^k L(𝒜_i) of languages of smaller DFAs. Otherwise, 𝒜 is prime. This notion of primality was introduced by Kupferman and Mosheiff in 2013, and while they proved that we can decide whether a DFA is composite, the precise complexity of this problem is still open, with a doubly-exponential gap between the upper and lower bounds. In this work, we focus on permutation DFAs, i.e., those for which the transition monoid is a group. We provide an NP algorithm to decide whether a permutation DFA is composite, and show that the difficulty of this problem comes from the number of non-accepting states of the instance: we give a fixed-parameter tractable algorithm with the number of rejecting states as the parameter. Moreover, we investigate the class of commutative permutation DFAs. Their structural properties allow us to decide compositionality in NL, and even in LOGSPACE if the alphabet size is fixed. Despite this low complexity, we show that complex behaviors still arise in this class: we provide a family of composite DFAs each requiring polynomially many factors with respect to its size. We also consider the variant of the problem that asks whether a DFA is k-factor composite, that is, decomposable into k smaller DFAs, for some given integer k ∈ ℕ. We show that, for commutative permutation DFAs, restricting the number of factors makes the decision computationally harder, and yields a problem with tight bounds: it is NP-complete. Finally, we show that in general, this problem is in PSPACE, and it is in LOGSPACE for DFAs with a singleton alphabet.","lang":"eng"}],"article_number":"18","year":"2021","citation":{"apa":"Jecker, I. R., Mazzocchi, N., & Wolf, P. (2021). Decomposing permutation automata. In 32nd International Conference on Concurrency Theory (Vol. 203). Paris, France: Schloss Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2021.18","chicago":"Jecker, Ismael R, Nicolas Mazzocchi, and Petra Wolf. “Decomposing Permutation Automata.” In 32nd International Conference on Concurrency Theory, Vol. 203. Schloss Dagstuhl - Leibniz Zentrum für Informatik, 2021. https://doi.org/10.4230/LIPIcs.CONCUR.2021.18.","short":"I.R. Jecker, N. Mazzocchi, P. Wolf, in:, 32nd International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz Zentrum für Informatik, 2021.","mla":"Jecker, Ismael R., et al. “Decomposing Permutation Automata.” 32nd International Conference on Concurrency Theory, vol. 203, 18, Schloss Dagstuhl - Leibniz Zentrum für Informatik, 2021, doi:10.4230/LIPIcs.CONCUR.2021.18.","ama":"Jecker IR, Mazzocchi N, Wolf P. Decomposing permutation automata. In: 32nd International Conference on Concurrency Theory. Vol 203. Schloss Dagstuhl - Leibniz Zentrum für Informatik; 2021. doi:10.4230/LIPIcs.CONCUR.2021.18","ista":"Jecker IR, Mazzocchi N, Wolf P. 2021. Decomposing permutation automata. 32nd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 203, 18.","ieee":"I. R. Jecker, N. Mazzocchi, and P. Wolf, “Decomposing permutation automata,” in 32nd International Conference on Concurrency Theory, Paris, France, 2021, vol. 203."},"_id":"10052","date_created":"2021-09-27T14:33:14Z","file":[{"date_created":"2021-10-01T11:10:53Z","relation":"main_file","date_updated":"2021-10-01T11:10:53Z","file_size":1003552,"file_name":"2021_CONCUR_Jecker.pdf","success":1,"access_level":"open_access","checksum":"4722c81be82265cf45e78adf9db91250","content_type":"application/pdf","file_id":"10064","creator":"cchlebak"}],"conference":{"end_date":"2021-08-27","location":"Paris, France","name":"CONCUR: Conference on Concurrency Theory","start_date":"2021-08-23"}}]