[{"doi":"10.1007/978-3-319-63387-9_6","date_published":"2017-01-01T00:00:00Z","date_created":"2018-12-11T11:47:35Z","page":"118 - 139","day":"01","year":"2017","publisher":"Springer","quality_controlled":"1","oa":1,"title":"Automated recurrence analysis for almost linear expected runtime bounds","editor":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"full_name":"Kunčak, Viktor","last_name":"Kunčak","first_name":"Viktor"}],"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Hongfei","full_name":"Fu, Hongfei","last_name":"Fu"},{"last_name":"Murhekar","full_name":"Murhekar, Aniket","first_name":"Aniket"}],"publist_id":"7166","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 118–39, doi:10.1007/978-3-319-63387-9_6.","ieee":"K. Chatterjee, H. Fu, and A. Murhekar, “Automated recurrence analysis for almost linear expected runtime bounds,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 118–139.","short":"K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 118–139.","apa":"Chatterjee, K., Fu, H., & Murhekar, A. (2017). Automated recurrence analysis for almost linear expected runtime bounds. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 118–139). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_6","ama":"Chatterjee K, Fu H, Murhekar A. Automated recurrence analysis for almost linear expected runtime bounds. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:118-139. doi:10.1007/978-3-319-63387-9_6","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Aniket Murhekar. “Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds.” edited by Rupak Majumdar and Viktor Kunčak, 10426:118–39. Springer, 2017. https://doi.org/10.1007/978-3-319-63387-9_6.","ista":"Chatterjee K, Fu H, Murhekar A. 2017. Automated recurrence analysis for almost linear expected runtime bounds. CAV: Computer Aided Verification, LNCS, vol. 10426, 118–139."},"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"volume":10426,"ec_funded":1,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-331963386-2"]},"publication_status":"published","month":"01","intvolume":" 10426","alternative_title":["LNCS"],"scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1705.00314","open_access":"1"}],"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. The motivation is that several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear or almost-linear (O(log n), O(n), O(n · log n), respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. The experimental results show that our approach can efficiently derive asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select, Coupon-Collector, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic expected-runtime complexity, or quadratic as compared to linear or almost-linear expected-runtime complexity), or ineffective."}],"department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T08:06:55Z","status":"public","type":"conference","conference":{"name":"CAV: Computer Aided Verification","location":"Heidelberg, Germany","end_date":"2017-07-28","start_date":"2017-07-24"},"_id":"628"},{"volume":10426,"ec_funded":1,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-331963386-2"]},"publication_status":"published","month":"07","intvolume":" 10426","alternative_title":["LNCS"],"scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1705.02326","open_access":"1"}],"oa_version":"Submitted Version","abstract":[{"text":"Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stopping criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stopping criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks.","lang":"eng"}],"department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T08:07:32Z","status":"public","type":"conference","conference":{"start_date":"2017-07-24","end_date":"2017-07-28","location":"Heidelberg, Germany","name":"CAV: Computer Aided Verification"},"_id":"645","doi":"10.1007/978-3-319-63387-9_10","date_published":"2017-07-13T00:00:00Z","date_created":"2018-12-11T11:47:41Z","page":"201 - 221","day":"13","year":"2017","quality_controlled":"1","publisher":"Springer","oa":1,"title":"Value iteration for long run average reward in markov decision processes","editor":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"last_name":"Kunčak","full_name":"Kunčak, Viktor","first_name":"Viktor"}],"author":[{"first_name":"Pranav","last_name":"Ashok","full_name":"Ashok, Pranav"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","last_name":"Daca"},{"orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"},{"first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias"}],"publist_id":"7135","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer, 2017. https://doi.org/10.1007/978-3-319-63387-9_10.","ista":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration for long run average reward in markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 10426, 201–221.","mla":"Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.","apa":"Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., & Meggendorfer, T. (2017). Value iteration for long run average reward in markov decision processes. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_10","ama":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration for long run average reward in markov decision processes. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:201-221. doi:10.1007/978-3-319-63387-9_10","short":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.","ieee":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value iteration for long run average reward in markov decision processes,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 201–221."},"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}]}]