[{"oa":1,"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","day":"27","ec_funded":1,"has_accepted_license":"1","scopus_import":"1","publisher":"IEEE","file":[{"relation":"main_file","file_id":"4792","creator":"system","file_name":"IST-2012-81-v1+1_The_complexity_of_quantitative_information_flow_problems.pdf","date_created":"2018-12-12T10:10:07Z","access_level":"open_access","date_updated":"2020-07-14T12:46:10Z","checksum":"1a25be0c62459fc7640db88af08ff63a","content_type":"application/pdf","file_size":299069}],"conference":{"name":"CSF: Computer Security Foundations","start_date":"2011-06-27","end_date":"2011-06-29","location":"Cernay-la-Ville, France"},"ddc":["000","005"],"citation":{"ama":"Cerny P, Chatterjee K, Henzinger TA. The complexity of quantitative information flow problems. In: IEEE; 2011:205-217. doi:<a href=\"https://doi.org/10.1109/CSF.2011.21\">10.1109/CSF.2011.21</a>","ieee":"P. Cerny, K. Chatterjee, and T. A. Henzinger, “The complexity of quantitative information flow problems,” presented at the CSF: Computer Security Foundations, Cernay-la-Ville, France, 2011, pp. 205–217.","mla":"Cerny, Pavol, et al. <i>The Complexity of Quantitative Information Flow Problems</i>. IEEE, 2011, pp. 205–17, doi:<a href=\"https://doi.org/10.1109/CSF.2011.21\">10.1109/CSF.2011.21</a>.","apa":"Cerny, P., Chatterjee, K., &#38; Henzinger, T. A. (2011). The complexity of quantitative information flow problems (pp. 205–217). Presented at the CSF: Computer Security Foundations, Cernay-la-Ville, France: IEEE. <a href=\"https://doi.org/10.1109/CSF.2011.21\">https://doi.org/10.1109/CSF.2011.21</a>","ista":"Cerny P, Chatterjee K, Henzinger TA. 2011. The complexity of quantitative information flow problems. CSF: Computer Security Foundations, 205–217.","short":"P. Cerny, K. Chatterjee, T.A. Henzinger, in:, IEEE, 2011, pp. 205–217.","chicago":"Cerny, Pavol, Krishnendu Chatterjee, and Thomas A Henzinger. “The Complexity of Quantitative Information Flow Problems,” 205–17. IEEE, 2011. <a href=\"https://doi.org/10.1109/CSF.2011.21\">https://doi.org/10.1109/CSF.2011.21</a>."},"page":"205 - 217","status":"public","year":"2011","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"date_updated":"2025-09-30T09:04:15Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"external_id":{"isi":["000300766400014"]},"abstract":[{"text":"In this paper, we investigate the computational complexity of quantitative information flow (QIF) problems. Information-theoretic quantitative relaxations of noninterference (based on Shannon entropy)have been introduced to enable more fine-grained reasoning about programs in situations where limited information flow is acceptable. The QIF bounding problem asks whether the information flow in a given program is bounded by a constant $d$. Our first result is that the QIF bounding problem is PSPACE-complete. The QIF memoryless synthesis problem asks whether it is possible to resolve nondeterministic choices in a given partial program in such a way that in the resulting deterministic program, the quantitative information flow is bounded by a given constant $d$. Our second result is that the QIF memoryless synthesis problem is also EXPTIME-complete. The QIF memoryless synthesis problem generalizes to QIF general synthesis problem which does not impose the memoryless requirement (that is, by allowing the synthesized program to have more variables then the original partial program). Our third result is that the QIF general synthesis problem is EXPTIME-hard.","lang":"eng"}],"type":"conference","file_date_updated":"2020-07-14T12:46:10Z","month":"06","corr_author":"1","pubrep_id":"81","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2018-12-11T12:02:54Z","doi":"10.1109/CSF.2011.21","oa_version":"Submitted Version","title":"The complexity of quantitative information flow problems","language":[{"iso":"eng"}],"publist_id":"3254","publication_status":"published","_id":"3361","isi":1,"date_published":"2011-06-27T00:00:00Z"},{"day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Tracol, Mathieu","last_name":"Tracol","first_name":"Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"year":"2011","date_updated":"2025-06-26T09:19:59Z","publisher":"ArXiv","ec_funded":1,"status":"public","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Tracol, M. (n.d.). The decidability frontier for probabilistic automata on infinite words. ArXiv. <a href=\"https://doi.org/10.48550/arXiv.1104.0127\">https://doi.org/10.48550/arXiv.1104.0127</a>","ieee":"K. Chatterjee, T. A. Henzinger, and M. Tracol, “The decidability frontier for probabilistic automata on infinite words.” ArXiv.","mla":"Chatterjee, Krishnendu, et al. <i>The Decidability Frontier for Probabilistic Automata on Infinite Words</i>. 1104.0127, ArXiv, doi:<a href=\"https://doi.org/10.48550/arXiv.1104.0127\">10.48550/arXiv.1104.0127</a>.","ama":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words. doi:<a href=\"https://doi.org/10.48550/arXiv.1104.0127\">10.48550/arXiv.1104.0127</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Mathieu Tracol. “The Decidability Frontier for Probabilistic Automata on Infinite Words.” ArXiv, n.d. <a href=\"https://doi.org/10.48550/arXiv.1104.0127\">https://doi.org/10.48550/arXiv.1104.0127</a>.","ista":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words. 1104.0127.","short":"K. Chatterjee, T.A. Henzinger, M. Tracol, (n.d.)."},"page":"19","article_number":"1104.0127","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"The decidability frontier for probabilistic automata on infinite words","oa_version":"Preprint","date_created":"2018-12-11T12:02:54Z","doi":"10.48550/arXiv.1104.0127","article_processing_charge":"No","main_file_link":[{"url":"https://arxiv.org/abs/1104.0127","open_access":"1"}],"arxiv":1,"type":"preprint","month":"04","abstract":[{"text":"We consider probabilistic automata on infinite words with acceptance defined by safety, reachability, Büchi, coBüchi, and limit-average conditions. We consider quantitative and qualitative decision problems. We present extensions and adaptations of proofs for probabilistic finite automata and present a complete characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems for probabilistic automata on infinite words.","lang":"eng"}],"external_id":{"arxiv":["1104.0127"]},"project":[{"name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","grant_number":"214373"}],"corr_author":"1","_id":"3363","date_published":"2011-04-01T00:00:00Z","language":[{"iso":"eng"}],"publication_status":"submitted","publist_id":"3251"},{"date_updated":"2021-01-12T07:42:58Z","year":"2011","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jobstmann, Barbara","first_name":"Barbara","last_name":"Jobstmann"},{"full_name":"Singh, Rohit","first_name":"Rohit","last_name":"Singh"}],"page":"267 - 271","ddc":["000","005"],"citation":{"apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2011). QUASY: quantitative synthesis tool (Vol. 6605, pp. 267–271). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">https://doi.org/10.1007/978-3-642-19835-9_24</a>","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. QUASY: quantitative synthesis tool. In: Vol 6605. Springer; 2011:267-271. doi:<a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">10.1007/978-3-642-19835-9_24</a>","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “QUASY: quantitative synthesis tool,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken, Germany, 2011, vol. 6605, pp. 267–271.","mla":"Chatterjee, Krishnendu, et al. <i>QUASY: Quantitative Synthesis Tool</i>. Vol. 6605, Springer, 2011, pp. 267–71, doi:<a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">10.1007/978-3-642-19835-9_24</a>.","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2011, pp. 267–271.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “QUASY: Quantitative Synthesis Tool,” 6605:267–71. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">https://doi.org/10.1007/978-3-642-19835-9_24</a>.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2011. QUASY: quantitative synthesis tool. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 6605, 267–271."},"status":"public","scopus_import":1,"has_accepted_license":"1","file":[{"file_id":"5022","relation":"main_file","file_name":"IST-2012-77-v1+1_QUASY-_quantitative_synthesis_tool.pdf","creator":"system","checksum":"762e52eb296f6dbfbf2a75d98b8ebaee","file_size":475661,"content_type":"application/pdf","date_created":"2018-12-12T10:13:37Z","date_updated":"2020-07-14T12:46:10Z","access_level":"open_access"}],"publisher":"Springer","conference":{"end_date":"2011-04-03","start_date":"2011-03-26","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Saarbrucken, Germany"},"volume":6605,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"day":"29","oa":1,"quality_controlled":"1","date_published":"2011-09-29T00:00:00Z","_id":"3365","publist_id":"3248","publication_status":"published","intvolume":"      6605","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-19835-9_24","oa_version":"Submitted Version","date_created":"2018-12-11T12:02:55Z","title":"QUASY: quantitative synthesis tool","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"pubrep_id":"77","abstract":[{"text":"We present the tool Quasy, a quantitative synthesis tool. Quasy takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. The user can choose between a system that satisfies and optimizes the specifications (a) under all possible environment behaviors or (b) under the most-likely environment behaviors given as a probability distribution on the possible input sequences. Quasy solves these two quantitative synthesis problems by reduction to instances of 2-player games and Markov Decision Processes (MDPs) with quantitative winning objectives. Quasy can also be seen as a game solver for quantitative games. Most notable, it can solve lexicographic mean-payoff games with 2 players, MDPs with mean-payoff objectives, and ergodic MDPs with mean-payoff parity objectives.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:10Z","type":"conference","month":"09"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","oa_version":"Submitted Version","doi":"10.1007/978-3-642-22110-1_20","date_created":"2018-12-11T12:02:55Z","title":"Quantitative synthesis for concurrent programs","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","grant_number":"214373"}],"abstract":[{"lang":"eng","text":"We present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a nondeterministic partial program and of a parametric performance model. The nondeterminism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the nondeterminism of the partial program so that both correctness is guaranteed and performance is optimal. As is standard for shared memory concurrency, correctness is formalized &quot;specification free&quot;, in particular as race freedom or deadlock freedom. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives. While we show, using game-theoretic methods, that the synthesis problem is Nexp-complete, we present an algorithmic method and an implementation that works efficiently for concurrent programs and performance models of practical interest. We have implemented a prototype tool and used it to synthesize finite-state concurrent programs that exhibit different programming patterns, for several performance models representing different architectures. "}],"type":"conference","month":"04","file_date_updated":"2020-07-14T12:46:10Z","pubrep_id":"76","corr_author":"1","related_material":{"record":[{"id":"5388","relation":"earlier_version","status":"public"}]},"_id":"3366","date_published":"2011-04-21T00:00:00Z","language":[{"iso":"eng"}],"publist_id":"3247","publication_status":"published","intvolume":"      6806","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"day":"21","volume":6806,"oa":1,"quality_controlled":"1","year":"2011","author":[{"full_name":"Cerny, Pavol","last_name":"Cerny","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Singh, Rohit","first_name":"Rohit","last_name":"Singh"}],"date_updated":"2024-10-21T06:03:04Z","editor":[{"full_name":"Gopalakrishnan, Ganesh","first_name":"Ganesh","last_name":"Gopalakrishnan"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"}],"ec_funded":1,"scopus_import":"1","has_accepted_license":"1","conference":{"location":"Snowbird, USA","end_date":"2011-07-20","start_date":"2011-07-14","name":"CAV: Computer Aided Verification"},"file":[{"file_id":"5174","relation":"main_file","file_name":"IST-2012-76-v1+1_Quantitative_synthesis_for_concurrent_programs.pdf","creator":"system","date_created":"2018-12-12T10:15:51Z","access_level":"open_access","date_updated":"2020-07-14T12:46:10Z","checksum":"c033689355f45742dc7c99b5af13ce7a","content_type":"application/pdf","file_size":508946}],"publisher":"Springer","page":"243 - 259","citation":{"ista":"Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. 2011. Quantitative synthesis for concurrent programs. CAV: Computer Aided Verification, LNCS, vol. 6806, 243–259.","chicago":"Cerny, Pavol, Krishnendu Chatterjee, Thomas A Henzinger, Arjun Radhakrishna, and Rohit Singh. “Quantitative Synthesis for Concurrent Programs.” edited by Ganesh Gopalakrishnan and Shaz Qadeer, 6806:243–59. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">https://doi.org/10.1007/978-3-642-22110-1_20</a>.","short":"P. Cerny, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, R. Singh, in:, G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 243–259.","ieee":"P. Cerny, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh, “Quantitative synthesis for concurrent programs,” presented at the CAV: Computer Aided Verification, Snowbird, USA, 2011, vol. 6806, pp. 243–259.","mla":"Cerny, Pavol, et al. <i>Quantitative Synthesis for Concurrent Programs</i>. Edited by Ganesh Gopalakrishnan and Shaz Qadeer, vol. 6806, Springer, 2011, pp. 243–59, doi:<a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">10.1007/978-3-642-22110-1_20</a>.","apa":"Cerny, P., Chatterjee, K., Henzinger, T. A., Radhakrishna, A., &#38; Singh, R. (2011). Quantitative synthesis for concurrent programs. In G. Gopalakrishnan &#38; S. Qadeer (Eds.) (Vol. 6806, pp. 243–259). Presented at the CAV: Computer Aided Verification, Snowbird, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">https://doi.org/10.1007/978-3-642-22110-1_20</a>","ama":"Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. Quantitative synthesis for concurrent programs. In: Gopalakrishnan G, Qadeer S, eds. Vol 6806. Springer; 2011:243-259. doi:<a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">10.1007/978-3-642-22110-1_20</a>"},"ddc":["000","004"],"status":"public"},{"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["IST Austria Technical Report"],"day":"11","has_accepted_license":"1","publisher":"IST Austria","file":[{"content_type":"application/pdf","file_size":388665,"checksum":"0b354264229045d982332fd2cb5b9a26","date_created":"2018-12-12T11:53:43Z","access_level":"open_access","date_updated":"2020-07-14T12:46:39Z","relation":"main_file","file_id":"5504","creator":"system","file_name":"IST-2011-0009_IST-2011-0009.pdf"}],"page":"20","ddc":["000","004"],"citation":{"short":"K. Chatterjee, M. Henzinger, An O(N2) Time Algorithm for Alternating Büchi Games, IST Austria, 2011.","chicago":"Chatterjee, Krishnendu, and Monika Henzinger. <i>An O(N2) Time Algorithm for Alternating Büchi Games</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0009\">https://doi.org/10.15479/AT:IST-2011-0009</a>.","ista":"Chatterjee K, Henzinger M. 2011. An O(n2) time algorithm for alternating Büchi games, IST Austria, 20p.","ieee":"K. Chatterjee and M. Henzinger, <i>An O(n2) time algorithm for alternating Büchi games</i>. IST Austria, 2011.","mla":"Chatterjee, Krishnendu, and Monika Henzinger. <i>An O(N2) Time Algorithm for Alternating Büchi Games</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0009\">10.15479/AT:IST-2011-0009</a>.","apa":"Chatterjee, K., &#38; Henzinger, M. (2011). <i>An O(n2) time algorithm for alternating Büchi games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0009\">https://doi.org/10.15479/AT:IST-2011-0009</a>","ama":"Chatterjee K, Henzinger M. <i>An O(N2) Time Algorithm for Alternating Büchi Games</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0009\">10.15479/AT:IST-2011-0009</a>"},"status":"public","year":"2011","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Monika H","last_name":"Henzinger","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530"}],"date_updated":"2025-07-10T11:52:28Z","abstract":[{"lang":"eng","text":"Computing the winning set for Büchi objectives in alternating games on graphs is a central problem in computer aided verification with a large number of applications. The long standing best known upper bound for solving the problem is ̃O(n·m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the ̃O(n·m) boundary by presenting a new technique that reduces the running time to O(n2). This bound also leads to O(n2) time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of O(n·m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n3)), and (3) in Markov decision processes (improving for m > n4/3 an earlier bound of O(min(m1.5, m·n2/3)). We also show that the same technique can be used to compute the maximal end-component decomposition of a graph in time O(n2), which is an improvement over earlier bounds for m > n4/3. Finally, we show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. This is the first dynamic algorithm for this problem."}],"type":"technical_report","month":"07","file_date_updated":"2020-07-14T12:46:39Z","pubrep_id":"15","publication_identifier":{"issn":["2664-1690"]},"department":[{"_id":"KrCh"}],"article_processing_charge":"No","oa_version":"Published Version","doi":"10.15479/AT:IST-2011-0009","date_created":"2018-12-12T11:38:59Z","title":"An O(n2) time algorithm for alternating Büchi games","language":[{"iso":"eng"}],"publication_status":"published","related_material":{"record":[{"status":"public","id":"3165","relation":"later_version"}]},"_id":"5379","date_published":"2011-07-11T00:00:00Z"},{"title":"Bounded rationality in concurrent parity games","date_created":"2018-12-12T11:39:00Z","oa_version":"Published Version","doi":"10.15479/AT:IST-2011-0008","alternative_title":["IST Austria Technical Report"],"day":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"16","abstract":[{"lang":"eng","text":"We consider 2-player games played on a finite state space for an infinite number of rounds.  The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. We study concurrent games with ω-regular winning conditions specified as parity objectives.  We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies.  In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite-precision;  and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies.  We show that the winning sets can be computed in O(n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms,that are obtained by characterization of the winning sets as μ-calculus formulas, are considerably more involved than those for turn-based games."}],"file_date_updated":"2020-07-14T12:46:39Z","type":"technical_report","month":"07","oa":1,"date_updated":"2025-06-26T09:28:52Z","date_published":"2011-07-11T00:00:00Z","_id":"5380","related_material":{"record":[{"status":"public","relation":"later_version","id":"3338"}]},"year":"2011","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"publication_status":"published","status":"public","citation":{"ieee":"K. Chatterjee, <i>Bounded rationality in concurrent parity games</i>. IST Austria, 2011.","mla":"Chatterjee, Krishnendu. <i>Bounded Rationality in Concurrent Parity Games</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0008\">10.15479/AT:IST-2011-0008</a>.","ama":"Chatterjee K. <i>Bounded Rationality in Concurrent Parity Games</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0008\">10.15479/AT:IST-2011-0008</a>","apa":"Chatterjee, K. (2011). <i>Bounded rationality in concurrent parity games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0008\">https://doi.org/10.15479/AT:IST-2011-0008</a>","chicago":"Chatterjee, Krishnendu. <i>Bounded Rationality in Concurrent Parity Games</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0008\">https://doi.org/10.15479/AT:IST-2011-0008</a>.","short":"K. Chatterjee, Bounded Rationality in Concurrent Parity Games, IST Austria, 2011.","ista":"Chatterjee K. 2011. Bounded rationality in concurrent parity games, IST Austria, 53p."},"ddc":["000"],"page":"53","has_accepted_license":"1","file":[{"file_id":"5544","relation":"main_file","file_name":"IST-2011-0008_IST-2011-0008.pdf","creator":"system","date_created":"2018-12-12T11:54:22Z","date_updated":"2020-07-14T12:46:39Z","access_level":"open_access","checksum":"0fd38186409be819a911c4990fa79d1f","file_size":500399,"content_type":"application/pdf"}],"publisher":"IST Austria","language":[{"iso":"eng"}]},{"publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"17","month":"07","file_date_updated":"2020-07-14T12:46:39Z","type":"technical_report","abstract":[{"text":"In two-player finite-state stochastic games of partial obser- vation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distri- bution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1) or pos- itively (i.e., with positive probability), no matter the strategy of the second player.\r\n\r\nWe classify such games according to the information and to 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, (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.\r\n\r\nOur main results for pure strategies are as follows: (1) For one-sided games with player 2 perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strate- gies are not sufficient, and present an exponential upper bound on mem- ory both for almost-sure 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 and present symbolic algo- rithms that avoid the explicit exponential construction. (2) For one-sided games with player 1 perfect observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and posi- tive 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 re- sult exhibit serious flaws in previous results in the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.","lang":"eng"}],"oa":1,"title":"Partial-observation stochastic games: How to win when belief fails","date_created":"2018-12-12T11:39:00Z","doi":"10.15479/AT:IST-2011-0007","oa_version":"Published Version","day":"05","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"status":"public","publication_status":"published","citation":{"mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Partial-Observation Stochastic Games: How to Win When Belief Fails</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0007\">10.15479/AT:IST-2011-0007</a>.","ieee":"K. Chatterjee and L. Doyen, <i>Partial-observation stochastic games: How to win when belief fails</i>. IST Austria, 2011.","apa":"Chatterjee, K., &#38; Doyen, L. (2011). <i>Partial-observation stochastic games: How to win when belief fails</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0007\">https://doi.org/10.15479/AT:IST-2011-0007</a>","ama":"Chatterjee K, Doyen L. <i>Partial-Observation Stochastic Games: How to Win When Belief Fails</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0007\">10.15479/AT:IST-2011-0007</a>","short":"K. Chatterjee, L. Doyen, Partial-Observation Stochastic Games: How to Win When Belief Fails, IST Austria, 2011.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Partial-Observation Stochastic Games: How to Win When Belief Fails</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0007\">https://doi.org/10.15479/AT:IST-2011-0007</a>.","ista":"Chatterjee K, Doyen L. 2011. Partial-observation stochastic games: How to win when belief fails, IST Austria, 43p."},"page":"43","ddc":["000","005"],"publisher":"IST Austria","file":[{"file_name":"IST-2011-0007_IST-2011-0007.pdf","creator":"system","file_id":"5488","relation":"main_file","file_size":574055,"content_type":"application/pdf","checksum":"06bf6dfc97f6006e3fd0e9a3f31bc961","date_updated":"2020-07-14T12:46:39Z","access_level":"open_access","date_created":"2018-12-12T11:53:27Z"}],"has_accepted_license":"1","language":[{"iso":"eng"}],"date_updated":"2025-09-30T08:08:45Z","date_published":"2011-07-05T00:00:00Z","related_material":{"record":[{"status":"public","relation":"later_version","id":"1903"},{"id":"2211","relation":"later_version","status":"public"},{"id":"2955","relation":"later_version","status":"public"}]},"_id":"5381","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"}],"year":"2011"},{"date_created":"2018-12-12T11:39:00Z","oa_version":"Published Version","doi":"10.15479/AT:IST-2011-0006","title":"Robustness of structurally equivalent concurrent parity games","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"27","alternative_title":["IST Austria Technical Report"],"pubrep_id":"18","publication_identifier":{"issn":["2664-1690"]},"oa":1,"file_date_updated":"2020-07-14T12:46:40Z","month":"06","type":"technical_report","abstract":[{"text":"We consider two-player stochastic games played on a finite state space for an infinite num- ber of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine a probability distribution over the successor states. We also consider the important special case of turn-based stochastic games where players make moves in turns, rather than concurrently. We study concurrent games with ω-regular winning conditions specified as parity objectives. The value for player 1 for a parity objective is the maximal probability with which the player can guarantee the satisfaction of the objective against all strategies of the opponent. We study the problem of continuity and robustness of the value function in concurrent and turn-based stochastic parity games with respect to imprecision in the transition probabilities. We present quantitative bounds on the difference of the value function (in terms of the imprecision of the transition probabilities) and show the value continuity for structurally equivalent concurrent games (two games are structurally equivalent if the support of the transition func- tion is same and the probabilities differ). We also show robustness of optimal strategies for structurally equivalent turn-based stochastic parity games. Finally we show that the value continuity property breaks without the structurally equivalent assumption (even for Markov chains) and show that our quantitative bound is asymptotically optimal. Hence our results are tight (the assumption is both necessary and sufficient) and optimal (our quantitative bound is asymptotically optimal).","lang":"eng"}],"date_published":"2011-06-27T00:00:00Z","date_updated":"2025-04-15T08:12:24Z","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"}],"year":"2011","_id":"5382","related_material":{"record":[{"id":"3341","relation":"later_version","status":"public"}]},"page":"18","ddc":["000","005"],"citation":{"short":"K. Chatterjee, Robustness of Structurally Equivalent Concurrent Parity Games, IST Austria, 2011.","chicago":"Chatterjee, Krishnendu. <i>Robustness of Structurally Equivalent Concurrent Parity Games</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0006\">https://doi.org/10.15479/AT:IST-2011-0006</a>.","ista":"Chatterjee K. 2011. Robustness of structurally equivalent concurrent parity games, IST Austria, 18p.","ama":"Chatterjee K. <i>Robustness of Structurally Equivalent Concurrent Parity Games</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0006\">10.15479/AT:IST-2011-0006</a>","mla":"Chatterjee, Krishnendu. <i>Robustness of Structurally Equivalent Concurrent Parity Games</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0006\">10.15479/AT:IST-2011-0006</a>.","ieee":"K. Chatterjee, <i>Robustness of structurally equivalent concurrent parity games</i>. IST Austria, 2011.","apa":"Chatterjee, K. (2011). <i>Robustness of structurally equivalent concurrent parity games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0006\">https://doi.org/10.15479/AT:IST-2011-0006</a>"},"status":"public","publication_status":"published","language":[{"iso":"eng"}],"publisher":"IST Austria","file":[{"creator":"system","file_name":"IST-2011-0006_IST-2011-0006.pdf","relation":"main_file","file_id":"5546","date_updated":"2020-07-14T12:46:40Z","access_level":"open_access","date_created":"2018-12-12T11:54:24Z","content_type":"application/pdf","file_size":335997,"checksum":"1322b652d6ab07eb5248298a3f91c1cf"}],"has_accepted_license":"1"},{"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["IST Austria Technical Report"],"day":"11","page":"30","ddc":["000","005"],"citation":{"chicago":"Chatterjee, Krishnendu, and Mathieu Tracol. <i>Decidable Problems for Probabilistic Automata on Infinite Words</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0004\">https://doi.org/10.15479/AT:IST-2011-0004</a>.","ista":"Chatterjee K, Tracol M. 2011. Decidable problems for probabilistic automata on infinite words, IST Austria, 30p.","short":"K. Chatterjee, M. Tracol, Decidable Problems for Probabilistic Automata on Infinite Words, IST Austria, 2011.","apa":"Chatterjee, K., &#38; Tracol, M. (2011). <i>Decidable problems for probabilistic automata on infinite words</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0004\">https://doi.org/10.15479/AT:IST-2011-0004</a>","ieee":"K. Chatterjee and M. Tracol, <i>Decidable problems for probabilistic automata on infinite words</i>. IST Austria, 2011.","ama":"Chatterjee K, Tracol M. <i>Decidable Problems for Probabilistic Automata on Infinite Words</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0004\">10.15479/AT:IST-2011-0004</a>","mla":"Chatterjee, Krishnendu, and Mathieu Tracol. <i>Decidable Problems for Probabilistic Automata on Infinite Words</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0004\">10.15479/AT:IST-2011-0004</a>."},"status":"public","has_accepted_license":"1","publisher":"IST Austria","file":[{"file_id":"5545","relation":"main_file","file_name":"IST-2011-004_IST-2011-0004.pdf","creator":"system","date_created":"2018-12-12T11:54:23Z","date_updated":"2020-07-14T12:46:40Z","access_level":"open_access","file_size":570827,"checksum":"f5a0f664fadc335990f5fcf138df19f1","content_type":"application/pdf"}],"date_updated":"2025-09-30T08:07:38Z","year":"2011","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mathieu","last_name":"Tracol","full_name":"Tracol, Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"corr_author":"1","pubrep_id":"20","publication_identifier":{"issn":["2664-1690"]},"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 for every ε > 0 there is a word that is accepted with probability at least 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 words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions."}],"type":"technical_report","file_date_updated":"2020-07-14T12:46:40Z","month":"04","doi":"10.15479/AT:IST-2011-0004","oa_version":"Published Version","date_created":"2018-12-12T11:39:01Z","title":"Decidable problems for probabilistic automata on infinite words","department":[{"_id":"KrCh"}],"publication_status":"published","language":[{"iso":"eng"}],"date_published":"2011-04-11T00:00:00Z","_id":"5384","related_material":{"record":[{"id":"2957","relation":"later_version","status":"public"}]}},{"language":[{"iso":"eng"}],"publication_status":"published","related_material":{"record":[{"id":"2038","relation":"later_version","status":"public"},{"status":"public","id":"3356","relation":"later_version"}]},"_id":"5385","date_published":"2011-04-04T00:00:00Z","abstract":[{"lang":"eng","text":"There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with “controlled-accumulation”, allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable."}],"type":"technical_report","file_date_updated":"2020-07-14T12:46:41Z","month":"04","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","call_identifier":"FP7"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","name":"Design for Embedded Systems","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"21","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Temporal specifications with accumulative values","oa_version":"Published Version","doi":"10.15479/AT:IST-2011-0003","date_created":"2018-12-12T11:39:02Z","ec_funded":1,"has_accepted_license":"1","publisher":"IST Austria","file":[{"date_created":"2018-12-12T11:53:00Z","date_updated":"2020-07-14T12:46:41Z","access_level":"open_access","checksum":"8491d0d48c4911620ecd5350b413c11e","file_size":366281,"content_type":"application/pdf","file_id":"5461","relation":"main_file","file_name":"IST-2011-0003_IST-2011-0003.pdf","creator":"system"}],"status":"public","ddc":["000","004"],"citation":{"chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. <i>Temporal Specifications with Accumulative Values</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">https://doi.org/10.15479/AT:IST-2011-0003</a>.","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, Temporal Specifications with Accumulative Values, IST Austria, 2011.","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications with accumulative values, IST Austria, 14p.","mla":"Boker, Udi, et al. <i>Temporal Specifications with Accumulative Values</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">10.15479/AT:IST-2011-0003</a>.","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. <i>Temporal Specifications with Accumulative Values</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">10.15479/AT:IST-2011-0003</a>","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., &#38; Kupferman, O. (2011). <i>Temporal specifications with accumulative values</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">https://doi.org/10.15479/AT:IST-2011-0003</a>","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, <i>Temporal specifications with accumulative values</i>. IST Austria, 2011."},"page":"14","year":"2011","author":[{"first_name":"Udi","last_name":"Boker","full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"date_updated":"2025-09-30T09:27:29Z","oa":1,"alternative_title":["IST Austria Technical Report"],"day":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"has_accepted_license":"1","file":[{"date_updated":"2020-07-14T12:46:41Z","access_level":"open_access","date_created":"2018-12-12T11:52:57Z","checksum":"824d6c70e6d3feb3e836b009e0b3cf73","content_type":"application/pdf","file_size":329976,"file_name":"IST-2011-0001_IST-2011-0001.pdf","creator":"system","file_id":"5458","relation":"main_file"}],"publisher":"IST Austria","language":[{"iso":"eng"}],"publication_status":"published","status":"public","ddc":["000","005"],"citation":{"ieee":"K. Chatterjee and L. Doyen, <i>Energy and mean-payoff parity Markov decision processes</i>. IST Austria, 2011.","ama":"Chatterjee K, Doyen L. <i>Energy and Mean-Payoff Parity Markov Decision Processes</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">10.15479/AT:IST-2011-0001</a>","apa":"Chatterjee, K., &#38; Doyen, L. (2011). <i>Energy and mean-payoff parity Markov decision processes</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">https://doi.org/10.15479/AT:IST-2011-0001</a>","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Energy and Mean-Payoff Parity Markov Decision Processes</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">10.15479/AT:IST-2011-0001</a>.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Energy and Mean-Payoff Parity Markov Decision Processes</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">https://doi.org/10.15479/AT:IST-2011-0001</a>.","short":"K. Chatterjee, L. Doyen, Energy and Mean-Payoff Parity Markov Decision Processes, IST Austria, 2011.","ista":"Chatterjee K, Doyen L. 2011. Energy and mean-payoff parity Markov decision processes, IST Austria, 20p."},"page":"20","related_material":{"record":[{"status":"public","relation":"later_version","id":"3345"}]},"_id":"5387","year":"2011","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"date_updated":"2025-04-15T08:12:14Z","date_published":"2011-02-16T00:00:00Z","abstract":[{"lang":"eng","text":"We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound."}],"month":"02","type":"technical_report","file_date_updated":"2020-07-14T12:46:41Z","oa":1,"publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"23","alternative_title":["IST Austria Technical Report"],"day":"16","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"title":"Energy and mean-payoff parity Markov decision processes","date_created":"2018-12-12T11:39:02Z","doi":"10.15479/AT:IST-2011-0001","oa_version":"Published Version"},{"date_updated":"2025-06-11T08:14:27Z","author":[{"full_name":"Cristau, Julien","first_name":"Julien","last_name":"Cristau"},{"first_name":"Claire","last_name":"David","full_name":"David, Claire"},{"id":"37327ACE-F248-11E8-B48F-1D18A9856A87","last_name":"Horn","first_name":"Florian","full_name":"Horn, Florian"}],"year":"2010","status":"public","publication":"Proceedings of GandALF 2010","citation":{"ieee":"J. Cristau, C. David, and F. Horn, “How do we remember the past in randomised strategies?,” in <i>Proceedings of GandALF 2010</i>, Minori, Amalfi Coast, Italy, 2010, vol. 25, pp. 30–39.","mla":"Cristau, Julien, et al. “How Do We Remember the Past in Randomised Strategies?” <i>Proceedings of GandALF 2010</i>, vol. 25, Open Publishing Association, 2010, pp. 30–39, doi:<a href=\"https://doi.org/10.4204/EPTCS.25.7\">10.4204/EPTCS.25.7</a>.","apa":"Cristau, J., David, C., &#38; Horn, F. (2010). How do we remember the past in randomised strategies? In <i>Proceedings of GandALF 2010</i> (Vol. 25, pp. 30–39). Minori, Amalfi Coast, Italy: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.25.7\">https://doi.org/10.4204/EPTCS.25.7</a>","ama":"Cristau J, David C, Horn F. How do we remember the past in randomised strategies? In: <i>Proceedings of GandALF 2010</i>. Vol 25. Open Publishing Association; 2010:30-39. doi:<a href=\"https://doi.org/10.4204/EPTCS.25.7\">10.4204/EPTCS.25.7</a>","short":"J. Cristau, C. David, F. Horn, in:, Proceedings of GandALF 2010, Open Publishing Association, 2010, pp. 30–39.","chicago":"Cristau, Julien, Claire David, and Florian Horn. “How Do We Remember the Past in Randomised Strategies?” In <i>Proceedings of GandALF 2010</i>, 25:30–39. Open Publishing Association, 2010. <a href=\"https://doi.org/10.4204/EPTCS.25.7\">https://doi.org/10.4204/EPTCS.25.7</a>.","ista":"Cristau J, David C, Horn F. 2010. How do we remember the past in randomised strategies? Proceedings of GandALF 2010. GandALF: Games, Automata, Logic, and Formal Verification, EPTCS, vol. 25, 30–39."},"page":"30 - 39","conference":{"location":"Minori, Amalfi Coast, Italy","name":"GandALF: Games, Automata, Logic, and Formal Verification","end_date":"2010-06-18","start_date":"2010-06-17"},"publisher":"Open Publishing Association","scopus_import":"1","volume":25,"day":"09","alternative_title":["EPTCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","oa":1,"date_published":"2010-06-09T00:00:00Z","_id":"489","intvolume":"        25","publication_status":"published","publist_id":"7332","language":[{"iso":"eng"}],"title":"How do we remember the past in randomised strategies?","oa_version":"Published Version","date_created":"2018-12-11T11:46:45Z","doi":"10.4204/EPTCS.25.7","article_processing_charge":"No","main_file_link":[{"url":"https://arxiv.org/abs/1006.1404","open_access":"1"}],"department":[{"_id":"KrCh"}],"corr_author":"1","month":"06","arxiv":1,"type":"conference","abstract":[{"text":"Graph games of infinite length are a natural model for open reactive processes: one player represents the controller, trying to ensure a given specification, and the other represents a hostile environment. The evolution of the system depends on the decisions of both players, supplemented by chance. In this work, we focus on the notion of randomised strategy. More specifically, we show that three natural definitions may lead to very different results: in the most general cases, an almost-surely winning situation may become almost-surely losing if the player is only allowed to use a weaker notion of strategy. In more reasonable settings, translations exist, but they require infinite memory, even in simple cases. Finally, some traditional problems becomes undecidable for the strongest type of strategies.","lang":"eng"}],"external_id":{"arxiv":["1006.1404"]}},{"has_accepted_license":"1","publisher":"IST Austria","file":[{"date_created":"2018-12-12T11:53:53Z","access_level":"open_access","date_updated":"2020-07-14T12:46:42Z","file_size":429101,"content_type":"application/pdf","checksum":"da38782d2388a6fa32109d10bb9bad67","file_id":"5515","relation":"main_file","file_name":"IST-2010-0004_IST-2010-0004.pdf","creator":"system"}],"language":[{"iso":"eng"}],"publication_status":"published","status":"public","page":"17","citation":{"apa":"Chatterjee, K., Cerny, P., Henzinger, T. A., Radhakrishna, A., &#38; Singh, R. (2010). <i>Quantitative synthesis for concurrent programs</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2010-0004\">https://doi.org/10.15479/AT:IST-2010-0004</a>","ama":"Chatterjee K, Cerny P, Henzinger TA, Radhakrishna A, Singh R. <i>Quantitative Synthesis for Concurrent Programs</i>. IST Austria; 2010. doi:<a href=\"https://doi.org/10.15479/AT:IST-2010-0004\">10.15479/AT:IST-2010-0004</a>","mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Synthesis for Concurrent Programs</i>. IST Austria, 2010, doi:<a href=\"https://doi.org/10.15479/AT:IST-2010-0004\">10.15479/AT:IST-2010-0004</a>.","ieee":"K. Chatterjee, P. Cerny, T. A. Henzinger, A. Radhakrishna, and R. Singh, <i>Quantitative synthesis for concurrent programs</i>. IST Austria, 2010.","chicago":"Chatterjee, Krishnendu, Pavol Cerny, Thomas A Henzinger, Arjun Radhakrishna, and Rohit Singh. <i>Quantitative Synthesis for Concurrent Programs</i>. IST Austria, 2010. <a href=\"https://doi.org/10.15479/AT:IST-2010-0004\">https://doi.org/10.15479/AT:IST-2010-0004</a>.","short":"K. Chatterjee, P. Cerny, T.A. Henzinger, A. Radhakrishna, R. Singh, Quantitative Synthesis for Concurrent Programs, IST Austria, 2010.","ista":"Chatterjee K, Cerny P, Henzinger TA, Radhakrishna A, Singh R. 2010. Quantitative synthesis for concurrent programs, IST Austria, 17p."},"ddc":["000","005"],"related_material":{"record":[{"id":"3366","relation":"later_version","status":"public"}]},"_id":"5388","year":"2010","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Singh, Rohit","last_name":"Singh","first_name":"Rohit"}],"date_updated":"2025-04-15T08:12:00Z","date_published":"2010-10-07T00:00:00Z","abstract":[{"lang":"eng","text":"We present an algorithmic method for the synthesis of concurrent programs that are optimal with respect to quantitative performance measures. The input consists of a sequential sketch, that is, a program that does not contain synchronization constructs, and of a parametric performance model that assigns costs to actions such as locking, context switching, and idling. The quantitative synthesis problem is to automatically introduce synchronization constructs into the sequential sketch so that both correctness is guaranteed and worst-case (or average-case) performance is optimized. Correctness is formalized as race freedom or linearizability.\r\n\r\nWe show that for worst-case performance, the problem can be modeled\r\nas a 2-player graph game with quantitative (limit-average) objectives, and\r\nfor average-case performance, as a 2 1/2 -player graph game (with probabilistic transitions). In both cases, the optimal correct program is derived from an optimal strategy in the corresponding quantitative game. We prove that the respective game problems are computationally expensive (NP-complete), and present several techniques that overcome the theoretical difficulty in cases of concurrent programs of practical interest.\r\n\r\nWe have implemented a prototype tool and used it for the automatic syn- thesis of programs that access a concurrent list. For certain parameter val- ues, our method automatically synthesizes various classical synchronization schemes for implementing a concurrent list, such as fine-grained locking or a lazy algorithm. For other parameter values, a new, hybrid synchronization style is synthesized, which uses both the lazy approach and coarse-grained locks (instead of standard fine-grained locks). The trade-off occurs because while fine-grained locking tends to decrease the cost that is due to waiting for locks, it increases cache size requirements."}],"file_date_updated":"2020-07-14T12:46:42Z","type":"technical_report","month":"10","oa":1,"publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"24","alternative_title":["IST Austria Technical Report"],"day":"07","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Quantitative synthesis for concurrent programs","date_created":"2018-12-12T11:39:03Z","doi":"10.15479/AT:IST-2010-0004","oa_version":"Published Version"},{"file_date_updated":"2020-07-14T12:46:43Z","type":"technical_report","month":"06","abstract":[{"lang":"eng","text":"The class of ω regular languages provide a robust specification language in verification. Every ω-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider the finitary parity and Streett (fairness) conditions. We present the topological, automata-theoretic and logical characterization of finitary languages defined by finitary parity and Streett conditions. We (a) show that the finitary parity and Streett languages are Σ2-complete; (b) present a complete characterization of the expressive power of various classes of automata with finitary and infinitary conditions (in particular we show that non-deterministic finitary parity and Streett automata cannot be determinized to deterministic finitary parity or Streett automata); and (c) show that the languages defined by non-deterministic finitary parity automata exactly characterize the star-free fragment of ωB-regular languages."}],"oa":1,"publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"26","day":"04","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"title":"Topological, automata-theoretic and logical characterization of finitary languages","date_created":"2018-12-12T11:39:03Z","oa_version":"Published Version","doi":"10.15479/AT:IST-2010-0002","file":[{"date_updated":"2020-07-14T12:46:43Z","access_level":"open_access","date_created":"2018-12-12T11:54:10Z","content_type":"application/pdf","checksum":"283d3604d76dd4d5161585d4c8625fbe","file_size":395662,"file_name":"IST-2010-0002_IST-2010-0002.pdf","creator":"system","file_id":"5532","relation":"main_file"}],"publisher":"IST Austria","has_accepted_license":"1","language":[{"iso":"eng"}],"status":"public","publication_status":"published","ddc":["000"],"page":"21","citation":{"ieee":"K. Chatterjee and N. Fijalkow, <i>Topological, automata-theoretic and logical characterization of finitary languages</i>. IST Austria, 2010.","apa":"Chatterjee, K., &#38; Fijalkow, N. (2010). <i>Topological, automata-theoretic and logical characterization of finitary languages</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2010-0002\">https://doi.org/10.15479/AT:IST-2010-0002</a>","ama":"Chatterjee K, Fijalkow N. <i>Topological, Automata-Theoretic and Logical Characterization of Finitary Languages</i>. IST Austria; 2010. doi:<a href=\"https://doi.org/10.15479/AT:IST-2010-0002\">10.15479/AT:IST-2010-0002</a>","mla":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. <i>Topological, Automata-Theoretic and Logical Characterization of Finitary Languages</i>. IST Austria, 2010, doi:<a href=\"https://doi.org/10.15479/AT:IST-2010-0002\">10.15479/AT:IST-2010-0002</a>.","chicago":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. <i>Topological, Automata-Theoretic and Logical Characterization of Finitary Languages</i>. IST Austria, 2010. <a href=\"https://doi.org/10.15479/AT:IST-2010-0002\">https://doi.org/10.15479/AT:IST-2010-0002</a>.","ista":"Chatterjee K, Fijalkow N. 2010. Topological, automata-theoretic and logical characterization of finitary languages, IST Austria, 21p.","short":"K. Chatterjee, N. Fijalkow, Topological, Automata-Theoretic and Logical Characterization of Finitary Languages, IST Austria, 2010."},"_id":"5390","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Fijalkow, Nathanaël","first_name":"Nathanaël","last_name":"Fijalkow"}],"year":"2010","date_updated":"2020-07-14T23:04:41Z","date_published":"2010-06-04T00:00:00Z"},{"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 objective. 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 polynomially 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"}],"arxiv":1,"month":"09","type":"conference","corr_author":"1","department":[{"_id":"KrCh"}],"article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1001.5183"}],"oa_version":"Preprint","date_created":"2018-12-11T12:05:31Z","doi":"10.1007/978-3-642-14162-1_50","title":"Energy parity games","language":[{"iso":"eng"}],"publist_id":"2330","publication_status":"published","intvolume":"      6199","_id":"3851","related_material":{"record":[{"status":"public","id":"2972","relation":"later_version"}]},"date_published":"2010-09-10T00:00:00Z","oa":1,"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"day":"10","volume":6199,"scopus_import":"1","publisher":"Springer","conference":{"start_date":"2010-07-06","end_date":"2010-07-10","name":"ICALP: Automata, Languages and Programming","location":"Bordeaux, France"},"citation":{"ista":"Chatterjee K, Doyen L. 2010. Energy parity games. ICALP: Automata, Languages and Programming, LNCS, vol. 6199, 599–610.","short":"K. Chatterjee, L. Doyen, in:, Springer, 2010, pp. 599–610.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Energy Parity Games,” 6199:599–610. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-14162-1_50\">https://doi.org/10.1007/978-3-642-14162-1_50</a>.","ieee":"K. Chatterjee and L. Doyen, “Energy parity games,” presented at the ICALP: Automata, Languages and Programming, Bordeaux, France, 2010, vol. 6199, pp. 599–610.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Energy Parity Games</i>. Vol. 6199, Springer, 2010, pp. 599–610, doi:<a href=\"https://doi.org/10.1007/978-3-642-14162-1_50\">10.1007/978-3-642-14162-1_50</a>.","ama":"Chatterjee K, Doyen L. Energy parity games. In: Vol 6199. Springer; 2010:599-610. doi:<a href=\"https://doi.org/10.1007/978-3-642-14162-1_50\">10.1007/978-3-642-14162-1_50</a>","apa":"Chatterjee, K., &#38; Doyen, L. (2010). Energy parity games (Vol. 6199, pp. 599–610). Presented at the ICALP: Automata, Languages and Programming, Bordeaux, France: Springer. <a href=\"https://doi.org/10.1007/978-3-642-14162-1_50\">https://doi.org/10.1007/978-3-642-14162-1_50</a>"},"page":"599 - 610","status":"public","year":"2010","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"}],"date_updated":"2025-09-30T08:02:20Z"},{"_id":"3852","date_published":"2010-06-08T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"        25","publication_status":"published","publist_id":"2329","department":[{"_id":"KrCh"}],"title":"Discounting in games across time scales","oa_version":"Published Version","doi":"10.4204/EPTCS.25.6","date_created":"2018-12-11T12:05:31Z","article_processing_charge":"No","type":"conference","arxiv":1,"month":"06","file_date_updated":"2020-07-14T12:46:17Z","abstract":[{"text":"We introduce two-level discounted games played by two players on a perfect-information stochastic game graph. The upper level game is a discounted game and the lower level game is an undiscounted reachability game. Two-level games model hierarchical and sequential decision making under uncertainty across different time scales. We show the existence of pure memoryless optimal strategies for both players and an ordered field property for such games. We show that if there is only one player (Markov decision processes), then the values can be computed in polynomial time. It follows that whether the value of a player is equal to a given rational constant in two-level discounted games can be decided in NP intersected coNP. We also give an alternate strategy improvement algorithm to compute the value. ","lang":"eng"}],"external_id":{"arxiv":["1006.1403"]},"pubrep_id":"491","corr_author":"1","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"}],"year":"2010","date_updated":"2024-10-09T20:54:08Z","conference":{"name":"GandALF: Games, Automata, Logic, and Formal Verification","start_date":"2010-06-17","end_date":"2010-06-18","location":"Minori, Italy"},"publisher":"EPTCS","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:46:17Z","date_created":"2018-12-12T10:12:19Z","content_type":"application/pdf","file_size":74598,"checksum":"2bdf1e9103710555c6251ca4153cb5e9","file_name":"IST-2016-491-v1+1_1006.1403v1.pdf","creator":"system","file_id":"4937","relation":"main_file"}],"scopus_import":"1","has_accepted_license":"1","status":"public","citation":{"chicago":"Chatterjee, Krishnendu, and Ritankar Majumdar. “Discounting in Games across Time Scales,” 25:22–29. EPTCS, 2010. <a href=\"https://doi.org/10.4204/EPTCS.25.6\">https://doi.org/10.4204/EPTCS.25.6</a>.","short":"K. Chatterjee, R. Majumdar, in:, EPTCS, 2010, pp. 22–29.","ista":"Chatterjee K, Majumdar R. 2010. Discounting in games across time scales. GandALF: Games, Automata, Logic, and Formal Verification, EPTCS, vol. 25, 22–29.","apa":"Chatterjee, K., &#38; Majumdar, R. (2010). Discounting in games across time scales (Vol. 25, pp. 22–29). Presented at the GandALF: Games, Automata, Logic, and Formal Verification, Minori, Italy: EPTCS. <a href=\"https://doi.org/10.4204/EPTCS.25.6\">https://doi.org/10.4204/EPTCS.25.6</a>","ieee":"K. Chatterjee and R. Majumdar, “Discounting in games across time scales,” presented at the GandALF: Games, Automata, Logic, and Formal Verification, Minori, Italy, 2010, vol. 25, pp. 22–29.","ama":"Chatterjee K, Majumdar R. Discounting in games across time scales. In: Vol 25. EPTCS; 2010:22-29. doi:<a href=\"https://doi.org/10.4204/EPTCS.25.6\">10.4204/EPTCS.25.6</a>","mla":"Chatterjee, Krishnendu, and Ritankar Majumdar. <i>Discounting in Games across Time Scales</i>. Vol. 25, EPTCS, 2010, pp. 22–29, doi:<a href=\"https://doi.org/10.4204/EPTCS.25.6\">10.4204/EPTCS.25.6</a>."},"ddc":["000"],"page":"22 - 29","day":"08","alternative_title":["EPTCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":25,"quality_controlled":"1","oa":1},{"language":[{"iso":"eng"}],"publist_id":"2328","intvolume":"      6269","publication_status":"published","_id":"3853","date_published":"2010-11-18T00:00:00Z","project":[{"name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","name":"Design for Embedded Systems"}],"file_date_updated":"2020-07-14T12:46:17Z","type":"conference","month":"11","abstract":[{"text":"Quantitative languages are an extension of boolean languages that assign to each word a real number. Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition weights. When the mode of branching of the automaton is deterministic, nondeterministic, or alternating, the corresponding class of quantitative languages is not robust as it is not closed under the pointwise operations of max, min, sum, and numerical complement. Nondeterministic and alternating mean-payoff automata are not decidable either, as the quantitative generalization of the problems of universality and language inclusion is undecidable. We introduce a new class of quantitative languages, defined by mean-payoff automaton expressions, which is robust and decidable: it is closed under the four pointwise operations, and we show that all decision problems are decidable for this class. Mean-payoff automaton expressions subsume deterministic meanpayoff automata, and we show that they have expressive power incomparable to nondeterministic and alternating mean-payoff automata. We also present for the first time an algorithm to compute distance between two quantitative languages, and in our case the quantitative languages are given as mean-payoff automaton expressions.","lang":"eng"}],"pubrep_id":"62","corr_author":"1","department":[{"_id":"KrCh"},{"_id":"HeEd"},{"_id":"ToHe"}],"date_created":"2018-12-11T12:05:31Z","oa_version":"Submitted Version","doi":"10.1007/978-3-642-15375-4_19","title":"Mean-payoff automaton expressions","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"relation":"main_file","file_id":"5163","creator":"system","file_name":"IST-2012-62-v1+1_Mean-payoff_automaton_expressions.pdf","content_type":"application/pdf","checksum":"4f753ae99d076553fb8733e2c8b390e2","file_size":233260,"date_created":"2018-12-12T10:15:41Z","access_level":"open_access","date_updated":"2020-07-14T12:46:17Z"}],"conference":{"name":"CONCUR: Concurrency Theory","start_date":"2010-08-31","end_date":"2010-09-03","location":"Paris, France"},"scopus_import":1,"has_accepted_license":"1","ec_funded":1,"citation":{"apa":"Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T. A., &#38; Rannou, P. (2010). Mean-payoff automaton expressions (Vol. 6269, pp. 269–283). Presented at the CONCUR: Concurrency Theory, Paris, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-642-15375-4_19\">https://doi.org/10.1007/978-3-642-15375-4_19</a>","ieee":"K. Chatterjee, L. Doyen, H. Edelsbrunner, T. A. Henzinger, and P. Rannou, “Mean-payoff automaton expressions,” presented at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 269–283.","ama":"Chatterjee K, Doyen L, Edelsbrunner H, Henzinger TA, Rannou P. Mean-payoff automaton expressions. In: Vol 6269. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:269-283. doi:<a href=\"https://doi.org/10.1007/978-3-642-15375-4_19\">10.1007/978-3-642-15375-4_19</a>","mla":"Chatterjee, Krishnendu, et al. <i>Mean-Payoff Automaton Expressions</i>. Vol. 6269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 269–83, doi:<a href=\"https://doi.org/10.1007/978-3-642-15375-4_19\">10.1007/978-3-642-15375-4_19</a>.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Herbert Edelsbrunner, Thomas A Henzinger, and Philippe Rannou. “Mean-Payoff Automaton Expressions,” 6269:269–83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15375-4_19\">https://doi.org/10.1007/978-3-642-15375-4_19</a>.","short":"K. Chatterjee, L. Doyen, H. Edelsbrunner, T.A. Henzinger, P. Rannou, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 269–283.","ista":"Chatterjee K, Doyen L, Edelsbrunner H, Henzinger TA, Rannou P. 2010. Mean-payoff automaton expressions. CONCUR: Concurrency Theory, LNCS, vol. 6269, 269–283."},"ddc":["000","005"],"page":"269 - 283","status":"public","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"first_name":"Herbert","last_name":"Edelsbrunner","full_name":"Edelsbrunner, Herbert","orcid":"0000-0002-9823-6833","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Rannou","first_name":"Philippe","full_name":"Rannou, Philippe"}],"year":"2010","date_updated":"2024-10-09T20:54:08Z","oa":1,"quality_controlled":"1","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","day":"18","alternative_title":["LNCS"],"volume":6269},{"publist_id":"2327","page":"284 - 296","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Obliging Games</i>. Vol. 6269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 284–96, doi:<a href=\"https://doi.org/10.1007/978-3-642-15375-4_20\">10.1007/978-3-642-15375-4_20</a>.","ieee":"K. Chatterjee, F. Horn, and C. Löding, “Obliging games,” presented at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 284–296.","ama":"Chatterjee K, Horn F, Löding C. Obliging games. In: Vol 6269. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:284-296. doi:<a href=\"https://doi.org/10.1007/978-3-642-15375-4_20\">10.1007/978-3-642-15375-4_20</a>","apa":"Chatterjee, K., Horn, F., &#38; Löding, C. (2010). Obliging games (Vol. 6269, pp. 284–296). Presented at the CONCUR: Concurrency Theory, Paris, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-642-15375-4_20\">https://doi.org/10.1007/978-3-642-15375-4_20</a>","short":"K. Chatterjee, F. Horn, C. Löding, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 284–296.","chicago":"Chatterjee, Krishnendu, Florian Horn, and Christof Löding. “Obliging Games,” 6269:284–96. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15375-4_20\">https://doi.org/10.1007/978-3-642-15375-4_20</a>.","ista":"Chatterjee K, Horn F, Löding C. 2010. Obliging games. CONCUR: Concurrency Theory, LNCS, vol. 6269, 284–296."},"intvolume":"      6269","status":"public","publication_status":"published","language":[{"iso":"eng"}],"conference":{"name":"CONCUR: Concurrency Theory","end_date":"2010-09-03","start_date":"2010-08-31","location":"Paris, France"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":1,"date_published":"2010-09-08T00:00:00Z","date_updated":"2024-10-09T20:54:07Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"37327ACE-F248-11E8-B48F-1D18A9856A87","full_name":"Horn, Florian","first_name":"Florian","last_name":"Horn"},{"first_name":"Christof","last_name":"Löding","full_name":"Löding, Christof"}],"year":"2010","_id":"3854","corr_author":"1","month":"09","type":"conference","quality_controlled":"1","abstract":[{"text":"Graph games of infinite length provide a natural model for open reactive systems: one player (Eve) represents the controller and the other player (Adam) represents the environment. The evolution of the system depends on the decisions of both players. The specification for the system is usually given as an ω-regular language L over paths and Eve’s goal is to ensure that the play belongs to L irrespective of Adam’s behaviour. The classical notion of winning strategies fails to capture several interesting scenarios. For example, strong fairness (Streett) conditions are specified by a number of request-grant pairs and require every pair that is requested infinitely often to be granted infinitely often: Eve might win just by preventing Adam from making any new request, but a “better” strategy would allow Adam to make as many requests as possible and still ensure fairness. To address such questions, we introduce the notion of obliging games, where Eve has to ensure a strong condition Φ, while always allowing Adam to satisfy a weak condition Ψ. We present a linear time reduction of obliging games with two Muller conditions Φ and Ψ to classical Muller games. We consider obliging Streett games and show they are co-NP complete, and show a natural quantitative optimisation problem for obliging Streett games is in FNP. We also show how obliging games can provide new and interesting semantics for multi-player games.","lang":"eng"}],"date_created":"2018-12-11T12:05:32Z","doi":"10.1007/978-3-642-15375-4_20","oa_version":"None","title":"Obliging games","volume":6269,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"day":"08","alternative_title":["LNCS"]},{"language":[{"iso":"eng"}],"intvolume":"      6281","publication_status":"published","publist_id":"2326","_id":"3855","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5395"}]},"date_published":"2010-08-01T00:00:00Z","file_date_updated":"2020-07-14T12:46:17Z","month":"08","type":"conference","abstract":[{"lang":"eng","text":"We study observation-based strategies for partially-observable Markov decision processes (POMDPs) with parity objectives. An observation-based strategy relies on partial information about the history of a play, namely, on the past sequence of observations. We consider qualitative analysis problems: given a POMDP with a parity objective, decide whether there exists an observation-based strategy to achieve the objective with probability 1 (almost-sure winning), or with positive probability (positive winning). Our main results are twofold. First, we present a complete picture of the computational complexity of the qualitative analysis problem for POMDPs with parity objectives and its subclasses: safety, reachability, Büchi, and coBüchi objectives. We establish several upper and lower bounds that were not known in the literature. Second, we give optimal bounds (matching upper and lower bounds) for the memory required by pure and randomized observation-based strategies for each class of objectives."}],"project":[{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","grant_number":"214373","call_identifier":"FP7"}],"corr_author":"1","pubrep_id":"61","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Qualitative analysis of partially-observable Markov Decision Processes","date_created":"2018-12-11T12:05:32Z","oa_version":"Submitted Version","doi":"10.1007/978-3-642-15155-2_24","publisher":"Springer","file":[{"content_type":"application/pdf","checksum":"b6c82ec82f194e5b0ab7c1c3800e4580","file_size":173948,"date_created":"2018-12-12T10:13:51Z","date_updated":"2020-07-14T12:46:17Z","access_level":"open_access","relation":"main_file","file_id":"5038","creator":"system","file_name":"IST-2012-61-v1+1_Qualitative_analysis_of_partially-observable_Markov_Decision_Processes.pdf"}],"conference":{"start_date":"2010-08-23","end_date":"2010-08-27","name":"MFCS: Mathematical Foundations of Computer Science","location":"Brno, Czech Republic"},"scopus_import":1,"ec_funded":1,"has_accepted_license":"1","status":"public","page":"258 - 269","citation":{"short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2010, pp. 258–269.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Qualitative Analysis of Partially-Observable Markov Decision Processes,” 6281:258–69. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15155-2_24\">https://doi.org/10.1007/978-3-642-15155-2_24</a>.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2010. Qualitative analysis of partially-observable Markov Decision Processes. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 6281, 258–269.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2010). Qualitative analysis of partially-observable Markov Decision Processes (Vol. 6281, pp. 258–269). Presented at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic: Springer. <a href=\"https://doi.org/10.1007/978-3-642-15155-2_24\">https://doi.org/10.1007/978-3-642-15155-2_24</a>","ama":"Chatterjee K, Doyen L, Henzinger TA. Qualitative analysis of partially-observable Markov Decision Processes. In: Vol 6281. Springer; 2010:258-269. doi:<a href=\"https://doi.org/10.1007/978-3-642-15155-2_24\">10.1007/978-3-642-15155-2_24</a>","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “Qualitative analysis of partially-observable Markov Decision Processes,” presented at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic, 2010, vol. 6281, pp. 258–269.","mla":"Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of Partially-Observable Markov Decision Processes</i>. Vol. 6281, Springer, 2010, pp. 258–69, doi:<a href=\"https://doi.org/10.1007/978-3-642-15155-2_24\">10.1007/978-3-642-15155-2_24</a>."},"ddc":["004"],"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"year":"2010","date_updated":"2024-10-09T21:08:23Z","quality_controlled":"1","oa":1,"day":"01","alternative_title":["LNCS"],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","volume":6281},{"intvolume":"      6281","publication_status":"published","publist_id":"2325","language":[{"iso":"eng"}],"date_published":"2010-09-06T00:00:00Z","related_material":{"record":[{"id":"1731","relation":"later_version","status":"public"}]},"_id":"3856","acknowledgement":"This research was supported by the European Union project COMBEST and the European Network of Excellence ArtistDesign.","corr_author":"1","pubrep_id":"60","month":"09","arxiv":1,"type":"conference","abstract":[{"lang":"eng","text":"We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (players interact simultaneously); and (b) turn-based (players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. We present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function (probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games. "}],"external_id":{"arxiv":["1006.0673"]},"project":[{"grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"title":"Randomness for free","date_created":"2018-12-11T12:05:32Z","doi":"10.1007/978-3-642-15155-2_23","oa_version":"Preprint","main_file_link":[{"url":"https://arxiv.org/abs/1006.0673","open_access":"1"}],"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"status":"public","page":"246 - 257","citation":{"short":"K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, in:, Springer, 2010, pp. 246–257.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger. “Randomness for Free,” 6281:246–57. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15155-2_23\">https://doi.org/10.1007/978-3-642-15155-2_23</a>.","ista":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2010. Randomness for free. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 6281, 246–257.","mla":"Chatterjee, Krishnendu, et al. <i>Randomness for Free</i>. Vol. 6281, Springer, 2010, pp. 246–57, doi:<a href=\"https://doi.org/10.1007/978-3-642-15155-2_23\">10.1007/978-3-642-15155-2_23</a>.","ieee":"K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for free,” presented at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic, 2010, vol. 6281, pp. 246–257.","apa":"Chatterjee, K., Doyen, L., Gimbert, H., &#38; Henzinger, T. A. (2010). Randomness for free (Vol. 6281, pp. 246–257). Presented at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic: Springer. <a href=\"https://doi.org/10.1007/978-3-642-15155-2_23\">https://doi.org/10.1007/978-3-642-15155-2_23</a>","ama":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. In: Vol 6281. Springer; 2010:246-257. doi:<a href=\"https://doi.org/10.1007/978-3-642-15155-2_23\">10.1007/978-3-642-15155-2_23</a>"},"conference":{"location":"Brno, Czech Republic","end_date":"2010-08-27","start_date":"2010-08-23","name":"MFCS: Mathematical Foundations of Computer Science"},"publisher":"Springer","ec_funded":1,"scopus_import":"1","date_updated":"2025-09-23T10:32:00Z","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"first_name":"Hugo","last_name":"Gimbert","full_name":"Gimbert, Hugo"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"year":"2010","quality_controlled":"1","oa":1,"volume":6281,"day":"06","alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"}]