[{"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Dvorák, Wolfgang","first_name":"Wolfgang","last_name":"Dvorák"},{"full_name":"Henzinger, Monika H","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","orcid":"0000-0002-5008-6530"},{"full_name":"Svozil, Alexander","first_name":"Alexander","last_name":"Svozil"}],"month":"08","conference":{"location":"Amsterdam, Netherlands","end_date":"2019-08-30","name":"CONCUR: International Conference on Concurrency Theory","start_date":"2019-08-27"},"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","file":[{"creator":"kschuh","content_type":"application/pdf","file_size":730112,"relation":"main_file","access_level":"open_access","file_name":"2019_LIPIcs_Chatterjee.pdf","file_id":"6922","checksum":"e1f0e4061212454574f34a1368d018ec","date_created":"2019-10-01T08:20:30Z","date_updated":"2020-07-14T12:47:43Z"}],"day":"01","oa_version":"Published Version","status":"public","type":"conference","alternative_title":["LIPIcs"],"article_processing_charge":"No","oa":1,"date_updated":"2022-08-12T10:54:34Z","title":"Near-linear time algorithms for Streett objectives in graphs and MDPs","intvolume":" 140","has_accepted_license":"1","scopus_import":"1","language":[{"iso":"eng"}],"publication":"Leibniz International Proceedings in Informatics","publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"abstract":[{"lang":"eng","text":"The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time O(min(n^2, m sqrt{m log n}) + b log n). In this work we present randomized near-linear time algorithms, with expected running time O~(m + b), where the O~ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors. "}],"project":[{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"date_published":"2019-08-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":140,"quality_controlled":"1","department":[{"_id":"KrCh"}],"year":"2019","citation":{"apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., & Svozil, A. (2019). Near-linear time algorithms for Streett objectives in graphs and MDPs. In Leibniz International Proceedings in Informatics (Vol. 140). Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.CONCUR.2019.7","short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","ama":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. Near-linear time algorithms for Streett objectives in graphs and MDPs. In: Leibniz International Proceedings in Informatics. Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.CONCUR.2019.7","ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and A. Svozil, “Near-linear time algorithms for Streett objectives in graphs and MDPs,” in Leibniz International Proceedings in Informatics, Amsterdam, Netherlands, 2019, vol. 140.","mla":"Chatterjee, Krishnendu, et al. “Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs.” Leibniz International Proceedings in Informatics, vol. 140, 7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.CONCUR.2019.7.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Alexander Svozil. “Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs.” In Leibniz International Proceedings in Informatics, Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.7.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. 2019. Near-linear time algorithms for Streett objectives in graphs and MDPs. Leibniz International Proceedings in Informatics. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 7."},"date_created":"2019-09-18T08:07:58Z","article_number":"7","ec_funded":1,"_id":"6887","file_date_updated":"2020-07-14T12:47:43Z","doi":"10.4230/LIPICS.CONCUR.2019.7"},{"doi":"10.4230/LIPICS.CONCUR.2019.6","file_date_updated":"2020-07-14T12:47:43Z","_id":"6889","article_number":"6","year":"2019","citation":{"ista":"Chatterjee K, Piterman N. 2019. Combinations of Qualitative Winning for Stochastic Parity Games. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 6.","mla":"Chatterjee, Krishnendu, and Nir Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. Vol. 140, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.CONCUR.2019.6.","chicago":"Chatterjee, Krishnendu, and Nir Piterman. “Combinations of Qualitative Winning for Stochastic Parity Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.6.","short":"K. Chatterjee, N. Piterman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","ieee":"K. Chatterjee and N. Piterman, “Combinations of Qualitative Winning for Stochastic Parity Games,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","ama":"Chatterjee K, Piterman N. Combinations of Qualitative Winning for Stochastic Parity Games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.CONCUR.2019.6","apa":"Chatterjee, K., & Piterman, N. (2019). Combinations of Qualitative Winning for Stochastic Parity Games (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.CONCUR.2019.6"},"date_created":"2019-09-18T08:11:43Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2019-08-01T00:00:00Z","department":[{"_id":"KrCh"}],"volume":140,"quality_controlled":"1","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"abstract":[{"text":"We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games. ","lang":"eng"}],"publication_status":"published","language":[{"iso":"eng"}],"has_accepted_license":"1","scopus_import":1,"intvolume":" 140","date_updated":"2021-01-12T08:09:28Z","oa":1,"title":"Combinations of Qualitative Winning for Stochastic Parity Games","alternative_title":["LIPIcs"],"status":"public","type":"conference","conference":{"start_date":"2019-08-27","name":"CONCUR: International Conference on Concurrency Theory","end_date":"2019-08-30","location":"Amsterdam, Netherlands"},"month":"08","day":"01","oa_version":"Published Version","file":[{"checksum":"7b2ecfd4d9d02360308c0ca986fc10a7","file_id":"6923","file_name":"2019_LIPIcs_Chatterjee.pdf","date_updated":"2020-07-14T12:47:43Z","date_created":"2019-10-01T08:49:45Z","creator":"kschuh","content_type":"application/pdf","relation":"main_file","file_size":509163,"access_level":"open_access"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Piterman","first_name":"Nir","full_name":"Piterman, Nir"}]},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"abstract":[{"lang":"eng","text":"The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning."}],"external_id":{"arxiv":["1909.00989"]},"publication_status":"published","date_published":"2019-10-10T00:00:00Z","publisher":"ACM","volume":3,"quality_controlled":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"related_material":{"record":[{"id":"10199","relation":"dissertation_contains","status":"public"}]},"article_number":"124","year":"2019","acknowledgement":"The authors would also like to thank anonymous referees for their valuable comments and helpful suggestions. This work is supported by the Austrian Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE), by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian Science Fund (FWF) Schrodinger grant J-4220.\r\n","keyword":["safety","risk","reliability and quality","software"],"citation":{"ista":"Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124.","mla":"Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, vol. 3, 124, ACM, 2019, doi:10.1145/3360550.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric Dynamic Partial Order Reduction.” In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Vol. 3. ACM, 2019. https://doi.org/10.1145/3360550.","short":"K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019.","ama":"Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. Vol 3. ACM; 2019. doi:10.1145/3360550","ieee":"K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Athens, Greece, 2019, vol. 3.","apa":"Chatterjee, K., Pavlogiannis, A., & Toman, V. (2019). Value-centric dynamic partial order reduction. In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Vol. 3). Athens, Greece: ACM. https://doi.org/10.1145/3360550"},"date_created":"2021-10-27T14:57:06Z","doi":"10.1145/3360550","_id":"10190","file_date_updated":"2021-11-12T11:41:56Z","month":"10","publication_identifier":{"eissn":["2475-1421"]},"conference":{"start_date":"2019-10-23","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","end_date":"2019-10-25","location":"Athens, Greece"},"file":[{"content_type":"application/pdf","file_size":570829,"relation":"main_file","access_level":"open_access","creator":"cchlebak","date_created":"2021-11-12T11:41:56Z","date_updated":"2021-11-12T11:41:56Z","success":1,"file_name":"2019_ACM_Chatterjee.pdf","file_id":"10278","checksum":"2149979c46964c4d117af06ccb6c0834"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","day":"10","main_file_link":[{"open_access":"1","url":"https://dl.acm.org/doi/10.1145/3360550"}],"oa_version":"Published Version","arxiv":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"},{"last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-9036-063X","first_name":"Viktor","full_name":"Toman, Viktor"}],"type":"conference","status":"public","has_accepted_license":"1","intvolume":" 3","article_processing_charge":"No","date_updated":"2025-07-14T09:10:15Z","oa":1,"title":"Value-centric dynamic partial order reduction","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","language":[{"iso":"eng"}]},{"file_date_updated":"2020-07-14T12:48:14Z","_id":"86","doi":"10.1007/978-3-319-95246-8_9","date_created":"2018-12-11T11:44:33Z","publist_id":"7968","citation":{"apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2018). Computing average response time. In M. Lohstroh, P. Derler, & M. Sirjani (Eds.), Principles of Modeling (Vol. 10760, pp. 143–161). Springer. https://doi.org/10.1007/978-3-319-95246-8_9","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling, Springer, 2018, pp. 143–161.","ama":"Chatterjee K, Henzinger TA, Otop J. Computing average response time. In: Lohstroh M, Derler P, Sirjani M, eds. Principles of Modeling. Vol 10760. Springer; 2018:143-161. doi:10.1007/978-3-319-95246-8_9","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Computing average response time,” in Principles of Modeling, vol. 10760, M. Lohstroh, P. Derler, and M. Sirjani, Eds. Springer, 2018, pp. 143–161.","mla":"Chatterjee, Krishnendu, et al. “Computing Average Response Time.” Principles of Modeling, edited by Marten Lohstroh et al., vol. 10760, Springer, 2018, pp. 143–61, doi:10.1007/978-3-319-95246-8_9.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Computing Average Response Time.” In Principles of Modeling, edited by Marten Lohstroh, Patricia Derler, and Marjan Sirjani, 10760:143–61. Springer, 2018. https://doi.org/10.1007/978-3-319-95246-8_9.","ista":"Chatterjee K, Henzinger TA, Otop J. 2018.Computing average response time. In: Principles of Modeling. LNCS, vol. 10760, 143–161."},"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11407-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.","year":"2018","ec_funded":1,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"page":"143 - 161","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":10760,"quality_controlled":"1","publisher":"Springer","date_published":"2018-07-20T00:00:00Z","publication_status":"published","abstract":[{"text":"Responsiveness—the requirement that every request to a system be eventually handled—is one of the fundamental liveness properties of a reactive system. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. We show how average response time can be computed on state-transition graphs, on Markov chains, and on game graphs. In all three cases, we give polynomial-time algorithms.","lang":"eng"}],"ddc":["000"],"language":[{"iso":"eng"}],"publication":"Principles of Modeling","title":"Computing average response time","oa":1,"date_updated":"2021-01-12T08:20:14Z","intvolume":" 10760","has_accepted_license":"1","scopus_import":1,"editor":[{"full_name":"Lohstroh, Marten","first_name":"Marten","last_name":"Lohstroh"},{"last_name":"Derler","first_name":"Patricia","full_name":"Derler, Patricia"},{"first_name":"Marjan","full_name":"Sirjani, Marjan","last_name":"Sirjani"}],"alternative_title":["LNCS"],"status":"public","type":"book_chapter","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Submitted Version","day":"20","file":[{"date_created":"2019-11-19T08:22:18Z","date_updated":"2020-07-14T12:48:14Z","checksum":"9995c6ce6957333baf616fc4f20be597","file_id":"7053","file_name":"2018_PrinciplesModeling_Chatterjee.pdf","relation":"main_file","content_type":"application/pdf","file_size":516307,"access_level":"open_access","creator":"dernst"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07"},{"status":"public","type":"journal_article","month":"01","day":"01","oa_version":"Published Version","file":[{"creator":"system","access_level":"open_access","relation":"main_file","file_size":1163507,"content_type":"application/pdf","checksum":"c2590ef160709d8054cf29ee173f1454","file_name":"IST-2018-960-v1+1_2017_Chatterjee_Automated_competetive.pdf","file_id":"5267","date_updated":"2020-07-14T12:47:56Z","date_created":"2018-12-12T10:17:14Z"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"},{"first_name":"Alexander","full_name":"Kößler, Alexander","last_name":"Kößler"},{"full_name":"Schmid, Ulrich","first_name":"Ulrich","last_name":"Schmid"}],"publication":"Real-Time Systems","language":[{"iso":"eng"}],"isi":1,"scopus_import":"1","has_accepted_license":"1","intvolume":" 54","oa":1,"pubrep_id":"960","date_updated":"2023-09-27T12:52:38Z","issue":"1","article_processing_charge":"No","title":"Automated competitive analysis of real time scheduling with graph games","publisher":"Springer","date_published":"2018-01-01T00:00:00Z","department":[{"_id":"KrCh"}],"page":"166 - 207","quality_controlled":"1","volume":54,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"isi":["000419955500006"]},"abstract":[{"text":"This paper is devoted to automatic competitive analysis of real-time scheduling algorithms for firm-deadline tasksets, where only completed tasks con- tribute some utility to the system. Given such a taskset T , the competitive ratio of an on-line scheduling algorithm A for T is the worst-case utility ratio of A over the utility achieved by a clairvoyant algorithm. We leverage the theory of quantitative graph games to address the competitive analysis and competitive synthesis problems. For the competitive analysis case, given any taskset T and any finite-memory on- line scheduling algorithm A , we show that the competitive ratio of A in T can be computed in polynomial time in the size of the state space of A . Our approach is flexible as it also provides ways to model meaningful constraints on the released task sequences that determine the competitive ratio. We provide an experimental study of many well-known on-line scheduling algorithms, which demonstrates the feasibility of our competitive analysis approach that effectively replaces human ingenuity (required Preliminary versions of this paper have appeared in Chatterjee et al. ( 2013 , 2014 ). B Andreas Pavlogiannis pavlogiannis@ist.ac.at Krishnendu Chatterjee krish.chat@ist.ac.at Alexander Kößler koe@ecs.tuwien.ac.at Ulrich Schmid s@ecs.tuwien.ac.at 1 IST Austria (Institute of Science and Technology Austria), Am Campus 1, 3400 Klosterneuburg, Austria 2 Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria 123 Real-Time Syst for finding worst-case scenarios) by computing power. For the competitive synthesis case, we are just given a taskset T , and the goal is to automatically synthesize an opti- mal on-line scheduling algorithm A , i.e., one that guarantees the largest competitive ratio possible for T . We show how the competitive synthesis problem can be reduced to a two-player graph game with partial information, and establish that the compu- tational complexity of solving this game is Np -complete. The competitive synthesis problem is hence in Np in the size of the state space of the non-deterministic labeled transition system encoding the taskset. Overall, the proposed framework assists in the selection of suitable scheduling algorithms for a given taskset, which is in fact the most common situation in real-time systems design. ","lang":"eng"}],"publication_status":"published","doi":"10.1007/s11241-017-9293-4","file_date_updated":"2020-07-14T12:47:56Z","_id":"738","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"2820"}]},"year":"2018","date_created":"2018-12-11T11:48:14Z","publist_id":"6929","citation":{"short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54 (2018) 166–207.","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “Automated competitive analysis of real time scheduling with graph games,” Real-Time Systems, vol. 54, no. 1. Springer, pp. 166–207, 2018.","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. 2018;54(1):166-207. doi:10.1007/s11241-017-9293-4","mla":"Chatterjee, Krishnendu, et al. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” Real-Time Systems, vol. 54, no. 1, Springer, 2018, pp. 166–207, doi:10.1007/s11241-017-9293-4.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” Real-Time Systems. Springer, 2018. https://doi.org/10.1007/s11241-017-9293-4.","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2018. Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. 54(1), 166–207.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2018). Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. Springer. https://doi.org/10.1007/s11241-017-9293-4"}},{"title":"Parameter-independent strategies for pMDPs via POMDPs","oa":1,"date_updated":"2023-09-13T09:38:28Z","article_processing_charge":"No","scopus_import":"1","intvolume":" 11024","isi":1,"language":[{"iso":"eng"}],"author":[{"first_name":"Sebastian","full_name":"Arming, Sebastian","last_name":"Arming"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Katoen","id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P","first_name":"Joost P"},{"full_name":"Sokolova, Ana","first_name":"Ana","last_name":"Sokolova"}],"arxiv":1,"main_file_link":[{"url":"https://arxiv.org/abs/1806.05126","open_access":"1"}],"oa_version":"Preprint","day":"15","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","conference":{"end_date":"2018-09-07","location":"Beijing, China","start_date":"2018-09-04","name":"QEST: Quantitative Evaluation of Systems"},"month":"08","alternative_title":["LNCS"],"status":"public","type":"conference","citation":{"apa":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J. P., & Sokolova, A. (2018). Parameter-independent strategies for pMDPs via POMDPs (Vol. 11024, pp. 53–70). Presented at the QEST: Quantitative Evaluation of Systems, Beijing, China: Springer. https://doi.org/10.1007/978-3-319-99154-2_4","short":"S. Arming, E. Bartocci, K. Chatterjee, J.P. Katoen, A. Sokolova, in:, Springer, 2018, pp. 53–70.","ieee":"S. Arming, E. Bartocci, K. Chatterjee, J. P. Katoen, and A. Sokolova, “Parameter-independent strategies for pMDPs via POMDPs,” presented at the QEST: Quantitative Evaluation of Systems, Beijing, China, 2018, vol. 11024, pp. 53–70.","ama":"Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A. Parameter-independent strategies for pMDPs via POMDPs. In: Vol 11024. Springer; 2018:53-70. doi:10.1007/978-3-319-99154-2_4","chicago":"Arming, Sebastian, Ezio Bartocci, Krishnendu Chatterjee, Joost P Katoen, and Ana Sokolova. “Parameter-Independent Strategies for PMDPs via POMDPs,” 11024:53–70. Springer, 2018. https://doi.org/10.1007/978-3-319-99154-2_4.","ista":"Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A. 2018. Parameter-independent strategies for pMDPs via POMDPs. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11024, 53–70.","mla":"Arming, Sebastian, et al. Parameter-Independent Strategies for PMDPs via POMDPs. Vol. 11024, Springer, 2018, pp. 53–70, doi:10.1007/978-3-319-99154-2_4."},"publist_id":"7975","date_created":"2018-12-11T11:44:31Z","year":"2018","_id":"79","doi":"10.1007/978-3-319-99154-2_4","publication_status":"published","external_id":{"isi":["000548912200004"],"arxiv":["1806.05126"]},"abstract":[{"text":"Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances. We study pMDPs with reachability objectives where the parameter values are unknown and impossible to measure directly during execution, but there is a probability distribution known over the parameter values. We study for the first time computing parameter-independent strategies that are expectation optimal, i.e., optimize the expected reachability probability under the probability distribution over the parameters. We present an encoding of our problem to partially observable MDPs (POMDPs), i.e., a reduction of our problem to computing optimal strategies in POMDPs. We evaluate our method experimentally on several benchmarks: a motivating (repeated) learner model; a series of benchmarks of varying configurations of a robot moving on a grid; and a consensus protocol.","lang":"eng"}],"page":"53-70","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","volume":11024,"publisher":"Springer","date_published":"2018-08-15T00:00:00Z"},{"month":"07","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"file_name":"2018_Nature_Hilbe.pdf","checksum":"011ab905cf9a410bc2b96f15174d654d","file_id":"7049","date_updated":"2020-07-14T12:45:02Z","date_created":"2019-11-19T08:09:57Z","creator":"dernst","relation":"main_file","access_level":"open_access","file_size":2834442,"content_type":"application/pdf"}],"day":"04","oa_version":"Submitted Version","author":[{"full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X"},{"first_name":"Štepán","full_name":"Šimsa, Štepán","last_name":"Šimsa"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"status":"public","type":"journal_article","isi":1,"intvolume":" 559","scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","issue":"7713","oa":1,"date_updated":"2023-09-11T13:43:22Z","title":"Evolution of cooperation in stochastic games","publication":"Nature","language":[{"iso":"eng"}],"ddc":["000"],"abstract":[{"text":"Social dilemmas occur when incentives for individuals are misaligned with group interests 1-7 . According to the 'tragedy of the commons', these misalignments can lead to overexploitation and collapse of public resources. The resulting behaviours can be analysed with the tools of game theory 8 . The theory of direct reciprocity 9-15 suggests that repeated interactions can alleviate such dilemmas, but previous work has assumed that the public resource remains constant over time. Here we introduce the idea that the public resource is instead changeable and depends on the strategic choices of individuals. An intuitive scenario is that cooperation increases the public resource, whereas defection decreases it. Thus, cooperation allows the possibility of playing a more valuable game with higher payoffs, whereas defection leads to a less valuable game. We analyse this idea using the theory of stochastic games 16-19 and evolutionary game theory. We find that the dependence of the public resource on previous interactions can greatly enhance the propensity for cooperation. For these results, the interaction between reciprocity and payoff feedback is crucial: neither repeated interactions in a constant environment nor single interactions in a changing environment yield similar cooperation rates. Our framework shows which feedbacks between exploitation and environment - either naturally occurring or designed - help to overcome social dilemmas.","lang":"eng"}],"external_id":{"isi":["000438240900054"]},"publication_status":"published","date_published":"2018-07-04T00:00:00Z","publisher":"Nature Publishing Group","volume":559,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"246 - 249","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"related_material":{"link":[{"url":"https://ist.ac.at/en/news/engineering-cooperation/","description":"News on IST Homepage","relation":"press_release"}]},"ec_funded":1,"year":"2018","acknowledgement":"European Research Council Start Grant 279307, Austrian Science Fund (FWF) grant P23499-N23, \r\nC.H. acknowledges support from the ISTFELLOW programme.","publist_id":"7764","citation":{"short":"C. Hilbe, Š. Šimsa, K. Chatterjee, M. Nowak, Nature 559 (2018) 246–249.","ieee":"C. Hilbe, Š. Šimsa, K. Chatterjee, and M. Nowak, “Evolution of cooperation in stochastic games,” Nature, vol. 559, no. 7713. Nature Publishing Group, pp. 246–249, 2018.","ama":"Hilbe C, Šimsa Š, Chatterjee K, Nowak M. Evolution of cooperation in stochastic games. Nature. 2018;559(7713):246-249. doi:10.1038/s41586-018-0277-x","mla":"Hilbe, Christian, et al. “Evolution of Cooperation in Stochastic Games.” Nature, vol. 559, no. 7713, Nature Publishing Group, 2018, pp. 246–49, doi:10.1038/s41586-018-0277-x.","ista":"Hilbe C, Šimsa Š, Chatterjee K, Nowak M. 2018. Evolution of cooperation in stochastic games. Nature. 559(7713), 246–249.","chicago":"Hilbe, Christian, Štepán Šimsa, Krishnendu Chatterjee, and Martin Nowak. “Evolution of Cooperation in Stochastic Games.” Nature. Nature Publishing Group, 2018. https://doi.org/10.1038/s41586-018-0277-x.","apa":"Hilbe, C., Šimsa, Š., Chatterjee, K., & Nowak, M. (2018). Evolution of cooperation in stochastic games. Nature. Nature Publishing Group. https://doi.org/10.1038/s41586-018-0277-x"},"date_created":"2018-12-11T11:44:56Z","doi":"10.1038/s41586-018-0277-x","_id":"157","file_date_updated":"2020-07-14T12:45:02Z"},{"citation":{"apa":"Ibsen-Jensen, R., Tkadlec, J., Chatterjee, K., & Nowak, M. (2018). Language acquisition with communication between learners. Journal of the Royal Society Interface. The Royal Society. https://doi.org/10.1098/rsif.2018.0073","ama":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. Language acquisition with communication between learners. Journal of the Royal Society Interface. 2018;15(140). doi:10.1098/rsif.2018.0073","ieee":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, and M. Nowak, “Language acquisition with communication between learners,” Journal of the Royal Society Interface, vol. 15, no. 140. The Royal Society, 2018.","short":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, M. Nowak, Journal of the Royal Society Interface 15 (2018).","chicago":"Ibsen-Jensen, Rasmus, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Language Acquisition with Communication between Learners.” Journal of the Royal Society Interface. The Royal Society, 2018. https://doi.org/10.1098/rsif.2018.0073.","mla":"Ibsen-Jensen, Rasmus, et al. “Language Acquisition with Communication between Learners.” Journal of the Royal Society Interface, vol. 15, no. 140, 20180073, The Royal Society, 2018, doi:10.1098/rsif.2018.0073.","ista":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. 2018. Language acquisition with communication between learners. Journal of the Royal Society Interface. 15(140), 20180073."},"publist_id":"7715","date_created":"2018-12-11T11:45:09Z","year":"2018","ec_funded":1,"related_material":{"record":[{"relation":"research_data","id":"9814","status":"public"}],"link":[{"relation":"supplementary_material","url":"https://dx.doi.org/10.6084/m9.figshare.c.4028971"}]},"article_number":"20180073","file_date_updated":"2020-07-14T12:45:22Z","article_type":"original","_id":"198","doi":"10.1098/rsif.2018.0073","publication_status":"published","external_id":{"isi":["000428576200023"],"pmid":["29593089"]},"abstract":[{"lang":"eng","text":"We consider a class of students learning a language from a teacher. The situation can be interpreted as a group of child learners receiving input from the linguistic environment. The teacher provides sample sentences. The students try to learn the grammar from the teacher. In addition to just listening to the teacher, the students can also communicate with each other. The students hold hypotheses about the grammar and change them if they receive counter evidence. The process stops when all students have converged to the correct grammar. We study how the time to convergence depends on the structure of the classroom by introducing and evaluating various complexity measures. We find that structured communication between students, although potentially introducing confusion, can greatly reduce some of the complexity measures. Our theory can also be interpreted as applying to the scientific process, where nature is the teacher and the scientists are the students."}],"ddc":["000"],"project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"KrCh"}],"volume":15,"quality_controlled":"1","publisher":"The Royal Society","date_published":"2018-03-01T00:00:00Z","title":"Language acquisition with communication between learners","date_updated":"2023-10-18T06:36:00Z","oa":1,"issue":"140","article_processing_charge":"No","scopus_import":"1","intvolume":" 15","has_accepted_license":"1","isi":1,"language":[{"iso":"eng"}],"publication":"Journal of the Royal Society Interface","author":[{"last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Tkadlec, Josef","first_name":"Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"oa_version":"Submitted Version","day":"01","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":219837,"creator":"dernst","date_created":"2019-02-12T07:54:37Z","date_updated":"2020-07-14T12:45:22Z","file_name":"2018_RS_IbsenJensen.pdf","file_id":"5955","checksum":"444e1a9d98eb0e780671be82b13025f3"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"03","publication_identifier":{"eissn":["1742-5662"]},"pmid":1,"status":"public","type":"journal_article"},{"external_id":{"pmid":["30429320"],"isi":["000451351000063"]},"abstract":[{"text":"Indirect reciprocity explores how humans act when their reputation is at stake, and which social norms they use to assess the actions of others. A crucial question in indirect reciprocity is which social norms can maintain stable cooperation in a society. Past research has highlighted eight such norms, called “leading-eight” strategies. This past research, however, is based on the assumption that all relevant information about other population members is publicly available and that everyone agrees on who is good or bad. Instead, here we explore the reputation dynamics when information is private and noisy. We show that under these conditions, most leading-eight strategies fail to evolve. Those leading-eight strategies that do evolve are unable to sustain full cooperation.Indirect reciprocity is a mechanism for cooperation based on shared moral systems and individual reputations. It assumes that members of a community routinely observe and assess each other and that they use this information to decide who is good or bad, and who deserves cooperation. When information is transmitted publicly, such that all community members agree on each other’s reputation, previous research has highlighted eight crucial moral systems. These “leading-eight” strategies can maintain cooperation and resist invasion by defectors. However, in real populations individuals often hold their own private views of others. Once two individuals disagree about their opinion of some third party, they may also see its subsequent actions in a different light. Their opinions may further diverge over time. Herein, we explore indirect reciprocity when information transmission is private and noisy. We find that in the presence of perception errors, most leading-eight strategies cease to be stable. Even if a leading-eight strategy evolves, cooperation rates may drop considerably when errors are common. Our research highlights the role of reliable information and synchronized reputations to maintain stable moral systems.","lang":"eng"}],"publication_status":"published","page":"12241-12246","department":[{"_id":"KrCh"}],"volume":115,"quality_controlled":"1","publisher":"National Academy of Sciences","date_published":"2018-11-27T00:00:00Z","project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"}],"ec_funded":1,"related_material":{"link":[{"relation":"press_release","url":"https://ist.ac.at/en/news/no-cooperation-without-open-communication/","description":"News on IST Homepage"}],"record":[{"relation":"dissertation_contains","id":"10293","status":"public"}]},"citation":{"short":"C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, M. Nowak, PNAS 115 (2018) 12241–12246.","ama":"Hilbe C, Schmid L, Tkadlec J, Chatterjee K, Nowak M. Indirect reciprocity with private, noisy, and incomplete information. PNAS. 2018;115(48):12241-12246. doi:10.1073/pnas.1810565115","ieee":"C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, and M. Nowak, “Indirect reciprocity with private, noisy, and incomplete information,” PNAS, vol. 115, no. 48. National Academy of Sciences, pp. 12241–12246, 2018.","chicago":"Hilbe, Christian, Laura Schmid, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Indirect Reciprocity with Private, Noisy, and Incomplete Information.” PNAS. National Academy of Sciences, 2018. https://doi.org/10.1073/pnas.1810565115.","mla":"Hilbe, Christian, et al. “Indirect Reciprocity with Private, Noisy, and Incomplete Information.” PNAS, vol. 115, no. 48, National Academy of Sciences, 2018, pp. 12241–46, doi:10.1073/pnas.1810565115.","ista":"Hilbe C, Schmid L, Tkadlec J, Chatterjee K, Nowak M. 2018. Indirect reciprocity with private, noisy, and incomplete information. PNAS. 115(48), 12241–12246.","apa":"Hilbe, C., Schmid, L., Tkadlec, J., Chatterjee, K., & Nowak, M. (2018). Indirect reciprocity with private, noisy, and incomplete information. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.1810565115"},"date_created":"2018-12-11T11:44:05Z","year":"2018","doi":"10.1073/pnas.1810565115","_id":"2","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pubmed/30429320"}],"day":"27","oa_version":"Submitted Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"11","author":[{"orcid":"0000-0001-5116-955X","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","full_name":"Hilbe, Christian"},{"first_name":"Laura","full_name":"Schmid, Laura","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid","orcid":"0000-0002-6978-7329"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"pmid":1,"type":"journal_article","status":"public","scopus_import":"1","intvolume":" 115","isi":1,"title":"Indirect reciprocity with private, noisy, and incomplete information","oa":1,"date_updated":"2025-07-14T09:10:09Z","issue":"48","article_processing_charge":"No","publication":"PNAS","language":[{"iso":"eng"}]},{"doi":"10.1007/978-3-319-96142-2_13","file_date_updated":"2020-07-14T12:44:53Z","_id":"141","ec_funded":1,"related_material":{"record":[{"status":"public","id":"10199","relation":"dissertation_contains"}]},"acknowledgement":"Acknowledgements. K. C. and M. H. are partially supported by the Vienna Science and Technology Fund (WWTF) grant ICT15-003. K. C. is partially supported by the Austrian Science Fund (FWF): S11407-N23 (RiSE/SHiNE), and an ERC Start Grant (279307: Graph Games). V. T. is partially supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie Grant Agreement No. 665385.","year":"2018","citation":{"apa":"Chatterjee, K., Henzinger, M. H., Loitzenbauer, V., Oraee, S., & Toman, V. (2018). Symbolic algorithms for graphs and Markov decision processes with fairness objectives (Vol. 10982, pp. 178–197). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96142-2_13","ieee":"K. Chatterjee, M. H. Henzinger, V. Loitzenbauer, S. Oraee, and V. Toman, “Symbolic algorithms for graphs and Markov decision processes with fairness objectives,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10982, pp. 178–197.","ama":"Chatterjee K, Henzinger MH, Loitzenbauer V, Oraee S, Toman V. Symbolic algorithms for graphs and Markov decision processes with fairness objectives. In: Vol 10982. Springer; 2018:178-197. doi:10.1007/978-3-319-96142-2_13","short":"K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, S. Oraee, V. Toman, in:, Springer, 2018, pp. 178–197.","mla":"Chatterjee, Krishnendu, et al. Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives. Vol. 10982, Springer, 2018, pp. 178–97, doi:10.1007/978-3-319-96142-2_13.","ista":"Chatterjee K, Henzinger MH, Loitzenbauer V, Oraee S, Toman V. 2018. Symbolic algorithms for graphs and Markov decision processes with fairness objectives. CAV: Computer Aided Verification, LNCS, vol. 10982, 178–197.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Veronika Loitzenbauer, Simin Oraee, and Viktor Toman. “Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives,” 10982:178–97. Springer, 2018. https://doi.org/10.1007/978-3-319-96142-2_13."},"publist_id":"7782","date_created":"2018-12-11T11:44:51Z","publisher":"Springer","date_published":"2018-07-18T00:00:00Z","department":[{"_id":"KrCh"}],"page":"178-197","volume":10982,"quality_controlled":"1","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","call_identifier":"H2020","name":"International IST Doctoral Program"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"isi":["000491469700013"]},"abstract":[{"lang":"eng","text":"Given a model and a specification, the fundamental model-checking problem asks for algorithmic verification of whether the model satisfies the specification. We consider graphs and Markov decision processes (MDPs), which are fundamental models for reactive systems. One of the very basic specifications that arise in verification of reactive systems is the strong fairness (aka Streett) objective. Given different types of requests and corresponding grants, the objective requires that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All ω -regular objectives can be expressed as Streett objectives and hence they are canonical in verification. To handle the state-space explosion, symbolic algorithms are required that operate on a succinct implicit representation of the system rather than explicitly accessing the system. While explicit algorithms for graphs and MDPs with Streett objectives have been widely studied, there has been no improvement of the basic symbolic algorithms. The worst-case numbers of symbolic steps required for the basic symbolic algorithms are as follows: quadratic for graphs and cubic for MDPs. In this work we present the first sub-quadratic symbolic algorithm for graphs with Streett objectives, and our algorithm is sub-quadratic even for MDPs. Based on our algorithmic insights we present an implementation of the new symbolic approach and show that it improves the existing approach on several academic benchmark examples."}],"publication_status":"published","language":[{"iso":"eng"}],"isi":1,"intvolume":" 10982","has_accepted_license":"1","scopus_import":"1","oa":1,"date_updated":"2025-07-14T09:10:15Z","article_processing_charge":"No","title":"Symbolic algorithms for graphs and Markov decision processes with fairness objectives","alternative_title":["LNCS"],"status":"public","type":"conference","conference":{"end_date":"2018-07-17","location":"Oxford, United Kingdom","start_date":"2018-07-14","name":"CAV: Computer Aided Verification"},"month":"07","oa_version":"Published Version","day":"18","file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_size":675606,"creator":"dernst","date_updated":"2020-07-14T12:44:53Z","date_created":"2018-12-18T08:52:38Z","file_name":"2018_LNCS_Chatterjee.pdf","checksum":"1a6ffa4febe8bb8ac28be3adb3eafebc","file_id":"5737"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Monika H","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","orcid":"0000-0002-5008-6530"},{"last_name":"Loitzenbauer","full_name":"Loitzenbauer, Veronika","first_name":"Veronika"},{"last_name":"Oraee","full_name":"Oraee, Simin","first_name":"Simin"},{"last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","first_name":"Viktor"}]},{"oa":1,"date_updated":"2025-06-02T08:53:48Z","article_processing_charge":"No","title":"Efficient algorithms for asymptotic bounds on termination time in VASS","isi":1,"scopus_import":"1","language":[{"iso":"eng"}],"author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"first_name":"Petr","full_name":"Novotny, Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dominik","full_name":"Velan, Dominik","last_name":"Velan"},{"full_name":"Zuleger, Florian","first_name":"Florian","last_name":"Zuleger"}],"conference":{"name":"LICS: Logic in Computer Science","start_date":"2018-07-09","location":"Oxford, United Kingdom","end_date":"2018-07-12"},"month":"07","publication_identifier":{"isbn":["978-1-4503-5583-4"]},"main_file_link":[{"url":"https://arxiv.org/abs/1804.10985","open_access":"1"}],"day":"09","oa_version":"Preprint","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","alternative_title":["ACM/IEEE Symposium on Logic in Computer Science"],"type":"conference","status":"public","year":"2018","citation":{"apa":"Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., & Zuleger, F. (2018). Efficient algorithms for asymptotic bounds on termination time in VASS (Vol. F138033, pp. 185–194). Presented at the LICS: Logic in Computer Science, Oxford, United Kingdom: IEEE. https://doi.org/10.1145/3209108.3209191","ista":"Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. 2018. Efficient algorithms for asymptotic bounds on termination time in VASS. LICS: Logic in Computer Science, ACM/IEEE Symposium on Logic in Computer Science, vol. F138033, 185–194.","mla":"Brázdil, Tomáš, et al. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. Vol. F138033, IEEE, 2018, pp. 185–94, doi:10.1145/3209108.3209191.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Antonín Kučera, Petr Novotný, Dominik Velan, and Florian Zuleger. “Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS,” F138033:185–94. IEEE, 2018. https://doi.org/10.1145/3209108.3209191.","short":"T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, F. Zuleger, in:, IEEE, 2018, pp. 185–194.","ieee":"T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger, “Efficient algorithms for asymptotic bounds on termination time in VASS,” presented at the LICS: Logic in Computer Science, Oxford, United Kingdom, 2018, vol. F138033, pp. 185–194.","ama":"Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. Efficient algorithms for asymptotic bounds on termination time in VASS. In: Vol F138033. IEEE; 2018:185-194. doi:10.1145/3209108.3209191"},"publist_id":"7780","date_created":"2018-12-11T11:44:51Z","ec_funded":1,"_id":"143","doi":"10.1145/3209108.3209191","publication_status":"published","external_id":{"isi":["000545262800020"]},"abstract":[{"lang":"eng","text":"Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. Our main contributions are as follows: First, we present a polynomial-time algorithm for deciding whether a given VASS has a linear asymptotic complexity. We also show that if the complexity of a VASS is not linear, it is at least quadratic. Second, we classify VASS according to quantitative properties of their cycles. We show that certain singularities in these properties are the key reason for non-polynomial asymptotic complexity of VASS. In absence of singularities, we show that the asymptotic complexity is always polynomial and of the form Θ(nk), for some integer k d, where d is the dimension of the VASS. We present a polynomial-time algorithm computing the optimal k. For general VASS, the same algorithm, which is based on a complete technique for the construction of ranking functions in VASS, produces a valid lower bound, i.e., a k such that the termination complexity is (nk). Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis."}],"project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"publisher":"IEEE","date_published":"2018-07-09T00:00:00Z","department":[{"_id":"KrCh"}],"page":"185 - 194","volume":"F138033","quality_controlled":"1"},{"language":[{"iso":"eng"}],"scopus_import":"1","intvolume":" 11275","editor":[{"last_name":"Ryu","full_name":"Ryu, Sukyoung","first_name":"Sukyoung"}],"isi":1,"title":"New approaches for almost-sure termination of probabilistic programs","article_processing_charge":"No","oa":1,"date_updated":"2025-06-02T08:53:41Z","status":"public","type":"conference","alternative_title":["LNCS"],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","main_file_link":[{"url":"http://arxiv.org/abs/1806.06683","open_access":"1"}],"oa_version":"Preprint","day":"01","month":"12","publication_identifier":{"issn":["03029743"],"isbn":["9783030027674"]},"conference":{"name":"16th Asian Symposium on Programming Languages and Systems, APLAS","start_date":"2018-12-02","location":"Wellington, New Zealand","end_date":"2018-12-06"},"arxiv":1,"author":[{"full_name":"Huang, Mingzhang","first_name":"Mingzhang","last_name":"Huang"},{"last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"doi":"10.1007/978-3-030-02768-1_11","_id":"5679","date_created":"2018-12-16T22:59:20Z","citation":{"short":"M. Huang, H. Fu, K. Chatterjee, in:, S. Ryu (Ed.), Springer, 2018, pp. 181–201.","ama":"Huang M, Fu H, Chatterjee K. New approaches for almost-sure termination of probabilistic programs. In: Ryu S, ed. Vol 11275. Springer; 2018:181-201. doi:10.1007/978-3-030-02768-1_11","ieee":"M. Huang, H. Fu, and K. Chatterjee, “New approaches for almost-sure termination of probabilistic programs,” presented at the 16th Asian Symposium on Programming Languages and Systems, APLAS, Wellington, New Zealand, 2018, vol. 11275, pp. 181–201.","chicago":"Huang, Mingzhang, Hongfei Fu, and Krishnendu Chatterjee. “New Approaches for Almost-Sure Termination of Probabilistic Programs.” edited by Sukyoung Ryu, 11275:181–201. Springer, 2018. https://doi.org/10.1007/978-3-030-02768-1_11.","mla":"Huang, Mingzhang, et al. New Approaches for Almost-Sure Termination of Probabilistic Programs. Edited by Sukyoung Ryu, vol. 11275, Springer, 2018, pp. 181–201, doi:10.1007/978-3-030-02768-1_11.","ista":"Huang M, Fu H, Chatterjee K. 2018. New approaches for almost-sure termination of probabilistic programs. 16th Asian Symposium on Programming Languages and Systems, APLAS, LNCS, vol. 11275, 181–201.","apa":"Huang, M., Fu, H., & Chatterjee, K. (2018). New approaches for almost-sure termination of probabilistic programs. In S. Ryu (Ed.) (Vol. 11275, pp. 181–201). Presented at the 16th Asian Symposium on Programming Languages and Systems, APLAS, Wellington, New Zealand: Springer. https://doi.org/10.1007/978-3-030-02768-1_11"},"year":"2018","volume":11275,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"181-201","date_published":"2018-12-01T00:00:00Z","publisher":"Springer","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"abstract":[{"text":"We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for the almost-sure termination problem. Moreover, using this approach we can obtain explicit optimal bounds on tail probabilities of non-termination within a given number of steps. Second, we present a new approach based on Central Limit Theorem for the almost-sure termination problem, and show that this approach can establish almost-sure termination of programs which none of the existing approaches can handle. Finally, we discuss algorithmic approaches for the two above methods that lead to automated analysis techniques for almost-sure termination of probabilistic programs.","lang":"eng"}],"external_id":{"isi":["000916310900011"],"arxiv":["1806.06683"]}},{"has_accepted_license":"1","scopus_import":"1","intvolume":" 1","isi":1,"title":"Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory","pubrep_id":"1045","date_updated":"2024-02-21T13:48:42Z","oa":1,"issue":"1","article_processing_charge":"No","publication":"Communications Biology","language":[{"iso":"eng"}],"oa_version":"Published Version","day":"14","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":1804194,"creator":"dernst","date_created":"2018-12-18T13:37:04Z","date_updated":"2020-07-14T12:47:10Z","file_name":"2018_CommBiology_Pavlogiannis.pdf","checksum":"a9db825fa3b64a51ff3de035ec973b3e","file_id":"5752"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"06","publication_identifier":{"issn":["2399-3642"]},"author":[{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Nowak, Martin A.","first_name":"Martin A.","last_name":"Nowak"}],"status":"public","type":"journal_article","ec_funded":1,"article_number":"71","related_material":{"record":[{"relation":"part_of_dissertation","id":"7196","status":"public"},{"status":"public","relation":"popular_science","id":"5559"}]},"citation":{"apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. A. (2018). Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. Springer Nature. https://doi.org/10.1038/s42003-018-0078-7","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. A. Nowak, “Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory,” Communications Biology, vol. 1, no. 1. Springer Nature, 2018.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. 2018;1(1). doi:10.1038/s42003-018-0078-7","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M.A. Nowak, Communications Biology 1 (2018).","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin A. Nowak. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” Communications Biology. Springer Nature, 2018. https://doi.org/10.1038/s42003-018-0078-7.","mla":"Pavlogiannis, Andreas, et al. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” Communications Biology, vol. 1, no. 1, 71, Springer Nature, 2018, doi:10.1038/s42003-018-0078-7.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. 2018. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. 1(1), 71."},"date_created":"2018-12-18T13:22:58Z","year":"2018","doi":"10.1038/s42003-018-0078-7","file_date_updated":"2020-07-14T12:47:10Z","_id":"5751","external_id":{"isi":["000461126500071"]},"abstract":[{"text":"Because of the intrinsic randomness of the evolutionary process, a mutant with a fitness advantage has some chance to be selected but no certainty. Any experiment that searches for advantageous mutants will lose many of them due to random drift. It is therefore of great interest to find population structures that improve the odds of advantageous mutants. Such structures are called amplifiers of natural selection: they increase the probability that advantageous mutants are selected. Arbitrarily strong amplifiers guarantee the selection of advantageous mutants, even for very small fitness advantage. Despite intensive research over the past decade, arbitrarily strong amplifiers have remained rare. Here we show how to construct a large variety of them. Our amplifiers are so simple that they could be useful in biotechnology, when optimizing biological molecules, or as a diagnostic tool, when searching for faster dividing cells or viruses. They could also occur in natural population structures.","lang":"eng"}],"ddc":["004","519","576"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publication_status":"published","department":[{"_id":"KrCh"}],"volume":1,"quality_controlled":"1","publisher":"Springer Nature","date_published":"2018-06-14T00:00:00Z","project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}]},{"publication_status":"published","author":[{"last_name":"Bloem","full_name":"Bloem, Roderick","first_name":"Roderick"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Jobstmann","full_name":"Jobstmann, Barbara","first_name":"Barbara"}],"month":"05","publication_identifier":{"isbn":["978-3-319-10574-1"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"Graph-based games are an important tool in computer science. They have applications in synthesis, verification, refinement, and far beyond. We review graphbased games with objectives on infinite plays. We give definitions and algorithms to solve the games and to give a winning strategy. The objectives we consider are mostly Boolean, but we also look at quantitative graph-based games and their objectives. Synthesis aims to turn temporal logic specifications into correct reactive systems. We explain the reduction of synthesis to graph-based games (or equivalently tree automata) using synthesis of LTL specifications as an example. We treat the classical approach that uses determinization of parity automata and more modern approaches.","lang":"eng"}],"oa_version":"None","day":"19","status":"public","type":"book_chapter","date_published":"2018-05-19T00:00:00Z","publisher":"Springer","quality_controlled":"1","page":"921 - 962","edition":"1","department":[{"_id":"KrCh"}],"year":"2018","date_updated":"2021-01-12T08:05:10Z","citation":{"mla":"Bloem, Roderick, et al. “Graph Games and Reactive Synthesis.” Handbook of Model Checking, edited by Thomas A Henzinger et al., 1st ed., Springer, 2018, pp. 921–62, doi:10.1007/978-3-319-10575-8_27.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, and Barbara Jobstmann. “Graph Games and Reactive Synthesis.” In Handbook of Model Checking, edited by Thomas A Henzinger, Edmund M. Clarke, Helmut Veith, and Roderick Bloem, 1st ed., 921–62. Springer, 2018. https://doi.org/10.1007/978-3-319-10575-8_27.","ista":"Bloem R, Chatterjee K, Jobstmann B. 2018.Graph games and reactive synthesis. In: Handbook of Model Checking. , 921–962.","short":"R. Bloem, K. Chatterjee, B. Jobstmann, in:, T.A. Henzinger, E.M. Clarke, H. Veith, R. Bloem (Eds.), Handbook of Model Checking, 1st ed., Springer, 2018, pp. 921–962.","ieee":"R. Bloem, K. Chatterjee, and B. Jobstmann, “Graph games and reactive synthesis,” in Handbook of Model Checking, 1st ed., T. A. Henzinger, E. M. Clarke, H. Veith, and R. Bloem, Eds. Springer, 2018, pp. 921–962.","ama":"Bloem R, Chatterjee K, Jobstmann B. Graph games and reactive synthesis. In: Henzinger TA, Clarke EM, Veith H, Bloem R, eds. Handbook of Model Checking. 1st ed. Springer; 2018:921-962. doi:10.1007/978-3-319-10575-8_27","apa":"Bloem, R., Chatterjee, K., & Jobstmann, B. (2018). Graph games and reactive synthesis. In T. A. Henzinger, E. M. Clarke, H. Veith, & R. Bloem (Eds.), Handbook of Model Checking (1st ed., pp. 921–962). Springer. https://doi.org/10.1007/978-3-319-10575-8_27"},"title":"Graph games and reactive synthesis","publist_id":"7995","date_created":"2018-12-11T11:44:24Z","editor":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Clarke","first_name":"Edmund M.","full_name":"Clarke, Edmund M."},{"full_name":"Veith, Helmut","first_name":"Helmut","last_name":"Veith"},{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"}],"scopus_import":1,"_id":"59","language":[{"iso":"eng"}],"publication":"Handbook of Model Checking","doi":"10.1007/978-3-319-10575-8_27"},{"title":"The Big Match with a clock and a bit of memory","article_processing_charge":"No","oa":1,"date_updated":"2023-09-19T10:45:15Z","has_accepted_license":"1","scopus_import":"1","isi":1,"language":[{"iso":"eng"}],"publication":"Proceedings of the 2018 ACM Conference on Economics and Computation - EC '18","author":[{"full_name":"Hansen, Kristoffer Arnsfelt","first_name":"Kristoffer Arnsfelt","last_name":"Hansen"},{"last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus"},{"first_name":"Abraham","full_name":"Neyman, Abraham","last_name":"Neyman"}],"file":[{"content_type":"application/pdf","relation":"main_file","file_size":302539,"access_level":"open_access","creator":"dernst","date_created":"2019-11-19T08:24:24Z","date_updated":"2020-07-14T12:47:14Z","checksum":"bb52683e349cfd864f4769a8f38f2798","file_name":"2018_EC18_Hansen.pdf","file_id":"7054"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"18","oa_version":"Submitted Version","publication_identifier":{"isbn":["9781450358293"]},"month":"06","conference":{"start_date":"2018-06-18","name":"EC: Conference on Economics and Computation","end_date":"2018-06-22","location":"Ithaca, NY, United States"},"status":"public","type":"conference","citation":{"mla":"Hansen, Kristoffer Arnsfelt, et al. “The Big Match with a Clock and a Bit of Memory.” Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18, ACM Press, 2018, pp. 149–50, doi:10.1145/3219166.3219198.","chicago":"Hansen, Kristoffer Arnsfelt, Rasmus Ibsen-Jensen, and Abraham Neyman. “The Big Match with a Clock and a Bit of Memory.” In Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18, 149–50. ACM Press, 2018. https://doi.org/10.1145/3219166.3219198.","ista":"Hansen KA, Ibsen-Jensen R, Neyman A. 2018. The Big Match with a clock and a bit of memory. Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18. EC: Conference on Economics and Computation, 149–150.","ieee":"K. A. Hansen, R. Ibsen-Jensen, and A. Neyman, “The Big Match with a clock and a bit of memory,” in Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18, Ithaca, NY, United States, 2018, pp. 149–150.","ama":"Hansen KA, Ibsen-Jensen R, Neyman A. The Big Match with a clock and a bit of memory. In: Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18. ACM Press; 2018:149-150. doi:10.1145/3219166.3219198","short":"K.A. Hansen, R. Ibsen-Jensen, A. Neyman, in:, Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18, ACM Press, 2018, pp. 149–150.","apa":"Hansen, K. A., Ibsen-Jensen, R., & Neyman, A. (2018). The Big Match with a clock and a bit of memory. In Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18 (pp. 149–150). Ithaca, NY, United States: ACM Press. https://doi.org/10.1145/3219166.3219198"},"date_created":"2019-02-13T10:31:41Z","year":"2018","_id":"5967","file_date_updated":"2020-07-14T12:47:14Z","doi":"10.1145/3219166.3219198","publication_status":"published","abstract":[{"text":"The Big Match is a multi-stage two-player game. In each stage Player 1 hides one or two pebbles in his hand, and his opponent has to guess that number; Player 1 loses a point if Player 2 is correct, and otherwise he wins a point. As soon as Player 1 hides one pebble, the players cannot change their choices in any future stage.\r\nBlackwell and Ferguson (1968) give an ε-optimal strategy for Player 1 that hides, in each stage, one pebble with a probability that depends on the entire past history. Any strategy that depends just on the clock or on a finite memory is worthless. The long-standing natural open problem has been whether every strategy that depends just on the clock and a finite memory is worthless. We prove that there is such a strategy that is ε-optimal. In fact, we show that just two states of memory are sufficient.\r\n","lang":"eng"}],"external_id":{"isi":["000492755100020"]},"ddc":["000"],"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"149-150","date_published":"2018-06-18T00:00:00Z","publisher":"ACM Press"},{"year":"2018","date_created":"2019-02-13T13:26:27Z","citation":{"short":"K. Chatterjee, H. Fu, A.K. Goharshady, N. Okati, in:, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4700–4707.","ama":"Chatterjee K, Fu H, Goharshady AK, Okati N. Computational approaches for stochastic shortest path on succinct MDPs. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. Vol 2018. IJCAI; 2018:4700-4707. doi:10.24963/ijcai.2018/653","ieee":"K. Chatterjee, H. Fu, A. K. Goharshady, and N. Okati, “Computational approaches for stochastic shortest path on succinct MDPs,” in Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018, pp. 4700–4707.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran Okati. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018:4700–4707. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/653.","mla":"Chatterjee, Krishnendu, et al. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, vol. 2018, IJCAI, 2018, pp. 4700–07, doi:10.24963/ijcai.2018/653.","ista":"Chatterjee K, Fu H, Goharshady AK, Okati N. 2018. Computational approaches for stochastic shortest path on succinct MDPs. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4700–4707.","apa":"Chatterjee, K., Fu, H., Goharshady, A. K., & Okati, N. (2018). Computational approaches for stochastic shortest path on succinct MDPs. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (Vol. 2018, pp. 4700–4707). Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/653"},"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"ec_funded":1,"_id":"5977","doi":"10.24963/ijcai.2018/653","publication_status":"published","abstract":[{"text":"We consider the stochastic shortest path (SSP)problem for succinct Markov decision processes(MDPs), where the MDP consists of a set of vari-ables, and a set of nondeterministic rules that up-date the variables. First, we show that several ex-amples from the AI literature can be modeled assuccinct MDPs. Then we present computationalapproaches for upper and lower bounds for theSSP problem: (a) for computing upper bounds, ourmethod is polynomial-time in the implicit descrip-tion of the MDP; (b) for lower bounds, we present apolynomial-time (in the size of the implicit descrip-tion) reduction to quadratic programming. Our ap-proach is applicable even to infinite-state MDPs.Finally, we present experimental results to demon-strate the effectiveness of our approach on severalclassical examples from the AI literature.","lang":"eng"}],"external_id":{"isi":["000764175404118"],"arxiv":["1804.08984"]},"project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"date_published":"2018-07-17T00:00:00Z","publisher":"IJCAI","quality_controlled":"1","volume":2018,"page":"4700-4707","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_updated":"2025-06-02T08:53:44Z","oa":1,"title":"Computational approaches for stochastic shortest path on succinct MDPs","isi":1,"scopus_import":"1","intvolume":" 2018","language":[{"iso":"eng"}],"publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","arxiv":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu","full_name":"Fu, Hongfei","first_name":"Hongfei"},{"full_name":"Goharshady, Amir","first_name":"Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady"},{"last_name":"Okati","first_name":"Nastaran","full_name":"Okati, Nastaran"}],"month":"07","publication_identifier":{"isbn":["978-099924112-7"],"issn":["10450823"]},"conference":{"location":"Stockholm, Sweden","end_date":"2018-07-19","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2018-07-13"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"17","main_file_link":[{"url":"https://arxiv.org/abs/1804.08984","open_access":"1"}],"oa_version":"Preprint","type":"conference","status":"public"},{"type":"journal_article","status":"public","publication_identifier":{"issn":["0164-0925"]},"month":"06","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.08517"}],"oa_version":"Submitted Version","day":"01","arxiv":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","first_name":"Petr"},{"last_name":"Hasheminezhad","first_name":"Rouzbeh","full_name":"Hasheminezhad, Rouzbeh"}],"publication":"ACM Transactions on Programming Languages and Systems","language":[{"iso":"eng"}],"isi":1,"scopus_import":"1","intvolume":" 40","issue":"2","article_processing_charge":"No","date_updated":"2023-09-19T14:38:42Z","oa":1,"title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","date_published":"2018-06-01T00:00:00Z","publisher":"Association for Computing Machinery (ACM)","volume":40,"quality_controlled":"1","department":[{"_id":"KrCh"}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"abstract":[{"lang":"eng","text":"In this article, we consider the termination problem of probabilistic programs with real-valued variables. Thequestions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1(almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); andquantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) tocompute a boundBsuch that the probability not to terminate afterBsteps decreases exponentially (con-centration problem). To solve these questions, we utilize the notion of ranking supermartingales, which isa powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmicsynthesis of linear ranking-supermartingales over affine probabilistic programs (Apps) with both angelic anddemonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Appsover which a linear ranking-supermartingale exists.Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor Apps with angelic non-determinism. Moreover, theNP-hardness result holds already for Appswithout probability and demonic non-determinism. Secondly, we show that the concentration problem overLRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show thatthe expectation problem over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate theeffectiveness of our approach to answer the qualitative and quantitative questions over Apps with at mostdemonic non-determinism."}],"external_id":{"arxiv":["1510.08517"],"isi":["000434634500003"]},"publication_status":"published","doi":"10.1145/3174800","_id":"5993","article_number":"7","related_material":{"record":[{"status":"public","id":"1438","relation":"earlier_version"}]},"ec_funded":1,"year":"2018","date_created":"2019-02-14T12:29:10Z","citation":{"apa":"Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2018). Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM). https://doi.org/10.1145/3174800","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018).","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2. Association for Computing Machinery (ACM), 2018.","ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. 2018;40(2). doi:10.1145/3174800","mla":"Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2, 7, Association for Computing Machinery (ACM), 2018, doi:10.1145/3174800.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3174800.","ista":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. 40(2), 7."}},{"language":[{"iso":"eng"}],"publication":"ACM Transactions on Programming Languages and Systems","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","article_processing_charge":"No","issue":"3","oa":1,"date_updated":"2024-03-25T23:30:19Z","scopus_import":"1","intvolume":" 40","isi":1,"status":"public","type":"journal_article","arxiv":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"01","main_file_link":[{"url":"https://arxiv.org/abs/1510.07565","open_access":"1"}],"oa_version":"Preprint","month":"08","publication_identifier":{"issn":["0164-0925"]},"_id":"6009","doi":"10.1145/3210257","date_created":"2019-02-14T14:31:52Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” ACM Transactions on Programming Languages and Systems, vol. 40, no. 3, 9, Association for Computing Machinery (ACM), 2018, doi:10.1145/3210257.","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 40(3), 9.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3210257.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” ACM Transactions on Programming Languages and Systems, vol. 40, no. 3. Association for Computing Machinery (ACM), 2018.","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 2018;40(3). doi:10.1145/3210257","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A. (2018). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM). https://doi.org/10.1145/3210257"},"year":"2018","article_number":"9","related_material":{"record":[{"relation":"earlier_version","id":"1437","status":"public"},{"status":"public","relation":"earlier_version","id":"5441"},{"status":"public","relation":"earlier_version","id":"5442"},{"status":"public","id":"8934","relation":"dissertation_contains"}]},"ec_funded":1,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"volume":40,"quality_controlled":"1","department":[{"_id":"KrCh"}],"date_published":"2018-08-01T00:00:00Z","publisher":"Association for Computing Machinery (ACM)","publication_status":"published","abstract":[{"text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n","lang":"eng"}],"external_id":{"arxiv":["1510.07565"],"isi":["000444694800001"]}},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"ddc":["000"],"abstract":[{"text":"We present a secure approach for maintaining andreporting credit history records on the Blockchain. Our ap-proach removes third-parties such as credit reporting agen-cies from the lending process and replaces them with smartcontracts. This allows customers to interact directly with thelenders or banks while ensuring the integrity, unmalleabilityand privacy of their credit data. Additionally, each customerhas full control over complete or selective disclosure of hercredit records, eliminating the risk of privacy violations or databreaches. Moreover, our approach provides strong guaranteesfor the lenders as well. A lender can check both correctness andcompleteness of the credit data disclosed to her. This is the firstapproach that can perform all credit reporting tasks withouta central authority or changing the financial mechanisms*.","lang":"eng"}],"external_id":{"arxiv":["1805.09104"],"isi":["000481634500196"]},"publication_status":"published","date_published":"2018-09-01T00:00:00Z","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","publisher":"IEEE","quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"1343-1348","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"ec_funded":1,"year":"2018","citation":{"apa":"Goharshady, A. K., Behrouz, A., & Chatterjee, K. (2018). Secure Credit Reporting on the Blockchain. In Proceedings of the IEEE International Conference on Blockchain (pp. 1343–1348). Halifax, Canada: IEEE. https://doi.org/10.1109/Cybermatics_2018.2018.00231","ista":"Goharshady AK, Behrouz A, Chatterjee K. 2018. Secure Credit Reporting on the Blockchain. Proceedings of the IEEE International Conference on Blockchain. IEEE International Conference on Blockchain, 1343–1348.","chicago":"Goharshady, Amir Kafshdar, Ali Behrouz, and Krishnendu Chatterjee. “Secure Credit Reporting on the Blockchain.” In Proceedings of the IEEE International Conference on Blockchain, 1343–48. IEEE, 2018. https://doi.org/10.1109/Cybermatics_2018.2018.00231.","mla":"Goharshady, Amir Kafshdar, et al. “Secure Credit Reporting on the Blockchain.” Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–48, doi:10.1109/Cybermatics_2018.2018.00231.","short":"A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–1348.","ieee":"A. K. Goharshady, A. Behrouz, and K. Chatterjee, “Secure Credit Reporting on the Blockchain,” in Proceedings of the IEEE International Conference on Blockchain, Halifax, Canada, 2018, pp. 1343–1348.","ama":"Goharshady AK, Behrouz A, Chatterjee K. Secure Credit Reporting on the Blockchain. In: Proceedings of the IEEE International Conference on Blockchain. IEEE; 2018:1343-1348. doi:10.1109/Cybermatics_2018.2018.00231"},"date_created":"2019-04-18T10:37:35Z","doi":"10.1109/Cybermatics_2018.2018.00231","_id":"6340","file_date_updated":"2020-07-14T12:47:27Z","month":"09","publication_identifier":{"isbn":["978-1-5386-7975-3 "]},"conference":{"name":"IEEE International Conference on Blockchain","start_date":"2018-07-30","location":"Halifax, Canada","end_date":"2018-08-03"},"file":[{"date_created":"2019-04-18T10:36:39Z","date_updated":"2020-07-14T12:47:27Z","file_name":"blockchain2018.pdf","checksum":"b25c9bb7cf6e7e6634e692d26d41ead8","file_id":"6341","relation":"main_file","content_type":"application/pdf","file_size":624338,"access_level":"open_access","creator":"akafshda"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"01","oa_version":"Submitted Version","arxiv":1,"author":[{"full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady"},{"last_name":"Behrouz","full_name":"Behrouz, Ali","first_name":"Ali"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"}],"type":"conference","status":"public","isi":1,"has_accepted_license":"1","scopus_import":"1","article_processing_charge":"No","oa":1,"date_updated":"2025-06-02T08:53:45Z","title":"Secure Credit Reporting on the Blockchain","publication":"Proceedings of the IEEE International Conference on Blockchain","language":[{"iso":"eng"}]},{"alternative_title":["LIPIcs"],"status":"public","type":"conference","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Goharshady, Amir","first_name":"Amir","orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"}],"arxiv":1,"conference":{"end_date":"2018-09-07","location":"Beijing, China","start_date":"2018-09-04","name":"CONCUR: Conference on Concurrency Theory"},"publication_identifier":{"isbn":["978-3-95977-087-3"]},"month":"09","oa_version":"Published Version","day":"01","file":[{"file_id":"5696","checksum":"68a055b1aaa241cc38375083cf832a7d","file_name":"2018_CONCUR_Chatterjee.pdf","date_updated":"2020-07-14T12:47:34Z","date_created":"2018-12-17T12:08:00Z","creator":"dernst","access_level":"open_access","relation":"main_file","file_size":1078309,"content_type":"application/pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"oa":1,"date_updated":"2025-06-02T08:53:46Z","article_processing_charge":"No","title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","scopus_import":"1","intvolume":" 118","has_accepted_license":"1","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2018-09-01T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":118,"publication_status":"published","ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"arxiv":["1806.03108"]},"abstract":[{"text":"Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.","lang":"eng"}],"file_date_updated":"2020-07-14T12:47:34Z","_id":"66","doi":"10.4230/LIPIcs.CONCUR.2018.11","year":"2018","publist_id":"7988","citation":{"apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Velner, Y. (2018). Ergodic mean-payoff games for the analysis of attacks in crypto-currencies (Vol. 118). Presented at the CONCUR: Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. 2018. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 118, 11.","mla":"Chatterjee, Krishnendu, et al. Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. Vol. 118, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.11.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. “Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and Y. Velner, “Ergodic mean-payoff games for the analysis of attacks in crypto-currencies,” presented at the CONCUR: Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.CONCUR.2018.11","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018."},"date_created":"2018-12-11T11:44:27Z","ec_funded":1,"article_number":"11","related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]}}]