[{"language":[{"iso":"eng"}],"isi":1,"month":"09","status":"public","publisher":"Springer","type":"journal_article","date_published":"2021-09-01T00:00:00Z","external_id":{"arxiv":["1504.07384"],"isi":["000645490300001"]},"project":[{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"page":"401-428","day":"01","quality_controlled":"1","arxiv":1,"intvolume":"        57","department":[{"_id":"KrCh"}],"ec_funded":1,"date_updated":"2023-10-10T11:13:20Z","publication":"Formal Methods in System Design","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus"},{"first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":57,"oa":1,"citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. 2021;57:401-428. doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 57, 401–428.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System Design</i>, vol. 57. Springer, pp. 401–428, 2021.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57, Springer, 2021, pp. 401–28, doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>. Springer, 2021. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>."},"year":"2021","abstract":[{"text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.","lang":"eng"}],"date_created":"2021-05-16T22:01:47Z","_id":"9393","scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/1504.07384","open_access":"1"}],"doi":"10.1007/s10703-021-00373-5","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","publication_identifier":{"eissn":["1572-8102"],"issn":["0925-9856"]},"article_type":"original","title":"Faster algorithms for quantitative verification in bounded treewidth graphs","publication_status":"published","article_processing_charge":"No","oa_version":"Preprint"},{"page":"166 - 207","day":"01","quality_controlled":"1","pubrep_id":"960","issue":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","publisher":"Springer","external_id":{"isi":["000419955500006"]},"date_published":"2018-01-01T00:00:00Z","type":"journal_article","language":[{"iso":"eng"}],"ddc":["000"],"month":"01","isi":1,"status":"public","publist_id":"6929","doi":"10.1007/s11241-017-9293-4","scopus_import":"1","title":"Automated competitive analysis of real time scheduling with graph games","publication_status":"published","file_date_updated":"2020-07-14T12:47:56Z","oa_version":"Published Version","article_processing_charge":"No","year":"2018","citation":{"ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “Automated competitive analysis of real time scheduling with graph games,” <i>Real-Time Systems</i>, vol. 54, no. 1. Springer, pp. 166–207, 2018.","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.","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. Automated competitive analysis of real time scheduling with graph games. <i>Real-Time Systems</i>. 2018;54(1):166-207. doi:<a href=\"https://doi.org/10.1007/s11241-017-9293-4\">10.1007/s11241-017-9293-4</a>","mla":"Chatterjee, Krishnendu, et al. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” <i>Real-Time Systems</i>, vol. 54, no. 1, Springer, 2018, pp. 166–207, doi:<a href=\"https://doi.org/10.1007/s11241-017-9293-4\">10.1007/s11241-017-9293-4</a>.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” <i>Real-Time Systems</i>. Springer, 2018. <a href=\"https://doi.org/10.1007/s11241-017-9293-4\">https://doi.org/10.1007/s11241-017-9293-4</a>.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., &#38; Schmid, U. (2018). Automated competitive analysis of real time scheduling with graph games. <i>Real-Time Systems</i>. Springer. <a href=\"https://doi.org/10.1007/s11241-017-9293-4\">https://doi.org/10.1007/s11241-017-9293-4</a>","short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54 (2018) 166–207."},"abstract":[{"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. ","lang":"eng"}],"_id":"738","date_created":"2018-12-11T11:48:14Z","file":[{"content_type":"application/pdf","file_id":"5267","creator":"system","checksum":"c2590ef160709d8054cf29ee173f1454","file_name":"IST-2018-960-v1+1_2017_Chatterjee_Automated_competetive.pdf","access_level":"open_access","date_updated":"2020-07-14T12:47:56Z","relation":"main_file","date_created":"2018-12-12T10:17:14Z","file_size":1163507}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","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"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"2820"}]},"volume":54,"intvolume":"        54","department":[{"_id":"KrCh"}],"publication":"Real-Time Systems","ec_funded":1,"date_updated":"2023-09-27T12:52:38Z"},{"scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1710.00675"}],"publication_status":"published","title":"Sensor synthesis for POMDPs with reachability objectives","article_processing_charge":"No","oa_version":"Preprint","citation":{"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.","ama":"Chatterjee K, Chemlík M, Topcu U. Sensor synthesis for POMDPs with reachability objectives. In: Vol 2018. AAAI Press; 2018:47-55.","mla":"Chatterjee, Krishnendu, et al. <i>Sensor Synthesis for POMDPs with Reachability Objectives</i>. Vol. 2018, 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.","apa":"Chatterjee, K., Chemlík, M., &#38; 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.","short":"K. Chatterjee, M. Chemlík, U. Topcu, in:, AAAI Press, 2018, pp. 47–55."},"year":"2018","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."}],"conference":{"start_date":"2018-06-24","name":"ICAPS: International Conference on Automated Planning and Scheduling","location":"Delft, Netherlands","end_date":"2018-06-29"},"date_created":"2018-12-11T11:44:16Z","_id":"34","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chemlík, Martin","first_name":"Martin","last_name":"Chemlík"},{"first_name":"Ufuk","last_name":"Topcu","full_name":"Topcu, Ufuk"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","volume":2018,"oa":1,"arxiv":1,"intvolume":"      2018","department":[{"_id":"KrCh"}],"ec_funded":1,"date_updated":"2023-09-19T14:44:14Z","page":"47 - 55","day":"01","quality_controlled":"1","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publisher":"AAAI Press","type":"conference","date_published":"2018-06-01T00:00:00Z","external_id":{"isi":["000492986200006"],"arxiv":["1710.00675"]},"language":[{"iso":"eng"}],"alternative_title":["ICAPS"],"isi":1,"month":"06","publist_id":"8021","status":"public"},{"publist_id":"6009","status":"public","isi":1,"month":"03","ddc":["004","006"],"language":[{"iso":"eng"}],"type":"journal_article","date_published":"2017-03-01T00:00:00Z","external_id":{"isi":["000388430000011"]},"publisher":"Elsevier","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","pubrep_id":"717","quality_controlled":"1","day":"01","page":"144 - 170","date_updated":"2023-09-20T11:15:31Z","ec_funded":1,"publication":"Journal of Computer and System Sciences","department":[{"_id":"KrCh"}],"intvolume":"        84","volume":84,"oa":1,"related_material":{"record":[{"id":"2305","status":"public","relation":"earlier_version"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"first_name":"Antonín","last_name":"Kučera","full_name":"Kučera, Antonín"}],"file":[{"checksum":"91271b23cf884d7c06d33bef0cd623b1","file_id":"4885","creator":"system","content_type":"application/pdf","file_size":708657,"date_created":"2018-12-12T10:11:30Z","date_updated":"2020-07-14T12:44:42Z","relation":"main_file","access_level":"open_access","file_name":"IST-2016-717-v1+1_1-s2.0-S0022000016300897-main.pdf"}],"date_created":"2018-12-11T11:51:12Z","_id":"1294","abstract":[{"lang":"eng","text":"We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints."}],"citation":{"short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and System Sciences 84 (2017) 144–170.","apa":"Brázdil, T., Chatterjee, K., Forejt, V., &#38; Kučera, A. (2017). Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>.","mla":"Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>, vol. 84, Elsevier, 2017, pp. 144–70, doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>.","ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2017. Trading performance for stability in Markov decision processes. Journal of Computer and System Sciences. 84, 144–170.","ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance for stability in Markov decision processes,” <i>Journal of Computer and System Sciences</i>, vol. 84. Elsevier, pp. 144–170, 2017.","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. 2017;84:144-170. doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>"},"year":"2017","oa_version":"Published Version","article_processing_charge":"No","file_date_updated":"2020-07-14T12:44:42Z","publication_status":"published","title":"Trading performance for stability in Markov decision processes","scopus_import":"1","doi":"10.1016/j.jcss.2016.09.009"},{"day":"01","page":"236 - 259","quality_controlled":"1","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publisher":"Academic Press","type":"journal_article","date_published":"2017-09-01T00:00:00Z","language":[{"iso":"eng"}],"publist_id":"6963","status":"public","month":"09","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the RICH Model Toolkit (ICT COST Action IC0901), and was carried out in partial fulfillment of the requirements for the Ph.D. degree of the second author.","scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1210.3141","open_access":"1"}],"doi":"10.1016/j.jcss.2017.04.005","oa_version":"Preprint","publication_status":"published","title":"Hyperplane separation technique for multidimensional mean-payoff games","abstract":[{"text":"We consider finite-state and recursive game graphs with multidimensional mean-payoff objectives. In recursive games two types of strategies are relevant: global strategies and modular strategies. Our contributions are: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of weights are fixed; whereas for arbitrary dimensions the problem is coNP-complete. (2) We show that one-player recursive games with multidimensional mean-payoff objectives can be solved in polynomial time. Both above algorithms are based on hyperplane separation technique. (3) For recursive games we show that under modular strategies the multidimensional problem is undecidable. We show that if the number of modules, exits, and the maximal absolute value of the weights are fixed, then one-dimensional recursive mean-payoff games under modular strategies can be solved in polynomial time, whereas for unbounded number of exits or modules the problem is NP-hard.","lang":"eng"}],"citation":{"ama":"Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional mean-payoff games. <i>Journal of Computer and System Sciences</i>. 2017;88:236-259. doi:<a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">10.1016/j.jcss.2017.04.005</a>","ieee":"K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional mean-payoff games,” <i>Journal of Computer and System Sciences</i>, vol. 88. Academic Press, pp. 236–259, 2017.","ista":"Chatterjee K, Velner Y. 2017. Hyperplane separation technique for multidimensional mean-payoff games. Journal of Computer and System Sciences. 88, 236–259.","mla":"Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” <i>Journal of Computer and System Sciences</i>, vol. 88, Academic Press, 2017, pp. 236–59, doi:<a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">10.1016/j.jcss.2017.04.005</a>.","apa":"Chatterjee, K., &#38; Velner, Y. (2017). Hyperplane separation technique for multidimensional mean-payoff games. <i>Journal of Computer and System Sciences</i>. Academic Press. <a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">https://doi.org/10.1016/j.jcss.2017.04.005</a>","short":"K. Chatterjee, Y. Velner, Journal of Computer and System Sciences 88 (2017) 236–259.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” <i>Journal of Computer and System Sciences</i>. Academic Press, 2017. <a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">https://doi.org/10.1016/j.jcss.2017.04.005</a>."},"year":"2017","date_created":"2018-12-11T11:48:07Z","_id":"717","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"}],"volume":88,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"2329"}]},"oa":1,"intvolume":"        88","date_updated":"2023-02-23T10:38:15Z","ec_funded":1,"publication":"Journal of Computer and System Sciences","department":[{"_id":"KrCh"}]},{"abstract":[{"lang":"eng","text":"Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms."}],"year":"2017","citation":{"ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” <i>Information and Computation</i>, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. <i>Information and Computation</i>. 2017;254(2):143-166. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2017). Quantitative fair simulation games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>"},"_id":"1066","date_created":"2018-12-11T11:49:58Z","doi":"10.1016/j.ic.2016.10.006","scopus_import":"1","article_processing_charge":"No","oa_version":"None","publication_status":"published","title":"Quantitative fair simulation games","intvolume":"       254","publication":"Information and Computation","date_updated":"2023-09-20T12:07:48Z","ec_funded":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"related_material":{"record":[{"id":"5428","relation":"earlier_version","status":"public"}]},"volume":254,"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"issue":"2","day":"01","page":"143 - 166","quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","publist_id":"6322","month":"06","isi":1,"publisher":"Elsevier","external_id":{"isi":["000402025600002"]},"date_published":"2017-06-01T00:00:00Z","type":"journal_article"},{"publication":"ACM Transactions on Computational Logic (TOCL)","date_updated":"2023-02-23T12:26:19Z","ec_funded":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"intvolume":"        18","arxiv":1,"oa":1,"related_material":{"record":[{"id":"1656","relation":"earlier_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5415"},{"status":"public","relation":"earlier_version","id":"5436"}]},"volume":18,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"_id":"467","date_created":"2018-12-11T11:46:38Z","abstract":[{"lang":"eng","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."}],"article_number":"31","year":"2017","citation":{"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,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>."},"oa_version":"Preprint","title":"Nested weighted automata","publication_status":"published","publication_identifier":{"issn":["15293785"]},"doi":"10.1145/3152769","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1606.03598"}],"scopus_import":1,"status":"public","publist_id":"7354","month":"12","language":[{"iso":"eng"}],"external_id":{"arxiv":["1606.03598"]},"date_published":"2017-12-01T00:00:00Z","type":"journal_article","publisher":"ACM","project":[{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"issue":"4","quality_controlled":"1","day":"01"},{"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"issue":"5","quality_controlled":"1","day":"01","page":"878 - 911","status":"public","publist_id":"5718","month":"08","language":[{"iso":"eng"}],"external_id":{"arxiv":["1309.2802"]},"date_published":"2016-08-01T00:00:00Z","type":"journal_article","publisher":"Elsevier","_id":"1477","date_created":"2018-12-11T11:52:15Z","abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) for POMDPs with all parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples."}],"year":"2016","citation":{"ama":"Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable Markov decision processes with ω-regular objectives. <i>Journal of Computer and System Sciences</i>. 2016;82(5):878-911. doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">10.1016/j.jcss.2016.02.009</a>","ista":"Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 82(5), 878–911.","ieee":"K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially observable Markov decision processes with ω-regular objectives,” <i>Journal of Computer and System Sciences</i>, vol. 82, no. 5. Elsevier, pp. 878–911, 2016.","mla":"Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” <i>Journal of Computer and System Sciences</i>, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">10.1016/j.jcss.2016.02.009</a>.","apa":"Chatterjee, K., Chmelik, M., &#38; Tracol, M. (2016). What is decidable about partially observable Markov decision processes with ω-regular objectives. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">https://doi.org/10.1016/j.jcss.2016.02.009</a>","short":"K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences 82 (2016) 878–911.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">https://doi.org/10.1016/j.jcss.2016.02.009</a>."},"oa_version":"Preprint","title":"What is decidable about partially observable Markov decision processes with ω-regular objectives","publication_status":"published","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1309.2802"}],"doi":"10.1016/j.jcss.2016.02.009","scopus_import":1,"publication":"Journal of Computer and System Sciences","date_updated":"2023-02-23T12:24:38Z","ec_funded":1,"department":[{"_id":"KrCh"}],"intvolume":"        82","arxiv":1,"oa":1,"related_material":{"record":[{"id":"2295","status":"public","relation":"earlier_version"},{"relation":"earlier_version","status":"public","id":"5400"}]},"volume":82,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"first_name":"Mathieu","last_name":"Tracol","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","full_name":"Tracol, Mathieu"}]},{"abstract":[{"lang":"eng","text":"Simple board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in the development of mathematical and logical skills, but also in the emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. We present an approach that generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. The presence of such states for standard game variants like 4×4 Tic-Tac-Toe opens up new games to be played that have never been played as the default start state is heavily biased. "}],"citation":{"chicago":"Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, 2:745–52. AAAI Press, 2015.","short":"U. Ahmed, K. Chatterjee, S. Gulwani, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI Press, 2015, pp. 745–752.","apa":"Ahmed, U., Chatterjee, K., &#38; Gulwani, S. (2015). Automatic generation of alternative starting positions for simple traditional board games. In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i> (Vol. 2, pp. 745–752). Austin, TX, USA: AAAI Press.","mla":"Ahmed, Umair, et al. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, vol. 2, AAAI Press, 2015, pp. 745–52.","ieee":"U. Ahmed, K. Chatterjee, and S. Gulwani, “Automatic generation of alternative starting positions for simple traditional board games,” in <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, Austin, TX, USA, 2015, vol. 2, pp. 745–752.","ista":"Ahmed U, Chatterjee K, Gulwani S. 2015. Automatic generation of alternative starting positions for simple traditional board games. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2, 745–752.","ama":"Ahmed U, Chatterjee K, Gulwani S. Automatic generation of alternative starting positions for simple traditional board games. In: <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>. Vol 2. AAAI Press; 2015:745-752."},"year":"2015","date_created":"2018-12-11T11:52:16Z","_id":"1481","conference":{"start_date":"2015-01-25","location":"Austin, TX, USA","name":"AAAI: Conference on Artificial Intelligence","end_date":"2015-01-30"},"acknowledgement":"A Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/146.\r\n","scopus_import":1,"main_file_link":[{"url":"https://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/download/9523/9300","open_access":"1"}],"oa_version":"None","article_processing_charge":"No","title":"Automatic generation of alternative starting positions for simple traditional board games","publication_status":"published","intvolume":"         2","date_updated":"2023-02-23T12:25:07Z","ec_funded":1,"publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Ahmed","first_name":"Umair","full_name":"Ahmed, Umair"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Sumit","last_name":"Gulwani","full_name":"Gulwani, Sumit"}],"volume":2,"related_material":{"record":[{"id":"5410","relation":"earlier_version","status":"public"}]},"oa":1,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"day":"01","page":"745 - 752","quality_controlled":"1","language":[{"iso":"eng"}],"publist_id":"5713","status":"public","month":"01","publisher":"AAAI Press","type":"conference","date_published":"2015-01-01T00:00:00Z"},{"project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"issue":"2","quality_controlled":"1","day":"01","page":"230 - 264","status":"public","publist_id":"5677","month":"10","language":[{"iso":"eng"}],"date_published":"2015-10-01T00:00:00Z","type":"journal_article","publisher":"Springer","_id":"1501","date_created":"2018-12-11T11:52:23Z","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. "}],"year":"2015","citation":{"ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” <i>Formal Methods in System Design</i>, vol. 47, no. 2. Springer, pp. 230–264, 2015.","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. 2015;47(2):230-264. doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>","apa":"Chatterjee, K., Chmelik, M., &#38; Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>.","mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>."},"oa_version":"Preprint","publication_status":"published","title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","doi":"10.1007/s10703-015-0235-2","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1405.0835"}],"scopus_import":1,"publication":"Formal Methods in System Design","date_updated":"2023-09-07T11:58:33Z","ec_funded":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"intvolume":"        47","related_material":{"record":[{"id":"1155","status":"public","relation":"dissertation_contains"}]},"oa":1,"volume":47,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","first_name":"Przemyslaw"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Joglekar, Manas","first_name":"Manas","last_name":"Joglekar"},{"first_name":"Nisarg","last_name":"Shah","full_name":"Shah, Nisarg"}],"related_material":{"record":[{"id":"2715","relation":"earlier_version","status":"public"}]},"oa":1,"volume":573,"intvolume":"       573","arxiv":1,"publication":"Theoretical Computer Science","date_updated":"2023-02-23T10:55:03Z","ec_funded":1,"department":[{"_id":"KrCh"}],"acknowledgement":"The research was supported by FWF Grant No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start Grant (279307: Graph Games), and the Microsoft Faculty Fellows Award. Nisarg Shah is also supported by NSF Grant CCF-1215883.\r\n","main_file_link":[{"url":"http://arxiv.org/abs/1202.4175","open_access":"1"}],"doi":"10.1016/j.tcs.2015.01.050","scopus_import":1,"oa_version":"Preprint","article_processing_charge":"No","publication_status":"published","title":"Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives","abstract":[{"text":"We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives, and examine the problem of computing the set of almost-sure winning vertices such that the objective can be ensured with probability 1 from these vertices. We study for the first time the average-case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average-case running time is linear (as compared to the worst-case linear number of iterations and quadratic time complexity). Second, for the average-case analysis over all MDPs we show that the expected number of iterations is constant and the average-case running time is linear (again as compared to the worst-case linear number of iterations and quadratic time complexity). Finally we also show that when all MDPs are equally likely, the probability that the classical algorithm requires more than a constant number of iterations is exponentially small.","lang":"eng"}],"year":"2015","citation":{"mla":"Chatterjee, Krishnendu, et al. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>, vol. 573, no. 3, Elsevier, 2015, pp. 71–89, doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>.","short":"K. Chatterjee, M. Joglekar, N. Shah, Theoretical Computer Science 573 (2015) 71–89.","chicago":"Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>.","apa":"Chatterjee, K., Joglekar, M., &#38; Shah, N. (2015). Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>","ama":"Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. 2015;573(3):71-89. doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>","ista":"Chatterjee K, Joglekar M, Shah N. 2015. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. Theoretical Computer Science. 573(3), 71–89.","ieee":"K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives,” <i>Theoretical Computer Science</i>, vol. 573, no. 3. Elsevier, pp. 71–89, 2015."},"_id":"1598","date_created":"2018-12-11T11:52:56Z","publisher":"Elsevier","date_published":"2015-03-30T00:00:00Z","external_id":{"arxiv":["1202.4175"]},"type":"journal_article","language":[{"iso":"eng"}],"status":"public","publist_id":"5571","month":"03","day":"30","page":"71 - 89","quality_controlled":"1","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"issue":"3"},{"oa_version":"Preprint","publication_status":"published","title":"Faster algorithms for algebraic path properties in recursive state machines with constant treewidth","acknowledgement":"We thank anonymous reviewers for helpful comments to improve the presentation of the paper.","scopus_import":1,"doi":"10.1145/2676726.2676979","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1410.7724"}],"date_created":"2018-12-11T11:52:58Z","_id":"1602","conference":{"name":"SIGPLAN: Symposium on Principles of Programming Languages","location":"Mumbai, India","end_date":"2015-01-17","start_date":"2015-01-15"},"abstract":[{"text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks.","lang":"eng"}],"citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. 2015;50(1):97-109. doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, and P. Goyal, “Faster algorithms for algebraic path properties in recursive state machines with constant treewidth,” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1. ACM, pp. 97–109, 2015.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. 2015. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 50(1), 97–109.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1, ACM, 2015, pp. 97–109, doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.","apa":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., &#38; Goyal, P. (2015). Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>"},"year":"2015","volume":50,"oa":1,"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"821"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Prateesh","last_name":"Goyal","full_name":"Goyal, Prateesh"}],"date_updated":"2023-09-07T12:01:58Z","ec_funded":1,"publication":"ACM SIGPLAN Notices","department":[{"_id":"KrCh"}],"intvolume":"        50","arxiv":1,"quality_controlled":"1","day":"01","page":"97 - 109","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"issue":"1","type":"journal_article","date_published":"2015-01-01T00:00:00Z","external_id":{"arxiv":["1410.7724"]},"publisher":"ACM","publist_id":"5565","status":"public","month":"01","language":[{"iso":"eng"}]},{"month":"01","publist_id":"5563","status":"public","language":[{"iso":"eng"}],"type":"journal_article","date_published":"2015-01-01T00:00:00Z","publisher":"ACM","issue":"1","project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"pubrep_id":"523","quality_controlled":"1","page":"539 - 551","day":"01","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T12:01:59Z","ec_funded":1,"publication":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT ","intvolume":"        50","volume":50,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5445"},{"id":"821","status":"public","relation":"dissertation_contains"}]},"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Mumbai, India","name":"SIGPLAN: Symposium on Principles of Programming Languages","end_date":"2015-01-17","start_date":"2015-01-15"},"date_created":"2018-12-11T11:52:59Z","_id":"1604","citation":{"apa":"Chatterjee, K., Pavlogiannis, A., &#38; Velner, Y. (2015). Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>.","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT  50 (2015) 539–551.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1, ACM, 2015, pp. 539–51, doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>.","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. 2015;50(1):539-551. doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural analysis,” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1. ACM, pp. 539–551, 2015.","ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551."},"year":"2015","abstract":[{"text":"We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs.","lang":"eng"}],"publication_status":"published","title":"Quantitative interprocedural analysis","oa_version":"None","scopus_import":1,"doi":"10.1145/2676726.2676968","publication_identifier":{"isbn":["978-1-4503-3300-9"]}},{"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","doi":"10.1007/978-3-319-21690-4_9","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1504.07384"}],"scopus_import":1,"oa_version":"Preprint","publication_status":"published","title":"Faster algorithms for quantitative verification in constant treewidth graphs","abstract":[{"text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.","lang":"eng"}],"year":"2015","citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification, LNCS, vol. 9206, 140–157.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in constant treewidth graphs,” presented at the CAV: Computer Aided Verification, San Francisco, CA, USA, 2015, vol. 9206, pp. 140–157.","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. Vol. 9206, Springer, 2015, pp. 140–57, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157). Presented at the CAV: Computer Aided Verification, San Francisco, CA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,” 9206:140–57. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>."},"_id":"1607","date_created":"2018-12-11T11:52:59Z","conference":{"end_date":"2015-07-24","location":"San Francisco, CA, USA","name":"CAV: Computer Aided Verification","start_date":"2015-07-18"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5430"},{"id":"5437","status":"public","relation":"earlier_version"},{"id":"821","status":"public","relation":"dissertation_contains"}]},"oa":1,"volume":9206,"intvolume":"      9206","ec_funded":1,"date_updated":"2023-09-07T12:01:59Z","department":[{"_id":"KrCh"}],"day":"16","page":"140 - 157","quality_controlled":"1","project":[{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publisher":"Springer","date_published":"2015-07-16T00:00:00Z","type":"conference","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"status":"public","publist_id":"5560","month":"07"},{"_id":"1610","date_created":"2018-12-11T11:53:01Z","conference":{"name":"ICALP: Automata, Languages and Programming","location":"Kyoto, Japan","end_date":"2015-07-10","start_date":"2015-07-06"},"abstract":[{"lang":"eng","text":"The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 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 pushdown automata 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 deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k."}],"year":"2015","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 121–133.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd International Colloquium</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>"},"oa_version":"None","article_processing_charge":"No","title":"Edit distance for pushdown automata","publication_status":"published","publication_identifier":{"isbn":["978-3-662-47665-9"]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.08259"}],"doi":"10.1007/978-3-662-47666-6_10","scopus_import":"1","publication":"42nd International Colloquium","ec_funded":1,"date_updated":"2023-02-23T12:26:24Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"intvolume":"      9135","arxiv":1,"oa":1,"related_material":{"record":[{"status":"public","relation":"later_version","id":"465"},{"relation":"earlier_version","status":"public","id":"5438"}]},"volume":9135,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"project":[{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"issue":"Part II","pubrep_id":"321","quality_controlled":"1","day":"01","page":"121 - 133","status":"public","publist_id":"5556","month":"07","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"date_published":"2015-07-01T00:00:00Z","external_id":{"arxiv":["1504.08259"]},"type":"conference","publisher":"Springer Nature"},{"language":[{"iso":"eng"}],"ddc":["000"],"status":"public","publist_id":"5536","month":"11","publisher":"Nature Publishing Group","date_published":"2015-11-25T00:00:00Z","type":"journal_article","pubrep_id":"466","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)"},"has_accepted_license":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"day":"25","quality_controlled":"1","intvolume":"         5","publication":"Scientific Reports","ec_funded":1,"date_updated":"2021-01-12T06:52:05Z","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Adlam, Ben","first_name":"Ben","last_name":"Adlam"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"oa":1,"volume":5,"abstract":[{"lang":"eng","text":"Population structure can facilitate evolution of cooperation. In a structured population, cooperators can form clusters which resist exploitation by defectors. Recently, it was observed that a shift update rule is an extremely strong amplifier of cooperation in a one dimensional spatial model. For the shift update rule, an individual is chosen for reproduction proportional to fecundity; the offspring is placed next to the parent; a random individual dies. Subsequently, the population is rearranged (shifted) until all individual cells are again evenly spaced out. For large population size and a one dimensional population structure, the shift update rule favors cooperation for any benefit-to-cost ratio greater than one. But every attempt to generalize shift updating to higher dimensions while maintaining its strong effect has failed. The reason is that in two dimensions the clusters are fragmented by the movements caused by rearranging the cells. Here we introduce the natural phenomenon of a repulsive force between cells of different types. After a birth and death event, the cells are being rearranged minimizing the overall energy expenditure. If the repulsive force is sufficiently high, shift becomes a strong promoter of cooperation in two dimensions."}],"article_number":"17147","year":"2015","citation":{"short":"A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).","chicago":"Pavlogiannis, Andreas, Krishnendu Chatterjee, Ben Adlam, and Martin Nowak. “Cellular Cooperation with Shift Updating and Repulsion.” <i>Scientific Reports</i>. Nature Publishing Group, 2015. <a href=\"https://doi.org/10.1038/srep17147\">https://doi.org/10.1038/srep17147</a>.","apa":"Pavlogiannis, A., Chatterjee, K., Adlam, B., &#38; Nowak, M. (2015). Cellular cooperation with shift updating and repulsion. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/srep17147\">https://doi.org/10.1038/srep17147</a>","mla":"Pavlogiannis, Andreas, et al. “Cellular Cooperation with Shift Updating and Repulsion.” <i>Scientific Reports</i>, vol. 5, 17147, Nature Publishing Group, 2015, doi:<a href=\"https://doi.org/10.1038/srep17147\">10.1038/srep17147</a>.","ama":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. Cellular cooperation with shift updating and repulsion. <i>Scientific Reports</i>. 2015;5. doi:<a href=\"https://doi.org/10.1038/srep17147\">10.1038/srep17147</a>","ieee":"A. Pavlogiannis, K. Chatterjee, B. Adlam, and M. Nowak, “Cellular cooperation with shift updating and repulsion,” <i>Scientific Reports</i>, vol. 5. Nature Publishing Group, 2015.","ista":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. 2015. Cellular cooperation with shift updating and repulsion. Scientific Reports. 5, 17147."},"_id":"1624","date_created":"2018-12-11T11:53:06Z","file":[{"checksum":"38e06d8310d2087cae5f6d4d4bfe082b","content_type":"application/pdf","creator":"system","file_id":"4947","date_updated":"2020-07-14T12:45:07Z","relation":"main_file","date_created":"2018-12-12T10:12:29Z","file_size":1021931,"file_name":"IST-2016-466-v1+1_srep17147.pdf","access_level":"open_access"}],"acknowledgement":"The research was supported by the Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft Faculty Fellows award. Support from the John Templeton foundation is gratefully acknowledged.","doi":"10.1038/srep17147","scopus_import":1,"file_date_updated":"2020-07-14T12:45:07Z","oa_version":"Published Version","publication_status":"published","title":"Cellular cooperation with shift updating and repulsion"},{"date_created":"2018-12-11T11:53:17Z","_id":"1656","conference":{"end_date":"2015-07-10","name":"LICS: Logic in Computer Science","location":"Kyoto, Japan","start_date":"2015-07-06"},"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, nor in any other know 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 run-time 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"}],"citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). Nested weighted automata. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174926, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174926.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>"},"article_number":"7174926","year":"2015","oa_version":"None","publication_status":"published","title":"Nested weighted automata","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.\r\nA Technical Report of the paper is available at: \r\nhttps://repository.ist.ac.at/331/\r\n","scopus_import":1,"doi":"10.1109/LICS.2015.72","date_updated":"2023-02-23T12:26:19Z","ec_funded":1,"publication":"Proceedings - Symposium on Logic in Computer Science","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"arxiv":1,"volume":"2015-July","related_material":{"record":[{"relation":"later_version","status":"public","id":"467"},{"status":"public","relation":"earlier_version","id":"5415"},{"relation":"earlier_version","status":"public","id":"5436"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"project":[{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","day":"31","publist_id":"5494","status":"public","month":"07","language":[{"iso":"eng"}],"type":"conference","date_published":"2015-07-31T00:00:00Z","external_id":{"arxiv":["1606.03598"]},"publisher":"IEEE"},{"oa_version":"None","title":"Quantitative temporal simulation and refinement distances for timed systems","quality_controlled":"1","publication_status":"published","day":"24","scopus_import":1,"page":"2291 - 2306","doi":"10.1109/TAC.2015.2404612","date_created":"2018-12-11T11:53:30Z","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"_id":"1694","issue":"9","abstract":[{"lang":"eng","text":"\r\nWe introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata.\r\n"}],"citation":{"chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 2015. <a href=\"https://doi.org/10.1109/TAC.2015.2404612\">https://doi.org/10.1109/TAC.2015.2404612</a>.","short":"K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015) 2291–2306.","apa":"Chatterjee, K., &#38; Prabhu, V. (2015). Quantitative temporal simulation and refinement distances for timed systems. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/TAC.2015.2404612\">https://doi.org/10.1109/TAC.2015.2404612</a>","mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 9, IEEE, 2015, pp. 2291–306, doi:<a href=\"https://doi.org/10.1109/TAC.2015.2404612\">10.1109/TAC.2015.2404612</a>.","ieee":"K. Chatterjee and V. Prabhu, “Quantitative temporal simulation and refinement distances for timed systems,” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 9. IEEE, pp. 2291–2306, 2015.","ista":"Chatterjee K, Prabhu V. 2015. Quantitative temporal simulation and refinement distances for timed systems. IEEE Transactions on Automatic Control. 60(9), 2291–2306.","ama":"Chatterjee K, Prabhu V. Quantitative temporal simulation and refinement distances for timed systems. <i>IEEE Transactions on Automatic Control</i>. 2015;60(9):2291-2306. doi:<a href=\"https://doi.org/10.1109/TAC.2015.2404612\">10.1109/TAC.2015.2404612</a>"},"year":"2015","volume":60,"type":"journal_article","date_published":"2015-02-24T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Prabhu, Vinayak","first_name":"Vinayak","last_name":"Prabhu"}],"publisher":"IEEE","date_updated":"2021-01-12T06:52:34Z","publist_id":"5450","ec_funded":1,"status":"public","publication":"IEEE Transactions on Automatic Control","department":[{"_id":"KrCh"}],"month":"02","intvolume":"        60","language":[{"iso":"eng"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Rabinovich, Alexander","last_name":"Rabinovich","first_name":"Alexander"},{"last_name":"Raskin","first_name":"Jean","full_name":"Raskin, Jean"}],"volume":241,"oa":1,"intvolume":"       241","ec_funded":1,"date_updated":"2021-01-12T06:52:36Z","publication":"Information and Computation","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148), ERC Start grant (279499: inVEST).","scopus_import":1,"main_file_link":[{"url":"http://arxiv.org/abs/1209.3234","open_access":"1"}],"doi":"10.1016/j.ic.2015.03.001","oa_version":"Preprint","title":"The complexity of multi-mean-payoff and multi-energy games","publication_status":"published","abstract":[{"lang":"eng","text":"In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf objectives are coNP-complete."}],"citation":{"ieee":"Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J. Raskin, “The complexity of multi-mean-payoff and multi-energy games,” <i>Information and Computation</i>, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.","ista":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015. The complexity of multi-mean-payoff and multi-energy games. Information and Computation. 241(4), 177–196.","ama":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. 2015;241(4):177-196. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>","mla":"Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” <i>Information and Computation</i>, vol. 241, no. 4, Elsevier, 2015, pp. 177–96, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>.","short":"Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.","apa":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &#38; Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>","chicago":"Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger, Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>."},"year":"2015","date_created":"2018-12-11T11:53:32Z","_id":"1698","publisher":"Elsevier","type":"journal_article","date_published":"2015-04-01T00:00:00Z","language":[{"iso":"eng"}],"publist_id":"5443","status":"public","month":"04","day":"01","page":"177 - 196","quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7"}],"issue":"4"},{"publisher":"Royal Society","pmid":1,"external_id":{"pmid":["26180069"]},"date_published":"2015-07-15T00:00:00Z","type":"journal_article","language":[{"iso":"eng"}],"status":"public","publist_id":"5425","month":"07","day":"15","quality_controlled":"1","project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"issue":"1812","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Reiter","first_name":"Johannes","full_name":"Reiter, Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353"},{"first_name":"Ayush","last_name":"Kanodia","full_name":"Kanodia, Ayush"},{"full_name":"Gupta, Raghav","last_name":"Gupta","first_name":"Raghav"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"}],"oa":1,"related_material":{"record":[{"id":"1400","relation":"dissertation_contains","status":"public"}]},"volume":282,"intvolume":"       282","publication":"Proceedings of the Royal Society of London Series B Biological Sciences","date_updated":"2023-09-07T11:40:43Z","department":[{"_id":"KrCh"}],"article_type":"original","acknowledgement":"This work was supported by grants from the John Templeton Foundation, ERC Start Grant (279307: Graph Games), FWF NFN Grant (No S11407N23 RiSE/SHiNE), FWF Grant (No P23499N23) and a Microsoft faculty fellows award.","doi":"10.1098/rspb.2015.1041","main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4528522/"}],"scopus_import":1,"oa_version":"Submitted Version","article_processing_charge":"No","title":"Biological auctions with multiple rewards","publication_status":"published","abstract":[{"text":"The competition for resources among cells, individuals or species is a fundamental characteristic of evolution. Biological all-pay auctions have been used to model situations where multiple individuals compete for a single resource. However, in many situations multiple resources with various values exist and single reward auctions are not applicable. We generalize the model to multiple rewards and study the evolution of strategies. In biological all-pay auctions the bid of an individual corresponds to its strategy and is equivalent to its payment in the auction. The decreasingly ordered rewards are distributed according to the decreasingly ordered bids of the participating individuals. The reproductive success of an individual is proportional to its fitness given by the sum of the rewards won minus its payments. Hence, successful bidding strategies spread in the population. We find that the results for the multiple reward case are very different from the single reward case. While the mixed strategy equilibrium in the single reward case with more than two players consists of mostly low-bidding individuals, we show that the equilibrium can convert to many high-bidding individuals and a few low-bidding individuals in the multiple reward case. Some reward values lead to a specialization among the individuals where one subpopulation competes for the rewards and the other subpopulation largely avoids costly competitions. Whether the mixed strategy equilibrium is an evolutionarily stable strategy (ESS) depends on the specific values of the rewards.","lang":"eng"}],"year":"2015","citation":{"ieee":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, and K. Chatterjee, “Biological auctions with multiple rewards,” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812. Royal Society, 2015.","ista":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. 2015. Biological auctions with multiple rewards. Proceedings of the Royal Society of London Series B Biological Sciences. 282(1812).","ama":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. 2015;282(1812). doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>","mla":"Reiter, Johannes, et al. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812, Royal Society, 2015, doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>.","apa":"Reiter, J., Kanodia, A., Gupta, R., Nowak, M., &#38; Chatterjee, K. (2015). Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>","short":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of the Royal Society of London Series B Biological Sciences 282 (2015).","chicago":"Reiter, Johannes, Ayush Kanodia, Raghav Gupta, Martin Nowak, and Krishnendu Chatterjee. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society, 2015. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>."},"_id":"1709","date_created":"2018-12-11T11:53:35Z"}]