[{"file_date_updated":"2020-07-14T12:47:34Z","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir","last_name":"Goharshady"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-3-95977-087-3"]},"publication_status":"published","article_number":"11","citation":{"short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","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., &#38; 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. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.11</a>","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.","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:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">10.4230/LIPIcs.CONCUR.2018.11</a>","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. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.11</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies</i>. Vol. 118, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">10.4230/LIPIcs.CONCUR.2018.11</a>."},"year":"2018","article_processing_charge":"No","conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2018-09-04","location":"Beijing, China","end_date":"2018-09-07"},"arxiv":1,"oa_version":"Published Version","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","call_identifier":"FP7","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"date_updated":"2026-08-30T22:31:01Z","_id":"66","title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","intvolume":"       118","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"volume":118,"month":"09","external_id":{"arxiv":["1806.03108"]},"day":"01","alternative_title":["LIPIcs"],"status":"public","abstract":[{"lang":"eng","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."}],"date_created":"2018-12-11T11:44:27Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":"1","quality_controlled":"1","date_published":"2018-09-01T00:00:00Z","type":"conference","doi":"10.4230/LIPIcs.CONCUR.2018.11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","department":[{"_id":"KrCh"}],"publist_id":"7988","file":[{"file_name":"2018_CONCUR_Chatterjee.pdf","checksum":"68a055b1aaa241cc38375083cf832a7d","creator":"dernst","relation":"main_file","file_size":1078309,"file_id":"5696","access_level":"open_access","date_created":"2018-12-17T12:08:00Z","content_type":"application/pdf","date_updated":"2020-07-14T12:47:34Z"}]},{"ddc":["000"],"tmp":{"short":"CC BY-NC-ND (4.0)","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"},"title":"Secure Credit Reporting on the Blockchain","external_id":{"arxiv":["1805.09104"],"isi":["000481634500196"]},"oa":1,"month":"09","ec_funded":1,"_id":"6340","related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"date_updated":"2026-08-30T22:31:01Z","article_processing_charge":"No","conference":{"location":"Halifax, Canada","end_date":"2018-08-03","name":"IEEE International Conference on Blockchain","start_date":"2018-07-30"},"year":"2018","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"}],"page":"1343-1348","arxiv":1,"oa_version":"Submitted Version","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-5386-7975-3 "]},"file_date_updated":"2020-07-14T12:47:27Z","author":[{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar"},{"first_name":"Ali","last_name":"Behrouz","full_name":"Behrouz, Ali"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"}],"publication_status":"published","citation":{"ieee":"A. K. Goharshady, A. Behrouz, and K. Chatterjee, “Secure Credit Reporting on the Blockchain,” in <i>Proceedings of the IEEE International Conference on Blockchain</i>, Halifax, Canada, 2018, pp. 1343–1348.","short":"A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE International Conference on Blockchain, IEEE, 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.","apa":"Goharshady, A. K., Behrouz, A., &#38; Chatterjee, K. (2018). Secure Credit Reporting on the Blockchain. In <i>Proceedings of the IEEE International Conference on Blockchain</i> (pp. 1343–1348). Halifax, Canada: IEEE. <a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">https://doi.org/10.1109/Cybermatics_2018.2018.00231</a>","chicago":"Goharshady, Amir Kafshdar, Ali Behrouz, and Krishnendu Chatterjee. “Secure Credit Reporting on the Blockchain.” In <i>Proceedings of the IEEE International Conference on Blockchain</i>, 1343–48. IEEE, 2018. <a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">https://doi.org/10.1109/Cybermatics_2018.2018.00231</a>.","ama":"Goharshady AK, Behrouz A, Chatterjee K. Secure Credit Reporting on the Blockchain. In: <i>Proceedings of the IEEE International Conference on Blockchain</i>. IEEE; 2018:1343-1348. doi:<a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">10.1109/Cybermatics_2018.2018.00231</a>","mla":"Goharshady, Amir Kafshdar, et al. “Secure Credit Reporting on the Blockchain.” <i>Proceedings of the IEEE International Conference on Blockchain</i>, IEEE, 2018, pp. 1343–48, doi:<a href=\"https://doi.org/10.1109/Cybermatics_2018.2018.00231\">10.1109/Cybermatics_2018.2018.00231</a>."},"publication":"Proceedings of the IEEE International Conference on Blockchain","department":[{"_id":"KrCh"}],"has_accepted_license":"1","file":[{"date_created":"2019-04-18T10:36:39Z","content_type":"application/pdf","date_updated":"2020-07-14T12:47:27Z","checksum":"b25c9bb7cf6e7e6634e692d26d41ead8","file_name":"blockchain2018.pdf","creator":"akafshda","relation":"main_file","access_level":"open_access","file_size":624338,"file_id":"6341"}],"doi":"10.1109/Cybermatics_2018.2018.00231","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","quality_controlled":"1","date_published":"2018-09-01T00:00:00Z","date_created":"2019-04-18T10:37:35Z","publisher":"IEEE","scopus_import":"1","type":"conference","abstract":[{"lang":"eng","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*."}],"status":"public","isi":1,"day":"01"},{"day":"01","abstract":[{"lang":"eng","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."}],"status":"public","alternative_title":["LNCS"],"type":"conference","date_published":"2018-04-01T00:00:00Z","quality_controlled":"1","scopus_import":"1","date_created":"2018-12-11T11:45:45Z","publisher":"Springer","file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:46:00Z","date_created":"2018-12-17T15:45:49Z","access_level":"open_access","file_id":"5716","file_size":1394993,"checksum":"9c8a8338c571903b599b6ca93abd2cce","file_name":"2018_ESOP_Chatterjee.pdf","creator":"dernst","relation":"main_file"}],"publist_id":"7554","department":[{"_id":"KrCh"}],"has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-319-89884-1_26","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Analysis of Smart Contracts</i>. Vol. 10801, Springer, 2018, pp. 739–67, doi:<a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">10.1007/978-3-319-89884-1_26</a>.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Yaron Velner. “Quantitative Analysis of Smart Contracts,” 10801:739–67. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">https://doi.org/10.1007/978-3-319-89884-1_26</a>.","ama":"Chatterjee K, Goharshady AK, Velner Y. Quantitative analysis of smart contracts. In: Vol 10801. Springer; 2018:739-767. doi:<a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">10.1007/978-3-319-89884-1_26</a>","apa":"Chatterjee, K., Goharshady, A. K., &#38; Velner, Y. (2018). Quantitative analysis of smart contracts (Vol. 10801, pp. 739–767). Presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece: Springer. <a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">https://doi.org/10.1007/978-3-319-89884-1_26</a>","ista":"Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 739–767.","short":"K. Chatterjee, A.K. Goharshady, Y. Velner, in:, Springer, 2018, pp. 739–767.","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."},"publication_status":"published","language":[{"iso":"eng"}],"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-1702-6584","first_name":"Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir","last_name":"Goharshady"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"file_date_updated":"2020-07-14T12:46:00Z","page":"739 - 767","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"}],"oa_version":"Published Version","conference":{"location":"Thessaloniki, Greece","end_date":"2018-04-19","name":"ESOP: European Symposium on Programming","start_date":"2018-04-16"},"article_processing_charge":"No","year":"2018","_id":"311","related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"date_updated":"2026-08-30T22:31:01Z","ec_funded":1,"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).","volume":10801,"month":"04","oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"intvolume":"     10801","title":"Quantitative analysis of smart contracts"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1145/3210257","department":[{"_id":"KrCh"}],"scopus_import":"1","publisher":"Association for Computing Machinery","date_created":"2019-02-14T14:31:52Z","date_published":"2018-08-01T00:00:00Z","quality_controlled":"1","issue":"3","type":"journal_article","status":"public","abstract":[{"text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n","lang":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.07565"}],"isi":1,"day":"01","intvolume":"        40","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","month":"08","volume":40,"oa":1,"external_id":{"isi":["000444694800001"],"arxiv":["1510.07565"]},"ec_funded":1,"related_material":{"record":[{"status":"public","id":"5441","relation":"earlier_version"},{"id":"5442","status":"public","relation":"earlier_version"},{"relation":"earlier_version","id":"1437","status":"public"},{"id":"8934","status":"public","relation":"dissertation_contains"}]},"date_updated":"2026-08-30T22:31:02Z","_id":"6009","year":"2018","article_processing_charge":"No","oa_version":"Preprint","arxiv":1,"corr_author":"1","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"}],"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"},{"orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"}],"publication_identifier":{"issn":["0164-0925"]},"language":[{"iso":"eng"}],"publication":"ACM Transactions on Programming Languages and Systems","citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3. Association for Computing Machinery, 2018.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., &#38; Pavlogiannis, A. (2018). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>","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.","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. 2018;40(3). doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery, 2018. <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>.","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3, 9, Association for Computing Machinery, 2018, doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>."},"publication_status":"published","article_number":"9"},{"quality_controlled":"1","date_published":"2018-07-17T00:00:00Z","scopus_import":"1","date_created":"2019-02-13T13:26:27Z","publisher":"IJCAI","type":"conference","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.24963/ijcai.2018/653","isi":1,"day":"17","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."}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.08984"}],"status":"public","ec_funded":1,"_id":"5977","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"date_updated":"2026-08-30T22:31:02Z","intvolume":"      2018","title":"Computational approaches for stochastic shortest path on succinct MDPs","external_id":{"arxiv":["1804.08984"],"isi":["000764175404118"]},"month":"07","volume":2018,"oa":1,"publication_identifier":{"isbn":["9780999241127"],"issn":["1045-0823"]},"language":[{"iso":"eng"}],"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"full_name":"Goharshady, Amir","last_name":"Goharshady","orcid":"0000-0003-1702-6584","first_name":"Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Nastaran","last_name":"Okati","full_name":"Okati, Nastaran"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, vol. 2018, IJCAI, 2018, pp. 4700–07, doi:<a href=\"https://doi.org/10.24963/ijcai.2018/653\">10.24963/ijcai.2018/653</a>.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran Okati. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” In <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, 2018:4700–4707. IJCAI, 2018. <a href=\"https://doi.org/10.24963/ijcai.2018/653\">https://doi.org/10.24963/ijcai.2018/653</a>.","ama":"Chatterjee K, Fu H, Goharshady AK, Okati N. Computational approaches for stochastic shortest path on succinct MDPs. In: <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>. Vol 2018. IJCAI; 2018:4700-4707. doi:<a href=\"https://doi.org/10.24963/ijcai.2018/653\">10.24963/ijcai.2018/653</a>","apa":"Chatterjee, K., Fu, H., Goharshady, A. K., &#38; Okati, N. (2018). Computational approaches for stochastic shortest path on succinct MDPs. In <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i> (Vol. 2018, pp. 4700–4707). Stockholm, Sweden: IJCAI. <a href=\"https://doi.org/10.24963/ijcai.2018/653\">https://doi.org/10.24963/ijcai.2018/653</a>","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.","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.","ieee":"K. Chatterjee, H. Fu, A. K. Goharshady, and N. Okati, “Computational approaches for stochastic shortest path on succinct MDPs,” in <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, Stockholm, Sweden, 2018, vol. 2018, pp. 4700–4707."},"publication_status":"published","publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2018-07-13","location":"Stockholm, Sweden","end_date":"2018-07-19"},"article_processing_charge":"No","year":"2018","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"}],"page":"4700-4707","oa_version":"Preprint","arxiv":1},{"issue":"1","type":"conference","quality_controlled":"1","date_published":"2017-01-01T00:00:00Z","scopus_import":"1","date_created":"2018-12-11T11:50:39Z","publisher":"ACM","publist_id":"6157","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1145/3009837.3009873","day":"01","isi":1,"main_file_link":[{"url":"https://arxiv.org/abs/1611.01063","open_access":"1"}],"abstract":[{"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. ","lang":"eng"}],"status":"public","alternative_title":["ACM SIGPLAN Notices"],"_id":"1194","related_material":{"record":[{"id":"14539","status":"public","relation":"dissertation_contains"}]},"date_updated":"2026-04-07T13:27:56Z","ec_funded":1,"external_id":{"isi":["000408311200013"],"arxiv":["1611.01063"]},"volume":52,"month":"01","oa":1,"intvolume":"        52","title":"Stochastic invariants for probabilistic termination","citation":{"short":"K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.","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.","apa":"Chatterjee, K., Novotný, P., &#38; Zikelic, D. (2017). Stochastic invariants for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles of Programming Languages, Paris, France: ACM. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>","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.","chicago":"Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>.","ama":"Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic termination. In: Vol 52. ACM; 2017:145-160. doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>","mla":"Chatterjee, Krishnendu, et al. <i>Stochastic Invariants for Probabilistic Termination</i>. Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>."},"publication_status":"published","publication_identifier":{"issn":["0730-8566"]},"language":[{"iso":"eng"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"},{"full_name":"Zikelic, Djordje","last_name":"Zikelic","first_name":"Djordje"}],"project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"grant_number":"291734","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"page":"145 - 160","arxiv":1,"oa_version":"Submitted Version","conference":{"name":"POPL: Principles of Programming Languages","start_date":"2017-01-15","location":"Paris, France","end_date":"2017-01-21"},"article_processing_charge":"No","year":"2017"},{"page":"144 - 170","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa_version":"Published Version","article_processing_charge":"No","year":"2017","citation":{"mla":"Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>, vol. 84, Elsevier, 2017, pp. 144–70, doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>.","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. 2017;84:144-170. doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>","apa":"Brázdil, T., Chatterjee, K., Forejt, V., &#38; Kučera, A. (2017). Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>","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.","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and System Sciences 84 (2017) 144–170.","ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance for stability in Markov decision processes,” <i>Journal of Computer and System Sciences</i>, vol. 84. Elsevier, pp. 144–170, 2017."},"publication_status":"published","publication":"Journal of Computer and System Sciences","language":[{"iso":"eng"}],"author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"full_name":"Kučera, Antonín","last_name":"Kučera","first_name":"Antonín"}],"file_date_updated":"2020-07-14T12:44:42Z","external_id":{"isi":["000388430000011"]},"month":"03","volume":84,"pubrep_id":"717","oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["004","006"],"intvolume":"        84","title":"Trading performance for stability in Markov decision processes","_id":"1294","related_material":{"record":[{"status":"public","id":"2305","relation":"earlier_version"}]},"date_updated":"2025-09-29T14:16:56Z","ec_funded":1,"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"}],"status":"public","day":"01","isi":1,"file":[{"creator":"system","relation":"main_file","checksum":"91271b23cf884d7c06d33bef0cd623b1","file_name":"IST-2016-717-v1+1_1-s2.0-S0022000016300897-main.pdf","file_id":"4885","file_size":708657,"access_level":"open_access","date_created":"2018-12-12T10:11:30Z","date_updated":"2020-07-14T12:44:42Z","content_type":"application/pdf"}],"publist_id":"6009","department":[{"_id":"KrCh"}],"has_accepted_license":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","doi":"10.1016/j.jcss.2016.09.009","type":"journal_article","date_published":"2017-03-01T00:00:00Z","quality_controlled":"1","scopus_import":"1","publisher":"Elsevier","date_created":"2018-12-11T11:51:12Z"},{"department":[{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1007/978-3-662-54577-5_26","quality_controlled":"1","date_published":"2017-03-31T00:00:00Z","publisher":"Springer","date_created":"2023-06-21T13:21:14Z","type":"conference","alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1701.05738"}],"abstract":[{"lang":"eng","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."}],"status":"public","isi":1,"day":"31","intvolume":"     10205","title":"Index appearance record for transforming Rabin automata into parity automata","external_id":{"arxiv":["1701.05738"],"isi":["000440734900026"]},"volume":10205,"month":"03","oa":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.","_id":"13160","date_updated":"2025-09-18T10:42:48Z","article_processing_charge":"No","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2017-04-22","location":"Uppsala, Sweden","end_date":"2017-04-29"},"year":"2017","page":"443-460","oa_version":"Preprint","arxiv":1,"corr_author":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783662545775"],"isbn":["9783662545768"]},"language":[{"iso":"eng"}],"author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan"},{"last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","orcid":"0000-0002-1712-2165"},{"first_name":"Clara","full_name":"Waldmann, Clara","last_name":"Waldmann"},{"first_name":"Maximilian","full_name":"Weininger, Maximilian","last_name":"Weininger"}],"citation":{"mla":"Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 10205, Springer, 2017, pp. 443–60, doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record for transforming Rabin automata into parity automata. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 10205. Springer; 2017:443-460. doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 10205:443–60. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>.","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.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 10205, pp. 443–460). Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>","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.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record for transforming Rabin automata into parity automata,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Uppsala, Sweden, 2017, vol. 10205, pp. 443–460."},"publication_status":"published","publication":"Tools and Algorithms for the Construction and Analysis of Systems"},{"date_created":"2018-12-11T11:51:50Z","publisher":"Elsevier","scopus_import":"1","quality_controlled":"1","date_published":"2017-02-01T00:00:00Z","type":"journal_article","issue":"2","doi":"10.1016/j.nahs.2016.04.006","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publist_id":"5800","isi":1,"day":"01","status":"public","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."}],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"ec_funded":1,"date_updated":"2025-06-11T06:33:00Z","related_material":{"record":[{"status":"public","id":"1689","relation":"earlier_version"}]},"_id":"1407","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","intvolume":"        23","oa":1,"volume":23,"month":"02","external_id":{"isi":["000390637000014"],"arxiv":["1410.5387"]},"author":[{"last_name":"Svoreňová","full_name":"Svoreňová, Mária","first_name":"Mária"},{"full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Cěrná, Ivana","last_name":"Cěrná","first_name":"Ivana"},{"first_name":"Cǎlin","full_name":"Belta, Cǎlin","last_name":"Belta"}],"language":[{"iso":"eng"}],"publication":"Nonlinear Analysis: Hybrid Systems","publication_status":"published","citation":{"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.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 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,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>.","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.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>.","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. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23(2):230-253. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>"},"year":"2017","article_processing_charge":"No","oa_version":"Preprint","arxiv":1,"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407"}],"page":"230 - 253"},{"isi":1,"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"}],"status":"public","quality_controlled":"1","date_published":"2017-03-06T00:00:00Z","publisher":"Nature Publishing Group","date_created":"2018-12-11T11:46:53Z","scopus_import":"1","type":"journal_article","issue":"1","has_accepted_license":"1","department":[{"_id":"KrCh"}],"publist_id":"7307","file":[{"file_size":1536783,"file_id":"5357","access_level":"open_access","checksum":"7d05cbdd914e194a019c0f91fb64e9a8","file_name":"IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf","relation":"main_file","creator":"system","content_type":"application/pdf","date_updated":"2020-07-14T12:46:36Z","date_created":"2018-12-12T10:18:35Z"}],"doi":"10.1038/s41598-017-00107-w","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2045-2322"]},"file_date_updated":"2020-07-14T12:46:36Z","author":[{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","orcid":"0000-0002-1097-9684"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"publication_status":"published","article_number":"82","citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. 2017;7(1). doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>","mla":"Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>, vol. 7, no. 1, 82, Nature Publishing Group, 2017, doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification on undirected population structures: Comets beat stars,” <i>Scientific Reports</i>, vol. 7, no. 1. Nature Publishing Group, 2017.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports 7 (2017).","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2017). Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 7(1), 82."},"publication":"Scientific Reports","article_processing_charge":"No","year":"2017","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"}],"oa_version":"Published Version","corr_author":"1","ec_funded":1,"_id":"512","date_updated":"2025-09-18T09:50:10Z","related_material":{"record":[{"id":"5449","status":"public","relation":"earlier_version"}]},"ddc":["004"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"title":"Amplification on undirected population structures: Comets beat stars","intvolume":"         7","external_id":{"isi":["000396867800013"]},"oa":1,"month":"03","volume":7,"pubrep_id":"938"},{"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","doi":"10.15479/AT:IST-2017-870-v1-1","file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:46:59Z","date_created":"2018-12-12T11:54:02Z","access_level":"open_access","file_id":"5524","file_size":960491,"checksum":"177a84a46e3ac17e87b31534ad16a4c9","file_name":"IST-2017-870-v1+1_main.pdf","relation":"main_file","creator":"system"}],"has_accepted_license":"1","department":[{"_id":"KrCh"}],"date_created":"2018-12-12T11:39:26Z","publisher":"IST Austria","date_published":"2017-10-23T00:00:00Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"status":"public","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"}],"day":"23","title":"Optimal Dyck reachability for data-dependence and alias analysis","ddc":["000"],"pubrep_id":"870","month":"10","oa":1,"related_material":{"record":[{"relation":"later_version","status":"public","id":"10416"}]},"date_updated":"2025-04-15T08:12:18Z","_id":"5455","year":"2017","article_processing_charge":"No","oa_version":"Published Version","page":"37","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Choudhary","full_name":"Choudhary, Bhavya","first_name":"Bhavya"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"file_date_updated":"2020-07-14T12:46:59Z","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"citation":{"ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and alias analysis, IST Austria, 37p.","apa":"Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). <i>Optimal Dyck reachability for data-dependence and alias analysis</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for Data-Dependence and Alias Analysis, IST Austria, 2017.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, <i>Optimal Dyck reachability for data-dependence and alias analysis</i>. IST Austria, 2017.","mla":"Chatterjee, Krishnendu, et al. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">10.15479/AT:IST-2017-870-v1-1</a>.","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria; 2017. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">10.15479/AT:IST-2017-870-v1-1</a>","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria, 2017. <a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>."},"publication_status":"published"},{"date_published":"2017-10-23T00:00:00Z","publisher":"IST Austria","date_created":"2018-12-12T11:39:26Z","_id":"5456","type":"technical_report","related_material":{"record":[{"status":"public","id":"5448","relation":"earlier_version"},{"id":"10417","status":"public","relation":"later_version"}]},"date_updated":"2025-05-20T09:45:08Z","ddc":["000"],"title":"Data-centric dynamic partial order reduction","has_accepted_license":"1","department":[{"_id":"KrCh"}],"file":[{"relation":"main_file","creator":"system","checksum":"d2635c4cf013000f0a1b09e80f9e4ab7","file_name":"IST-2017-872-v1+1_main.pdf","access_level":"open_access","file_size":910347,"file_id":"5487","date_created":"2018-12-12T11:53:26Z","date_updated":"2020-07-14T12:46:59Z","content_type":"application/pdf"}],"doi":"10.15479/AT:IST-2017-872-v1-1","oa":1,"pubrep_id":"872","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"file_date_updated":"2020-07-14T12:46:59Z","author":[{"first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"full_name":"Sinha, Nishant","last_name":"Sinha","first_name":"Nishant"},{"full_name":"Vaidya, Kapil","last_name":"Vaidya","first_name":"Kapil"}],"publication_status":"published","citation":{"mla":"Chalupa, Marek, et al. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">10.15479/AT:IST-2017-872-v1-1</a>.","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria, 2017. <a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>.","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria; 2017. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">10.15479/AT:IST-2017-872-v1-1</a>","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., &#38; Vaidya, K. (2017). <i>Data-centric dynamic partial order reduction</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2017.","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, <i>Data-centric dynamic partial order reduction</i>. IST Austria, 2017."},"day":"23","year":"2017","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."}],"page":"36","status":"public","oa_version":"Published Version"},{"article_processing_charge":"No","conference":{"end_date":"2017-08-25","location":"Aalborg, Denmark","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science"},"year":"2017","oa_version":"Published Version","corr_author":"1","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-395977046-0"]},"file_date_updated":"2020-07-14T12:47:00Z","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"article_number":"61","publication_status":"published","citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>","mla":"Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","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.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Nowak, M. (2017). Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>"},"publication":"Leibniz International Proceedings in Informatics","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["004"],"title":"Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs","intvolume":"        83","oa":1,"month":"11","pubrep_id":"924","volume":83,"_id":"551","date_updated":"2025-07-10T11:52:51Z","alternative_title":["LIPIcs"],"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. "}],"status":"public","day":"01","department":[{"_id":"KrCh"}],"has_accepted_license":"1","file":[{"access_level":"open_access","file_size":535077,"file_id":"5322","relation":"main_file","creator":"system","checksum":"2eed5224c0e4e259484a1d71acb8ba6a","file_name":"IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf","date_updated":"2020-07-14T12:47:00Z","content_type":"application/pdf","date_created":"2018-12-12T10:18:04Z"}],"publist_id":"7263","doi":"10.4230/LIPIcs.MFCS.2017.61","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2017-11-01T00:00:00Z","quality_controlled":"1","date_created":"2018-12-11T11:47:08Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":"1","type":"conference"},{"date_updated":"2025-07-10T11:52:52Z","_id":"552","ec_funded":1,"pubrep_id":"923","month":"11","volume":83,"oa":1,"intvolume":"        83","title":"Faster algorithms for mean-payoff parity games","ddc":["004"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","short":"CC BY (3.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)"},"publication":"Leibniz International Proceedings in Informatics","citation":{"mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Mean-Payoff Parity Games.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 39, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">10.4230/LIPIcs.MFCS.2017.39</a>.","ama":"Chatterjee K, Henzinger M, Svozil A. Faster algorithms for mean-payoff parity games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">10.4230/LIPIcs.MFCS.2017.39</a>","chicago":"Chatterjee, Krishnendu, Monika Henzinger, and Alexander Svozil. “Faster Algorithms for Mean-Payoff Parity Games.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>.","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.","apa":"Chatterjee, K., Henzinger, M., &#38; Svozil, A. (2017). Faster algorithms for mean-payoff parity games. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>","short":"K. Chatterjee, M. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ieee":"K. Chatterjee, M. Henzinger, and A. Svozil, “Faster algorithms for mean-payoff parity games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83."},"article_number":"39","publication_status":"published","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H"},{"first_name":"Alexander","last_name":"Svozil","full_name":"Svozil, Alexander"}],"file_date_updated":"2020-07-14T12:47:00Z","publication_identifier":{"isbn":["978-395977046-0"]},"language":[{"iso":"eng"}],"oa_version":"Published Version","corr_author":"1","project":[{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"}],"year":"2017","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2017-08-21","location":"Aalborg, Denmark","end_date":"2017-08-25"},"article_processing_charge":"No","type":"conference","license":"https://creativecommons.org/licenses/by/3.0/","scopus_import":"1","date_created":"2018-12-11T11:47:08Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","date_published":"2017-11-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.4230/LIPIcs.MFCS.2017.39","publist_id":"7262","file":[{"file_name":"IST-2018-923-v1+1_LIPIcs-MFCS-2017-39.pdf","checksum":"c67f4866ddbfd555afef1f63ae9a8fc7","creator":"system","relation":"main_file","file_id":"5248","file_size":610339,"access_level":"open_access","date_created":"2018-12-12T10:16:57Z","content_type":"application/pdf","date_updated":"2020-07-14T12:47:00Z"}],"has_accepted_license":"1","department":[{"_id":"KrCh"}],"day":"01","status":"public","abstract":[{"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).","lang":"eng"}],"alternative_title":["LIPIcs"]},{"conference":{"name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2017-08-21","location":"Aalborg, Denmark","end_date":"2017-08-25"},"article_processing_charge":"No","year":"2017","corr_author":"1","arxiv":1,"oa_version":"Published Version","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-395977046-0"]},"file_date_updated":"2020-07-14T12:47:00Z","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hansen, Kristofer","last_name":"Hansen","first_name":"Kristofer"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389"}],"article_number":"55","publication_status":"published","citation":{"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.","apa":"Chatterjee, K., Hansen, K., &#38; Ibsen-Jensen, R. (2017). Strategy complexity of concurrent safety games. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>","ieee":"K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent safety games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","short":"K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","mla":"Chatterjee, Krishnendu, et al. “Strategy Complexity of Concurrent Safety Games.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 55, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>.","ama":"Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent safety games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>","chicago":"Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy Complexity of Concurrent Safety Games.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>."},"publication":"Leibniz International Proceedings in Informatics","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["004"],"title":"Strategy complexity of concurrent safety games","intvolume":"        83","external_id":{"arxiv":["1506.02434"]},"oa":1,"volume":83,"month":"11","pubrep_id":"922","_id":"553","date_updated":"2025-06-04T09:37:06Z","alternative_title":["LIPIcs"],"abstract":[{"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. ","lang":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/1506.02434","open_access":"1"}],"status":"public","day":"01","has_accepted_license":"1","department":[{"_id":"KrCh"}],"file":[{"file_id":"4753","file_size":549967,"access_level":"open_access","checksum":"7101facb56ade363205c695d72dbd173","file_name":"IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf","relation":"main_file","creator":"system","content_type":"application/pdf","date_updated":"2020-07-14T12:47:00Z","date_created":"2018-12-12T10:09:29Z"}],"publist_id":"7261","doi":"10.4230/LIPIcs.MFCS.2017.55","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2017-11-01T00:00:00Z","quality_controlled":"1","date_created":"2018-12-11T11:47:08Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":"1","type":"conference"},{"date_published":"2017-01-02T00:00:00Z","ec_funded":1,"publisher":"Institute of Science and Technology Austria","date_created":"2018-12-12T12:31:32Z","_id":"5559","date_updated":"2025-04-15T08:12:19Z","related_material":{"record":[{"relation":"research_paper","status":"public","id":"5452"},{"relation":"research_paper","id":"5751","status":"public"}]},"type":"research_data","ddc":["519"],"title":"Strong amplifiers of natural selection","file":[{"content_type":"video/mp4","date_updated":"2020-07-14T12:47:02Z","date_created":"2018-12-12T13:05:18Z","access_level":"open_access","file_id":"5644","file_size":32987015,"file_name":"IST-2017-51-v1+2_illustration.mp4","checksum":"b427dd46a30096a1911b245640c47af8","relation":"main_file","creator":"system"}],"has_accepted_license":"1","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","oa":1,"doi":"10.15479/AT:ISTA:51","author":[{"full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Tkadlec, Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","last_name":"Nowak ","full_name":"Nowak , Martin"}],"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. <a href=\"https://doi.org/10.15479/AT:ISTA:51\">https://doi.org/10.15479/AT:ISTA:51</a>.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak  M. Strong amplifiers of natural selection. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>","mla":"Pavlogiannis, Andreas, et al. <i>Strong Amplifiers of Natural Selection</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak , “Strong amplifiers of natural selection.” Institute of Science and Technology Austria, 2017.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak , (2017).","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak , M. (2017). Strong amplifiers of natural selection. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:51\">https://doi.org/10.15479/AT:ISTA:51</a>","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak  M. 2017. Strong amplifiers of natural selection, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>."},"day":"02","keyword":["natural selection"],"datarep_id":"51","article_processing_charge":"No","year":"2017","abstract":[{"text":"Strong amplifiers of natural selection","lang":"eng"}],"project":[{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","status":"public"},{"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-3-319-63120-2"],"issn":["0302-9743"]},"file_date_updated":"2020-07-14T12:47:25Z","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"publication_status":"published","citation":{"ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in <i>Models, Algorithms, Logics and Tools</i>, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017, pp. 367–381.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2017.The cost of exactness in quantitative reachability. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, 367–381.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, &#38; R. Mardare (Eds.), <i>Models, Algorithms, Logics and Tools</i> (Vol. 10460, pp. 367–381). Springer. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost of Exactness in Quantitative Reachability.” In <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto, Giorgio Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare, 10460:367–81. Theoretical Computer Science and General Issues. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>.","ama":"Chatterjee K, Doyen L, Henzinger TA. The cost of exactness in quantitative reachability. In: Aceto L, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, eds. <i>Models, Algorithms, Logics and Tools</i>. Vol 10460. Theoretical Computer Science and General Issues. Springer; 2017:367-381. doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>","mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>."},"publication":"Models, Algorithms, Logics and Tools","article_processing_charge":"No","year":"2017","project":[{"call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"page":"367 - 381","oa_version":"Submitted Version","ec_funded":1,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 and S11407-N23 (RiSE/SHiNE), and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003.","_id":"625","date_updated":"2025-04-15T06:26:15Z","ddc":["000"],"title":"The cost of exactness in quantitative reachability","intvolume":"     10460","oa":1,"volume":10460,"month":"07","day":"25","alternative_title":["LNCS"],"abstract":[{"text":"In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the computational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.","lang":"eng"}],"status":"public","quality_controlled":"1","date_published":"2017-07-25T00:00:00Z","date_created":"2018-12-11T11:47:34Z","publisher":"Springer","series_title":"Theoretical Computer Science and General Issues","scopus_import":"1","type":"book_chapter","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"has_accepted_license":"1","file":[{"relation":"main_file","creator":"dernst","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","checksum":"b2402766ec02c79801aac634bd8f9f6c","file_size":192826,"file_id":"7048","access_level":"open_access","date_created":"2019-11-19T08:06:50Z","date_updated":"2020-07-14T12:47:25Z","content_type":"application/pdf"}],"publist_id":"7170","doi":"10.1007/978-3-319-63121-9_18","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","editor":[{"first_name":"Luca","last_name":"Aceto","full_name":"Aceto, Luca"},{"first_name":"Giorgio","last_name":"Bacci","full_name":"Bacci, Giorgio"},{"last_name":"Ingólfsdóttir","full_name":"Ingólfsdóttir, Anna","first_name":"Anna"},{"first_name":"Axel","full_name":"Legay, Axel","last_name":"Legay"},{"first_name":"Radu","last_name":"Mardare","full_name":"Mardare, Radu"}]},{"_id":"628","date_updated":"2025-09-11T07:28:26Z","ec_funded":1,"external_id":{"isi":["000432196400006"],"arxiv":["1705.00314"]},"oa":1,"volume":10426,"month":"01","title":"Automated recurrence analysis for almost linear expected runtime bounds","intvolume":"     10426","publication_status":"published","citation":{"chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Aniket Murhekar. “Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds.” edited by Rupak Majumdar and Viktor Kunčak, 10426:118–39. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">https://doi.org/10.1007/978-3-319-63387-9_6</a>.","ama":"Chatterjee K, Fu H, Murhekar A. Automated recurrence analysis for almost linear expected runtime bounds. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:118-139. doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">10.1007/978-3-319-63387-9_6</a>","mla":"Chatterjee, Krishnendu, et al. <i>Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 118–39, doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">10.1007/978-3-319-63387-9_6</a>.","ieee":"K. Chatterjee, H. Fu, and A. Murhekar, “Automated recurrence analysis for almost linear expected runtime bounds,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 118–139.","short":"K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 118–139.","ista":"Chatterjee K, Fu H, Murhekar A. 2017. Automated recurrence analysis for almost linear expected runtime bounds. CAV: Computer Aided Verification, LNCS, vol. 10426, 118–139.","apa":"Chatterjee, K., Fu, H., &#38; Murhekar, A. (2017). Automated recurrence analysis for almost linear expected runtime bounds. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10426, pp. 118–139). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">https://doi.org/10.1007/978-3-319-63387-9_6</a>"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-331963386-2"]},"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Fu","full_name":"Fu, Hongfei","first_name":"Hongfei"},{"first_name":"Aniket","last_name":"Murhekar","full_name":"Murhekar, Aniket"}],"project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"}],"page":"118 - 139","oa_version":"Submitted Version","arxiv":1,"conference":{"start_date":"2017-07-24","name":"CAV: Computer Aided Verification","end_date":"2017-07-28","location":"Heidelberg, Germany"},"article_processing_charge":"No","year":"2017","type":"conference","date_published":"2017-01-01T00:00:00Z","quality_controlled":"1","date_created":"2018-12-11T11:47:35Z","publisher":"Springer","scopus_import":"1","department":[{"_id":"KrCh"}],"publist_id":"7166","doi":"10.1007/978-3-319-63387-9_6","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","editor":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"first_name":"Viktor","last_name":"Kunčak","full_name":"Kunčak, Viktor"}],"day":"01","isi":1,"main_file_link":[{"url":"https://arxiv.org/abs/1705.00314","open_access":"1"}],"abstract":[{"text":"We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. The motivation is that several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear or almost-linear (O(log n), O(n), O(n · log n), respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. The experimental results show that our approach can efficiently derive asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select, Coupon-Collector, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic expected-runtime complexity, or quadratic as compared to linear or almost-linear expected-runtime complexity), or ineffective.","lang":"eng"}],"status":"public","alternative_title":["LNCS"]},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"6387","department":[{"_id":"KrCh"}],"type":"conference","scopus_import":"1","date_created":"2018-12-11T11:49:40Z","publisher":"AAAI Press","quality_controlled":"1","date_published":"2017-01-01T00:00:00Z","status":"public","abstract":[{"text":"A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the “expectation” and “threshold” approaches and consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we are given a threshold t and the objective is to find a policy σ such that a) each possible outcome of σ yields a discounted-sum payoff of at least t, and b) the expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks.","lang":"eng"}],"main_file_link":[{"url":"http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092","open_access":"1"}],"day":"01","isi":1,"month":"01","volume":5,"oa":1,"external_id":{"isi":["000485630703107"]},"intvolume":"         5","title":"Optimizing expectation with guarantees in POMDPs","date_updated":"2025-04-14T13:51:03Z","_id":"1009","acknowledgement":"he research leading to these results was supported by the Austrian Science Fund (FWF) NFN Grant no. S11407-N23 (RiSE/SHiNE); two ERC Starting grants (279307: Graph Games, 279499: inVEST); the Vienna Science and Tech- nology Fund (WWTF) through project ICT15-003; and the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. [291734].","ec_funded":1,"oa_version":"Submitted Version","project":[{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"page":"3725 - 3732","year":"2017","article_processing_charge":"No","conference":{"start_date":"2017-02-04","name":"AAAI: Conference on Artificial Intelligence","end_date":"2017-02-10","location":"San Francisco, CA, United States"},"publication":"Proceedings of the 31st AAAI Conference on Artificial Intelligence","citation":{"apa":"Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., &#38; Zikelic, D. (2017). Optimizing expectation with guarantees in POMDPs. In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i> (Vol. 5, pp. 3725–3732). San Francisco, CA, United States: AAAI Press.","ista":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. 2017. Optimizing expectation with guarantees in POMDPs. Proceedings of the 31st AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 5, 3725–3732.","short":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, D. Zikelic, in:, Proceedings of the 31st AAAI Conference on Artificial Intelligence, AAAI Press, 2017, pp. 3725–3732.","ieee":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing expectation with guarantees in POMDPs,” in <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, San Francisco, CA, United States, 2017, vol. 5, pp. 3725–3732.","mla":"Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.” <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, vol. 5, AAAI Press, 2017, pp. 3725–32.","chicago":"Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, 5:3725–32. AAAI Press, 2017.","ama":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation with guarantees in POMDPs. In: <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>. Vol 5. AAAI Press; 2017:3725-3732."},"publication_status":"published","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Guillermo","full_name":"Pérez, Guillermo","last_name":"Pérez"},{"first_name":"Jean","last_name":"Raskin","full_name":"Raskin, Jean"},{"first_name":"Djordje","last_name":"Zikelic","full_name":"Zikelic, Djordje"}],"language":[{"iso":"eng"}]},{"date_created":"2018-12-11T11:49:41Z","publisher":"Springer","scopus_import":"1","quality_controlled":"1","date_published":"2017-03-19T00:00:00Z","type":"conference","doi":"10.1007/978-3-662-54434-1_11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","editor":[{"first_name":"Hongseok","last_name":"Yang","full_name":"Yang, Hongseok"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publist_id":"6384","isi":1,"day":"19","alternative_title":["LNCS"],"status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.04914"}],"abstract":[{"text":"Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.","lang":"eng"}],"ec_funded":1,"date_updated":"2025-06-04T08:09:18Z","_id":"1011","title":"Faster algorithms for weighted recursive state machines","intvolume":"     10201","oa":1,"volume":10201,"month":"03","external_id":{"arxiv":["1701.04914"],"isi":["000681702400011"]},"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kragl, Bernhard","last_name":"Kragl","orcid":"0000-0001-7745-9117","first_name":"Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Samarth","full_name":"Mishra, Samarth","last_name":"Mishra"},{"full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"]},"publication_status":"published","citation":{"ieee":"K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms for weighted recursive state machines,” presented at the ESOP: European Symposium on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","apa":"Chatterjee, K., Kragl, B., Mishra, S., &#38; Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>","chicago":"Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis. “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok Yang, 10201:287–313. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>.","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Weighted Recursive State Machines</i>. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>."},"year":"2017","conference":{"location":"Uppsala, Sweden","end_date":"2017-04-29","name":"ESOP: European Symposium on Programming","start_date":"2017-04-22"},"article_processing_charge":"No","arxiv":1,"oa_version":"Submitted Version","page":"287 - 313","project":[{"call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"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 Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"}]}]