[{"conference":{"start_date":"2013-04-08","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2013-04-11","location":"Philadelphia, PA, United States"},"publication_identifier":{"isbn":["978-1-4503-1567-8 "]},"month":"04","day":"01","oa_version":"None","abstract":[{"lang":"eng","text":"In this paper, we introduce the powerful framework of graph games for the analysis of real-time scheduling with firm deadlines. We introduce a novel instance of a partial-observation game that is suitable for this purpose, and prove decidability of all the involved decision problems. We derive a graph game that allows the automated computation of the competitive ratio (along with an optimal witness algorithm for the competitive ratio) and establish an NP-completeness proof for the graph game problem. For a given on-line algorithm, we present polynomial time solution for computing (i) the worst-case utility; (ii) the worst-case utility ratio w.r.t. a clairvoyant off-line algorithm; and (iii) the competitive ratio. A major strength of the proposed approach lies in its flexibility w.r.t. incorporating additional constraints on the adversary and/or the algorithm, including limited maximum or average load, finiteness of periods of overload, etc., which are easily added by means of additional instances of standard objective functions for graph games. "}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kößler, Alexander","first_name":"Alexander","last_name":"Kößler"},{"first_name":"Ulrich","full_name":"Schmid, Ulrich","last_name":"Schmid"}],"publication_status":"published","publisher":"ACM","date_published":"2013-04-01T00:00:00Z","status":"public","type":"conference","department":[{"_id":"KrCh"}],"page":"163 - 172","quality_controlled":"1","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"related_material":{"record":[{"id":"738","relation":"later_version","status":"public"}]},"scopus_import":1,"date_updated":"2023-09-27T12:52:38Z","year":"2013","publist_id":"3981","date_created":"2018-12-11T11:59:46Z","citation":{"apa":"Chatterjee, K., Kößler, A., &#38; Schmid, U. (2013). Automated analysis of real-time scheduling using graph games. In <i>Proceedings of the 16th International conference on Hybrid systems: Computation and control</i> (pp. 163–172). Philadelphia, PA, United States: ACM. <a href=\"https://doi.org/10.1145/2461328.2461356\">https://doi.org/10.1145/2461328.2461356</a>","short":"K. Chatterjee, A. Kößler, U. Schmid, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, ACM, 2013, pp. 163–172.","ama":"Chatterjee K, Kößler A, Schmid U. Automated analysis of real-time scheduling using graph games. In: <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2013:163-172. doi:<a href=\"https://doi.org/10.1145/2461328.2461356\">10.1145/2461328.2461356</a>","ieee":"K. Chatterjee, A. Kößler, and U. Schmid, “Automated analysis of real-time scheduling using graph games,” in <i>Proceedings of the 16th International conference on Hybrid systems: Computation and control</i>, Philadelphia, PA, United States, 2013, pp. 163–172.","mla":"Chatterjee, Krishnendu, et al. “Automated Analysis of Real-Time Scheduling Using Graph Games.” <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2013, pp. 163–72, doi:<a href=\"https://doi.org/10.1145/2461328.2461356\">10.1145/2461328.2461356</a>.","chicago":"Chatterjee, Krishnendu, Alexander Kößler, and Ulrich Schmid. “Automated Analysis of Real-Time Scheduling Using Graph Games.” In <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>, 163–72. ACM, 2013. <a href=\"https://doi.org/10.1145/2461328.2461356\">https://doi.org/10.1145/2461328.2461356</a>.","ista":"Chatterjee K, Kößler A, Schmid U. 2013. Automated analysis of real-time scheduling using graph games. Proceedings of the 16th International conference on Hybrid systems: Computation and control. HSCC: Hybrid Systems - Computation and Control, 163–172."},"title":"Automated analysis of real-time scheduling using graph games","publication":"Proceedings of the 16th International conference on Hybrid systems: Computation and control","doi":"10.1145/2461328.2461356","language":[{"iso":"eng"}],"_id":"2820"},{"language":[{"iso":"eng"}],"_id":"2824","publication":"Information and Computation","doi":"10.1016/j.ic.2013.04.003","date_updated":"2021-01-12T06:59:58Z","year":"2013","date_created":"2018-12-11T11:59:47Z","publist_id":"3977","title":"Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems","citation":{"apa":"Chatterjee, K., &#38; Prabhu, V. (2013). Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">https://doi.org/10.1016/j.ic.2013.04.003</a>","short":"K. Chatterjee, V. Prabhu, Information and Computation 228–229 (2013) 83–119.","ieee":"K. Chatterjee and V. Prabhu, “Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems,” <i>Information and Computation</i>, vol. 228–229. Elsevier, pp. 83–119, 2013.","ama":"Chatterjee K, Prabhu V. Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. <i>Information and Computation</i>. 2013;228-229:83-119. doi:<a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">10.1016/j.ic.2013.04.003</a>","mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient, Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” <i>Information and Computation</i>, vol. 228–229, Elsevier, 2013, pp. 83–119, doi:<a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">10.1016/j.ic.2013.04.003</a>.","ista":"Chatterjee K, Prabhu V. 2013. Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. Information and Computation. 228–229, 83–119.","chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient, Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” <i>Information and Computation</i>. Elsevier, 2013. <a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">https://doi.org/10.1016/j.ic.2013.04.003</a>."},"ec_funded":1,"scopus_import":1,"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publisher":"Elsevier","status":"public","type":"journal_article","date_published":"2013-04-24T00:00:00Z","page":"83-119","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":"228-229","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Prabhu","first_name":"Vinayak","full_name":"Prabhu, Vinayak"}],"publication_status":"published","month":"04","day":"24","oa_version":"None","abstract":[{"text":"We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a Zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a logarithmic (in the number of clocks) number of memory bits (i.e. a linear number of memory states). Precisely, we show that for safety objectives, a memory of size (3 + lg (| C | + 1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential memory states bound. We also settle the open question of whether winning region-based strategies require memory for safety objectives by showing with an example the necessity of memory for such strategies to win for safety objectives. Finally, we show that the decision problem of determining if there exists a receptive player-1 winning strategy for safety objectives is EXPTIME-complete over timed automaton games.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"_id":"2831","doi":"10.1007/s10703-012-0180-2","citation":{"apa":"Chatterjee, K., Henzinger, M. H., Joglekar, M., &#38; Shah, N. (2013). Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-012-0180-2\">https://doi.org/10.1007/s10703-012-0180-2</a>","mla":"Chatterjee, Krishnendu, et al. “Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives.” <i>Formal Methods in System Design</i>, vol. 42, no. 3, Springer, 2013, pp. 301–27, doi:<a href=\"https://doi.org/10.1007/s10703-012-0180-2\">10.1007/s10703-012-0180-2</a>.","ista":"Chatterjee K, Henzinger MH, Joglekar M, Shah N. 2013. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. 42(3), 301–327.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Manas Joglekar, and Nisarg Shah. “Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives.” <i>Formal Methods in System Design</i>. Springer, 2013. <a href=\"https://doi.org/10.1007/s10703-012-0180-2\">https://doi.org/10.1007/s10703-012-0180-2</a>.","short":"K. Chatterjee, M.H. Henzinger, M. Joglekar, N. Shah, Formal Methods in System Design 42 (2013) 301–327.","ama":"Chatterjee K, Henzinger MH, Joglekar M, Shah N. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. <i>Formal Methods in System Design</i>. 2013;42(3):301-327. doi:<a href=\"https://doi.org/10.1007/s10703-012-0180-2\">10.1007/s10703-012-0180-2</a>","ieee":"K. Chatterjee, M. H. Henzinger, M. Joglekar, and N. Shah, “Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives,” <i>Formal Methods in System Design</i>, vol. 42, no. 3. Springer, pp. 301–327, 2013."},"publist_id":"3968","date_created":"2018-12-11T11:59:49Z","year":"2013","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3342"}]},"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"page":"301 - 327","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":42,"publisher":"Springer","date_published":"2013-06-01T00:00:00Z","publication_status":"published","external_id":{"arxiv":["1104.3348"]},"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes O(n · √ m) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes O(n · √ n) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(n · √ K) symbolic steps, where K is the maximal number of edges of strongly connected components (scc's) of the MDP. The win-lose algorithm requires symbolic computation of scc's. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5×n symbolic steps, whereas our new algorithm takes 4×n symbolic steps."}],"language":[{"iso":"eng"}],"publication":"Formal Methods in System Design","title":"Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives","oa":1,"date_updated":"2023-02-23T11:23:04Z","issue":"3","article_processing_charge":"No","scopus_import":"1","intvolume":"        42","type":"journal_article","status":"public","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"last_name":"Joglekar","first_name":"Manas","full_name":"Joglekar, Manas"},{"last_name":"Shah","first_name":"Nisarg","full_name":"Shah, Nisarg"}],"arxiv":1,"main_file_link":[{"url":"http://arxiv.org/abs/1104.3348","open_access":"1"}],"day":"01","oa_version":"Preprint","user_id":"72615eeb-f1f3-11ec-aa25-d4573ddc34fd","month":"06"},{"external_id":{"arxiv":["1004.2697"]},"abstract":[{"text":"We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents and the trusted third party as path formulas in linear temporal logic and prove that the satisfaction of these objectives imply fairness; a property required of fair exchange protocols. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of AGS as follows: (a) any solution of AGS is attack-free; no subset of participants can violate the objectives of the other participants; (b) the Asokan-Shoup-Waidner certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch non-repudiation protocol is a solution of AGS; and (d) AGS presents a new and symmetric fair non-repudiation protocol that is attack-free. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can both automatically discover vulnerabilities in protocols and generate correct protocols. The solution to AGS can be computed efficiently as the secure equilibrium solution of three-player graph games. ","lang":"eng"}],"publication_status":"published","page":"825 - 859","department":[{"_id":"KrCh"}],"volume":26,"quality_controlled":"1","publisher":"Springer","date_published":"2013-07-04T00:00:00Z","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"citation":{"ama":"Chatterjee K, Raman V. Assume-guarantee synthesis for digital contract signing. <i>Formal Aspects of Computing</i>. 2013;26(4):825-859. doi:<a href=\"https://doi.org/10.1007/s00165-013-0283-6\">10.1007/s00165-013-0283-6</a>","ieee":"K. Chatterjee and V. Raman, “Assume-guarantee synthesis for digital contract signing,” <i>Formal Aspects of Computing</i>, vol. 26, no. 4. Springer, pp. 825–859, 2013.","short":"K. Chatterjee, V. Raman, Formal Aspects of Computing 26 (2013) 825–859.","ista":"Chatterjee K, Raman V. 2013. Assume-guarantee synthesis for digital contract signing. Formal Aspects of Computing. 26(4), 825–859.","mla":"Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis for Digital Contract Signing.” <i>Formal Aspects of Computing</i>, vol. 26, no. 4, Springer, 2013, pp. 825–59, doi:<a href=\"https://doi.org/10.1007/s00165-013-0283-6\">10.1007/s00165-013-0283-6</a>.","chicago":"Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis for Digital Contract Signing.” <i>Formal Aspects of Computing</i>. Springer, 2013. <a href=\"https://doi.org/10.1007/s00165-013-0283-6\">https://doi.org/10.1007/s00165-013-0283-6</a>.","apa":"Chatterjee, K., &#38; Raman, V. (2013). Assume-guarantee synthesis for digital contract signing. <i>Formal Aspects of Computing</i>. Springer. <a href=\"https://doi.org/10.1007/s00165-013-0283-6\">https://doi.org/10.1007/s00165-013-0283-6</a>"},"date_created":"2018-12-11T11:59:51Z","publist_id":"3963","year":"2013","doi":"10.1007/s00165-013-0283-6","_id":"2836","oa_version":"Preprint","main_file_link":[{"url":"http://arxiv.org/abs/1004.2697","open_access":"1"}],"day":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Raman","full_name":"Raman, Vishwanath","first_name":"Vishwanath"}],"arxiv":1,"type":"journal_article","status":"public","scopus_import":1,"intvolume":"        26","title":"Assume-guarantee synthesis for digital contract signing","oa":1,"date_updated":"2021-01-12T07:00:06Z","issue":"4","publication":"Formal Aspects of Computing","language":[{"iso":"eng"}]},{"publication":"Journal of Computer and System Sciences","language":[{"iso":"eng"}],"has_accepted_license":"1","intvolume":"        79","scopus_import":1,"issue":"5","article_processing_charge":"No","date_updated":"2021-01-12T07:00:16Z","oa":1,"pubrep_id":"388","title":"Strategy improvement for concurrent reachability and turn based stochastic safety games","status":"public","type":"journal_article","month":"08","file":[{"date_created":"2018-12-12T10:18:48Z","date_updated":"2020-07-14T12:45:51Z","checksum":"6d3ee12cceb946a0abe69594b6a22409","file_id":"5370","file_name":"IST-2015-388-v1+1_1-s2.0-S0022000012001778-main.pdf","content_type":"application/pdf","file_size":425488,"access_level":"open_access","relation":"main_file","creator":"system"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"Published Version","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"De Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"doi":"10.1016/j.jcss.2012.12.001","article_type":"original","_id":"2854","file_date_updated":"2020-07-14T12:45:51Z","ec_funded":1,"year":"2013","acknowledgement":"This work was partially supported in part by the NSF grants CCR-0132780, CNS-0720884, CCR-0225610, by the Swiss National Science Foundation, ERC Start Grant Graph Games (Project No. 279307), FWF NFN Grant S11407-N23 (RiSE), and a Microsoft faculty fellows","publist_id":"3938","citation":{"ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for concurrent reachability and turn based stochastic safety games,” <i>Journal of Computer and System Sciences</i>, vol. 79, no. 5. Elsevier, pp. 640–657, 2013.","ama":"Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent reachability and turn based stochastic safety games. <i>Journal of Computer and System Sciences</i>. 2013;79(5):640-657. doi:<a href=\"https://doi.org/10.1016/j.jcss.2012.12.001\">10.1016/j.jcss.2012.12.001</a>","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, Journal of Computer and System Sciences 79 (2013) 640–657.","mla":"Chatterjee, Krishnendu, et al. “Strategy Improvement for Concurrent Reachability and Turn Based Stochastic Safety Games.” <i>Journal of Computer and System Sciences</i>, vol. 79, no. 5, Elsevier, 2013, pp. 640–57, doi:<a href=\"https://doi.org/10.1016/j.jcss.2012.12.001\">10.1016/j.jcss.2012.12.001</a>.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy Improvement for Concurrent Reachability and Turn Based Stochastic Safety Games.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2013. <a href=\"https://doi.org/10.1016/j.jcss.2012.12.001\">https://doi.org/10.1016/j.jcss.2012.12.001</a>.","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2013. Strategy improvement for concurrent reachability and turn based stochastic safety games. Journal of Computer and System Sciences. 79(5), 640–657.","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2013). Strategy improvement for concurrent reachability and turn based stochastic safety games. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2012.12.001\">https://doi.org/10.1016/j.jcss.2012.12.001</a>"},"date_created":"2018-12-11T11:59:57Z","date_published":"2013-08-01T00:00:00Z","publisher":"Elsevier","quality_controlled":"1","volume":79,"page":"640 - 657","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"ddc":["000"],"abstract":[{"text":"We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. First, we present a simple proof of the fact that in concurrent reachability games, for all ε&gt;0, memoryless ε-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an ε-optimal strategy achieves the objective with probability within ε of the value of the game. In contrast to previous proofs of this fact, our proof is more elementary and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives. Finally, we present a strategy-improvement algorithm for turn-based stochastic games (where each player selects moves in turns) with safety objectives. Our algorithms yield sequences of player-1 strategies which ensure probabilities of winning that converge monotonically (from below) to the value of the game. © 2012 Elsevier Inc.","lang":"eng"}],"publication_status":"published"},{"intvolume":"         6","has_accepted_license":"1","scopus_import":1,"title":"The effect of one additional driver mutation on tumor progression","pubrep_id":"415","date_updated":"2023-09-07T11:40:43Z","oa":1,"issue":"1","publication":"Evolutionary Applications","language":[{"iso":"eng"}],"oa_version":"Published Version","day":"01","file":[{"date_updated":"2020-07-14T12:45:51Z","date_created":"2018-12-12T10:15:50Z","checksum":"e2955b3889f8a823c3d5a72cb16f8957","file_id":"5173","file_name":"IST-2016-415-v1+1_Reiter_et_al-2013-Evolutionary_Applications.pdf","access_level":"open_access","file_size":1172037,"content_type":"application/pdf","relation":"main_file","creator":"system"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","author":[{"first_name":"Johannes","full_name":"Reiter, Johannes","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353"},{"first_name":"Ivana","full_name":"Božić, Ivana","last_name":"Božić"},{"first_name":"Benjamin","full_name":"Allen, Benjamin","last_name":"Allen","id":"135B5B70-E9D2-11E9-BD74-BB415DA2B523"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"status":"public","type":"journal_article","ec_funded":1,"related_material":{"record":[{"id":"1400","relation":"dissertation_contains","status":"public"}]},"date_created":"2018-12-11T11:59:58Z","publist_id":"3931","citation":{"apa":"Reiter, J., Božić, I., Allen, B., Chatterjee, K., &#38; Nowak, M. (2013). The effect of one additional driver mutation on tumor progression. <i>Evolutionary Applications</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1111/eva.12020\">https://doi.org/10.1111/eva.12020</a>","short":"J. Reiter, I. Božić, B. Allen, K. Chatterjee, M. Nowak, Evolutionary Applications 6 (2013) 34–45.","ama":"Reiter J, Božić I, Allen B, Chatterjee K, Nowak M. The effect of one additional driver mutation on tumor progression. <i>Evolutionary Applications</i>. 2013;6(1):34-45. doi:<a href=\"https://doi.org/10.1111/eva.12020\">10.1111/eva.12020</a>","ieee":"J. Reiter, I. Božić, B. Allen, K. Chatterjee, and M. Nowak, “The effect of one additional driver mutation on tumor progression,” <i>Evolutionary Applications</i>, vol. 6, no. 1. Wiley-Blackwell, pp. 34–45, 2013.","ista":"Reiter J, Božić I, Allen B, Chatterjee K, Nowak M. 2013. The effect of one additional driver mutation on tumor progression. Evolutionary Applications. 6(1), 34–45.","mla":"Reiter, Johannes, et al. “The Effect of One Additional Driver Mutation on Tumor Progression.” <i>Evolutionary Applications</i>, vol. 6, no. 1, Wiley-Blackwell, 2013, pp. 34–45, doi:<a href=\"https://doi.org/10.1111/eva.12020\">10.1111/eva.12020</a>.","chicago":"Reiter, Johannes, Ivana Božić, Benjamin Allen, Krishnendu Chatterjee, and Martin Nowak. “The Effect of One Additional Driver Mutation on Tumor Progression.” <i>Evolutionary Applications</i>. Wiley-Blackwell, 2013. <a href=\"https://doi.org/10.1111/eva.12020\">https://doi.org/10.1111/eva.12020</a>."},"year":"2013","doi":"10.1111/eva.12020","file_date_updated":"2020-07-14T12:45:51Z","_id":"2858","abstract":[{"lang":"eng","text":"Tumor growth is caused by the acquisition of driver mutations, which enhance the net reproductive rate of cells. Driver mutations may increase cell division, reduce cell death, or allow cells to overcome density-limiting effects. We study the dynamics of tumor growth as one additional driver mutation is acquired. Our models are based on two-type branching processes that terminate in either tumor disappearance or tumor detection. In our first model, both cell types grow exponentially, with a faster rate for cells carrying the additional driver. We find that the additional driver mutation does not affect the survival probability of the lesion, but can substantially reduce the time to reach the detectable size if the lesion is slow growing. In our second model, cells lacking the additional driver cannot exceed a fixed carrying capacity, due to density limitations. In this case, the time to detection depends strongly on this carrying capacity. Our model provides a quantitative framework for studying tumor dynamics during different stages of progression. We observe that early, small lesions need additional drivers, while late stage metastases are only marginally affected by them. These results help to explain why additional driver mutations are typically not detected in fast-growing metastases."}],"ddc":["570"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publication_status":"published","department":[{"_id":"KrCh"}],"page":"34 - 45","volume":6,"quality_controlled":"1","publisher":"Wiley-Blackwell","date_published":"2013-01-01T00:00:00Z","project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"}]},{"intvolume":"      7721","scopus_import":1,"title":"Controllable-choice message sequence graphs","date_updated":"2020-08-11T10:09:52Z","oa":1,"language":[{"iso":"eng"}],"day":"09","oa_version":"Submitted Version","main_file_link":[{"url":"http://arxiv.org/abs/1209.4499","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2012-10-25","name":"MEMICS: Mathematical and Engineering Methods in Computer Science","end_date":"2012-10-28","location":"Znojmo, Czech Republic"},"month":"01","author":[{"last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","first_name":"Martin"},{"last_name":"Řehák","first_name":"Vojtěch","full_name":"Řehák, Vojtěch"}],"alternative_title":["LNCS"],"type":"conference","status":"public","ec_funded":1,"citation":{"short":"M. Chmelik, V. Řehák, 7721 (2013) 118–130.","ama":"Chmelik M, Řehák V. Controllable-choice message sequence graphs. 2013;7721:118-130. doi:<a href=\"https://doi.org/10.1007/978-3-642-36046-6_12\">10.1007/978-3-642-36046-6_12</a>","ieee":"M. Chmelik and V. Řehák, “Controllable-choice message sequence graphs,” vol. 7721. Springer, pp. 118–130, 2013.","mla":"Chmelik, Martin, and Vojtěch Řehák. <i>Controllable-Choice Message Sequence Graphs</i>. Vol. 7721, Springer, 2013, pp. 118–30, doi:<a href=\"https://doi.org/10.1007/978-3-642-36046-6_12\">10.1007/978-3-642-36046-6_12</a>.","ista":"Chmelik M, Řehák V. 2013. Controllable-choice message sequence graphs. 7721, 118–130.","chicago":"Chmelik, Martin, and Vojtěch Řehák. “Controllable-Choice Message Sequence Graphs.” Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-36046-6_12\">https://doi.org/10.1007/978-3-642-36046-6_12</a>.","apa":"Chmelik, M., &#38; Řehák, V. (2013). Controllable-choice message sequence graphs. Presented at the MEMICS: Mathematical and Engineering Methods in Computer Science, Znojmo, Czech Republic: Springer. <a href=\"https://doi.org/10.1007/978-3-642-36046-6_12\">https://doi.org/10.1007/978-3-642-36046-6_12</a>"},"date_created":"2018-12-11T12:00:09Z","publist_id":"3873","year":"2013","doi":"10.1007/978-3-642-36046-6_12","_id":"2886","abstract":[{"text":"We focus on the realizability problem of Message Sequence Graphs (MSG), i.e. the problem whether a given MSG specification is correctly distributable among parallel components communicating via messages. This fundamental problem of MSG is known to be undecidable. We introduce a well motivated restricted class of MSG, so called controllable-choice MSG, and show that all its models are realizable and moreover it is decidable whether a given MSG model is a member of this class. In more detail, this class of MSG specifications admits a deadlock-free realization by overloading existing messages with additional bounded control data. We also show that the presented class is the largest known subclass of MSG that allows for deadlock-free realization.","lang":"eng"}],"series_title":"Lecture Notes in Computer Science","publication_status":"published","page":"118 - 130","department":[{"_id":"KrCh"}],"volume":7721,"quality_controlled":"1","publisher":"Springer","date_published":"2013-01-09T00:00:00Z","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}]},{"intvolume":"        42","scopus_import":1,"acknowledgement":"This research was supported in part by the National Science Foundation CAREER award CCR-0132780, by the ONR grant N00014-02-1-0671, by the National Science Foundation grants CCR-0427202 and CCR-0234690, and by the ARP award TO.030.MM.D.","date_updated":"2021-01-12T07:41:10Z","year":"2013","issue":"2","title":"Code aware resource management","citation":{"ieee":"K. Chatterjee, L. De Alfaro, M. Faella, R. Majumdar, and V. Raman, “Code aware resource management,” <i>Formal Methods in System Design</i>, vol. 42, no. 2. Springer, pp. 142–174, 2013.","ama":"Chatterjee K, De Alfaro L, Faella M, Majumdar R, Raman V. Code aware resource management. <i>Formal Methods in System Design</i>. 2013;42(2):142-174. doi:<a href=\"https://doi.org/10.1007/s10703-012-0170-4\">10.1007/s10703-012-0170-4</a>","short":"K. Chatterjee, L. De Alfaro, M. Faella, R. Majumdar, V. Raman, Formal Methods in System Design 42 (2013) 142–174.","ista":"Chatterjee K, De Alfaro L, Faella M, Majumdar R, Raman V. 2013. Code aware resource management. Formal Methods in System Design. 42(2), 142–174.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Ritankar Majumdar, and Vishwanath Raman. “Code Aware Resource Management.” <i>Formal Methods in System Design</i>. Springer, 2013. <a href=\"https://doi.org/10.1007/s10703-012-0170-4\">https://doi.org/10.1007/s10703-012-0170-4</a>.","mla":"Chatterjee, Krishnendu, et al. “Code Aware Resource Management.” <i>Formal Methods in System Design</i>, vol. 42, no. 2, Springer, 2013, pp. 142–74, doi:<a href=\"https://doi.org/10.1007/s10703-012-0170-4\">10.1007/s10703-012-0170-4</a>.","apa":"Chatterjee, K., De Alfaro, L., Faella, M., Majumdar, R., &#38; Raman, V. (2013). Code aware resource management. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-012-0170-4\">https://doi.org/10.1007/s10703-012-0170-4</a>"},"publist_id":"3583","date_created":"2018-12-11T12:01:29Z","publication":"Formal Methods in System Design","doi":"10.1007/s10703-012-0170-4","_id":"3116","language":[{"iso":"eng"}],"month":"04","day":"01","oa_version":"None","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Multithreaded programs coordinate their interaction through synchronization primitives like mutexes and semaphores, which are managed by an OS-provided resource manager. We propose algorithms for the automatic construction of code-aware resource managers for multithreaded embedded applications. Such managers use knowledge about the structure and resource usage (mutex and semaphore usage) of the threads to guarantee deadlock freedom and progress while managing resources in an efficient way. Our algorithms compute managers as winning strategies in certain infinite games, and produce a compact code description of these strategies. We have implemented the algorithms in the tool Cynthesis. Given a multithreaded program in C, the tool produces C code implementing a code-aware resource manager. We show in experiments that Cynthesis produces compact resource managers within a few minutes on a set of embedded benchmarks with up to 6 threads. © 2012 Springer Science+Business Media, LLC."}],"publication_status":"published","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"first_name":"Marco","full_name":"Faella, Marco","last_name":"Faella"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"},{"last_name":"Raman","first_name":"Vishwanath","full_name":"Raman, Vishwanath"}],"publisher":"Springer","status":"public","type":"journal_article","date_published":"2013-04-01T00:00:00Z","page":"142 - 174","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":42},{"publication":"CONCUR 2012 - Concurrency Theory","language":[{"iso":"eng"}],"intvolume":"      7454","scopus_import":"1","editor":[{"last_name":"Koutny","first_name":"Maciej","full_name":"Koutny, Maciej"},{"last_name":"Ulidowski","full_name":"Ulidowski, Irek","first_name":"Irek"}],"title":"Strategy synthesis for multi-dimensional quantitative objectives","date_updated":"2023-02-23T10:55:06Z","article_processing_charge":"No","alternative_title":["LNCS"],"type":"conference","status":"public","oa_version":"Preprint","day":"15","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Newcastle upon Tyne, United Kingdom","end_date":"2012-09-07","name":"CONCUR: Conference on Concurrency Theory","start_date":"2012-09-04"},"month":"09","publication_identifier":{"issn":["0302-9743","1611-3349"],"eisbn":["9783642329401"],"isbn":["9783642329395"]},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Randour","full_name":"Randour, Mickael","first_name":"Mickael"},{"first_name":"Jean-François","full_name":"Raskin, Jean-François","last_name":"Raskin"}],"arxiv":1,"doi":"10.1007/978-3-642-32940-1_10","_id":"10904","ec_funded":1,"related_material":{"record":[{"id":"2716","relation":"later_version","status":"public"}]},"citation":{"short":"K. Chatterjee, M. Randour, J.-F. Raskin, in:, M. Koutny, I. Ulidowski (Eds.), CONCUR 2012 - Concurrency Theory, Springer, Berlin, Heidelberg, 2012, pp. 115–131.","ama":"Chatterjee K, Randour M, Raskin J-F. Strategy synthesis for multi-dimensional quantitative objectives. In: Koutny M, Ulidowski I, eds. <i>CONCUR 2012 - Concurrency Theory</i>. Vol 7454. Berlin, Heidelberg: Springer; 2012:115-131. doi:<a href=\"https://doi.org/10.1007/978-3-642-32940-1_10\">10.1007/978-3-642-32940-1_10</a>","ieee":"K. Chatterjee, M. Randour, and J.-F. Raskin, “Strategy synthesis for multi-dimensional quantitative objectives,” in <i>CONCUR 2012 - Concurrency Theory</i>, Newcastle upon Tyne, United Kingdom, 2012, vol. 7454, pp. 115–131.","ista":"Chatterjee K, Randour M, Raskin J-F. 2012. Strategy synthesis for multi-dimensional quantitative objectives. CONCUR 2012 - Concurrency Theory. CONCUR: Conference on Concurrency Theory, LNCS, vol. 7454, 115–131.","mla":"Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” <i>CONCUR 2012 - Concurrency Theory</i>, edited by Maciej Koutny and Irek Ulidowski, vol. 7454, Springer, 2012, pp. 115–31, doi:<a href=\"https://doi.org/10.1007/978-3-642-32940-1_10\">10.1007/978-3-642-32940-1_10</a>.","chicago":"Chatterjee, Krishnendu, Mickael Randour, and Jean-François Raskin. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” In <i>CONCUR 2012 - Concurrency Theory</i>, edited by Maciej Koutny and Irek Ulidowski, 7454:115–31. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-32940-1_10\">https://doi.org/10.1007/978-3-642-32940-1_10</a>.","apa":"Chatterjee, K., Randour, M., &#38; Raskin, J.-F. (2012). Strategy synthesis for multi-dimensional quantitative objectives. In M. Koutny &#38; I. Ulidowski (Eds.), <i>CONCUR 2012 - Concurrency Theory</i> (Vol. 7454, pp. 115–131). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-32940-1_10\">https://doi.org/10.1007/978-3-642-32940-1_10</a>"},"date_created":"2022-03-21T08:00:21Z","acknowledgement":"Author supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407 (RiSE), ERC Start Grant (279307: Graph Games), Microsoft faculty fellowship.","year":"2012","department":[{"_id":"KrCh"}],"page":"115-131","quality_controlled":"1","volume":7454,"publisher":"Springer","date_published":"2012-09-15T00:00:00Z","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"external_id":{"arxiv":["1201.5073"]},"abstract":[{"text":"Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.","lang":"eng"}],"publication_status":"published","place":"Berlin, Heidelberg"},{"date_published":"2012-10-01T00:00:00Z","publisher":"Springer","volume":7501,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"301-312","project":[{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"abstract":[{"text":"Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While the existence of polynomial-time algorithms has been a major open problem for decades, there is no algorithm that solves any non-trivial subclass in polynomial time.\r\nIn this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several counter examples that show that many previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting graph structures need not help.","lang":"eng"}],"external_id":{"arxiv":["1604.08234"]},"publication_status":"published","doi":"10.1007/978-3-642-33090-2_27","_id":"10905","related_material":{"record":[{"id":"535","relation":"later_version","status":"public"}]},"ec_funded":1,"year":"2012","acknowledgement":"Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games), and a Microsoft Faculty Fellows Award","citation":{"chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” In <i>Algorithms – ESA 2012</i>, 7501:301–12. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">https://doi.org/10.1007/978-3-642-33090-2_27</a>.","mla":"Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” <i>Algorithms – ESA 2012</i>, vol. 7501, Springer, 2012, pp. 301–12, doi:<a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">10.1007/978-3-642-33090-2_27</a>.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2012. Polynomial-time algorithms for energy games with special weight structures. Algorithms – ESA 2012. ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.","ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” in <i>Algorithms – ESA 2012</i>, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312.","ama":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. In: <i>Algorithms – ESA 2012</i>. Vol 7501. Springer; 2012:301-312. doi:<a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">10.1007/978-3-642-33090-2_27</a>","short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms – ESA 2012, Springer, 2012, pp. 301–312.","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., &#38; Nanongkai, D. (2012). Polynomial-time algorithms for energy games with special weight structures. In <i>Algorithms – ESA 2012</i> (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">https://doi.org/10.1007/978-3-642-33090-2_27</a>"},"date_created":"2022-03-21T08:01:45Z","type":"conference","status":"public","alternative_title":["LNCS"],"month":"10","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783642330902"],"eissn":["1611-3349"],"isbn":["9783642330896"]},"conference":{"location":"Ljubljana, Slovenia","end_date":"2012-09-12","name":"ESA: European Symposium on Algorithms","start_date":"2012-09-10"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","main_file_link":[{"url":"https://arxiv.org/abs/1604.08234","open_access":"1"}],"oa_version":"Preprint","day":"01","arxiv":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"last_name":"Krinninger","full_name":"Krinninger, Sebastian","first_name":"Sebastian"},{"first_name":"Danupon","full_name":"Nanongkai, Danupon","last_name":"Nanongkai"}],"publication":"Algorithms – ESA 2012","language":[{"iso":"eng"}],"scopus_import":"1","intvolume":"      7501","article_processing_charge":"No","oa":1,"date_updated":"2023-09-05T14:09:30Z","title":"Polynomial-time algorithms for energy games with special weight structures"},{"doi":"10.4230/LIPIcs.FSTTCS.2012.461","_id":"2715","file_date_updated":"2020-07-14T12:45:45Z","related_material":{"record":[{"id":"1598","relation":"later_version","status":"public"}]},"ec_funded":1,"citation":{"short":"K. Chatterjee, M. Joglekar, N. Shah, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 461–473.","ama":"Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. In: Vol 18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2012:461-473. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">10.4230/LIPIcs.FSTTCS.2012.461</a>","ieee":"K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives,” presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India, 2012, vol. 18, pp. 461–473.","chicago":"Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives,” 18:461–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>.","ista":"Chatterjee K, Joglekar M, Shah N. 2012. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 461–473.","mla":"Chatterjee, Krishnendu, et al. <i>Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives</i>. Vol. 18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 461–73, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">10.4230/LIPIcs.FSTTCS.2012.461</a>.","apa":"Chatterjee, K., Joglekar, M., &#38; Shah, N. (2012). Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives (Vol. 18, pp. 461–473). Presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>"},"publist_id":"4180","date_created":"2018-12-11T11:59:13Z","year":"2012","volume":18,"quality_controlled":"1","page":"461 - 473","department":[{"_id":"KrCh"}],"date_published":"2012-12-10T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning vertices from where the objective can be ensured with probability 1. 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 given that all MDPs are equally likely, the probability that the classical algorithm requires more than constant number of iterations is exponentially small."}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"ddc":["000"],"publication_status":"published","language":[{"iso":"eng"}],"intvolume":"        18","scopus_import":1,"has_accepted_license":"1","title":"Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives","date_updated":"2023-02-23T10:06:04Z","oa":1,"pubrep_id":"525","type":"conference","status":"public","alternative_title":["LIPIcs"],"file":[{"access_level":"open_access","relation":"main_file","file_size":519040,"content_type":"application/pdf","creator":"system","date_created":"2018-12-12T10:13:53Z","date_updated":"2020-07-14T12:45:45Z","checksum":"d4d644ed1a885dbfc4fa1ef4c5724dab","file_id":"5040","file_name":"IST-2016-525-v1+1_42_1_.pdf"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","day":"10","month":"12","conference":{"name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","start_date":"2012-12-15","location":"Hyderabad, India","end_date":"2012-12-17"},"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Manas","full_name":"Joglekar, Manas","last_name":"Joglekar"},{"last_name":"Shah","first_name":"Nisarg","full_name":"Shah, Nisarg"}]},{"_id":"2848","doi":"10.1016/j.jtbi.2012.02.021","citation":{"short":"K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.","ieee":"K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations with different learners,” <i>Journal of Theoretical Biology</i>, vol. 301. Elsevier, pp. 161–173, 2012.","ama":"Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations with different learners. <i>Journal of Theoretical Biology</i>. 2012;301:161-173. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">10.1016/j.jtbi.2012.02.021</a>","ista":"Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 301, 161–173.","chicago":"Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical Biology</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">https://doi.org/10.1016/j.jtbi.2012.02.021</a>.","mla":"Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical Biology</i>, vol. 301, Elsevier, 2012, pp. 161–73, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">10.1016/j.jtbi.2012.02.021</a>.","apa":"Chatterjee, K., Zufferey, D., &#38; Nowak, M. (2012). Evolutionary game dynamics in populations with different learners. <i>Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">https://doi.org/10.1016/j.jtbi.2012.02.021</a>"},"date_created":"2018-12-11T11:59:55Z","publist_id":"3946","year":"2012","ec_funded":1,"project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","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","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"161 - 173","quality_controlled":"1","volume":301,"publisher":"Elsevier","date_published":"2012-05-21T00:00:00Z","publication_status":"published","external_id":{"pmid":["22394652"]},"abstract":[{"lang":"eng","text":"We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics."}],"language":[{"iso":"eng"}],"publication":"Journal of Theoretical Biology","title":"Evolutionary game dynamics in populations with different learners","date_updated":"2021-01-12T07:00:12Z","oa":1,"scopus_import":1,"intvolume":"       301","pmid":1,"status":"public","type":"journal_article","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey","full_name":"Zufferey, Damien","first_name":"Damien"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/","open_access":"1"}],"day":"21","oa_version":"Submitted Version","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"05"},{"_id":"2916","doi":"10.4204/EPTCS.96.3","year":"2012","date_created":"2018-12-11T12:00:19Z","citation":{"apa":"Cerny, P., Chmelik, M., Henzinger, T. A., &#38; Radhakrishna, A. (2012). Interface Simulation Distances. In <i>Electronic Proceedings in Theoretical Computer Science</i> (Vol. 96, pp. 29–42). Napoli, Italy: EPTCS. <a href=\"https://doi.org/10.4204/EPTCS.96.3\">https://doi.org/10.4204/EPTCS.96.3</a>","ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2012. Interface Simulation Distances. Electronic Proceedings in Theoretical Computer Science. GandALF: Games, Automata, Logic, and Formal Verification vol. 96, 29–42.","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” <i>Electronic Proceedings in Theoretical Computer Science</i>, vol. 96, EPTCS, 2012, pp. 29–42, doi:<a href=\"https://doi.org/10.4204/EPTCS.96.3\">10.4204/EPTCS.96.3</a>.","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” In <i>Electronic Proceedings in Theoretical Computer Science</i>, 96:29–42. EPTCS, 2012. <a href=\"https://doi.org/10.4204/EPTCS.96.3\">https://doi.org/10.4204/EPTCS.96.3</a>.","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, 2012, pp. 29–42.","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface Simulation Distances. In: <i>Electronic Proceedings in Theoretical Computer Science</i>. Vol 96. EPTCS; 2012:29-42. doi:<a href=\"https://doi.org/10.4204/EPTCS.96.3\">10.4204/EPTCS.96.3</a>","ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface Simulation Distances,” in <i>Electronic Proceedings in Theoretical Computer Science</i>, Napoli, Italy, 2012, vol. 96, pp. 29–42."},"publist_id":"3827","related_material":{"record":[{"status":"public","id":"1733","relation":"later_version"}]},"ec_funded":1,"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_published":"2012-10-07T00:00:00Z","publisher":"EPTCS","volume":96,"quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"page":"29 - 42","publication_status":"published","abstract":[{"text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a quantitative measure for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intu- itively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, and that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.","lang":"eng"}],"external_id":{"arxiv":["1210.2450"]},"language":[{"iso":"eng"}],"publication":"Electronic Proceedings in Theoretical Computer Science","oa":1,"date_updated":"2023-02-23T10:12:05Z","title":"Interface Simulation Distances","scopus_import":1,"intvolume":"        96","type":"conference","status":"public","arxiv":1,"author":[{"full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","full_name":"Radhakrishna, Arjun"}],"month":"10","conference":{"start_date":"2012-09-06","name":"GandALF: Games, Automata, Logic, and Formal Verification","end_date":"2012-09-08","location":"Napoli, Italy"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"http://arxiv.org/abs/1210.2450","open_access":"1"}],"day":"07","oa_version":"Submitted Version"},{"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Prabhu","first_name":"Vinayak","full_name":"Prabhu, Vinayak"}],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1207.7019"}],"oa_version":"Preprint","day":"01","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"name":"EMSOFT: Embedded Software ","start_date":"2012-10-07","location":"Tampere, Finland","end_date":"2012-10-12"},"month":"10","status":"public","type":"conference","title":"Finite automata with time delay blocks","oa":1,"date_updated":"2021-01-12T07:39:53Z","scopus_import":1,"language":[{"iso":"eng"}],"publication":"roceedings of the tenth ACM international conference on Embedded software","publication_status":"published","abstract":[{"lang":"eng","text":"The notion of delays arises naturally in many computational models, such as, in the design of circuits, control systems, and dataflow languages. In this work, we introduce automata with delay blocks (ADBs), extending finite state automata with variable time delay blocks, for deferring individual transition output symbols, in a discrete-time setting. We show that the ADB languages strictly subsume the regular languages, and are incomparable in expressive power to the context-free languages. We show that ADBs are closed under union, concatenation and Kleene star, and under intersection with regular languages, but not closed under complementation and intersection with other ADB languages. We show that the emptiness and the membership problems are decidable in polynomial time for ADBs, whereas the universality problem is undecidable. Finally we consider the linear-time model checking problem, i.e., whether the language of an ADB is contained in a regular language, and show that the model checking problem is PSPACE-complete. Copyright 2012 ACM."}],"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"page":"43 - 52","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","publisher":"ACM","date_published":"2012-10-01T00:00:00Z","publist_id":"3799","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Prabhu, V. (2012). Finite automata with time delay blocks. In <i>roceedings of the tenth ACM international conference on Embedded software</i> (pp. 43–52). Tampere, Finland: ACM. <a href=\"https://doi.org/10.1145/2380356.2380370\">https://doi.org/10.1145/2380356.2380370</a>","ista":"Chatterjee K, Henzinger TA, Prabhu V. 2012. Finite automata with time delay blocks. roceedings of the tenth ACM international conference on Embedded software. EMSOFT: Embedded Software , 43–52.","mla":"Chatterjee, Krishnendu, et al. “Finite Automata with Time Delay Blocks.” <i>Roceedings of the Tenth ACM International Conference on Embedded Software</i>, ACM, 2012, pp. 43–52, doi:<a href=\"https://doi.org/10.1145/2380356.2380370\">10.1145/2380356.2380370</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Finite Automata with Time Delay Blocks.” In <i>Roceedings of the Tenth ACM International Conference on Embedded Software</i>, 43–52. ACM, 2012. <a href=\"https://doi.org/10.1145/2380356.2380370\">https://doi.org/10.1145/2380356.2380370</a>.","short":"K. Chatterjee, T.A. Henzinger, V. Prabhu, in:, Roceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 43–52.","ama":"Chatterjee K, Henzinger TA, Prabhu V. Finite automata with time delay blocks. In: <i>Roceedings of the Tenth ACM International Conference on Embedded Software</i>. ACM; 2012:43-52. doi:<a href=\"https://doi.org/10.1145/2380356.2380370\">10.1145/2380356.2380370</a>","ieee":"K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Finite automata with time delay blocks,” in <i>roceedings of the tenth ACM international conference on Embedded software</i>, Tampere, Finland, 2012, pp. 43–52."},"date_created":"2018-12-11T12:00:26Z","acknowledgement":"This work has been financially supported in part by the European Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract # 270180 (NOPTILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008 (Modeling and control of Networked vehicle systems in persistent autonomous operations); by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification; FWF NFN Grant No S11407-N23 (RiSE); ERC Start grant (279307: Graph Games); Microsoft faculty fellows award; ERC Advanced grant QUAREM; and FWF Grant No S11403-N23 (RiSE).","year":"2012","ec_funded":1,"_id":"2936","doi":"10.1145/2380356.2380370"},{"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","volume":7561,"page":"385 - 399","department":[{"_id":"KrCh"}],"date_published":"2012-06-01T00:00:00Z","publisher":"Springer","publication_status":"published","abstract":[{"lang":"eng","text":"We introduce games with probabilistic uncertainty, a model for controller synthesis in which the controller observes the state through imprecise sensors that provide correct information about the current state with a fixed probability. That is, in each step, the sensors return an observed state, and given the observed state, there is a probability distribution (due to the estimation error) over the actual current state. The controller must base its decision on the observed state (rather than the actual current state, which it does not know). On the other hand, we assume that the environment can perfectly observe the current state. We show that controller synthesis for qualitative ω-regular objectives in our model can be reduced in polynomial time to standard partial-observation stochastic games, and vice-versa. As a consequence we establish the precise decidability frontier for the new class of games, and establish optimal complexity results for all the decidable problems."}],"_id":"2947","doi":"10.1007/978-3-642-33386-6_30","publist_id":"3785","citation":{"apa":"Chatterjee, K., Chmelik, M., &#38; Majumdar, R. (2012). Equivalence of games with probabilistic uncertainty and partial observation games (Vol. 7561, pp. 385–399). Presented at the  ATVA: Automated Technology for Verification and Analysis, Thiruvananthapuram, India: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">https://doi.org/10.1007/978-3-642-33386-6_30</a>","ista":"Chatterjee K, Chmelik M, Majumdar R. 2012. Equivalence of games with probabilistic uncertainty and partial observation games.  ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 7561, 385–399.","mla":"Chatterjee, Krishnendu, et al. <i>Equivalence of Games with Probabilistic Uncertainty and Partial Observation Games</i>. Vol. 7561, Springer, 2012, pp. 385–99, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">10.1007/978-3-642-33386-6_30</a>.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Ritankar Majumdar. “Equivalence of Games with Probabilistic Uncertainty and Partial Observation Games,” 7561:385–99. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">https://doi.org/10.1007/978-3-642-33386-6_30</a>.","short":"K. Chatterjee, M. Chmelik, R. Majumdar, in:, Springer, 2012, pp. 385–399.","ama":"Chatterjee K, Chmelik M, Majumdar R. Equivalence of games with probabilistic uncertainty and partial observation games. In: Vol 7561. Springer; 2012:385-399. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">10.1007/978-3-642-33386-6_30</a>","ieee":"K. Chatterjee, M. Chmelik, and R. Majumdar, “Equivalence of games with probabilistic uncertainty and partial observation games,” presented at the  ATVA: Automated Technology for Verification and Analysis, Thiruvananthapuram, India, 2012, vol. 7561, pp. 385–399."},"date_created":"2018-12-11T12:00:29Z","year":"2012","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","ec_funded":1,"type":"conference","status":"public","alternative_title":["LNCS"],"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar","first_name":"Ritankar"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1202.4140"}],"day":"01","month":"06","conference":{"start_date":"2012-10-03","name":" ATVA: Automated Technology for Verification and Analysis","end_date":"2012-10-06","location":"Thiruvananthapuram, India"},"language":[{"iso":"eng"}],"title":"Equivalence of games with probabilistic uncertainty and partial observation games","date_updated":"2021-01-12T07:39:58Z","oa":1,"scopus_import":1,"intvolume":"      7561"},{"abstract":[{"text":"We consider two-player stochastic games played on finite graphs with reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1), or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, the players (a) may not be allowed to use randomization (pure strategies), or (b) may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) may use full randomization. Our main results for pure strategies are as follows. (1) For one-sided games with player 1 having partial observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almostsure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete. (2) For one-sided games with player 2 having partial observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibits serious flaws in previous results of the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.","lang":"eng"}],"external_id":{"arxiv":["1107.2141"]},"publication_status":"published","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_published":"2012-08-23T00:00:00Z","publisher":"IEEE","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"status":"public","id":"2211","relation":"later_version"},{"relation":"earlier_version","id":"5381","status":"public"}]},"article_number":"6280436","ec_funded":1,"publist_id":"3771","citation":{"apa":"Chatterjee, K., &#38; Doyen, L. (2012). Partial-observation stochastic games: How to win when belief fails. In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Dubrovnik, Croatia: IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.28\">https://doi.org/10.1109/LICS.2012.28</a>","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 6280436, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.28\">10.1109/LICS.2012.28</a>.","ista":"Chatterjee K, Doyen L. 2012. Partial-observation stochastic games: How to win when belief fails. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280436.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.28\">https://doi.org/10.1109/LICS.2012.28</a>.","short":"K. Chatterjee, L. Doyen, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.","ama":"Chatterjee K, Doyen L. Partial-observation stochastic games: How to win when belief fails. In: <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.28\">10.1109/LICS.2012.28</a>","ieee":"K. Chatterjee and L. Doyen, “Partial-observation stochastic games: How to win when belief fails,” in <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Dubrovnik, Croatia, 2012."},"date_created":"2018-12-11T12:00:32Z","year":"2012","acknowledgement":"This work was partially supported by FWF Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","doi":"10.1109/LICS.2012.28","_id":"2955","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1107.2141"}],"day":"23","month":"08","conference":{"location":"Dubrovnik, Croatia","end_date":"2012-06-28","name":"LICS: Logic in Computer Science","start_date":"2012-06-25"},"arxiv":1,"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"type":"conference","status":"public","scopus_import":1,"title":"Partial-observation stochastic games: How to win when belief fails","date_updated":"2023-02-23T12:23:43Z","oa":1,"publication":"Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science","language":[{"iso":"eng"}]},{"publisher":"IEEE","status":"public","type":"conference","date_published":"2012-08-23T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"conference":{"location":"Dubrovnik, Croatia ","end_date":"2012-06-28","name":"LICS: Logic in Computer Science","start_date":"2012-06-25"},"month":"08","day":"23","oa_version":"None","abstract":[{"lang":"eng","text":"Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and parity objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean payoff objectives. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two-player pushdown games. Finally we also show that all the problems have the same computational complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"}],"publication_status":"published","publication":"Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science","doi":"10.1109/LICS.2012.30","language":[{"iso":"eng"}],"_id":"2956","ec_funded":1,"scopus_import":1,"article_number":"6280438","related_material":{"record":[{"id":"5377","relation":"earlier_version","status":"public"}]},"date_updated":"2023-02-23T12:23:30Z","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 Israeli Centers of Research Excellence (ICORE) program, (Center No. 4/11), 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.\r\nA Technical Report of this paper is available via internal link.","year":"2012","date_created":"2018-12-11T12:00:32Z","publist_id":"3770","title":"Mean payoff pushdown games","citation":{"short":"K. Chatterjee, Y. Velner, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.","ama":"Chatterjee K, Velner Y. Mean payoff pushdown games. In: <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.30\">10.1109/LICS.2012.30</a>","ieee":"K. Chatterjee and Y. Velner, “Mean payoff pushdown games,” in <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Dubrovnik, Croatia , 2012.","mla":"Chatterjee, Krishnendu, and Yaron Velner. “Mean Payoff Pushdown Games.” <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 6280438, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.30\">10.1109/LICS.2012.30</a>.","ista":"Chatterjee K, Velner Y. 2012. Mean payoff pushdown games. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280438.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “Mean Payoff Pushdown Games.” In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.30\">https://doi.org/10.1109/LICS.2012.30</a>.","apa":"Chatterjee, K., &#38; Velner, Y. (2012). Mean payoff pushdown games. In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Dubrovnik, Croatia : IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.30\">https://doi.org/10.1109/LICS.2012.30</a>"}},{"scopus_import":1,"title":"Decidable problems for probabilistic automata on infinite words","oa":1,"date_updated":"2023-02-23T12:23:51Z","publication":"Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/1107.2091","open_access":"1"}],"day":"23","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"LICS: Logic in Computer Science","start_date":"2012-06-25","location":"Dubrovnik, Croatia ","end_date":"2012-06-28"},"month":"08","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Tracol","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","full_name":"Tracol, Mathieu","first_name":"Mathieu"}],"arxiv":1,"type":"conference","status":"public","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5384"}]},"article_number":"6280437","citation":{"chicago":"Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.29\">https://doi.org/10.1109/LICS.2012.29</a>.","mla":"Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 6280437, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.29\">10.1109/LICS.2012.29</a>.","ista":"Chatterjee K, Tracol M. 2012. Decidable problems for probabilistic automata on infinite words. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280437.","short":"K. Chatterjee, M. Tracol, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.","ieee":"K. Chatterjee and M. Tracol, “Decidable problems for probabilistic automata on infinite words,” in <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Dubrovnik, Croatia , 2012.","ama":"Chatterjee K, Tracol M. Decidable problems for probabilistic automata on infinite words. In: <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.29\">10.1109/LICS.2012.29</a>","apa":"Chatterjee, K., &#38; Tracol, M. (2012). Decidable problems for probabilistic automata on infinite words. In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Dubrovnik, Croatia : IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.29\">https://doi.org/10.1109/LICS.2012.29</a>"},"publist_id":"3769","date_created":"2018-12-11T12:00:33Z","year":"2012","doi":"10.1109/LICS.2012.29","_id":"2957","external_id":{"arxiv":["1107.2091"]},"abstract":[{"lang":"eng","text":"We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether words are accepted with probability arbitrarily close to 1. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape (regular) words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. For most decidable problems we show an optimal PSPACE-complete complexity bound."}],"publication_status":"published","department":[{"_id":"KrCh"}],"quality_controlled":"1","publisher":"IEEE","date_published":"2012-08-23T00:00:00Z","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}]},{"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"}],"arxiv":1,"month":"11","day":"02","oa_version":"Published Version","file":[{"file_id":"5935","checksum":"719e4a5af5a01ad3f2f7f7f05b3c2b09","file_name":"2012_Elsevier_Chatterjee.pdf","date_updated":"2020-07-14T12:45:57Z","date_created":"2019-02-06T11:56:22Z","creator":"kschuh","access_level":"open_access","file_size":351271,"relation":"main_file","content_type":"application/pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","status":"public","pubrep_id":"935","oa":1,"date_updated":"2023-02-23T11:45:29Z","title":"Energy parity games","intvolume":"       458","has_accepted_license":"1","scopus_import":1,"language":[{"iso":"eng"}],"publication":"Theoretical Computer Science","publication_status":"published","ddc":["004"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"external_id":{"arxiv":["1001.5183"]},"abstract":[{"text":"Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (i.e., the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objectives. Our main results are as follows: (a) exponential memory is sufficient and may be necessary for winning strategies in energy parity games; (b) the problem of deciding the winner in energy parity games can be solved in NP ∩ coNP; and (c) we give an algorithm to solve energy parity by reduction to energy games. We also show that the problem of deciding the winner in energy parity games is logspace-equivalent to the problem of deciding the winner in mean-payoff parity games, which can thus be solved in NP ∩ coNP. As a consequence we also obtain a conceptually simple algorithm to solve mean-payoff parity games.","lang":"eng"}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publisher":"Elsevier","date_published":"2012-11-02T00:00:00Z","department":[{"_id":"KrCh"}],"page":"49 - 60","volume":458,"quality_controlled":"1","year":"2012","date_created":"2018-12-11T12:00:37Z","publist_id":"3736","citation":{"apa":"Chatterjee, K., &#38; Doyen, L. (2012). Energy parity games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">https://doi.org/10.1016/j.tcs.2012.07.038</a>","short":"K. Chatterjee, L. Doyen, Theoretical Computer Science 458 (2012) 49–60.","ama":"Chatterjee K, Doyen L. Energy parity games. <i>Theoretical Computer Science</i>. 2012;458:49-60. doi:<a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">10.1016/j.tcs.2012.07.038</a>","ieee":"K. Chatterjee and L. Doyen, “Energy parity games,” <i>Theoretical Computer Science</i>, vol. 458. Elsevier, pp. 49–60, 2012.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Energy Parity Games.” <i>Theoretical Computer Science</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">https://doi.org/10.1016/j.tcs.2012.07.038</a>.","ista":"Chatterjee K, Doyen L. 2012. Energy parity games. Theoretical Computer Science. 458, 49–60.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Energy Parity Games.” <i>Theoretical Computer Science</i>, vol. 458, Elsevier, 2012, pp. 49–60, doi:<a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">10.1016/j.tcs.2012.07.038</a>."},"ec_funded":1,"related_material":{"record":[{"id":"3851","relation":"earlier_version","status":"public"}]},"file_date_updated":"2020-07-14T12:45:57Z","_id":"2972","doi":"10.1016/j.tcs.2012.07.038"},{"has_accepted_license":"1","scopus_import":1,"intvolume":"        43","title":"A survey of partial-observation stochastic parity games","issue":"2","pubrep_id":"303","oa":1,"date_updated":"2021-01-12T07:41:15Z","publication":"Formal Methods in System Design","language":[{"iso":"eng"}],"file":[{"file_name":"IST-2014-303-v1+1_Survey_Partial-Observation_Stochastic_Parity_Games.pdf","file_id":"4882","checksum":"dd3d590f383bb2ac6cfda1489ac1c42a","date_created":"2018-12-12T10:11:27Z","date_updated":"2020-07-14T12:46:00Z","creator":"system","file_size":163983,"access_level":"open_access","content_type":"application/pdf","relation":"main_file"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"Submitted Version","month":"10","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"status":"public","type":"journal_article","ec_funded":1,"publist_id":"3570","date_created":"2018-12-11T12:01:33Z","citation":{"ista":"Chatterjee K, Doyen L, Henzinger TA. 2012. A survey of partial-observation stochastic parity games. Formal Methods in System Design. 43(2), 268–284.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey of Partial-Observation Stochastic Parity Games.” <i>Formal Methods in System Design</i>. Springer, 2012. <a href=\"https://doi.org/10.1007/s10703-012-0164-2\">https://doi.org/10.1007/s10703-012-0164-2</a>.","mla":"Chatterjee, Krishnendu, et al. “A Survey of Partial-Observation Stochastic Parity Games.” <i>Formal Methods in System Design</i>, vol. 43, no. 2, Springer, 2012, pp. 268–84, doi:<a href=\"https://doi.org/10.1007/s10703-012-0164-2\">10.1007/s10703-012-0164-2</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design 43 (2012) 268–284.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partial-observation stochastic parity games,” <i>Formal Methods in System Design</i>, vol. 43, no. 2. Springer, pp. 268–284, 2012.","ama":"Chatterjee K, Doyen L, Henzinger TA. A survey of partial-observation stochastic parity games. <i>Formal Methods in System Design</i>. 2012;43(2):268-284. doi:<a href=\"https://doi.org/10.1007/s10703-012-0164-2\">10.1007/s10703-012-0164-2</a>","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2012). A survey of partial-observation stochastic parity games. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-012-0164-2\">https://doi.org/10.1007/s10703-012-0164-2</a>"},"year":"2012","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF NFN Grant No. S11407-N23(RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, ERC Advanced grant QUAREM, and FWF Grant No. S11403-N23 (RiSE).","doi":"10.1007/s10703-012-0164-2","_id":"3128","file_date_updated":"2020-07-14T12:46:00Z","abstract":[{"text":"We consider two-player zero-sum stochastic games on graphs with ω-regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of deciding the winner in such games, and in classes of interest obtained as special cases, based on the information and the power of randomization available to the players, on the class of objectives and on the winning mode. On the basis of information, these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have complete view of the game). The one-sided partial-observation games have two important subclasses: the one-player games, known as partial-observation Markov decision processes (POMDPs), and the blind one-player games, known as probabilistic automata. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Finally, various classes of games are obtained by restricting the parity objective to a reachability, safety, Büchi, or coBüchi condition. We also consider several winning modes, such as sure-winning (i.e., all outcomes of a strategy have to satisfy the winning condition), almost-sure winning (i.e., winning with probability 1), limit-sure winning (i.e., winning with probability arbitrarily close to 1), and value-threshold winning (i.e., winning with probability at least ν, where ν is a given rational). ","lang":"eng"}],"ddc":["005"],"publication_status":"published","volume":43,"quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"268 - 284","date_published":"2012-10-01T00:00:00Z","publisher":"Springer","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}]}]