[{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"311","ddc":["000"],"title":"Quantitative analysis of smart contracts","status":"public","intvolume":" 10801","oa_version":"Published Version","file":[{"file_size":1394993,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2018_ESOP_Chatterjee.pdf","checksum":"9c8a8338c571903b599b6ca93abd2cce","date_created":"2018-12-17T15:45:49Z","date_updated":"2020-07-14T12:46:00Z","relation":"main_file","file_id":"5716"}],"type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts.","lang":"eng"}],"citation":{"ama":"Chatterjee K, Goharshady AK, Velner Y. Quantitative analysis of smart contracts. In: Vol 10801. Springer; 2018:739-767. doi:10.1007/978-3-319-89884-1_26","ista":"Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 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.","apa":"Chatterjee, K., Goharshady, A. K., & Velner, Y. (2018). Quantitative analysis of smart contracts (Vol. 10801, pp. 739–767). Presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89884-1_26","mla":"Chatterjee, Krishnendu, et al. Quantitative Analysis of Smart Contracts. Vol. 10801, Springer, 2018, pp. 739–67, doi:10.1007/978-3-319-89884-1_26.","short":"K. Chatterjee, A.K. Goharshady, Y. Velner, in:, Springer, 2018, pp. 739–767.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Yaron Velner. “Quantitative Analysis of Smart Contracts,” 10801:739–67. Springer, 2018. https://doi.org/10.1007/978-3-319-89884-1_26."},"page":"739 - 767","date_published":"2018-04-01T00:00:00Z","scopus_import":"1","day":"01","article_processing_charge":"No","has_accepted_license":"1","year":"2018","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).","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"Springer","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Goharshady, Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"date_created":"2018-12-11T11:45:45Z","date_updated":"2024-03-28T23:30:33Z","volume":10801,"file_date_updated":"2020-07-14T12:46:00Z","ec_funded":1,"publist_id":"7554","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"quality_controlled":"1","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"conference":{"name":"ESOP: European Symposium on Programming","start_date":"2018-04-16","location":"Thessaloniki, Greece","end_date":"2018-04-19"},"doi":"10.1007/978-3-319-89884-1_26","language":[{"iso":"eng"}],"month":"04"},{"language":[{"iso":"eng"}],"doi":"10.1109/Cybermatics_2018.2018.00231","conference":{"location":"Halifax, Canada","start_date":"2018-07-30","end_date":"2018-08-03","name":"IEEE International Conference on Blockchain"},"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"quality_controlled":"1","isi":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"oa":1,"external_id":{"isi":["000481634500196"],"arxiv":["1805.09104"]},"publication_identifier":{"isbn":["978-1-5386-7975-3 "]},"month":"09","date_created":"2019-04-18T10:37:35Z","date_updated":"2024-03-28T23:30:34Z","related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"author":[{"first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"},{"first_name":"Ali","last_name":"Behrouz","full_name":"Behrouz, Ali"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"}],"publisher":"IEEE","department":[{"_id":"KrCh"}],"publication_status":"published","year":"2018","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","ec_funded":1,"file_date_updated":"2020-07-14T12:47:27Z","date_published":"2018-09-01T00:00:00Z","page":"1343-1348","citation":{"mla":"Goharshady, Amir Kafshdar, et al. “Secure Credit Reporting on the Blockchain.” Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–48, doi:10.1109/Cybermatics_2018.2018.00231.","short":"A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–1348.","chicago":"Goharshady, Amir Kafshdar, Ali Behrouz, and Krishnendu Chatterjee. “Secure Credit Reporting on the Blockchain.” In Proceedings of the IEEE International Conference on Blockchain, 1343–48. IEEE, 2018. https://doi.org/10.1109/Cybermatics_2018.2018.00231.","ama":"Goharshady AK, Behrouz A, Chatterjee K. Secure Credit Reporting on the Blockchain. In: Proceedings of the IEEE International Conference on Blockchain. IEEE; 2018:1343-1348. doi:10.1109/Cybermatics_2018.2018.00231","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.","ieee":"A. K. Goharshady, A. Behrouz, and K. Chatterjee, “Secure Credit Reporting on the Blockchain,” in Proceedings of the IEEE International Conference on Blockchain, Halifax, Canada, 2018, pp. 1343–1348.","apa":"Goharshady, A. K., Behrouz, A., & Chatterjee, K. (2018). Secure Credit Reporting on the Blockchain. In Proceedings of the IEEE International Conference on Blockchain (pp. 1343–1348). Halifax, Canada: IEEE. https://doi.org/10.1109/Cybermatics_2018.2018.00231"},"publication":"Proceedings of the IEEE International Conference on Blockchain","has_accepted_license":"1","article_processing_charge":"No","day":"01","scopus_import":"1","file":[{"access_level":"open_access","file_name":"blockchain2018.pdf","file_size":624338,"content_type":"application/pdf","creator":"akafshda","relation":"main_file","file_id":"6341","checksum":"b25c9bb7cf6e7e6634e692d26d41ead8","date_updated":"2020-07-14T12:47:27Z","date_created":"2019-04-18T10:36:39Z"}],"oa_version":"Submitted Version","ddc":["000"],"title":"Secure Credit Reporting on the Blockchain","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"6340","abstract":[{"text":"We present a secure approach for maintaining andreporting credit history records on the Blockchain. Our ap-proach removes third-parties such as credit reporting agen-cies from the lending process and replaces them with smartcontracts. This allows customers to interact directly with thelenders or banks while ensuring the integrity, unmalleabilityand privacy of their credit data. Additionally, each customerhas full control over complete or selective disclosure of hercredit records, eliminating the risk of privacy violations or databreaches. Moreover, our approach provides strong guaranteesfor the lenders as well. A lender can check both correctness andcompleteness of the credit data disclosed to her. This is the firstapproach that can perform all credit reporting tasks withouta central authority or changing the financial mechanisms*.","lang":"eng"}],"type":"conference"},{"month":"08","publication_identifier":{"issn":["0164-0925"]},"quality_controlled":"1","isi":1,"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"main_file_link":[{"url":"https://arxiv.org/abs/1510.07565","open_access":"1"}],"external_id":{"isi":["000444694800001"],"arxiv":["1510.07565"]},"oa":1,"language":[{"iso":"eng"}],"doi":"10.1145/3210257","article_number":"9","ec_funded":1,"publication_status":"published","publisher":"Association for Computing Machinery (ACM)","department":[{"_id":"KrCh"}],"year":"2018","date_created":"2019-02-14T14:31:52Z","date_updated":"2024-03-28T23:30:34Z","volume":40,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis"}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1437"},{"status":"public","relation":"earlier_version","id":"5441"},{"id":"5442","status":"public","relation":"earlier_version"},{"id":"8934","relation":"dissertation_contains","status":"public"}]},"scopus_import":"1","day":"01","article_processing_charge":"No","publication":"ACM Transactions on Programming Languages and Systems","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 40(3), 9.","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” ACM Transactions on Programming Languages and Systems, vol. 40, no. 3. Association for Computing Machinery (ACM), 2018.","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A. (2018). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM). https://doi.org/10.1145/3210257","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 2018;40(3). doi:10.1145/3210257","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3210257.","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” ACM Transactions on Programming Languages and Systems, vol. 40, no. 3, 9, Association for Computing Machinery (ACM), 2018, doi:10.1145/3210257.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018)."},"date_published":"2018-08-01T00:00:00Z","type":"journal_article","abstract":[{"lang":"eng","text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n"}],"issue":"3","status":"public","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","intvolume":" 40","_id":"6009","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Preprint"},{"day":"17","article_processing_charge":"No","scopus_import":"1","date_published":"2018-07-17T00:00:00Z","publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","citation":{"ama":"Chatterjee K, Fu H, Goharshady AK, Okati N. Computational approaches for stochastic shortest path on succinct MDPs. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. Vol 2018. IJCAI; 2018:4700-4707. doi:10.24963/ijcai.2018/653","ista":"Chatterjee K, Fu H, Goharshady AK, Okati N. 2018. Computational approaches for stochastic shortest path on succinct MDPs. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4700–4707.","ieee":"K. Chatterjee, H. Fu, A. K. Goharshady, and N. Okati, “Computational approaches for stochastic shortest path on succinct MDPs,” in Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018, pp. 4700–4707.","apa":"Chatterjee, K., Fu, H., Goharshady, A. K., & Okati, N. (2018). Computational approaches for stochastic shortest path on succinct MDPs. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (Vol. 2018, pp. 4700–4707). Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/653","mla":"Chatterjee, Krishnendu, et al. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, vol. 2018, IJCAI, 2018, pp. 4700–07, doi:10.24963/ijcai.2018/653.","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.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran Okati. “Computational Approaches for Stochastic Shortest Path on Succinct MDPs.” In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018:4700–4707. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/653."},"page":"4700-4707","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."}],"type":"conference","oa_version":"Preprint","_id":"5977","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"Computational approaches for stochastic shortest path on succinct MDPs","status":"public","intvolume":" 2018","month":"07","publication_identifier":{"issn":["10450823"],"isbn":["978-099924112-7"]},"conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence","end_date":"2018-07-19","start_date":"2018-07-13","location":"Stockholm, Sweden"},"doi":"10.24963/ijcai.2018/653","language":[{"iso":"eng"}],"external_id":{"arxiv":["1804.08984"],"isi":["000764175404118"]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.08984"}],"oa":1,"isi":1,"quality_controlled":"1","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Fu","first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei"},{"last_name":"Goharshady","first_name":"Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir"},{"full_name":"Okati, Nastaran","first_name":"Nastaran","last_name":"Okati"}],"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"date_created":"2019-02-13T13:26:27Z","date_updated":"2024-03-28T23:30:34Z","volume":2018,"year":"2018","publication_status":"published","publisher":"IJCAI","department":[{"_id":"KrCh"}]},{"oa_version":"Submitted Version","intvolume":" 115","title":"Indirect reciprocity with private, noisy, and incomplete information","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"2","issue":"48","abstract":[{"text":"Indirect reciprocity explores how humans act when their reputation is at stake, and which social norms they use to assess the actions of others. A crucial question in indirect reciprocity is which social norms can maintain stable cooperation in a society. Past research has highlighted eight such norms, called “leading-eight” strategies. This past research, however, is based on the assumption that all relevant information about other population members is publicly available and that everyone agrees on who is good or bad. Instead, here we explore the reputation dynamics when information is private and noisy. We show that under these conditions, most leading-eight strategies fail to evolve. Those leading-eight strategies that do evolve are unable to sustain full cooperation.Indirect reciprocity is a mechanism for cooperation based on shared moral systems and individual reputations. It assumes that members of a community routinely observe and assess each other and that they use this information to decide who is good or bad, and who deserves cooperation. When information is transmitted publicly, such that all community members agree on each other’s reputation, previous research has highlighted eight crucial moral systems. These “leading-eight” strategies can maintain cooperation and resist invasion by defectors. However, in real populations individuals often hold their own private views of others. Once two individuals disagree about their opinion of some third party, they may also see its subsequent actions in a different light. Their opinions may further diverge over time. Herein, we explore indirect reciprocity when information transmission is private and noisy. We find that in the presence of perception errors, most leading-eight strategies cease to be stable. Even if a leading-eight strategy evolves, cooperation rates may drop considerably when errors are common. Our research highlights the role of reliable information and synchronized reputations to maintain stable moral systems.","lang":"eng"}],"type":"journal_article","date_published":"2018-11-27T00:00:00Z","page":"12241-12246","citation":{"ama":"Hilbe C, Schmid L, Tkadlec J, Chatterjee K, Nowak M. Indirect reciprocity with private, noisy, and incomplete information. PNAS. 2018;115(48):12241-12246. doi:10.1073/pnas.1810565115","ista":"Hilbe C, Schmid L, Tkadlec J, Chatterjee K, Nowak M. 2018. Indirect reciprocity with private, noisy, and incomplete information. PNAS. 115(48), 12241–12246.","apa":"Hilbe, C., Schmid, L., Tkadlec, J., Chatterjee, K., & Nowak, M. (2018). Indirect reciprocity with private, noisy, and incomplete information. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.1810565115","ieee":"C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, and M. Nowak, “Indirect reciprocity with private, noisy, and incomplete information,” PNAS, vol. 115, no. 48. National Academy of Sciences, pp. 12241–12246, 2018.","mla":"Hilbe, Christian, et al. “Indirect Reciprocity with Private, Noisy, and Incomplete Information.” PNAS, vol. 115, no. 48, National Academy of Sciences, 2018, pp. 12241–46, doi:10.1073/pnas.1810565115.","short":"C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, M. Nowak, PNAS 115 (2018) 12241–12246.","chicago":"Hilbe, Christian, Laura Schmid, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Indirect Reciprocity with Private, Noisy, and Incomplete Information.” PNAS. National Academy of Sciences, 2018. https://doi.org/10.1073/pnas.1810565115."},"publication":"PNAS","article_processing_charge":"No","day":"27","scopus_import":"1","volume":115,"date_created":"2018-12-11T11:44:05Z","date_updated":"2024-03-28T23:30:45Z","related_material":{"link":[{"relation":"press_release","description":"News on IST Homepage","url":"https://ist.ac.at/en/news/no-cooperation-without-open-communication/"}],"record":[{"status":"public","relation":"dissertation_contains","id":"10293"}]},"author":[{"full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X"},{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6978-7329","first_name":"Laura","last_name":"Schmid","full_name":"Schmid, Laura"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef","last_name":"Tkadlec"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"department":[{"_id":"KrCh"}],"publisher":"National Academy of Sciences","publication_status":"published","pmid":1,"year":"2018","ec_funded":1,"language":[{"iso":"eng"}],"doi":"10.1073/pnas.1810565115","project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"isi":1,"quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pubmed/30429320"}],"oa":1,"external_id":{"pmid":["30429320"],"isi":["000451351000063"]},"month":"11"},{"article_processing_charge":"No","day":"07","scopus_import":"1","date_published":"2017-12-07T00:00:00Z","article_type":"original","citation":{"chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121.","mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:10.1145/3158121.","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.","apa":"Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158121","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158121"},"publication":"Proceedings of the ACM on Programming Languages","issue":"POPL","abstract":[{"text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.","lang":"eng"}],"type":"journal_article","oa_version":"Published Version","intvolume":" 2","title":"A new proof rule for almost-sure termination","status":"public","_id":"10418","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication_identifier":{"eissn":["2475-1421"]},"month":"12","language":[{"iso":"eng"}],"doi":"10.1145/3158121","conference":{"name":"POPL: Programming Languages","end_date":"2018-01-13","location":"Los Angeles, CA, United States","start_date":"2018-01-07"},"quality_controlled":"1","external_id":{"arxiv":["1711.03588"]},"main_file_link":[{"open_access":"1","url":"https://dl.acm.org/doi/10.1145/3158121"}],"oa":1,"article_number":"33","volume":2,"date_created":"2021-12-05T23:01:49Z","date_updated":"2021-12-07T08:04:14Z","author":[{"last_name":"Mciver","first_name":"Annabelle","full_name":"Mciver, Annabelle"},{"last_name":"Morgan","first_name":"Carroll","full_name":"Morgan, Carroll"},{"last_name":"Kaminski","first_name":"Benjamin Lucien","full_name":"Kaminski, Benjamin Lucien"},{"first_name":"Joost P","last_name":"Katoen","id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P"}],"publisher":"Association for Computing Machinery","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","year":"2017"},{"publication_identifier":{"issn":["1860-5974"]},"month":"09","doi":"10.23638/LMCS-13(3:26)2017","language":[{"iso":"eng"}],"external_id":{"arxiv":["1410.0833"]},"tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"oa":1,"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"quality_controlled":"1","publist_id":"7357","ec_funded":1,"file_date_updated":"2020-07-14T12:46:32Z","license":"https://creativecommons.org/licenses/by-nd/4.0/","article_number":"26","related_material":{"record":[{"id":"1661","relation":"earlier_version","status":"public"}]},"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","first_name":"Monika H"},{"full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer","first_name":"Veronika"}],"volume":13,"date_created":"2018-12-11T11:46:37Z","date_updated":"2023-02-23T10:08:55Z","year":"2017","department":[{"_id":"KrCh"}],"publisher":"International Federation of Computational Logic","publication_status":"published","has_accepted_license":"1","article_processing_charge":"No","day":"26","scopus_import":"1","date_published":"2017-09-26T00:00:00Z","citation":{"ista":"Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.","apa":"Chatterjee, K., Henzinger, M. H., & Loitzenbauer, V. (2017). Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:26)2017","ieee":"K. Chatterjee, M. H. Henzinger, and V. Loitzenbauer, “Improved algorithms for parity and Streett objectives,” Logical Methods in Computer Science, vol. 13, no. 3. International Federation of Computational Logic, 2017.","ama":"Chatterjee K, Henzinger MH, Loitzenbauer V. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:26)2017","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for Parity and Streett Objectives.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:26)2017.","mla":"Chatterjee, Krishnendu, et al. “Improved Algorithms for Parity and Streett Objectives.” Logical Methods in Computer Science, vol. 13, no. 3, 26, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:26)2017.","short":"K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, Logical Methods in Computer Science 13 (2017)."},"publication":"Logical Methods in Computer Science","issue":"3","abstract":[{"lang":"eng","text":"The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs in time O(n2+nklogn). For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years."}],"type":"journal_article","pubrep_id":"956","file":[{"relation":"main_file","file_id":"5010","checksum":"12d469ae69b80361333d7dead965cf5d","date_updated":"2020-07-14T12:46:32Z","date_created":"2018-12-12T10:13:27Z","access_level":"open_access","file_name":"IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf","content_type":"application/pdf","file_size":582940,"creator":"system"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"464","intvolume":" 13","status":"public","ddc":["004"],"title":"Improved algorithms for parity and Streett objectives"},{"pubrep_id":"957","oa_version":"Published Version","file":[{"file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":511832,"file_id":"5354","relation":"main_file","date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:18:32Z","checksum":"bfa405385ec6229ad5ead89ab5751639"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"466","intvolume":" 13","ddc":["004"],"status":"public","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","issue":"2","abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. ","lang":"eng"}],"type":"journal_article","date_published":"2017-07-03T00:00:00Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science, vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(2:15)2017.","short":"K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017).","chicago":"Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(2:15)2017.","ama":"Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 2017;13(2). doi:10.23638/LMCS-13(2:15)2017","ista":"Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15.","apa":"Chatterjee, K., Křetínská, Z., & Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(2:15)2017","ieee":"K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” Logical Methods in Computer Science, vol. 13, no. 2. International Federation of Computational Logic, 2017."},"publication":"Logical Methods in Computer Science","has_accepted_license":"1","day":"03","scopus_import":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1657"},{"id":"5429","status":"public","relation":"earlier_version"},{"relation":"earlier_version","status":"public","id":"5435"}]},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Křetínská, Zuzana","last_name":"Křetínská","first_name":"Zuzana"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan"}],"volume":13,"date_updated":"2023-02-23T12:26:16Z","date_created":"2018-12-11T11:46:38Z","year":"2017","publisher":"International Federation of Computational Logic","department":[{"_id":"KrCh"}],"publication_status":"published","publist_id":"7355","ec_funded":1,"file_date_updated":"2020-07-14T12:46:33Z","article_number":"15","doi":"10.23638/LMCS-13(2:15)2017","language":[{"iso":"eng"}],"oa":1,"tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"project":[{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2590DB08-B435-11E9-9278-68D0E5697425","grant_number":"701309","name":"Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020)","call_identifier":"H2020"}],"quality_controlled":"1","publication_identifier":{"issn":["18605974"]},"month":"07"},{"month":"12","publication_identifier":{"issn":["15293785"]},"language":[{"iso":"eng"}],"doi":"10.1145/3152769","quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"external_id":{"arxiv":["1606.03598"]},"oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}],"ec_funded":1,"publist_id":"7354","article_number":"31","date_created":"2018-12-11T11:46:38Z","date_updated":"2023-02-23T12:26:19Z","volume":18,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1656"},{"id":"5415","status":"public","relation":"earlier_version"},{"id":"5436","status":"public","relation":"earlier_version"}]},"publication_status":"published","publisher":"ACM","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2017","day":"01","scopus_import":1,"date_published":"2017-12-01T00:00:00Z","publication":"ACM Transactions on Computational Logic (TOCL)","citation":{"ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 2017;18(4). doi:10.1145/3152769","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 18(4), 31.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 4. ACM, 2017.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2017). Nested weighted automata. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3152769","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 4, 31, ACM, 2017, doi:10.1145/3152769.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” ACM Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3152769."},"abstract":[{"text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.","lang":"eng"}],"issue":"4","type":"journal_article","oa_version":"Preprint","status":"public","title":"Nested weighted automata","intvolume":" 18","_id":"467","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"type":"journal_article","abstract":[{"lang":"eng","text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. "}],"issue":"3","ddc":["004"],"status":"public","title":"Edit distance for pushdown automata","intvolume":" 13","_id":"465","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","file":[{"file_name":"IST-2015-321-v1+1_main.pdf","access_level":"open_access","creator":"system","file_size":279071,"content_type":"application/pdf","file_id":"5090","relation":"main_file","date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:14:37Z","checksum":"08041379ba408d40664f449eb5907a8f"},{"checksum":"08041379ba408d40664f449eb5907a8f","date_created":"2018-12-12T10:14:38Z","date_updated":"2020-07-14T12:46:33Z","file_id":"5091","relation":"main_file","creator":"system","file_size":279071,"content_type":"application/pdf","access_level":"open_access","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf"}],"pubrep_id":"955","scopus_import":1,"day":"13","has_accepted_license":"1","publication":"Logical Methods in Computer Science","citation":{"mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:23)2017.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:23)2017.","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:23)2017","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2017). Edit distance for pushdown automata. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:23)2017","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” Logical Methods in Computer Science, vol. 13, no. 3. International Federation of Computational Logic, 2017."},"date_published":"2017-09-13T00:00:00Z","file_date_updated":"2020-07-14T12:46:33Z","publist_id":"7356","ec_funded":1,"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"International Federation of Computational Logic","year":"2017","date_created":"2018-12-11T11:46:37Z","date_updated":"2023-02-23T12:26:25Z","volume":13,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"related_material":{"record":[{"id":"1610","status":"public","relation":"earlier_version"},{"id":"5438","status":"public","relation":"earlier_version"}]},"month":"09","publication_identifier":{"issn":["18605974"]},"quality_controlled":"1","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.23638/LMCS-13(3:23)2017"},{"month":"03","publication_identifier":{"issn":["20452322"]},"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"doi":"10.1038/s41598-017-00107-w","article_number":"82","file_date_updated":"2020-07-14T12:46:36Z","ec_funded":1,"publist_id":"7307","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"Nature Publishing Group","year":"2017","date_updated":"2023-02-23T12:26:57Z","date_created":"2018-12-11T11:46:53Z","volume":7,"author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"first_name":"Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5449"}]},"scopus_import":1,"day":"06","article_processing_charge":"No","has_accepted_license":"1","publication":"Scientific Reports","citation":{"short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports 7 (2017).","mla":"Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures: Comets Beat Stars.” Scientific Reports, vol. 7, no. 1, 82, Nature Publishing Group, 2017, doi:10.1038/s41598-017-00107-w.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.” Scientific Reports. Nature Publishing Group, 2017. https://doi.org/10.1038/s41598-017-00107-w.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 2017;7(1). doi:10.1038/s41598-017-00107-w","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification on undirected population structures: Comets beat stars,” Scientific Reports, vol. 7, no. 1. Nature Publishing Group, 2017.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2017). Amplification on undirected population structures: Comets beat stars. Scientific Reports. Nature Publishing Group. https://doi.org/10.1038/s41598-017-00107-w","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 7(1), 82."},"date_published":"2017-03-06T00:00:00Z","type":"journal_article","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"}],"issue":"1","ddc":["004"],"title":"Amplification on undirected population structures: Comets beat stars","status":"public","intvolume":" 7","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"512","oa_version":"Published Version","file":[{"file_name":"IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":1536783,"file_id":"5357","relation":"main_file","date_updated":"2020-07-14T12:46:36Z","date_created":"2018-12-12T10:18:35Z","checksum":"7d05cbdd914e194a019c0f91fb64e9a8"}],"pubrep_id":"938"},{"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5455"}]},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Bhavya","last_name":"Choudhary","full_name":"Choudhary, Bhavya"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis"}],"volume":2,"date_created":"2021-12-05T23:01:48Z","date_updated":"2023-02-23T12:27:13Z","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant (279307: Graph Games).\r\n","year":"2017","publisher":"Association for Computing Machinery","department":[{"_id":"KrCh"}],"publication_status":"published","ec_funded":1,"file_date_updated":"2021-12-07T08:06:28Z","article_number":"30","doi":"10.1145/3158118","conference":{"end_date":"2018-01-13","start_date":"2018-01-07","location":"Los Angeles, CA, United States","name":"POPL: Programming Languages"},"language":[{"iso":"eng"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["1910.00241"]},"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"quality_controlled":"1","publication_identifier":{"eissn":["2475-1421"]},"month":"12","file":[{"content_type":"application/pdf","file_size":460188,"creator":"cchlebak","access_level":"open_access","file_name":"2017_ACMProgLang_Chatterjee.pdf","checksum":"faa3f7b3fe8aab84b50ed805c26a0ee5","success":1,"date_created":"2021-12-07T08:06:28Z","date_updated":"2021-12-07T08:06:28Z","relation":"main_file","file_id":"10421"}],"oa_version":"Published Version","_id":"10416","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","intvolume":" 2","ddc":["000"],"title":"Optimal Dyck reachability for data-dependence and Alias analysis","status":"public","issue":"POPL","abstract":[{"text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graph where the edges are labeled with different types of opening and closing parentheses, and the reachability information is computed via paths whose parentheses are properly matched. We present new results for Dyck reachability 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 as follows: First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph with n nodes and m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)), where α(n) is the inverse Ackermann function, improving the previously known O(n2) time bound; (ii) a matching lower bound that shows that our algorithm is optimal wrt to worst-case complexity; and (iii) an optimal average-case upper bound of O(m) time, improving the previously known O(m · logn) bound. Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtain analysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almost linear 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 Matrix Multiplication, which is a long-standing open problem. Thus we establish that the existing combinatorial algorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the same hardness holds for graphs of constant treewidth. Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependence analysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform all existing methods on the two problems, over real-world benchmarks.","lang":"eng"}],"type":"journal_article","date_published":"2017-12-27T00:00:00Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 30, Association for Computing Machinery, 2017, doi:10.1145/3158118.","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 2 (2017).","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158118.","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158118","ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. 2(POPL), 30.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability for data-dependence and Alias analysis,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.","apa":"Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158118"},"publication":"Proceedings of the ACM on Programming Languages","article_type":"original","has_accepted_license":"1","article_processing_charge":"No","day":"27","scopus_import":"1"},{"date_updated":"2023-02-21T15:54:10Z","date_created":"2018-12-12T11:39:26Z","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Choudhary, Bhavya","first_name":"Bhavya","last_name":"Choudhary"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"10416"}]},"publication_status":"published","publisher":"IST Austria","department":[{"_id":"KrCh"}],"year":"2017","file_date_updated":"2020-07-14T12:46:59Z","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2017-870-v1-1","oa":1,"month":"10","publication_identifier":{"issn":["2664-1690"]},"file":[{"relation":"main_file","file_id":"5524","date_updated":"2020-07-14T12:46:59Z","date_created":"2018-12-12T11:54:02Z","checksum":"177a84a46e3ac17e87b31534ad16a4c9","file_name":"IST-2017-870-v1+1_main.pdf","access_level":"open_access","content_type":"application/pdf","file_size":960491,"creator":"system"}],"oa_version":"Published Version","pubrep_id":"870","title":"Optimal Dyck reachability for data-dependence and alias analysis","ddc":["000"],"status":"public","_id":"5455","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","abstract":[{"lang":"eng","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."}],"alternative_title":["IST Austria Technical Report"],"type":"technical_report","date_published":"2017-10-23T00:00:00Z","page":"37","citation":{"chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2017-870-v1-1.","mla":"Chatterjee, Krishnendu, et al. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria, 2017, doi:10.15479/AT:IST-2017-870-v1-1.","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for Data-Dependence and Alias Analysis, IST Austria, 2017.","ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and alias analysis, IST Austria, 37p.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, Optimal Dyck reachability for data-dependence and alias analysis. IST Austria, 2017.","apa":"Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and alias analysis. IST Austria. https://doi.org/10.15479/AT:IST-2017-870-v1-1","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria; 2017. doi:10.15479/AT:IST-2017-870-v1-1"},"day":"23","article_processing_charge":"No","has_accepted_license":"1"},{"department":[{"_id":"KrCh"}],"publisher":"Association for Computing Machinery","publication_status":"published","year":"2017","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061.","volume":2,"date_created":"2021-12-05T23:01:49Z","date_updated":"2023-02-23T12:27:16Z","related_material":{"record":[{"id":"5448","status":"public","relation":"earlier_version"},{"status":"public","relation":"earlier_version","id":"5456"}]},"author":[{"full_name":"Chalupa, Marek","first_name":"Marek","last_name":"Chalupa"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"},{"first_name":"Nishant","last_name":"Sinha","full_name":"Sinha, Nishant"},{"first_name":"Kapil","last_name":"Vaidya","full_name":"Vaidya, Kapil"}],"article_number":"31","ec_funded":1,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"quality_controlled":"1","oa":1,"external_id":{"arxiv":["1610.01188"]},"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158119","open_access":"1"}],"language":[{"iso":"eng"}],"doi":"10.1145/3158119","conference":{"name":"POPL: Programming Languages","location":"Los Angeles, CA, United States","start_date":"2018-01-07","end_date":"2018-01-13"},"publication_identifier":{"eissn":["2475-1421"]},"month":"12","intvolume":" 2","status":"public","title":"Data-centric dynamic partial order reduction","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"10417","oa_version":"Published Version","type":"journal_article","issue":"POPL","abstract":[{"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\n\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.","lang":"eng"}],"article_type":"original","citation":{"chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158119.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings of the ACM on Programming Languages 2 (2017).","mla":"Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 31, Association for Computing Machinery, 2017, doi:10.1145/3158119.","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric dynamic partial order reduction,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.","apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K. (2017). Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158119","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. 2(POPL), 31.","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158119"},"publication":"Proceedings of the ACM on Programming Languages","date_published":"2017-12-27T00:00:00Z","scopus_import":"1","article_processing_charge":"No","day":"27"},{"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","day":"23","month":"10","citation":{"ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction, IST Austria, 36p.","apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K. (2017). Data-centric dynamic partial order reduction. IST Austria. https://doi.org/10.15479/AT:IST-2017-872-v1-1","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, Data-centric dynamic partial order reduction. IST Austria, 2017.","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-Centric Dynamic Partial Order Reduction. IST Austria; 2017. doi:10.15479/AT:IST-2017-872-v1-1","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2017-872-v1-1.","mla":"Chalupa, Marek, et al. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2017, doi:10.15479/AT:IST-2017-872-v1-1.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2017."},"oa":1,"page":"36","doi":"10.15479/AT:IST-2017-872-v1-1","date_published":"2017-10-23T00:00:00Z","language":[{"iso":"eng"}],"type":"technical_report","alternative_title":["IST Austria Technical Report"],"file_date_updated":"2020-07-14T12:46:59Z","abstract":[{"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.","lang":"eng"}],"_id":"5456","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2017","department":[{"_id":"KrCh"}],"publisher":"IST Austria","status":"public","ddc":["000"],"title":"Data-centric dynamic partial order reduction","publication_status":"published","pubrep_id":"872","related_material":{"record":[{"id":"10417","relation":"later_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5448"}]},"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"},{"full_name":"Sinha, Nishant","first_name":"Nishant","last_name":"Sinha"},{"last_name":"Vaidya","first_name":"Kapil","full_name":"Vaidya, Kapil"}],"file":[{"relation":"main_file","file_id":"5487","checksum":"d2635c4cf013000f0a1b09e80f9e4ab7","date_updated":"2020-07-14T12:46:59Z","date_created":"2018-12-12T11:53:26Z","access_level":"open_access","file_name":"IST-2017-872-v1+1_main.pdf","file_size":910347,"content_type":"application/pdf","creator":"system"}],"oa_version":"Published Version","date_updated":"2023-02-23T12:26:54Z","date_created":"2018-12-12T11:39:26Z"},{"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. "}],"type":"conference","alternative_title":["LIPIcs"],"pubrep_id":"924","file":[{"checksum":"2eed5224c0e4e259484a1d71acb8ba6a","date_updated":"2020-07-14T12:47:00Z","date_created":"2018-12-12T10:18:04Z","relation":"main_file","file_id":"5322","file_size":535077,"content_type":"application/pdf","creator":"system","access_level":"open_access","file_name":"IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf"}],"oa_version":"Published Version","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"551","intvolume":" 83","status":"public","title":"Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs","ddc":["004"],"has_accepted_license":"1","day":"01","scopus_import":1,"date_published":"2017-11-01T00:00:00Z","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 Leibniz International Proceedings in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.61.","mla":"Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” Leibniz International Proceedings in Informatics, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.61.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","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 (SG), LIPIcs, vol. 83, 61.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2017). Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In Leibniz International Proceedings in Informatics (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.61","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs,” in Leibniz International Proceedings in Informatics, Aalborg, Denmark, 2017, vol. 83.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In: Leibniz International Proceedings in Informatics. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.61"},"publication":"Leibniz International Proceedings in Informatics","publist_id":"7263","file_date_updated":"2020-07-14T12:47:00Z","article_number":"61","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"volume":83,"date_created":"2018-12-11T11:47:08Z","date_updated":"2021-01-12T08:02:34Z","year":"2017","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"publication_status":"published","publication_identifier":{"isbn":["978-395977046-0"]},"month":"11","doi":"10.4230/LIPIcs.MFCS.2017.61","conference":{"end_date":"2017-08-25","location":"Aalborg, Denmark","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"quality_controlled":"1"},{"month":"11","publication_identifier":{"isbn":["978-395977046-0"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","short":"CC BY (3.0)","image":"/images/cc_by.png"},"quality_controlled":"1","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"conference":{"end_date":"2017-08-25","location":"Aalborg, Denmark","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"doi":"10.4230/LIPIcs.MFCS.2017.39","language":[{"iso":"eng"}],"article_number":"39","file_date_updated":"2020-07-14T12:47:00Z","publist_id":"7262","ec_funded":1,"license":"https://creativecommons.org/licenses/by/3.0/","year":"2017","publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","last_name":"Henzinger","full_name":"Henzinger, Monika H"},{"first_name":"Alexander","last_name":"Svozil","full_name":"Svozil, Alexander"}],"date_updated":"2023-02-14T10:06:46Z","date_created":"2018-12-11T11:47:08Z","volume":83,"scopus_import":"1","day":"01","has_accepted_license":"1","article_processing_charge":"No","publication":"Leibniz International Proceedings in Informatics","citation":{"chicago":"Chatterjee, Krishnendu, Monika H Henzinger, and Alexander Svozil. “Faster Algorithms for Mean-Payoff Parity Games.” In Leibniz International Proceedings in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.39.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Mean-Payoff Parity Games.” Leibniz International Proceedings in Informatics, vol. 83, 39, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.39.","short":"K. Chatterjee, M.H. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Chatterjee K, Henzinger MH, Svozil A. 2017. Faster algorithms for mean-payoff parity games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 39.","apa":"Chatterjee, K., Henzinger, M. H., & Svozil, A. (2017). Faster algorithms for mean-payoff parity games. In Leibniz International Proceedings in Informatics (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.39","ieee":"K. Chatterjee, M. H. Henzinger, and A. Svozil, “Faster algorithms for mean-payoff parity games,” in Leibniz International Proceedings in Informatics, Aalborg, Denmark, 2017, vol. 83.","ama":"Chatterjee K, Henzinger MH, Svozil A. Faster algorithms for mean-payoff parity games. In: Leibniz International Proceedings in Informatics. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.39"},"date_published":"2017-11-01T00:00:00Z","type":"conference","alternative_title":["LIPIcs"],"abstract":[{"lang":"eng","text":"Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a meanpayoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with n vertices, m edges, parity objectives with d priorities, and maximal absolute reward value W for mean-payoff objectives, are as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for the value problem. Our main contributions are faster algorithms, and the running times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem, and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective)."}],"_id":"552","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"title":"Faster algorithms for mean-payoff parity games","status":"public","intvolume":" 83","pubrep_id":"923","file":[{"file_name":"IST-2018-923-v1+1_LIPIcs-MFCS-2017-39.pdf","access_level":"open_access","file_size":610339,"content_type":"application/pdf","creator":"system","relation":"main_file","file_id":"5248","date_created":"2018-12-12T10:16:57Z","date_updated":"2020-07-14T12:47:00Z","checksum":"c67f4866ddbfd555afef1f63ae9a8fc7"}],"oa_version":"Published Version"},{"language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.MFCS.2017.55","conference":{"name":"MFCS: Mathematical Foundations of Computer Science (SG)","location":"Aalborg, Denmark","start_date":"2017-08-21","end_date":"2017-08-25"},"quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1506.02434"}],"publication_identifier":{"isbn":["978-395977046-0"]},"month":"11","volume":83,"date_updated":"2021-01-12T08:02:35Z","date_created":"2018-12-11T11:47:08Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Hansen, Kristofer","first_name":"Kristofer","last_name":"Hansen"},{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"publication_status":"published","year":"2017","publist_id":"7261","file_date_updated":"2020-07-14T12:47:00Z","article_number":"55","date_published":"2017-11-01T00:00:00Z","citation":{"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.” Leibniz International Proceedings in Informatics, vol. 83, 55, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.55.","chicago":"Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy Complexity of Concurrent Safety Games.” In Leibniz International Proceedings in Informatics, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.55.","ama":"Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent safety games. In: Leibniz International Proceedings in Informatics. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.55","apa":"Chatterjee, K., Hansen, K., & Ibsen-Jensen, R. (2017). Strategy complexity of concurrent safety games. In Leibniz International Proceedings in Informatics (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.55","ieee":"K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent safety games,” in Leibniz International Proceedings in Informatics, Aalborg, Denmark, 2017, vol. 83.","ista":"Chatterjee K, Hansen K, Ibsen-Jensen R. 2017. Strategy complexity of concurrent safety games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 55."},"publication":"Leibniz International Proceedings in Informatics","has_accepted_license":"1","day":"01","scopus_import":1,"oa_version":"Published Version","file":[{"file_name":"IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf","access_level":"open_access","creator":"system","file_size":549967,"content_type":"application/pdf","file_id":"4753","relation":"main_file","date_created":"2018-12-12T10:09:29Z","date_updated":"2020-07-14T12:47:00Z","checksum":"7101facb56ade363205c695d72dbd173"}],"pubrep_id":"922","intvolume":" 83","ddc":["004"],"title":"Strategy complexity of concurrent safety games","status":"public","_id":"553","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We consider two player, zero-sum, finite-state concurrent reachability games, played for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. Player 1 wins iff a designated goal state is eventually visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed. Our main results are as follows: We show that: (i) the optimal bound on the patience of optimal and -optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. "}],"alternative_title":["LIPIcs"],"type":"conference"},{"month":"07","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-319-63120-2"]},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-63121-9_18","quality_controlled":"1","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"oa":1,"file_date_updated":"2020-07-14T12:47:25Z","ec_funded":1,"publist_id":"7170","date_created":"2018-12-11T11:47:34Z","date_updated":"2022-05-23T08:54:02Z","volume":10460,"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"}],"publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"editor":[{"last_name":"Aceto","first_name":"Luca","full_name":"Aceto, Luca"},{"last_name":"Bacci","first_name":"Giorgio","full_name":"Bacci, Giorgio"},{"first_name":"Anna","last_name":"Ingólfsdóttir","full_name":"Ingólfsdóttir, Anna"},{"full_name":"Legay, Axel","last_name":"Legay","first_name":"Axel"},{"full_name":"Mardare, Radu","first_name":"Radu","last_name":"Mardare"}],"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.","year":"2017","day":"25","has_accepted_license":"1","article_processing_charge":"No","series_title":"Theoretical Computer Science and General Issues","scopus_import":"1","date_published":"2017-07-25T00:00:00Z","page":"367 - 381","publication":"Models, Algorithms, Logics and Tools","citation":{"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. Models, Algorithms, Logics and Tools. Vol 10460. Theoretical Computer Science and General Issues. Springer; 2017:367-381. doi:10.1007/978-3-319-63121-9_18","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., & Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, & R. Mardare (Eds.), Models, Algorithms, Logics and Tools (Vol. 10460, pp. 367–381). Springer. https://doi.org/10.1007/978-3-319-63121-9_18","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in Models, Algorithms, Logics and Tools, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381.","mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” Models, Algorithms, Logics and Tools, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:10.1007/978-3-319-63121-9_18.","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.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost of Exactness in Quantitative Reachability.” In Models, Algorithms, Logics and Tools, 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. https://doi.org/10.1007/978-3-319-63121-9_18."},"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"}],"alternative_title":["LNCS"],"type":"book_chapter","file":[{"content_type":"application/pdf","file_size":192826,"creator":"dernst","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","access_level":"open_access","date_updated":"2020-07-14T12:47:25Z","date_created":"2019-11-19T08:06:50Z","checksum":"b2402766ec02c79801aac634bd8f9f6c","relation":"main_file","file_id":"7048"}],"oa_version":"Submitted Version","title":"The cost of exactness in quantitative reachability","ddc":["000"],"status":"public","intvolume":" 10460","_id":"625","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"_id":"628","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Automated recurrence analysis for almost linear expected runtime bounds","intvolume":" 10426","oa_version":"Submitted Version","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","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."}],"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. https://doi.org/10.1007/978-3-319-63387-9_6.","short":"K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 118–139.","mla":"Chatterjee, Krishnendu, et al. Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 118–39, doi:10.1007/978-3-319-63387-9_6.","apa":"Chatterjee, K., Fu, H., & Murhekar, A. (2017). Automated recurrence analysis for almost linear expected runtime bounds. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 118–139). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_6","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.","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.","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:10.1007/978-3-319-63387-9_6"},"page":"118 - 139","date_published":"2017-01-01T00:00:00Z","scopus_import":1,"day":"01","year":"2017","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"Springer","editor":[{"last_name":"Majumdar","first_name":"Rupak","full_name":"Majumdar, Rupak"},{"first_name":"Viktor","last_name":"Kunčak","full_name":"Kunčak, Viktor"}],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Fu, Hongfei","first_name":"Hongfei","last_name":"Fu"},{"first_name":"Aniket","last_name":"Murhekar","full_name":"Murhekar, Aniket"}],"date_created":"2018-12-11T11:47:35Z","date_updated":"2021-01-12T08:06:55Z","volume":10426,"ec_funded":1,"publist_id":"7166","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.00314"}],"oa":1,"quality_controlled":"1","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"conference":{"name":"CAV: Computer Aided Verification","start_date":"2017-07-24","location":"Heidelberg, Germany","end_date":"2017-07-28"},"doi":"10.1007/978-3-319-63387-9_6","language":[{"iso":"eng"}],"month":"01","publication_identifier":{"isbn":["978-331963386-2"]}}]