[{"title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","has_accepted_license":"1","intvolume":" 118","year":"2018","date_created":"2018-12-11T11:44:27Z","publication_identifier":{"isbn":["978-3-95977-087-3"]},"external_id":{"arxiv":["1806.03108"]},"ddc":["000"],"file_date_updated":"2020-07-14T12:47:34Z","citation":{"short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","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.","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","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.","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.","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","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."},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","article_processing_charge":"No","file":[{"relation":"main_file","checksum":"68a055b1aaa241cc38375083cf832a7d","access_level":"open_access","file_id":"5696","date_created":"2018-12-17T12:08:00Z","date_updated":"2020-07-14T12:47:34Z","file_size":1078309,"file_name":"2018_CONCUR_Chatterjee.pdf","creator":"dernst","content_type":"application/pdf"}],"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"}],"conference":{"start_date":"2018-09-04","location":"Beijing, China","end_date":"2018-09-07","name":"CONCUR: Conference on Concurrency Theory"},"day":"01","date_published":"2018-09-01T00:00:00Z","oa":1,"arxiv":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","first_name":"Amir","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"}],"doi":"10.4230/LIPIcs.CONCUR.2018.11","status":"public","date_updated":"2026-07-03T22:35:24Z","publist_id":"7988","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"volume":118,"month":"09","publication_status":"published","_id":"66","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","article_number":"11","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"type":"conference","department":[{"_id":"KrCh"}],"alternative_title":["LIPIcs"],"ec_funded":1,"scopus_import":"1"},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2026-07-03T22:35:25Z","publist_id":"7554","volume":10801,"publication_status":"published","month":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"311","oa_version":"Published Version","page":"739 - 767","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"quality_controlled":"1","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"}],"language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"type":"conference","scopus_import":"1","ec_funded":1,"alternative_title":["LNCS"],"has_accepted_license":"1","title":"Quantitative analysis of smart contracts","intvolume":" 10801","date_created":"2018-12-11T11:45:45Z","year":"2018","ddc":["000"],"file_date_updated":"2020-07-14T12:46:00Z","publisher":"Springer","file":[{"relation":"main_file","access_level":"open_access","checksum":"9c8a8338c571903b599b6ca93abd2cce","file_id":"5716","date_created":"2018-12-17T15:45:49Z","date_updated":"2020-07-14T12:46:00Z","file_size":1394993,"file_name":"2018_ESOP_Chatterjee.pdf","creator":"dernst","content_type":"application/pdf"}],"article_processing_charge":"No","citation":{"apa":"Chatterjee, K., Goharshady, A. K., & Velner, Y. (2018). Quantitative analysis of smart contracts (Vol. 10801, pp. 739–767). Presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89884-1_26","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Yaron Velner. “Quantitative Analysis of Smart Contracts,” 10801:739–67. Springer, 2018. https://doi.org/10.1007/978-3-319-89884-1_26.","ieee":"K. Chatterjee, A. K. Goharshady, and Y. Velner, “Quantitative analysis of smart contracts,” presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece, 2018, vol. 10801, pp. 739–767.","ista":"Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 739–767.","ama":"Chatterjee K, Goharshady AK, Velner Y. Quantitative analysis of smart contracts. In: Vol 10801. Springer; 2018:739-767. doi:10.1007/978-3-319-89884-1_26","mla":"Chatterjee, Krishnendu, et al. Quantitative Analysis of Smart Contracts. Vol. 10801, Springer, 2018, pp. 739–67, doi:10.1007/978-3-319-89884-1_26.","short":"K. Chatterjee, A.K. Goharshady, Y. Velner, in:, Springer, 2018, pp. 739–767."},"day":"01","conference":{"end_date":"2018-04-19","name":"ESOP: European Symposium on Programming","start_date":"2018-04-16","location":"Thessaloniki, Greece"},"abstract":[{"text":"Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts.","lang":"eng"}],"oa":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir","full_name":"Goharshady, Amir","orcid":"0000-0003-1702-6584"},{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"}],"date_published":"2018-04-01T00:00:00Z","acknowledgement":"The research was partially supported by Vienna Science and Technology Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Starting grant (279307: Graph Games).","doi":"10.1007/978-3-319-89884-1_26"},{"month":"09","publication_status":"published","isi":1,"status":"public","date_updated":"2026-07-03T22:35:26Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)"},"quality_controlled":"1","related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"_id":"6340","page":"1343-1348","oa_version":"Submitted Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","language":[{"iso":"eng"}],"publication":"Proceedings of the IEEE International Conference on Blockchain","project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"}],"ec_funded":1,"scopus_import":"1","type":"conference","department":[{"_id":"KrCh"}],"date_created":"2019-04-18T10:37:35Z","year":"2018","publication_identifier":{"isbn":["978-1-5386-7975-3 "]},"external_id":{"arxiv":["1805.09104"],"isi":["000481634500196"]},"title":"Secure Credit Reporting on the Blockchain","has_accepted_license":"1","citation":{"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.","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","short":"A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–1348.","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","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.","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.","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."},"article_processing_charge":"No","file":[{"access_level":"open_access","checksum":"b25c9bb7cf6e7e6634e692d26d41ead8","relation":"main_file","file_id":"6341","date_created":"2019-04-18T10:36:39Z","content_type":"application/pdf","file_name":"blockchain2018.pdf","creator":"akafshda","date_updated":"2020-07-14T12:47:27Z","file_size":624338}],"publisher":"IEEE","file_date_updated":"2020-07-14T12:47:27Z","ddc":["000"],"date_published":"2018-09-01T00:00:00Z","oa":1,"arxiv":1,"author":[{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Behrouz","first_name":"Ali","full_name":"Behrouz, Ali"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"}],"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"}],"conference":{"start_date":"2018-07-30","location":"Halifax, Canada","end_date":"2018-08-03","name":"IEEE International Conference on Blockchain"},"day":"01","doi":"10.1109/Cybermatics_2018.2018.00231"},{"month":"08","publication_status":"published","volume":40,"isi":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.07565"}],"status":"public","date_updated":"2026-07-03T22:35:26Z","related_material":{"record":[{"status":"public","id":"5441","relation":"earlier_version"},{"id":"5442","status":"public","relation":"earlier_version"},{"id":"1437","status":"public","relation":"earlier_version"},{"relation":"dissertation_contains","id":"8934","status":"public"}]},"quality_controlled":"1","article_number":"9","_id":"6009","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"}],"publication":"ACM Transactions on Programming Languages and Systems","corr_author":"1","scopus_import":"1","ec_funded":1,"department":[{"_id":"KrCh"}],"type":"journal_article","publication_identifier":{"issn":["0164-0925"]},"external_id":{"arxiv":["1510.07565"],"isi":["000444694800001"]},"intvolume":" 40","year":"2018","date_created":"2019-02-14T14:31:52Z","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","article_processing_charge":"No","publisher":"Association for Computing Machinery","citation":{"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.","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, 2018.","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, 2018. https://doi.org/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. 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).","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","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, 2018, doi:10.1145/3210257."},"oa":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","orcid":"0000-0003-4783-0389"},{"orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"}],"arxiv":1,"date_published":"2018-08-01T00:00:00Z","day":"01","abstract":[{"lang":"eng","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"}],"doi":"10.1145/3210257","issue":"3"},{"title":"Computational approaches for stochastic shortest path on succinct MDPs","intvolume":" 2018","year":"2018","date_created":"2019-02-13T13:26:27Z","publication_identifier":{"issn":["1045-0823"],"isbn":["9780999241127"]},"external_id":{"arxiv":["1804.08984"],"isi":["000764175404118"]},"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","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.","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.","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"},"publisher":"IJCAI","article_processing_charge":"No","conference":{"end_date":"2018-07-19","name":"IJCAI: International Joint Conference on Artificial Intelligence","location":"Stockholm, Sweden","start_date":"2018-07-13"},"abstract":[{"lang":"eng","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."}],"day":"17","date_published":"2018-07-17T00:00:00Z","oa":1,"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Hongfei","full_name":"Fu, Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","full_name":"Goharshady, Amir","first_name":"Amir","orcid":"0000-0003-1702-6584"},{"last_name":"Okati","full_name":"Okati, Nastaran","first_name":"Nastaran"}],"arxiv":1,"doi":"10.24963/ijcai.2018/653","date_updated":"2026-07-03T22:35:29Z","status":"public","main_file_link":[{"url":"https://arxiv.org/abs/1804.08984","open_access":"1"}],"month":"07","publication_status":"published","volume":2018,"isi":1,"page":"4700-4707","_id":"5977","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"type":"conference","department":[{"_id":"KrCh"}],"ec_funded":1,"scopus_import":"1"},{"language":[{"iso":"eng"}],"project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"291734","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"scopus_import":"1","ec_funded":1,"alternative_title":["ACM SIGPLAN Notices"],"department":[{"_id":"KrCh"}],"type":"conference","isi":1,"month":"01","publication_status":"published","volume":52,"main_file_link":[{"url":"https://arxiv.org/abs/1611.01063","open_access":"1"}],"publist_id":"6157","status":"public","date_updated":"2026-04-07T13:27:56Z","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"14539"}]},"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1194","oa_version":"Submitted Version","page":"145 - 160","arxiv":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Novotny, Petr","first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zikelic","full_name":"Zikelic, Djordje","first_name":"Djordje"}],"oa":1,"date_published":"2017-01-01T00:00:00Z","day":"01","conference":{"end_date":"2017-01-21","name":"POPL: Principles of Programming Languages","start_date":"2017-01-15","location":"Paris, France"},"abstract":[{"lang":"eng","text":"Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider the probabilistic behavior of the programs, the invariants are obtained completely ignoring the probabilistic aspect. In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We define the notion of {\\em stochastic invariants}, which are constraints along with a probability bound that the constraints hold. We introduce a concept of {\\em repulsing supermartingales}. First, we show that repulsing supermartingales can be used to obtain bounds on the probability of the stochastic invariants. Second, we show the effectiveness of repulsing supermartingales in the following three ways: (1)~With a combination of ranking and repulsing supermartingales we can compute lower bounds on the probability of termination; (2)~repulsing supermartingales provide witnesses for refutation of almost-sure termination; and (3)~with a combination of ranking and repulsing supermartingales we can establish persistence properties of probabilistic programs. We also present results on related computational problems and an experimental evaluation of our approach on academic examples. "}],"doi":"10.1145/3009837.3009873","issue":"1","external_id":{"isi":["000408311200013"],"arxiv":["1611.01063"]},"publication_identifier":{"issn":["0730-8566"]},"date_created":"2018-12-11T11:50:39Z","year":"2017","intvolume":" 52","title":"Stochastic invariants for probabilistic termination","publisher":"ACM","article_processing_charge":"No","citation":{"ieee":"K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic termination,” presented at the POPL: Principles of Programming Languages, Paris, France, 2017, vol. 52, no. 1, pp. 145–160.","ista":"Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 52, 145–160.","apa":"Chatterjee, K., Novotný, P., & Zikelic, D. (2017). Stochastic invariants for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles of Programming Languages, Paris, France: ACM. https://doi.org/10.1145/3009837.3009873","chicago":"Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. https://doi.org/10.1145/3009837.3009873.","short":"K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.","mla":"Chatterjee, Krishnendu, et al. Stochastic Invariants for Probabilistic Termination. Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:10.1145/3009837.3009873.","ama":"Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic termination. In: Vol 52. ACM; 2017:145-160. doi:10.1145/3009837.3009873"}},{"doi":"10.1016/j.jcss.2016.09.009","day":"01","abstract":[{"text":"We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints.","lang":"eng"}],"author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"full_name":"Kučera, Antonín","first_name":"Antonín","last_name":"Kučera"}],"oa":1,"date_published":"2017-03-01T00:00:00Z","ddc":["004","006"],"file_date_updated":"2020-07-14T12:44:42Z","publisher":"Elsevier","article_processing_charge":"No","file":[{"access_level":"open_access","checksum":"91271b23cf884d7c06d33bef0cd623b1","relation":"main_file","file_id":"4885","date_created":"2018-12-12T10:11:30Z","date_updated":"2020-07-14T12:44:42Z","file_size":708657,"content_type":"application/pdf","creator":"system","file_name":"IST-2016-717-v1+1_1-s2.0-S0022000016300897-main.pdf"}],"citation":{"chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Trading Performance for Stability in Markov Decision Processes.” Journal of Computer and System Sciences. Elsevier, 2017. https://doi.org/10.1016/j.jcss.2016.09.009.","apa":"Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2017). Trading performance for stability in Markov decision processes. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.09.009","ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2017. Trading performance for stability in Markov decision processes. Journal of Computer and System Sciences. 84, 144–170.","ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance for stability in Markov decision processes,” Journal of Computer and System Sciences, vol. 84. Elsevier, pp. 144–170, 2017.","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability in Markov decision processes. Journal of Computer and System Sciences. 2017;84:144-170. doi:10.1016/j.jcss.2016.09.009","mla":"Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision Processes.” Journal of Computer and System Sciences, vol. 84, Elsevier, 2017, pp. 144–70, doi:10.1016/j.jcss.2016.09.009.","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and System Sciences 84 (2017) 144–170."},"has_accepted_license":"1","title":"Trading performance for stability in Markov decision processes","external_id":{"isi":["000388430000011"]},"date_created":"2018-12-11T11:51:12Z","year":"2017","intvolume":" 84","department":[{"_id":"KrCh"}],"type":"journal_article","scopus_import":"1","ec_funded":1,"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publication":"Journal of Computer and System Sciences","language":[{"iso":"eng"}],"pubrep_id":"717","oa_version":"Published Version","_id":"1294","page":"144 - 170","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"relation":"earlier_version","id":"2305","status":"public"}]},"quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2025-09-29T14:16:56Z","publist_id":"6009","isi":1,"volume":84,"publication_status":"published","month":"03"},{"date_updated":"2025-09-18T10:42:48Z","status":"public","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1701.05738","open_access":"1"}],"month":"03","volume":10205,"publication_status":"published","isi":1,"_id":"13160","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","page":"443-460","oa_version":"Preprint","quality_controlled":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems","language":[{"iso":"eng"}],"type":"conference","department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"corr_author":"1","title":"Index appearance record for transforming Rabin automata into parity automata","intvolume":" 10205","year":"2017","date_created":"2023-06-21T13:21:14Z","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783662545768"],"eisbn":["9783662545775"],"issn":["0302-9743"]},"external_id":{"arxiv":["1701.05738"],"isi":["000440734900026"]},"citation":{"apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 10205, pp. 443–460). Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_26","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” In Tools and Algorithms for the Construction and Analysis of Systems, 10205:443–60. Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_26.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance record for transforming Rabin automata into parity automata. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record for transforming Rabin automata into parity automata,” in Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205, pp. 443–460.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record for transforming Rabin automata into parity automata. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol 10205. Springer; 2017:443-460. doi:10.1007/978-3-662-54577-5_26","mla":"Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460."},"publisher":"Springer","article_processing_charge":"No","conference":{"location":"Uppsala, Sweden","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2017-04-29"},"abstract":[{"text":"Transforming deterministic ω\r\n-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.","lang":"eng"}],"day":"31","date_published":"2017-03-31T00:00:00Z","oa":1,"author":[{"full_name":"Kretinsky, Jan","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"},{"orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"first_name":"Clara","full_name":"Waldmann, Clara","last_name":"Waldmann"},{"last_name":"Weininger","full_name":"Weininger, Maximilian","first_name":"Maximilian"}],"arxiv":1,"acknowledgement":"This work is partially funded by the DFG project “Verified Model Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.","doi":"10.1007/978-3-662-54577-5_26"},{"citation":{"ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2. Elsevier, pp. 230–253, 2017."},"article_processing_charge":"No","publisher":"Elsevier","year":"2017","date_created":"2018-12-11T11:51:50Z","intvolume":" 23","external_id":{"isi":["000390637000014"],"arxiv":["1410.5387"]},"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","doi":"10.1016/j.nahs.2016.04.006","issue":"2","date_published":"2017-02-01T00:00:00Z","author":[{"last_name":"Svoreňová","full_name":"Svoreňová, Mária","first_name":"Mária"},{"first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"},{"first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ivana","full_name":"Cěrná, Ivana","last_name":"Cěrná"},{"last_name":"Belta","full_name":"Belta, Cǎlin","first_name":"Cǎlin"}],"arxiv":1,"oa":1,"abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study."}],"day":"01","quality_controlled":"1","related_material":{"record":[{"status":"public","id":"1689","relation":"earlier_version"}]},"_id":"1407","page":"230 - 253","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Preprint","isi":1,"volume":23,"publication_status":"published","month":"02","date_updated":"2025-06-11T06:33:00Z","publist_id":"5800","status":"public","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"ec_funded":1,"scopus_import":"1","type":"journal_article","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"publication":"Nonlinear Analysis: Hybrid Systems","project":[{"grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}]},{"article_processing_charge":"No","file":[{"creator":"system","file_name":"IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf","content_type":"application/pdf","file_size":582940,"date_updated":"2020-07-14T12:46:32Z","date_created":"2018-12-12T10:13:27Z","file_id":"5010","relation":"main_file","access_level":"open_access","checksum":"12d469ae69b80361333d7dead965cf5d"}],"publisher":"International Federation of Computational Logic","citation":{"apa":"Chatterjee, K., Henzinger, M., & Loitzenbauer, V. (2017). Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:26)2017","chicago":"Chatterjee, Krishnendu, Monika Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for Parity and Streett Objectives.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:26)2017.","ieee":"K. Chatterjee, M. Henzinger, and V. Loitzenbauer, “Improved algorithms for parity and Streett objectives,” Logical Methods in Computer Science, vol. 13, no. 3. International Federation of Computational Logic, 2017.","ista":"Chatterjee K, Henzinger M, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.","mla":"Chatterjee, Krishnendu, et al. “Improved Algorithms for Parity and Streett Objectives.” Logical Methods in Computer Science, vol. 13, no. 3, 26, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:26)2017.","ama":"Chatterjee K, Henzinger M, Loitzenbauer V. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:26)2017","short":"K. Chatterjee, M. Henzinger, V. Loitzenbauer, Logical Methods in Computer Science 13 (2017)."},"ddc":["004"],"file_date_updated":"2020-07-14T12:46:32Z","publication_identifier":{"issn":["1860-5974"]},"external_id":{"arxiv":["1410.0833"],"isi":["000419163000001"]},"intvolume":" 13","date_created":"2018-12-11T11:46:37Z","year":"2017","has_accepted_license":"1","title":"Improved algorithms for parity and Streett objectives","doi":"10.23638/LMCS-13(3:26)2017","issue":"3","oa":1,"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H"},{"last_name":"Loitzenbauer","first_name":"Veronika","full_name":"Loitzenbauer, Veronika"}],"arxiv":1,"date_published":"2017-09-26T00:00:00Z","day":"26","abstract":[{"lang":"eng","text":"The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs in time O(n2+nklogn). For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years."}],"related_material":{"record":[{"status":"public","id":"1661","relation":"earlier_version"}]},"quality_controlled":"1","article_number":"26","license":"https://creativecommons.org/licenses/by-nd/4.0/","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","_id":"464","oa_version":"Published Version","month":"09","publication_status":"published","volume":13,"isi":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png"},"publist_id":"7357","status":"public","date_updated":"2025-09-23T09:20:52Z","scopus_import":"1","corr_author":"1","ec_funded":1,"department":[{"_id":"KrCh"}],"type":"journal_article","language":[{"iso":"eng"}],"pubrep_id":"956","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"}],"publication":"Logical Methods in Computer Science"},{"abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"day":"13","date_published":"2017-09-13T00:00:00Z","oa":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen"},{"first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"}],"issue":"3","doi":"10.23638/LMCS-13(3:23)2017","title":"Edit distance for pushdown automata","has_accepted_license":"1","intvolume":" 13","year":"2017","date_created":"2018-12-11T11:46:37Z","publication_identifier":{"issn":["1860-5974"]},"external_id":{"isi":["000419163000005"]},"file_date_updated":"2020-07-14T12:46:33Z","ddc":["004"],"citation":{"apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2017). Edit distance for pushdown automata. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:23)2017","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:23)2017.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” Logical Methods in Computer Science, vol. 13, no. 3. International Federation of Computational Logic, 2017.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:23)2017","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:23)2017.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017)."},"publisher":"International Federation of Computational Logic","file":[{"date_created":"2018-12-12T10:14:37Z","file_name":"IST-2015-321-v1+1_main.pdf","creator":"system","content_type":"application/pdf","file_size":279071,"date_updated":"2020-07-14T12:46:33Z","relation":"main_file","access_level":"open_access","checksum":"08041379ba408d40664f449eb5907a8f","file_id":"5090"},{"date_updated":"2020-07-14T12:46:33Z","file_size":279071,"file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","creator":"system","content_type":"application/pdf","date_created":"2018-12-12T10:14:38Z","file_id":"5091","relation":"main_file","checksum":"08041379ba408d40664f449eb5907a8f","access_level":"open_access"}],"article_processing_charge":"No","publication":"Logical Methods in Computer Science","project":[{"name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407"}],"pubrep_id":"955","language":[{"iso":"eng"}],"type":"journal_article","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ec_funded":1,"scopus_import":"1","corr_author":"1","date_updated":"2026-04-29T06:14:48Z","publist_id":"7356","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png"},"month":"09","volume":13,"publication_status":"published","isi":1,"_id":"465","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"Published Version","quality_controlled":"1","related_material":{"record":[{"id":"5438","status":"public","relation":"earlier_version"},{"relation":"earlier_version","status":"public","id":"1610"}]}},{"oa_version":"Published Version","_id":"466","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5429"},{"id":"5435","status":"public","relation":"earlier_version"},{"relation":"earlier_version","status":"public","id":"1657"}]},"quality_controlled":"1","article_number":"15","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png"},"publist_id":"7355","date_updated":"2025-09-29T11:00:42Z","status":"public","publication_status":"published","month":"07","volume":13,"isi":1,"department":[{"_id":"KrCh"}],"type":"journal_article","corr_author":"1","scopus_import":"1","ec_funded":1,"project":[{"call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"},{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"701309","call_identifier":"H2020","name":"Atomic Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes","_id":"2590DB08-B435-11E9-9278-68D0E5697425"}],"publication":"Logical Methods in Computer Science","language":[{"iso":"eng"}],"pubrep_id":"957","ddc":["004"],"file_date_updated":"2020-07-14T12:46:33Z","publisher":"International Federation of Computational Logic","file":[{"checksum":"bfa405385ec6229ad5ead89ab5751639","access_level":"open_access","relation":"main_file","file_id":"5354","date_created":"2018-12-12T10:18:32Z","content_type":"application/pdf","creator":"system","file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf","file_size":511832,"date_updated":"2020-07-14T12:46:33Z"}],"article_processing_charge":"No","citation":{"ama":"Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 2017;13(2). doi:10.23638/LMCS-13(2:15)2017","mla":"Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science, vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(2:15)2017.","short":"K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017).","chicago":"Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(2:15)2017.","apa":"Chatterjee, K., Křetínská, Z., & Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(2:15)2017","ieee":"K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” Logical Methods in Computer Science, vol. 13, no. 2. International Federation of Computational Logic, 2017.","ista":"Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15."},"has_accepted_license":"1","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","publication_identifier":{"issn":["1860-5974"]},"external_id":{"isi":["000419160800002"]},"intvolume":" 13","year":"2017","date_created":"2018-12-11T11:46:38Z","issue":"2","doi":"10.23638/LMCS-13(2:15)2017","day":"03","abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. ","lang":"eng"}],"oa":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Křetínská","full_name":"Křetínská, Zuzana","first_name":"Zuzana"},{"last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","first_name":"Jan"}],"date_published":"2017-07-03T00:00:00Z"},{"doi":"10.1145/3152769","issue":"4","date_published":"2017-12-01T00:00:00Z","oa":1,"arxiv":1,"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.","lang":"eng"}],"day":"01","citation":{"apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2017). Nested weighted automata. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3152769","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” ACM Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3152769.","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 18(4), 31.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 4. ACM, 2017.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 2017;18(4). doi:10.1145/3152769","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 4, 31, ACM, 2017, doi:10.1145/3152769.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017)."},"publisher":"ACM","article_processing_charge":"No","intvolume":" 18","date_created":"2018-12-11T11:46:38Z","year":"2017","publication_identifier":{"issn":["1529-3785"]},"external_id":{"isi":["000419237100006"],"arxiv":["1606.03598"]},"title":"Nested weighted automata","ec_funded":1,"corr_author":"1","scopus_import":"1","type":"journal_article","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"language":[{"iso":"eng"}],"publication":"ACM Transactions on Computational Logic (TOCL)","project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","grant_number":"Z211"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","article_number":"31","related_material":{"record":[{"status":"public","id":"5415","relation":"earlier_version"},{"relation":"earlier_version","id":"5436","status":"public"},{"relation":"earlier_version","id":"1656","status":"public"}]},"_id":"467","oa_version":"Preprint","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":18,"month":"12","publication_status":"published","isi":1,"date_updated":"2025-09-23T09:39:58Z","publist_id":"7354","status":"public","main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}]},{"publisher":"Nature Publishing Group","article_processing_charge":"No","file":[{"relation":"main_file","checksum":"7d05cbdd914e194a019c0f91fb64e9a8","access_level":"open_access","file_id":"5357","date_created":"2018-12-12T10:18:35Z","creator":"system","file_name":"IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:46:36Z","file_size":1536783}],"citation":{"ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification on undirected population structures: Comets beat stars,” Scientific Reports, vol. 7, no. 1. Nature Publishing Group, 2017.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 7(1), 82.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.” Scientific Reports. Nature Publishing Group, 2017. https://doi.org/10.1038/s41598-017-00107-w.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2017). Amplification on undirected population structures: Comets beat stars. Scientific Reports. Nature Publishing Group. https://doi.org/10.1038/s41598-017-00107-w","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports 7 (2017).","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 2017;7(1). doi:10.1038/s41598-017-00107-w","mla":"Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures: Comets Beat Stars.” Scientific Reports, vol. 7, no. 1, 82, Nature Publishing Group, 2017, doi:10.1038/s41598-017-00107-w."},"ddc":["004"],"file_date_updated":"2020-07-14T12:46:36Z","publication_identifier":{"issn":["2045-2322"]},"external_id":{"isi":["000396867800013"]},"intvolume":" 7","year":"2017","date_created":"2018-12-11T11:46:53Z","has_accepted_license":"1","title":"Amplification on undirected population structures: Comets beat stars","doi":"10.1038/s41598-017-00107-w","issue":"1","oa":1,"author":[{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","first_name":"Josef","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"date_published":"2017-03-06T00:00:00Z","day":"06","abstract":[{"text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population. The fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure. Amplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade. In this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Cometswarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively. ","lang":"eng"}],"related_material":{"record":[{"relation":"earlier_version","id":"5449","status":"public"}]},"quality_controlled":"1","article_number":"82","oa_version":"Published Version","_id":"512","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":7,"publication_status":"published","month":"03","isi":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publist_id":"7307","date_updated":"2025-09-18T09:50:10Z","status":"public","corr_author":"1","scopus_import":"1","ec_funded":1,"department":[{"_id":"KrCh"}],"type":"journal_article","language":[{"iso":"eng"}],"pubrep_id":"938","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"publication":"Scientific Reports"},{"alternative_title":["IST Austria Technical Report"],"department":[{"_id":"KrCh"}],"type":"technical_report","language":[{"iso":"eng"}],"pubrep_id":"870","related_material":{"record":[{"relation":"later_version","id":"10416","status":"public"}]},"_id":"5455","oa_version":"Published Version","page":"37","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","month":"10","publication_status":"published","status":"public","date_updated":"2025-04-15T08:12:18Z","doi":"10.15479/AT:IST-2017-870-v1-1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Choudhary","full_name":"Choudhary, Bhavya","first_name":"Bhavya"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"}],"oa":1,"date_published":"2017-10-23T00:00:00Z","day":"23","abstract":[{"text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graphwhere the edges are labeled with different types of opening and closing parentheses, and the reachabilityinformation is computed via paths whose parentheses are properly matched. We present new results for Dyckreachability problems with applications to alias analysis and data-dependence analysis. Our main contributions,that include improved upper bounds as well as lower bounds that establish optimality guarantees, are asfollows:First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph withnnodes andmedges, we present: (i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching lower bound that shows that our algorithm is optimalwrt to worst-case complexity; and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtainanalysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almostlinear time, after which the contribution of the library in the complexity of the client analysis is only linear,and only wrt the number of call sites.Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean MatrixMultiplication, which is a long-standing open problem. Thus we establish that the existing combinatorialalgorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the samehardness holds for graphs of constant treewidth.Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependenceanalysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform allexisting methods on the two problems, over real-world benchmarks.","lang":"eng"}],"publisher":"IST Austria","article_processing_charge":"No","file":[{"relation":"main_file","checksum":"177a84a46e3ac17e87b31534ad16a4c9","access_level":"open_access","file_id":"5524","date_created":"2018-12-12T11:54:02Z","date_updated":"2020-07-14T12:46:59Z","file_size":960491,"creator":"system","file_name":"IST-2017-870-v1+1_main.pdf","content_type":"application/pdf"}],"citation":{"ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria; 2017. doi:10.15479/AT:IST-2017-870-v1-1","mla":"Chatterjee, Krishnendu, et al. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria, 2017, doi:10.15479/AT:IST-2017-870-v1-1.","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for Data-Dependence and Alias Analysis, IST Austria, 2017.","apa":"Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and alias analysis. IST Austria. https://doi.org/10.15479/AT:IST-2017-870-v1-1","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2017-870-v1-1.","ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and alias analysis, IST Austria, 37p.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, Optimal Dyck reachability for data-dependence and alias analysis. IST Austria, 2017."},"file_date_updated":"2020-07-14T12:46:59Z","ddc":["000"],"publication_identifier":{"issn":["2664-1690"]},"year":"2017","date_created":"2018-12-12T11:39:26Z","has_accepted_license":"1","title":"Optimal Dyck reachability for data-dependence and alias analysis"},{"type":"technical_report","department":[{"_id":"KrCh"}],"doi":"10.15479/AT:IST-2017-872-v1-1","alternative_title":["IST Austria Technical Report"],"abstract":[{"lang":"eng","text":"We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.\r\nWe introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.\r\n1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence. \r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes."}],"day":"23","date_published":"2017-10-23T00:00:00Z","pubrep_id":"872","oa":1,"language":[{"iso":"eng"}],"author":[{"first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Sinha, Nishant","first_name":"Nishant","last_name":"Sinha"},{"first_name":"Kapil","full_name":"Vaidya, Kapil","last_name":"Vaidya"}],"oa_version":"Published Version","_id":"5456","page":"36","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"file_date_updated":"2020-07-14T12:46:59Z","citation":{"ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, Data-centric dynamic partial order reduction. IST Austria, 2017.","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction, IST Austria, 36p.","apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K. (2017). Data-centric dynamic partial order reduction. IST Austria. https://doi.org/10.15479/AT:IST-2017-872-v1-1","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2017-872-v1-1.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2017.","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-Centric Dynamic Partial Order Reduction. IST Austria; 2017. doi:10.15479/AT:IST-2017-872-v1-1","mla":"Chalupa, Marek, et al. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2017, doi:10.15479/AT:IST-2017-872-v1-1."},"file":[{"file_size":910347,"date_updated":"2020-07-14T12:46:59Z","creator":"system","file_name":"IST-2017-872-v1+1_main.pdf","content_type":"application/pdf","date_created":"2018-12-12T11:53:26Z","file_id":"5487","relation":"main_file","access_level":"open_access","checksum":"d2635c4cf013000f0a1b09e80f9e4ab7"}],"publisher":"IST Austria","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5448"},{"id":"10417","status":"public","relation":"later_version"}]},"title":"Data-centric dynamic partial order reduction","date_updated":"2025-05-20T09:45:08Z","status":"public","has_accepted_license":"1","year":"2017","date_created":"2018-12-12T11:39:26Z","publication_identifier":{"issn":["2664-1690"]},"month":"10","publication_status":"published"},{"doi":"10.4230/LIPIcs.MFCS.2017.61","date_published":"2017-11-01T00:00:00Z","oa":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"abstract":[{"lang":"eng","text":"Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates the reproductive strength. The evolutionary dynamics happens as follows: in the initial step, in a population of all resident individuals a mutant is introduced, and then at each step, an individual is chosen proportional to the fitness of its type to reproduce, and the offspring replaces a neighbor uniformly at random. The process stops when all individuals are either residents or mutants. The probability that all individuals in the end are mutants is called the fixation probability, which is a key factor in the rate of evolution. We consider the problem of approximating the fixation probability. The class of algorithms that is extremely relevant for approximation of the fixation probabilities is the Monte-Carlo simulation of the process. Previous results present a polynomial-time Monte-Carlo algorithm for undirected graphs when r is given in unary. First, we present a simple modification: instead of simulating each step, we discard ineffective steps, where no node changes type (i.e., either residents replace residents, or mutants replace mutants). Using the above simple modification and our result that the number of effective steps is concentrated around the expected number of effective steps, we present faster polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are always at least a factor O(n2/ log n) faster as compared to the previous algorithms, where n is the number of nodes, and is polynomial even if r is given in binary. We also present lower bounds showing that the upper bound on the expected number of effective steps we present is asymptotically tight for undirected graphs. "}],"conference":{"start_date":"2017-08-21","location":"Aalborg, Denmark","name":"MFCS: Mathematical Foundations of Computer Science","end_date":"2017-08-25"},"day":"01","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In: Leibniz International Proceedings in Informatics. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.61","mla":"Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” Leibniz International Proceedings in Informatics, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.61.","ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2017. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 83, 61.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs,” in Leibniz International Proceedings in Informatics, Aalborg, Denmark, 2017, vol. 83.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” In Leibniz International Proceedings in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.61.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2017). Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In Leibniz International Proceedings in Informatics (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.61"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","article_processing_charge":"No","file":[{"date_created":"2018-12-12T10:18:04Z","date_updated":"2020-07-14T12:47:00Z","file_size":535077,"content_type":"application/pdf","file_name":"IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf","creator":"system","checksum":"2eed5224c0e4e259484a1d71acb8ba6a","access_level":"open_access","relation":"main_file","file_id":"5322"}],"file_date_updated":"2020-07-14T12:47:00Z","ddc":["004"],"intvolume":" 83","date_created":"2018-12-11T11:47:08Z","year":"2017","publication_identifier":{"isbn":["978-395977046-0"]},"title":"Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs","has_accepted_license":"1","alternative_title":["LIPIcs"],"scopus_import":"1","corr_author":"1","type":"conference","department":[{"_id":"KrCh"}],"pubrep_id":"924","language":[{"iso":"eng"}],"publication":"Leibniz International Proceedings in Informatics","quality_controlled":"1","article_number":"61","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"551","oa_version":"Published Version","month":"11","volume":83,"publication_status":"published","publist_id":"7263","status":"public","date_updated":"2025-07-10T11:52:51Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"}},{"publication":"Leibniz International Proceedings in Informatics","project":[{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"pubrep_id":"923","language":[{"iso":"eng"}],"type":"conference","department":[{"_id":"KrCh"}],"ec_funded":1,"alternative_title":["LIPIcs"],"scopus_import":"1","corr_author":"1","publist_id":"7262","status":"public","date_updated":"2025-07-10T11:52:52Z","tmp":{"image":"/images/cc_by.png","short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"month":"11","publication_status":"published","volume":83,"oa_version":"Published Version","_id":"552","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","license":"https://creativecommons.org/licenses/by/3.0/","quality_controlled":"1","article_number":"39","conference":{"location":"Aalborg, Denmark","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science","end_date":"2017-08-25"},"abstract":[{"lang":"eng","text":"Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a meanpayoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with n vertices, m edges, parity objectives with d priorities, and maximal absolute reward value W for mean-payoff objectives, are as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for the value problem. Our main contributions are faster algorithms, and the running times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem, and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective)."}],"day":"01","date_published":"2017-11-01T00:00:00Z","oa":1,"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Monika H","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger"},{"last_name":"Svozil","full_name":"Svozil, Alexander","first_name":"Alexander"}],"doi":"10.4230/LIPIcs.MFCS.2017.39","title":"Faster algorithms for mean-payoff parity games","has_accepted_license":"1","intvolume":" 83","date_created":"2018-12-11T11:47:08Z","year":"2017","publication_identifier":{"isbn":["978-395977046-0"]},"ddc":["004"],"file_date_updated":"2020-07-14T12:47:00Z","citation":{"short":"K. Chatterjee, M. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Mean-Payoff Parity Games.” Leibniz International Proceedings in Informatics, vol. 83, 39, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.39.","ama":"Chatterjee K, Henzinger M, Svozil A. Faster algorithms for mean-payoff parity games. In: Leibniz International Proceedings in Informatics. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.39","ieee":"K. Chatterjee, M. Henzinger, and A. Svozil, “Faster algorithms for mean-payoff parity games,” in Leibniz International Proceedings in Informatics, Aalborg, Denmark, 2017, vol. 83.","ista":"Chatterjee K, Henzinger M, Svozil A. 2017. Faster algorithms for mean-payoff parity games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 83, 39.","chicago":"Chatterjee, Krishnendu, Monika Henzinger, and Alexander Svozil. “Faster Algorithms for Mean-Payoff Parity Games.” In Leibniz International Proceedings in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.39.","apa":"Chatterjee, K., Henzinger, M., & Svozil, A. (2017). Faster algorithms for mean-payoff parity games. In Leibniz International Proceedings in Informatics (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.39"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","article_processing_charge":"No","file":[{"access_level":"open_access","checksum":"c67f4866ddbfd555afef1f63ae9a8fc7","relation":"main_file","file_id":"5248","date_created":"2018-12-12T10:16:57Z","file_size":610339,"date_updated":"2020-07-14T12:47:00Z","content_type":"application/pdf","creator":"system","file_name":"IST-2018-923-v1+1_LIPIcs-MFCS-2017-39.pdf"}]},{"file_date_updated":"2020-07-14T12:47:00Z","ddc":["004"],"citation":{"apa":"Chatterjee, K., Hansen, K., & Ibsen-Jensen, R. (2017). Strategy complexity of concurrent safety games. In Leibniz International Proceedings in Informatics (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.55","chicago":"Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy Complexity of Concurrent Safety Games.” In Leibniz International Proceedings in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.55.","ieee":"K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent safety games,” in Leibniz International Proceedings in Informatics, Aalborg, Denmark, 2017, vol. 83.","ista":"Chatterjee K, Hansen K, Ibsen-Jensen R. 2017. Strategy complexity of concurrent safety games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 83, 55.","mla":"Chatterjee, Krishnendu, et al. “Strategy Complexity of Concurrent Safety Games.” Leibniz International Proceedings in Informatics, vol. 83, 55, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.55.","ama":"Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent safety games. In: Leibniz International Proceedings in Informatics. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.55","short":"K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017."},"article_processing_charge":"No","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"file_id":"4753","access_level":"open_access","checksum":"7101facb56ade363205c695d72dbd173","relation":"main_file","file_size":549967,"date_updated":"2020-07-14T12:47:00Z","content_type":"application/pdf","creator":"system","file_name":"IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf","date_created":"2018-12-12T10:09:29Z"}],"title":"Strategy complexity of concurrent safety games","has_accepted_license":"1","year":"2017","date_created":"2018-12-11T11:47:08Z","intvolume":" 83","external_id":{"arxiv":["1506.02434"]},"publication_identifier":{"isbn":["978-395977046-0"]},"doi":"10.4230/LIPIcs.MFCS.2017.55","conference":{"end_date":"2017-08-25","name":"MFCS: Mathematical Foundations of Computer Science","location":"Aalborg, Denmark","start_date":"2017-08-21"},"abstract":[{"lang":"eng","text":"We consider two player, zero-sum, finite-state concurrent reachability games, played for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. Player 1 wins iff a designated goal state is eventually visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed. Our main results are as follows: We show that: (i) the optimal bound on the patience of optimal and -optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. "}],"day":"01","date_published":"2017-11-01T00:00:00Z","arxiv":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Hansen","first_name":"Kristofer","full_name":"Hansen, Kristofer"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"_id":"553","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","article_number":"55","quality_controlled":"1","publist_id":"7261","date_updated":"2025-06-04T09:37:06Z","status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1506.02434"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"volume":83,"publication_status":"published","month":"11","type":"conference","department":[{"_id":"KrCh"}],"alternative_title":["LIPIcs"],"scopus_import":"1","corr_author":"1","publication":"Leibniz International Proceedings in Informatics","pubrep_id":"922","language":[{"iso":"eng"}]},{"date_updated":"2025-04-15T08:12:19Z","status":"public","title":"Strong amplifiers of natural selection","has_accepted_license":"1","year":"2017","date_created":"2018-12-12T12:31:32Z","month":"01","_id":"5559","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","ddc":["519"],"file_date_updated":"2020-07-14T12:47:02Z","citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak . “Strong Amplifiers of Natural Selection.” Institute of Science and Technology Austria, 2017. https://doi.org/10.15479/AT:ISTA:51.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak , M. (2017). Strong amplifiers of natural selection. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:51","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Strong amplifiers of natural selection, Institute of Science and Technology Austria, 10.15479/AT:ISTA:51.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak , “Strong amplifiers of natural selection.” Institute of Science and Technology Austria, 2017.","mla":"Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection. Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:51.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Strong amplifiers of natural selection. 2017. doi:10.15479/AT:ISTA:51","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak , (2017)."},"related_material":{"record":[{"id":"5452","status":"public","relation":"research_paper"},{"relation":"research_paper","status":"public","id":"5751"}]},"article_processing_charge":"No","publisher":"Institute of Science and Technology Austria","file":[{"file_size":32987015,"date_updated":"2020-07-14T12:47:02Z","content_type":"video/mp4","creator":"system","file_name":"IST-2017-51-v1+2_illustration.mp4","date_created":"2018-12-12T13:05:18Z","file_id":"5644","access_level":"open_access","checksum":"b427dd46a30096a1911b245640c47af8","relation":"main_file"}],"keyword":["natural selection"],"abstract":[{"lang":"eng","text":"Strong amplifiers of natural selection"}],"project":[{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"}],"day":"02","date_published":"2017-01-02T00:00:00Z","author":[{"first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"},{"orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Martin","full_name":"Nowak , Martin","last_name":"Nowak "}],"datarep_id":"51","oa":1,"type":"research_data","department":[{"_id":"KrCh"}],"ec_funded":1,"doi":"10.15479/AT:ISTA:51"}]