[{"file_date_updated":"2020-07-14T12:47:14Z","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"ACM Press","year":"2018","date_updated":"2023-09-19T10:45:15Z","date_created":"2019-02-13T10:31:41Z","author":[{"full_name":"Hansen, Kristoffer Arnsfelt","last_name":"Hansen","first_name":"Kristoffer Arnsfelt"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Neyman, Abraham","last_name":"Neyman","first_name":"Abraham"}],"month":"06","publication_identifier":{"isbn":["9781450358293"]},"isi":1,"quality_controlled":"1","oa":1,"external_id":{"isi":["000492755100020"]},"language":[{"iso":"eng"}],"conference":{"end_date":"2018-06-22","location":"Ithaca, NY, United States","start_date":"2018-06-18","name":"EC: Conference on Economics and Computation"},"doi":"10.1145/3219166.3219198","type":"conference","abstract":[{"text":"The Big Match is a multi-stage two-player game. In each stage Player 1 hides one or two pebbles in his hand, and his opponent has to guess that number; Player 1 loses a point if Player 2 is correct, and otherwise he wins a point. As soon as Player 1 hides one pebble, the players cannot change their choices in any future stage.\r\nBlackwell and Ferguson (1968) give an ε-optimal strategy for Player 1 that hides, in each stage, one pebble with a probability that depends on the entire past history. Any strategy that depends just on the clock or on a finite memory is worthless. The long-standing natural open problem has been whether every strategy that depends just on the clock and a finite memory is worthless. We prove that there is such a strategy that is ε-optimal. In fact, we show that just two states of memory are sufficient.\r\n","lang":"eng"}],"title":"The Big Match with a clock and a bit of memory","status":"public","ddc":["000"],"_id":"5967","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"checksum":"bb52683e349cfd864f4769a8f38f2798","date_updated":"2020-07-14T12:47:14Z","date_created":"2019-11-19T08:24:24Z","relation":"main_file","file_id":"7054","content_type":"application/pdf","file_size":302539,"creator":"dernst","access_level":"open_access","file_name":"2018_EC18_Hansen.pdf"}],"oa_version":"Submitted Version","scopus_import":"1","day":"18","has_accepted_license":"1","article_processing_charge":"No","page":"149-150","publication":"Proceedings of the 2018 ACM Conference on Economics and Computation - EC '18","citation":{"ista":"Hansen KA, Ibsen-Jensen R, Neyman A. 2018. The Big Match with a clock and a bit of memory. Proceedings of the 2018 ACM Conference on Economics and Computation - EC ’18. EC: Conference on Economics and Computation, 149–150.","ieee":"K. A. Hansen, R. Ibsen-Jensen, and A. Neyman, “The Big Match with a clock and a bit of memory,” in Proceedings of the 2018 ACM Conference on Economics and Computation - EC ’18, Ithaca, NY, United States, 2018, pp. 149–150.","apa":"Hansen, K. A., Ibsen-Jensen, R., & Neyman, A. (2018). The Big Match with a clock and a bit of memory. In Proceedings of the 2018 ACM Conference on Economics and Computation - EC ’18 (pp. 149–150). Ithaca, NY, United States: ACM Press. https://doi.org/10.1145/3219166.3219198","ama":"Hansen KA, Ibsen-Jensen R, Neyman A. The Big Match with a clock and a bit of memory. In: Proceedings of the 2018 ACM Conference on Economics and Computation - EC ’18. ACM Press; 2018:149-150. doi:10.1145/3219166.3219198","chicago":"Hansen, Kristoffer Arnsfelt, Rasmus Ibsen-Jensen, and Abraham Neyman. “The Big Match with a Clock and a Bit of Memory.” In Proceedings of the 2018 ACM Conference on Economics and Computation - EC ’18, 149–50. ACM Press, 2018. https://doi.org/10.1145/3219166.3219198.","mla":"Hansen, Kristoffer Arnsfelt, et al. “The Big Match with a Clock and a Bit of Memory.” Proceedings of the 2018 ACM Conference on Economics and Computation - EC ’18, ACM Press, 2018, pp. 149–50, doi:10.1145/3219166.3219198.","short":"K.A. Hansen, R. Ibsen-Jensen, A. Neyman, in:, Proceedings of the 2018 ACM Conference on Economics and Computation - EC ’18, ACM Press, 2018, pp. 149–150."},"date_published":"2018-06-18T00:00:00Z"},{"scopus_import":"1","article_processing_charge":"No","day":"01","citation":{"apa":"Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2018). Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM). https://doi.org/10.1145/3174800","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2. Association for Computing Machinery (ACM), 2018.","ista":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. 40(2), 7.","ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. 2018;40(2). doi:10.1145/3174800","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3174800.","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018).","mla":"Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2, 7, Association for Computing Machinery (ACM), 2018, doi:10.1145/3174800."},"publication":"ACM Transactions on Programming Languages and Systems","date_published":"2018-06-01T00:00:00Z","type":"journal_article","issue":"2","abstract":[{"text":"In this article, we consider the termination problem of probabilistic programs with real-valued variables. Thequestions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1(almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); andquantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) tocompute a boundBsuch that the probability not to terminate afterBsteps decreases exponentially (con-centration problem). To solve these questions, we utilize the notion of ranking supermartingales, which isa powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmicsynthesis of linear ranking-supermartingales over affine probabilistic programs (Apps) with both angelic anddemonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Appsover which a linear ranking-supermartingale exists.Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor Apps with angelic non-determinism. Moreover, theNP-hardness result holds already for Appswithout probability and demonic non-determinism. Secondly, we show that the concentration problem overLRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show thatthe expectation problem over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate theeffectiveness of our approach to answer the qualitative and quantitative questions over Apps with at mostdemonic non-determinism.","lang":"eng"}],"intvolume":" 40","title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"5993","oa_version":"Submitted Version","publication_identifier":{"issn":["0164-0925"]},"month":"06","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","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"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"}],"quality_controlled":"1","isi":1,"external_id":{"isi":["000434634500003"],"arxiv":["1510.08517"]},"main_file_link":[{"url":"https://arxiv.org/abs/1510.08517","open_access":"1"}],"oa":1,"language":[{"iso":"eng"}],"doi":"10.1145/3174800","article_number":"7","ec_funded":1,"publisher":"Association for Computing Machinery (ACM)","department":[{"_id":"KrCh"}],"publication_status":"published","year":"2018","volume":40,"date_created":"2019-02-14T12:29:10Z","date_updated":"2023-09-19T14:38:42Z","related_material":{"record":[{"id":"1438","relation":"earlier_version","status":"public"}]},"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Fu, Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","last_name":"Fu"},{"full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","first_name":"Petr"},{"full_name":"Hasheminezhad, Rouzbeh","last_name":"Hasheminezhad","first_name":"Rouzbeh"}]},{"publist_id":"8030","ec_funded":1,"date_created":"2018-12-11T11:44:13Z","date_updated":"2023-09-19T14:44:59Z","volume":"2018-July","author":[{"full_name":"Horák, Karel","last_name":"Horák","first_name":"Karel"},{"full_name":"Bošanský, Branislav","last_name":"Bošanský","first_name":"Branislav"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"}],"publication_status":"published","publisher":"IJCAI","department":[{"_id":"KrCh"}],"year":"2018","acknowledgement":"∗This work has been 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). This research was sponsored by the Army Research Laboratory and was accomplished under Cooperative Agreement Number W911NF-13-2-0045 (ARL Cyber Security CRA). ","month":"07","language":[{"iso":"eng"}],"conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2018-07-13","location":"Stockholm, Sweden","end_date":"2018-07-19"},"doi":"10.24963/ijcai.2018/662","isi":1,"quality_controlled":"1","project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"main_file_link":[{"url":"https://doi.org/10.24963/ijcai.2018/662","open_access":"1"}],"oa":1,"external_id":{"isi":["000764175404127"]},"abstract":[{"lang":"eng","text":"Partially observable Markov decision processes (POMDPs) are the standard models for planning under uncertainty with both finite and infinite horizon. Besides the well-known discounted-sum objective, indefinite-horizon objective (aka Goal-POMDPs) is another classical objective for POMDPs. In this case, given a set of target states and a positive cost for each transition, the optimization objective is to minimize the expected total cost until a target state is reached. In the literature, RTDP-Bel or heuristic search value iteration (HSVI) have been used for solving Goal-POMDPs. Neither of these algorithms has theoretical convergence guarantees, and HSVI may even fail to terminate its trials. We give the following contributions: (1) We discuss the challenges introduced in Goal-POMDPs and illustrate how they prevent the original HSVI from converging. (2) We present a novel algorithm inspired by HSVI, termed Goal-HSVI, and show that our algorithm has convergence guarantees. (3) We show that Goal-HSVI outperforms RTDP-Bel on a set of well-known examples."}],"type":"conference","oa_version":"Published Version","status":"public","title":"Goal-HSVI: Heuristic search value iteration for goal-POMDPs","_id":"25","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"01","article_processing_charge":"No","scopus_import":"1","date_published":"2018-07-01T00:00:00Z","page":"4764 - 4770","publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","citation":{"ama":"Horák K, Bošanský B, Chatterjee K. Goal-HSVI: Heuristic search value iteration for goal-POMDPs. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. Vol 2018-July. IJCAI; 2018:4764-4770. doi:10.24963/ijcai.2018/662","ista":"Horák K, Bošanský B, Chatterjee K. 2018. Goal-HSVI: Heuristic search value iteration for goal-POMDPs. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018–July, 4764–4770.","ieee":"K. Horák, B. Bošanský, and K. Chatterjee, “Goal-HSVI: Heuristic search value iteration for goal-POMDPs,” in Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018–July, pp. 4764–4770.","apa":"Horák, K., Bošanský, B., & Chatterjee, K. (2018). Goal-HSVI: Heuristic search value iteration for goal-POMDPs. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (Vol. 2018–July, pp. 4764–4770). Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/662","mla":"Horák, Karel, et al. “Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs.” Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, vol. 2018–July, IJCAI, 2018, pp. 4764–70, doi:10.24963/ijcai.2018/662.","short":"K. Horák, B. Bošanský, K. Chatterjee, in:, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4764–4770.","chicago":"Horák, Karel, Branislav Bošanský, and Krishnendu Chatterjee. “Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs.” In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018–July:4764–70. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/662."}},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IJCAI","publication_status":"published","year":"2018","acknowledgement":"This research was supported by the Vienna Science and Technology Fund (WWTF) grant ICT15-003; Austrian Science Fund (FWF): S11407-N23(RiSE/SHiNE);and an ERC Start Grant (279307:Graph Games).\r\n","volume":2018,"date_updated":"2023-09-19T14:45:48Z","date_created":"2018-12-11T11:44:13Z","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Elgyütt","first_name":"Adrian","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","full_name":"Elgyütt, Adrian"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Rouillé, Owen","first_name":"Owen","last_name":"Rouillé"}],"ec_funded":1,"publist_id":"8031","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"isi":1,"quality_controlled":"1","external_id":{"isi":["000764175404117"],"arxiv":["1804.10601"]},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.10601"}],"language":[{"iso":"eng"}],"doi":"10.24963/ijcai.2018/652","conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence","location":"Stockholm, Sweden","start_date":"2018-07-13","end_date":"2018-07-19"},"month":"07","intvolume":" 2018","status":"public","title":"Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"24","oa_version":"Preprint","type":"conference","abstract":[{"text":"Partially-observable Markov decision processes (POMDPs) with discounted-sum payoff are a standard framework to model a wide range of problems related to decision making under uncertainty. Traditionally, the goal has been to obtain policies that optimize the expectation of the discounted-sum payoff. A key drawback of the expectation measure is that even low probability events with extreme payoff can significantly affect the expectation, and thus the obtained policies are not necessarily risk-averse. An alternate approach is to optimize the probability that the payoff is above a certain threshold, which allows obtaining risk-averse policies, but ignores optimization of the expectation. We consider the expectation optimization with probabilistic guarantee (EOPG) problem, where the goal is to optimize the expectation ensuring that the payoff is above a given threshold with at least a specified probability. We present several results on the EOPG problem, including the first algorithm to solve it.","lang":"eng"}],"page":"4692 - 4699","citation":{"ama":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. In: Vol 2018. IJCAI; 2018:4692-4699. doi:10.24963/ijcai.2018/652","ieee":"K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé, “Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives,” presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018, pp. 4692–4699.","apa":"Chatterjee, K., Elgyütt, A., Novotný, P., & Rouillé, O. (2018). Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives (Vol. 2018, pp. 4692–4699). Presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden: IJCAI. https://doi.org/10.24963/ijcai.2018/652","ista":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. 2018. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4692–4699.","short":"K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp. 4692–4699.","mla":"Chatterjee, Krishnendu, et al. Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives. Vol. 2018, IJCAI, 2018, pp. 4692–99, doi:10.24963/ijcai.2018/652.","chicago":"Chatterjee, Krishnendu, Adrian Elgyütt, Petr Novotný, and Owen Rouillé. “Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives,” 2018:4692–99. IJCAI, 2018. https://doi.org/10.24963/ijcai.2018/652."},"date_published":"2018-07-01T00:00:00Z","scopus_import":"1","article_processing_charge":"No","day":"01"},{"date_published":"2018-06-01T00:00:00Z","citation":{"mla":"Chatterjee, Krishnendu, et al. Sensor Synthesis for POMDPs with Reachability Objectives. Vol. 2018, AAAI Press, 2018, pp. 47–55.","short":"K. Chatterjee, M. Chemlík, U. Topcu, in:, AAAI Press, 2018, pp. 47–55.","chicago":"Chatterjee, Krishnendu, Martin Chemlík, and Ufuk Topcu. “Sensor Synthesis for POMDPs with Reachability Objectives,” 2018:47–55. AAAI Press, 2018.","ama":"Chatterjee K, Chemlík M, Topcu U. Sensor synthesis for POMDPs with reachability objectives. In: Vol 2018. AAAI Press; 2018:47-55.","ista":"Chatterjee K, Chemlík M, Topcu U. 2018. Sensor synthesis for POMDPs with reachability objectives. ICAPS: International Conference on Automated Planning and Scheduling, ICAPS, vol. 2018, 47–55.","ieee":"K. Chatterjee, M. Chemlík, and U. Topcu, “Sensor synthesis for POMDPs with reachability objectives,” presented at the ICAPS: International Conference on Automated Planning and Scheduling, Delft, Netherlands, 2018, vol. 2018, pp. 47–55.","apa":"Chatterjee, K., Chemlík, M., & Topcu, U. (2018). Sensor synthesis for POMDPs with reachability objectives (Vol. 2018, pp. 47–55). Presented at the ICAPS: International Conference on Automated Planning and Scheduling, Delft, Netherlands: AAAI Press."},"page":"47 - 55","article_processing_charge":"No","day":"01","scopus_import":"1","oa_version":"Preprint","_id":"34","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","intvolume":" 2018","status":"public","title":"Sensor synthesis for POMDPs with reachability objectives","abstract":[{"lang":"eng","text":"Partially observable Markov decision processes (POMDPs) are widely used in probabilistic planning problems in which an agent interacts with an environment using noisy and imprecise sensors. We study a setting in which the sensors are only partially defined and the goal is to synthesize “weakest” additional sensors, such that in the resulting POMDP, there is a small-memory policy for the agent that almost-surely (with probability 1) satisfies a reachability objective. We show that the problem is NP-complete, and present a symbolic algorithm by encoding the problem into SAT instances. We illustrate trade-offs between the amount of memory of the policy and the number of additional sensors on a simple example. We have implemented our approach and consider three classical POMDP examples from the literature, and show that in all the examples the number of sensors can be significantly decreased (as compared to the existing solutions in the literature) without increasing the complexity of the policies."}],"type":"conference","alternative_title":["ICAPS"],"conference":{"name":"ICAPS: International Conference on Automated Planning and Scheduling","end_date":"2018-06-29","start_date":"2018-06-24","location":"Delft, Netherlands"},"language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/1710.00675","open_access":"1"}],"oa":1,"external_id":{"isi":["000492986200006"],"arxiv":["1710.00675"]},"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"isi":1,"quality_controlled":"1","month":"06","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Chemlík, Martin","first_name":"Martin","last_name":"Chemlík"},{"first_name":"Ufuk","last_name":"Topcu","full_name":"Topcu, Ufuk"}],"volume":2018,"date_created":"2018-12-11T11:44:16Z","date_updated":"2023-09-19T14:44:14Z","year":"2018","department":[{"_id":"KrCh"}],"publisher":"AAAI Press","publication_status":"published","ec_funded":1,"publist_id":"8021"},{"year":"2018","publication_status":"published","publisher":"AAAI Press","department":[{"_id":"KrCh"}],"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Wolfgang","last_name":"Dvorák","full_name":"Dvorák, Wolfgang"},{"orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"full_name":"Svozil, Alexander","last_name":"Svozil","first_name":"Alexander"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"9293"}]},"date_created":"2018-12-11T11:44:17Z","date_updated":"2023-09-26T10:41:41Z","publist_id":"8020","ec_funded":1,"oa":1,"external_id":{"isi":["000492986200007"],"arxiv":["1804.07031"]},"main_file_link":[{"url":"https://arxiv.org/abs/1804.07031","open_access":"1"}],"quality_controlled":"1","isi":1,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"conference":{"location":"Delft, Netherlands","start_date":"2018-06-24","end_date":"2018-06-29","name":"ICAPS: International Conference on Automated Planning and Scheduling"},"language":[{"iso":"eng"}],"month":"06","_id":"35","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","title":"Algorithms and conditional lower bounds for planning problems","oa_version":"None","type":"conference","abstract":[{"text":"We consider planning problems for graphs, Markov decision processes (MDPs), and games on graphs. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems where there are k different target sets, and the problems are as follows: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) objective-separation results showing that for MDPs the coverage problem is harder than the sequential target problem.","lang":"eng"}],"publication":"28th International Conference on Automated Planning and Scheduling ","citation":{"mla":"Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for Planning Problems.” 28th International Conference on Automated Planning and Scheduling , AAAI Press, 2018.","short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, A. Svozil, in:, 28th International Conference on Automated Planning and Scheduling , AAAI Press, 2018.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Alexander Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” In 28th International Conference on Automated Planning and Scheduling . AAAI Press, 2018.","ama":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. Algorithms and conditional lower bounds for planning problems. In: 28th International Conference on Automated Planning and Scheduling . AAAI Press; 2018.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. 2018. Algorithms and conditional lower bounds for planning problems. 28th International Conference on Automated Planning and Scheduling . ICAPS: International Conference on Automated Planning and Scheduling.","ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and A. Svozil, “Algorithms and conditional lower bounds for planning problems,” in 28th International Conference on Automated Planning and Scheduling , Delft, Netherlands, 2018.","apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., & Svozil, A. (2018). Algorithms and conditional lower bounds for planning problems. In 28th International Conference on Automated Planning and Scheduling . Delft, Netherlands: AAAI Press."},"date_published":"2018-06-01T00:00:00Z","scopus_import":"1","day":"01","article_processing_charge":"No"},{"type":"journal_article","abstract":[{"lang":"eng","text":"This paper is devoted to automatic competitive analysis of real-time scheduling algorithms for firm-deadline tasksets, where only completed tasks con- tribute some utility to the system. Given such a taskset T , the competitive ratio of an on-line scheduling algorithm A for T is the worst-case utility ratio of A over the utility achieved by a clairvoyant algorithm. We leverage the theory of quantitative graph games to address the competitive analysis and competitive synthesis problems. For the competitive analysis case, given any taskset T and any finite-memory on- line scheduling algorithm A , we show that the competitive ratio of A in T can be computed in polynomial time in the size of the state space of A . Our approach is flexible as it also provides ways to model meaningful constraints on the released task sequences that determine the competitive ratio. We provide an experimental study of many well-known on-line scheduling algorithms, which demonstrates the feasibility of our competitive analysis approach that effectively replaces human ingenuity (required Preliminary versions of this paper have appeared in Chatterjee et al. ( 2013 , 2014 ). B Andreas Pavlogiannis pavlogiannis@ist.ac.at Krishnendu Chatterjee krish.chat@ist.ac.at Alexander Kößler koe@ecs.tuwien.ac.at Ulrich Schmid s@ecs.tuwien.ac.at 1 IST Austria (Institute of Science and Technology Austria), Am Campus 1, 3400 Klosterneuburg, Austria 2 Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria 123 Real-Time Syst for finding worst-case scenarios) by computing power. For the competitive synthesis case, we are just given a taskset T , and the goal is to automatically synthesize an opti- mal on-line scheduling algorithm A , i.e., one that guarantees the largest competitive ratio possible for T . We show how the competitive synthesis problem can be reduced to a two-player graph game with partial information, and establish that the compu- tational complexity of solving this game is Np -complete. The competitive synthesis problem is hence in Np in the size of the state space of the non-deterministic labeled transition system encoding the taskset. Overall, the proposed framework assists in the selection of suitable scheduling algorithms for a given taskset, which is in fact the most common situation in real-time systems design. "}],"issue":"1","title":"Automated competitive analysis of real time scheduling with graph games","status":"public","ddc":["000"],"intvolume":" 54","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"738","file":[{"relation":"main_file","file_id":"5267","date_created":"2018-12-12T10:17:14Z","date_updated":"2020-07-14T12:47:56Z","checksum":"c2590ef160709d8054cf29ee173f1454","file_name":"IST-2018-960-v1+1_2017_Chatterjee_Automated_competetive.pdf","access_level":"open_access","file_size":1163507,"content_type":"application/pdf","creator":"system"}],"oa_version":"Published Version","pubrep_id":"960","scopus_import":"1","day":"01","article_processing_charge":"No","has_accepted_license":"1","page":"166 - 207","publication":"Real-Time Systems","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” Real-Time Systems. Springer, 2018. https://doi.org/10.1007/s11241-017-9293-4.","mla":"Chatterjee, Krishnendu, et al. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” Real-Time Systems, vol. 54, no. 1, Springer, 2018, pp. 166–207, doi:10.1007/s11241-017-9293-4.","short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54 (2018) 166–207.","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2018. Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. 54(1), 166–207.","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “Automated competitive analysis of real time scheduling with graph games,” Real-Time Systems, vol. 54, no. 1. Springer, pp. 166–207, 2018.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2018). Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. Springer. https://doi.org/10.1007/s11241-017-9293-4","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. 2018;54(1):166-207. doi:10.1007/s11241-017-9293-4"},"date_published":"2018-01-01T00:00:00Z","file_date_updated":"2020-07-14T12:47:56Z","ec_funded":1,"publist_id":"6929","publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"}],"year":"2018","date_created":"2018-12-11T11:48:14Z","date_updated":"2023-09-27T12:52:38Z","volume":54,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"full_name":"Kößler, Alexander","last_name":"Kößler","first_name":"Alexander"},{"last_name":"Schmid","first_name":"Ulrich","full_name":"Schmid, Ulrich"}],"related_material":{"record":[{"id":"2820","relation":"earlier_version","status":"public"}]},"month":"01","quality_controlled":"1","isi":1,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"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":{"isi":["000419955500006"]},"language":[{"iso":"eng"}],"doi":"10.1007/s11241-017-9293-4"},{"month":"03","publication_identifier":{"eissn":["1742-5662"]},"language":[{"iso":"eng"}],"doi":"10.1098/rsif.2018.0073","quality_controlled":"1","isi":1,"project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"oa":1,"external_id":{"pmid":["29593089"],"isi":["000428576200023"]},"file_date_updated":"2020-07-14T12:45:22Z","publist_id":"7715","ec_funded":1,"article_number":"20180073","date_created":"2018-12-11T11:45:09Z","date_updated":"2023-10-18T06:36:00Z","volume":15,"author":[{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef","last_name":"Tkadlec"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"related_material":{"record":[{"status":"public","relation":"research_data","id":"9814"}],"link":[{"relation":"supplementary_material","url":"https://dx.doi.org/10.6084/m9.figshare.c.4028971"}]},"publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"The Royal Society","year":"2018","pmid":1,"day":"01","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1","date_published":"2018-03-01T00:00:00Z","article_type":"original","publication":"Journal of the Royal Society Interface","citation":{"ista":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. 2018. Language acquisition with communication between learners. Journal of the Royal Society Interface. 15(140), 20180073.","ieee":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, and M. Nowak, “Language acquisition with communication between learners,” Journal of the Royal Society Interface, vol. 15, no. 140. The Royal Society, 2018.","apa":"Ibsen-Jensen, R., Tkadlec, J., Chatterjee, K., & Nowak, M. (2018). Language acquisition with communication between learners. Journal of the Royal Society Interface. The Royal Society. https://doi.org/10.1098/rsif.2018.0073","ama":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. Language acquisition with communication between learners. Journal of the Royal Society Interface. 2018;15(140). doi:10.1098/rsif.2018.0073","chicago":"Ibsen-Jensen, Rasmus, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Language Acquisition with Communication between Learners.” Journal of the Royal Society Interface. The Royal Society, 2018. https://doi.org/10.1098/rsif.2018.0073.","mla":"Ibsen-Jensen, Rasmus, et al. “Language Acquisition with Communication between Learners.” Journal of the Royal Society Interface, vol. 15, no. 140, 20180073, The Royal Society, 2018, doi:10.1098/rsif.2018.0073.","short":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, M. Nowak, Journal of the Royal Society Interface 15 (2018)."},"abstract":[{"lang":"eng","text":"We consider a class of students learning a language from a teacher. The situation can be interpreted as a group of child learners receiving input from the linguistic environment. The teacher provides sample sentences. The students try to learn the grammar from the teacher. In addition to just listening to the teacher, the students can also communicate with each other. The students hold hypotheses about the grammar and change them if they receive counter evidence. The process stops when all students have converged to the correct grammar. We study how the time to convergence depends on the structure of the classroom by introducing and evaluating various complexity measures. We find that structured communication between students, although potentially introducing confusion, can greatly reduce some of the complexity measures. Our theory can also be interpreted as applying to the scientific process, where nature is the teacher and the scientists are the students."}],"issue":"140","type":"journal_article","oa_version":"Submitted Version","file":[{"file_id":"5955","relation":"main_file","date_updated":"2020-07-14T12:45:22Z","date_created":"2019-02-12T07:54:37Z","checksum":"444e1a9d98eb0e780671be82b13025f3","file_name":"2018_RS_IbsenJensen.pdf","access_level":"open_access","creator":"dernst","file_size":219837,"content_type":"application/pdf"}],"title":"Language acquisition with communication between learners","status":"public","ddc":["000"],"intvolume":" 15","_id":"198","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"citation":{"ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. 2018;1(1). doi:10.1038/s42003-018-0078-7","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. A. Nowak, “Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory,” Communications Biology, vol. 1, no. 1. Springer Nature, 2018.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. A. (2018). Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. Springer Nature. https://doi.org/10.1038/s42003-018-0078-7","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. 2018. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. 1(1), 71.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M.A. Nowak, Communications Biology 1 (2018).","mla":"Pavlogiannis, Andreas, et al. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” Communications Biology, vol. 1, no. 1, 71, Springer Nature, 2018, doi:10.1038/s42003-018-0078-7.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin A. Nowak. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” Communications Biology. Springer Nature, 2018. https://doi.org/10.1038/s42003-018-0078-7."},"publication":"Communications Biology","date_published":"2018-06-14T00:00:00Z","scopus_import":"1","article_processing_charge":"No","has_accepted_license":"1","day":"14","intvolume":" 1","ddc":["004","519","576"],"status":"public","title":"Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory","_id":"5751","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Published Version","file":[{"file_size":1804194,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2018_CommBiology_Pavlogiannis.pdf","checksum":"a9db825fa3b64a51ff3de035ec973b3e","date_updated":"2020-07-14T12:47:10Z","date_created":"2018-12-18T13:37:04Z","relation":"main_file","file_id":"5752"}],"pubrep_id":"1045","type":"journal_article","issue":"1","abstract":[{"text":"Because of the intrinsic randomness of the evolutionary process, a mutant with a fitness advantage has some chance to be selected but no certainty. Any experiment that searches for advantageous mutants will lose many of them due to random drift. It is therefore of great interest to find population structures that improve the odds of advantageous mutants. Such structures are called amplifiers of natural selection: they increase the probability that advantageous mutants are selected. Arbitrarily strong amplifiers guarantee the selection of advantageous mutants, even for very small fitness advantage. Despite intensive research over the past decade, arbitrarily strong amplifiers have remained rare. Here we show how to construct a large variety of them. Our amplifiers are so simple that they could be useful in biotechnology, when optimizing biological molecules, or as a diagnostic tool, when searching for faster dividing cells or viruses. They could also occur in natural population structures.","lang":"eng"}],"project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","isi":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":{"isi":["000461126500071"]},"oa":1,"language":[{"iso":"eng"}],"doi":"10.1038/s42003-018-0078-7","publication_identifier":{"issn":["2399-3642"]},"month":"06","department":[{"_id":"KrCh"}],"publisher":"Springer Nature","publication_status":"published","year":"2018","volume":1,"date_updated":"2024-02-21T13:48:42Z","date_created":"2018-12-18T13:22:58Z","related_material":{"record":[{"id":"7196","relation":"part_of_dissertation","status":"public"},{"id":"5559","relation":"popular_science","status":"public"}]},"author":[{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"},{"full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Nowak","first_name":"Martin A.","full_name":"Nowak, Martin A."}],"article_number":"71","ec_funded":1,"file_date_updated":"2020-07-14T12:47:10Z"},{"date_published":"2018-09-01T00:00:00Z","citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. “Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","mla":"Chatterjee, Krishnendu, et al. Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. Vol. 118, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.11.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and Y. Velner, “Ergodic mean-payoff games for the analysis of attacks in crypto-currencies,” presented at the CONCUR: Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Velner, Y. (2018). Ergodic mean-payoff games for the analysis of attacks in crypto-currencies (Vol. 118). Presented at the CONCUR: Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. 2018. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 118, 11.","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.CONCUR.2018.11"},"has_accepted_license":"1","article_processing_charge":"No","day":"01","scopus_import":"1","file":[{"relation":"main_file","file_id":"5696","date_created":"2018-12-17T12:08:00Z","date_updated":"2020-07-14T12:47:34Z","checksum":"68a055b1aaa241cc38375083cf832a7d","file_name":"2018_CONCUR_Chatterjee.pdf","access_level":"open_access","file_size":1078309,"content_type":"application/pdf","creator":"dernst"}],"oa_version":"Published Version","_id":"66","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 118","ddc":["000"],"title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","status":"public","abstract":[{"text":"Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.","lang":"eng"}],"type":"conference","alternative_title":["LIPIcs"],"doi":"10.4230/LIPIcs.CONCUR.2018.11","conference":{"location":"Beijing, China","start_date":"2018-09-04","end_date":"2018-09-07","name":"CONCUR: Conference on Concurrency Theory"},"language":[{"iso":"eng"}],"external_id":{"arxiv":["1806.03108"]},"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,"project":[{"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"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","publication_identifier":{"isbn":["978-3-95977-087-3"]},"month":"09","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir","full_name":"Goharshady, Amir"},{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"volume":118,"date_created":"2018-12-11T11:44:27Z","date_updated":"2024-03-28T23:30:34Z","year":"2018","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"publication_status":"published","ec_funded":1,"publist_id":"7988","file_date_updated":"2020-07-14T12:47:34Z","article_number":"11"},{"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-89884-1_26","conference":{"end_date":"2018-04-19","location":"Thessaloniki, Greece","start_date":"2018-04-16","name":"ESOP: European Symposium on Programming"},"project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"_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","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"quality_controlled":"1","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"},"month":"04","volume":10801,"date_created":"2018-12-11T11:45:45Z","date_updated":"2024-03-28T23:30:33Z","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","first_name":"Amir","last_name":"Goharshady","full_name":"Goharshady, Amir"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"department":[{"_id":"KrCh"}],"publisher":"Springer","publication_status":"published","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).","year":"2018","ec_funded":1,"publist_id":"7554","file_date_updated":"2020-07-14T12:46:00Z","date_published":"2018-04-01T00:00:00Z","page":"739 - 767","citation":{"ista":"Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 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","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.","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","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.","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."},"has_accepted_license":"1","article_processing_charge":"No","day":"01","scopus_import":"1","oa_version":"Published Version","file":[{"date_created":"2018-12-17T15:45:49Z","date_updated":"2020-07-14T12:46:00Z","checksum":"9c8a8338c571903b599b6ca93abd2cce","relation":"main_file","file_id":"5716","content_type":"application/pdf","file_size":1394993,"creator":"dernst","file_name":"2018_ESOP_Chatterjee.pdf","access_level":"open_access"}],"intvolume":" 10801","status":"public","ddc":["000"],"title":"Quantitative analysis of smart contracts","_id":"311","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"alternative_title":["LNCS"],"type":"conference"},{"language":[{"iso":"eng"}],"conference":{"name":"IEEE International Conference on Blockchain","end_date":"2018-08-03","location":"Halifax, Canada","start_date":"2018-07-30"},"doi":"10.1109/Cybermatics_2018.2018.00231","isi":1,"quality_controlled":"1","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"oa":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"},"external_id":{"arxiv":["1805.09104"],"isi":["000481634500196"]},"month":"09","publication_identifier":{"isbn":["978-1-5386-7975-3 "]},"date_created":"2019-04-18T10:37:35Z","date_updated":"2024-03-28T23:30:34Z","author":[{"full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","last_name":"Goharshady"},{"full_name":"Behrouz, Ali","first_name":"Ali","last_name":"Behrouz"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"}],"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"IEEE","year":"2018","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","file_date_updated":"2020-07-14T12:47:27Z","ec_funded":1,"date_published":"2018-09-01T00:00:00Z","page":"1343-1348","publication":"Proceedings of the IEEE International Conference on Blockchain","citation":{"apa":"Goharshady, A. K., Behrouz, A., & Chatterjee, K. (2018). Secure Credit Reporting on the Blockchain. In Proceedings of the IEEE International Conference on Blockchain (pp. 1343–1348). Halifax, Canada: IEEE. https://doi.org/10.1109/Cybermatics_2018.2018.00231","ieee":"A. K. Goharshady, A. Behrouz, and K. Chatterjee, “Secure Credit Reporting on the Blockchain,” in Proceedings of the IEEE International Conference on Blockchain, Halifax, Canada, 2018, pp. 1343–1348.","ista":"Goharshady AK, Behrouz A, Chatterjee K. 2018. Secure Credit Reporting on the Blockchain. Proceedings of the IEEE International Conference on Blockchain. IEEE International Conference on Blockchain, 1343–1348.","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","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.","short":"A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–1348.","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."},"day":"01","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1","oa_version":"Submitted Version","file":[{"date_created":"2019-04-18T10:36:39Z","date_updated":"2020-07-14T12:47:27Z","checksum":"b25c9bb7cf6e7e6634e692d26d41ead8","file_id":"6341","relation":"main_file","creator":"akafshda","file_size":624338,"content_type":"application/pdf","file_name":"blockchain2018.pdf","access_level":"open_access"}],"status":"public","ddc":["000"],"title":"Secure Credit Reporting on the Blockchain","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"6340","abstract":[{"lang":"eng","text":"We present a secure approach for maintaining andreporting credit history records on the Blockchain. Our ap-proach removes third-parties such as credit reporting agen-cies from the lending process and replaces them with smartcontracts. This allows customers to interact directly with thelenders or banks while ensuring the integrity, unmalleabilityand privacy of their credit data. Additionally, each customerhas full control over complete or selective disclosure of hercredit records, eliminating the risk of privacy violations or databreaches. Moreover, our approach provides strong guaranteesfor the lenders as well. A lender can check both correctness andcompleteness of the credit data disclosed to her. This is the firstapproach that can perform all credit reporting tasks withouta central authority or changing the financial mechanisms*."}],"type":"conference"},{"month":"08","publication_identifier":{"issn":["0164-0925"]},"main_file_link":[{"url":"https://arxiv.org/abs/1510.07565","open_access":"1"}],"oa":1,"external_id":{"isi":["000444694800001"],"arxiv":["1510.07565"]},"quality_controlled":"1","isi":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":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"doi":"10.1145/3210257","language":[{"iso":"eng"}],"article_number":"9","ec_funded":1,"year":"2018","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"Association for Computing Machinery (ACM)","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","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","first_name":"Rasmus"},{"full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1437"},{"id":"5441","relation":"earlier_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5442"},{"relation":"dissertation_contains","status":"public","id":"8934"}]},"date_updated":"2024-03-28T23:30:34Z","date_created":"2019-02-14T14:31:52Z","volume":40,"scopus_import":"1","day":"01","article_processing_charge":"No","publication":"ACM Transactions on Programming Languages and Systems","citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” 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","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 40(3), 9.","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. 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.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","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."},"date_published":"2018-08-01T00:00:00Z","type":"journal_article","abstract":[{"text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n","lang":"eng"}],"issue":"3","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"6009","status":"public","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","intvolume":" 40","oa_version":"Preprint"},{"ec_funded":1,"volume":2018,"date_created":"2019-02-13T13:26:27Z","date_updated":"2024-03-28T23:30:34Z","related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"full_name":"Goharshady, Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir"},{"full_name":"Okati, Nastaran","first_name":"Nastaran","last_name":"Okati"}],"publisher":"IJCAI","department":[{"_id":"KrCh"}],"publication_status":"published","year":"2018","publication_identifier":{"issn":["10450823"],"isbn":["978-099924112-7"]},"month":"07","language":[{"iso":"eng"}],"doi":"10.24963/ijcai.2018/653","conference":{"end_date":"2018-07-19","start_date":"2018-07-13","location":"Stockholm, Sweden","name":"IJCAI: International Joint Conference on Artificial Intelligence"},"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"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","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"quality_controlled":"1","isi":1,"oa":1,"external_id":{"arxiv":["1804.08984"],"isi":["000764175404118"]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.08984"}],"abstract":[{"text":"We consider the stochastic shortest path (SSP)problem for succinct Markov decision processes(MDPs), where the MDP consists of a set of vari-ables, and a set of nondeterministic rules that up-date the variables. First, we show that several ex-amples from the AI literature can be modeled assuccinct MDPs. Then we present computationalapproaches for upper and lower bounds for theSSP problem: (a) for computing upper bounds, ourmethod is polynomial-time in the implicit descrip-tion of the MDP; (b) for lower bounds, we present apolynomial-time (in the size of the implicit descrip-tion) reduction to quadratic programming. Our ap-proach is applicable even to infinite-state MDPs.Finally, we present experimental results to demon-strate the effectiveness of our approach on severalclassical examples from the AI literature.","lang":"eng"}],"type":"conference","oa_version":"Preprint","intvolume":" 2018","status":"public","title":"Computational approaches for stochastic shortest path on succinct MDPs","_id":"5977","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","day":"17","scopus_import":"1","date_published":"2018-07-17T00:00:00Z","page":"4700-4707","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","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","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.","ista":"Chatterjee K, Fu H, Goharshady AK, Okati N. 2018. Computational approaches for stochastic shortest path on succinct MDPs. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4700–4707.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, N. Okati, in:, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4700–4707.","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.","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."},"publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence"},{"month":"11","doi":"10.1073/pnas.1810565115","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pubmed/30429320"}],"external_id":{"isi":["000451351000063"],"pmid":["30429320"]},"oa":1,"project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","isi":1,"ec_funded":1,"related_material":{"record":[{"id":"10293","status":"public","relation":"dissertation_contains"}],"link":[{"url":"https://ist.ac.at/en/news/no-cooperation-without-open-communication/","relation":"press_release","description":"News on IST Homepage"}]},"author":[{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","first_name":"Christian","last_name":"Hilbe","full_name":"Hilbe, Christian"},{"full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid","first_name":"Laura"},{"first_name":"Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"volume":115,"date_created":"2018-12-11T11:44:05Z","date_updated":"2024-03-28T23:30:45Z","pmid":1,"year":"2018","department":[{"_id":"KrCh"}],"publisher":"National Academy of Sciences","publication_status":"published","article_processing_charge":"No","day":"27","scopus_import":"1","date_published":"2018-11-27T00:00:00Z","citation":{"short":"C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, M. Nowak, PNAS 115 (2018) 12241–12246.","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.","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.","ama":"Hilbe C, Schmid L, Tkadlec J, Chatterjee K, Nowak M. Indirect reciprocity with private, noisy, and incomplete information. PNAS. 2018;115(48):12241-12246. doi:10.1073/pnas.1810565115","ieee":"C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, and M. Nowak, “Indirect reciprocity with private, noisy, and incomplete information,” PNAS, vol. 115, no. 48. National Academy of Sciences, pp. 12241–12246, 2018.","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","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."},"publication":"PNAS","page":"12241-12246","issue":"48","abstract":[{"lang":"eng","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."}],"type":"journal_article","oa_version":"Submitted Version","_id":"2","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","intvolume":" 115","status":"public","title":"Indirect reciprocity with private, noisy, and incomplete information"},{"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","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","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.","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","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.","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","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.","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.","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","article_processing_charge":"No","day":"07","scopus_import":"1","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"},{"full_name":"Morgan, Carroll","first_name":"Carroll","last_name":"Morgan"},{"first_name":"Benjamin Lucien","last_name":"Kaminski","full_name":"Kaminski, Benjamin Lucien"},{"last_name":"Katoen","first_name":"Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Association for Computing Machinery","publication_status":"published","year":"2017","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.","article_number":"33","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","oa":1,"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158121","open_access":"1"}],"external_id":{"arxiv":["1711.03588"]},"publication_identifier":{"eissn":["2475-1421"]},"month":"12"},{"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Monika H","last_name":"Henzinger","first_name":"Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Loitzenbauer","first_name":"Veronika","full_name":"Loitzenbauer, Veronika"}],"related_material":{"record":[{"id":"1661","relation":"earlier_version","status":"public"}]},"date_updated":"2023-02-23T10:08:55Z","date_created":"2018-12-11T11:46:37Z","volume":13,"year":"2017","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"International Federation of Computational Logic","file_date_updated":"2020-07-14T12:46:32Z","publist_id":"7357","ec_funded":1,"article_number":"26","doi":"10.23638/LMCS-13(3:26)2017","language":[{"iso":"eng"}],"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"},"external_id":{"arxiv":["1410.0833"]},"oa":1,"quality_controlled":"1","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"month":"09","publication_identifier":{"issn":["1860-5974"]},"pubrep_id":"956","file":[{"file_name":"IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":582940,"file_id":"5010","relation":"main_file","date_created":"2018-12-12T10:13:27Z","date_updated":"2020-07-14T12:46:32Z","checksum":"12d469ae69b80361333d7dead965cf5d"}],"oa_version":"Published Version","_id":"464","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"status":"public","title":"Improved algorithms for parity and Streett objectives","intvolume":" 13","abstract":[{"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.","lang":"eng"}],"issue":"3","type":"journal_article","date_published":"2017-09-26T00:00:00Z","publication":"Logical Methods in Computer Science","citation":{"short":"K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, Logical Methods in Computer Science 13 (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.","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.","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","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.","ista":"Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26."},"day":"26","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1"},{"date_updated":"2023-02-23T12:26:16Z","date_created":"2018-12-11T11:46:38Z","volume":13,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Křetínská","first_name":"Zuzana","full_name":"Křetínská, Zuzana"},{"first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1657"},{"id":"5429","relation":"earlier_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5435"}]},"publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"International Federation of Computational Logic","year":"2017","file_date_updated":"2020-07-14T12:46:33Z","ec_funded":1,"publist_id":"7355","article_number":"15","language":[{"iso":"eng"}],"doi":"10.23638/LMCS-13(2:15)2017","quality_controlled":"1","project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"grant_number":"701309","_id":"2590DB08-B435-11E9-9278-68D0E5697425","name":"Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020)","call_identifier":"H2020"}],"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"},"month":"07","publication_identifier":{"issn":["18605974"]},"file":[{"file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf","access_level":"open_access","creator":"system","file_size":511832,"content_type":"application/pdf","file_id":"5354","relation":"main_file","date_created":"2018-12-12T10:18:32Z","date_updated":"2020-07-14T12:46:33Z","checksum":"bfa405385ec6229ad5ead89ab5751639"}],"oa_version":"Published Version","pubrep_id":"957","ddc":["004"],"title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","status":"public","intvolume":" 13","_id":"466","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","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. "}],"issue":"2","type":"journal_article","date_published":"2017-07-03T00:00:00Z","publication":"Logical Methods in Computer Science","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.","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.","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"},"day":"03","has_accepted_license":"1","scopus_import":1},{"month":"12","publication_identifier":{"issn":["15293785"]},"doi":"10.1145/3152769","language":[{"iso":"eng"}],"oa":1,"external_id":{"arxiv":["1606.03598"]},"main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}],"quality_controlled":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publist_id":"7354","ec_funded":1,"article_number":"31","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1656"},{"status":"public","relation":"earlier_version","id":"5415"},{"status":"public","relation":"earlier_version","id":"5436"}]},"date_updated":"2023-02-23T12:26:19Z","date_created":"2018-12-11T11:46:38Z","volume":18,"year":"2017","publication_status":"published","publisher":"ACM","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"day":"01","scopus_import":1,"date_published":"2017-12-01T00:00:00Z","publication":"ACM Transactions on Computational Logic (TOCL)","citation":{"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.","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"},"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","_id":"467","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Nested weighted automata","status":"public","intvolume":" 18"},{"year":"2017","publisher":"International Federation of Computational Logic","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","related_material":{"record":[{"id":"1610","status":"public","relation":"earlier_version"},{"id":"5438","status":"public","relation":"earlier_version"}]},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"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":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"volume":13,"date_created":"2018-12-11T11:46:37Z","date_updated":"2023-02-23T12:26:25Z","ec_funded":1,"publist_id":"7356","file_date_updated":"2020-07-14T12:46:33Z","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":[{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"}],"quality_controlled":"1","doi":"10.23638/LMCS-13(3:23)2017","language":[{"iso":"eng"}],"publication_identifier":{"issn":["18605974"]},"month":"09","_id":"465","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 13","ddc":["004"],"title":"Edit distance for pushdown automata","status":"public","pubrep_id":"955","file":[{"creator":"system","file_size":279071,"content_type":"application/pdf","access_level":"open_access","file_name":"IST-2015-321-v1+1_main.pdf","checksum":"08041379ba408d40664f449eb5907a8f","date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:14:37Z","file_id":"5090","relation":"main_file"},{"date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:14:38Z","checksum":"08041379ba408d40664f449eb5907a8f","relation":"main_file","file_id":"5091","content_type":"application/pdf","file_size":279071,"creator":"system","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","access_level":"open_access"}],"oa_version":"Published Version","type":"journal_article","issue":"3","abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"citation":{"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","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.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:23)2017.","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."},"publication":"Logical Methods in Computer Science","date_published":"2017-09-13T00:00:00Z","scopus_import":1,"has_accepted_license":"1","day":"13"}]