[{"datarep_id":"28","oa":1,"type":"research_data","ec_funded":1,"file":[{"file_id":"5597","date_updated":"2020-07-14T12:47:00Z","relation":"main_file","date_created":"2018-12-12T13:02:31Z","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","creator":"system","checksum":"b8bcb43c0893023cda66c1b69c16ac62","file_size":49557109,"content_type":"application/zip","access_level":"open_access"}],"year":"2015","keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"article_processing_charge":"No","date_published":"2015-08-13T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Institute of Science and Technology Austria","abstract":[{"text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication.","lang":"eng"}],"date_created":"2018-12-12T12:31:29Z","has_accepted_license":"1","month":"08","ddc":["004"],"status":"public","file_date_updated":"2020-07-14T12:47:00Z","related_material":{"record":[{"relation":"popular_science","id":"1603","status":"public"}]},"day":"13","contributor":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan"}],"license":"https://creativecommons.org/publicdomain/zero/1.0/","author":[{"id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","full_name":"Fellner, Andreas","first_name":"Andreas","last_name":"Fellner"}],"date_updated":"2025-09-23T08:23:15Z","title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"tmp":{"short":"CC0 (1.0)","name":"Creative Commons Public Domain Dedication (CC0 1.0)","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","image":"/images/cc_0.png"},"doi":"10.15479/AT:ISTA:28","citation":{"short":"A. Fellner, (2015).","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>.","ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>","mla":"Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute of Science and Technology Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015."},"project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"oa_version":"Published Version","publist_id":"5564","_id":"5549"},{"date_published":"2015-01-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","article_processing_charge":"No","year":"2015","oa":1,"type":"conference","ec_funded":1,"page":"1018-1029","status":"public","publication":"Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms","corr_author":"1","month":"01","issue":"1","intvolume":"      2015","OA_type":"green","language":[{"iso":"eng"}],"publisher":"SIAM","date_created":"2022-02-25T12:18:43Z","abstract":[{"lang":"eng","text":"We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy)."}],"title":"The value 1 problem under finite-memory strategies for concurrent mean-payoff games","date_updated":"2025-06-26T06:54:08Z","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"}],"external_id":{"arxiv":["1409.6690"]},"conference":{"end_date":"2015-01-06","start_date":"2015-01-04","name":"SODA: Symposium on Discrete Algorithms","location":"San Diego, CA, United States"},"OA_place":"publisher","arxiv":1,"day":"01","acknowledgement":"The research was partly supported by FWF Grant No P 23499-N23, FWF NFN Grant\r\nNo S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","publication_identifier":{"isbn":["978-161197374-7"]},"quality_controlled":"1","oa_version":"Preprint","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1409.6690","open_access":"1"}],"_id":"10796","citation":{"mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under Finite-Memory Strategies for Concurrent Mean-Payoff Games.” <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>, vol. 2015, no. 1, SIAM, 2015, pp. 1018–29, doi:<a href=\"https://doi.org/10.1137/1.9781611973730.69\">10.1137/1.9781611973730.69</a>.","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The value 1 problem under finite-memory strategies for concurrent mean-payoff games,” in <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>, San Diego, CA, United States, 2015, vol. 2015, no. 1, pp. 1018–1029.","ista":"Chatterjee K, Ibsen-Jensen R. 2015. The value 1 problem under finite-memory strategies for concurrent mean-payoff games. Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms vol. 2015, 1018–1029.","ama":"Chatterjee K, Ibsen-Jensen R. The value 1 problem under finite-memory strategies for concurrent mean-payoff games. In: <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>. Vol 2015. SIAM; 2015:1018-1029. doi:<a href=\"https://doi.org/10.1137/1.9781611973730.69\">10.1137/1.9781611973730.69</a>","apa":"Chatterjee, K., &#38; Ibsen-Jensen, R. (2015). The value 1 problem under finite-memory strategies for concurrent mean-payoff games. In <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i> (Vol. 2015, pp. 1018–1029). San Diego, CA, United States: SIAM. <a href=\"https://doi.org/10.1137/1.9781611973730.69\">https://doi.org/10.1137/1.9781611973730.69</a>","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under Finite-Memory Strategies for Concurrent Mean-Payoff Games.” In <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>, 2015:1018–29. SIAM, 2015. <a href=\"https://doi.org/10.1137/1.9781611973730.69\">https://doi.org/10.1137/1.9781611973730.69</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, in:, Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2015, pp. 1018–1029."},"doi":"10.1137/1.9781611973730.69","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"volume":2015,"department":[{"_id":"KrCh"}],"scopus_import":"1"},{"oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"url":"http://arxiv.org/abs/1006.0673","open_access":"1"}],"_id":"1731","publist_id":"5395","volume":245,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","doi":"10.1016/j.ic.2015.06.003","citation":{"short":"K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation 245 (2015) 3–16.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger. “Randomness for Free.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>.","ama":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. <i>Information and Computation</i>. 2015;245(12):3-16. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>","ista":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free. Information and Computation. 245(12), 3–16.","apa":"Chatterjee, K., Doyen, L., Gimbert, H., &#38; Henzinger, T. A. (2015). Randomness for free. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>","mla":"Chatterjee, Krishnendu, et al. “Randomness for Free.” <i>Information and Computation</i>, vol. 245, no. 12, Elsevier, 2015, pp. 3–16, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>.","ieee":"K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for free,” <i>Information and Computation</i>, vol. 245, no. 12. Elsevier, pp. 3–16, 2015."},"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"},{"grant_number":"214373","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"full_name":"Gimbert, Hugo","last_name":"Gimbert","first_name":"Hugo"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"title":"Randomness for free","date_updated":"2025-09-23T10:32:00Z","arxiv":1,"day":"01","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3856"}]},"external_id":{"arxiv":["1006.0673"],"isi":["000368899100002"]},"issue":"12","status":"public","corr_author":"1","month":"12","publication":"Information and Computation","publisher":"Elsevier","date_created":"2018-12-11T11:53:42Z","abstract":[{"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 (both players interact simultaneously); and (b) turn-based (both 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. In this work 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. ","lang":"eng"}],"intvolume":"       245","language":[{"iso":"eng"}],"publication_status":"published","article_processing_charge":"No","year":"2015","date_published":"2015-12-01T00:00:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","page":"3 - 16","oa":1,"ec_funded":1,"isi":1,"type":"journal_article"},{"department":[{"_id":"KrCh"}],"scopus_import":1,"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"doi":"10.1109/ICRA.2015.7139019","citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications,” 325–30. IEEE, 2015. <a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">https://doi.org/10.1109/ICRA.2015.7139019</a>.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, IEEE, 2015, pp. 325–330.","mla":"Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IEEE, 2015, pp. 325–30, doi:<a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">10.1109/ICRA.2015.7139019</a>.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Qualitative analysis of POMDPs with temporal logic specifications for robotics applications,” presented at the ICRA: International Conference on Robotics and Automation, Seattle, WA, United States, 2015, pp. 325–330.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., &#38; Kanodia, A. (2015). Qualitative analysis of POMDPs with temporal logic specifications for robotics applications (pp. 325–330). Presented at the ICRA: International Conference on Robotics and Automation, Seattle, WA, United States: IEEE. <a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">https://doi.org/10.1109/ICRA.2015.7139019</a>","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. ICRA: International Conference on Robotics and Automation, 325–330.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. In: IEEE; 2015:325-330. doi:<a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">10.1109/ICRA.2015.7139019</a>"},"publist_id":"5394","_id":"1732","main_file_link":[{"url":"http://arxiv.org/abs/1409.3360","open_access":"1"}],"oa_version":"Preprint","quality_controlled":"1","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5424"},{"id":"5426","relation":"earlier_version","status":"public"}]},"day":"01","arxiv":1,"conference":{"name":"ICRA: International Conference on Robotics and Automation","location":"Seattle, WA, United States","start_date":"2015-05-26","end_date":"2015-05-30"},"external_id":{"arxiv":["1409.3360"]},"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin"},{"full_name":"Gupta, Raghav","last_name":"Gupta","first_name":"Raghav"},{"full_name":"Kanodia, Ayush","last_name":"Kanodia","first_name":"Ayush"}],"date_updated":"2023-02-23T12:25:52Z","title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","date_created":"2018-12-11T11:53:43Z","abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty."}],"publisher":"IEEE","language":[{"iso":"eng"}],"status":"public","month":"01","page":"325 - 330","type":"conference","ec_funded":1,"oa":1,"year":"2015","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2015-01-01T00:00:00Z"},{"alternative_title":["LNCS"],"abstract":[{"text":"Synthesis of program parts is particularly useful for concurrent systems. However, most approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis (AGS) provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize.We resolve this shortcoming by defining AGS under partial information. We analyze the complexity and decidability in different settings, showing that the problem has a high worstcase complexity and is undecidable in many interesting cases. Based on these observations, we present a pragmatic algorithm based on bounded synthesis, and demonstrate its practical applicability on several examples.","lang":"eng"}],"date_created":"2018-12-11T11:54:17Z","publisher":"Springer","language":[{"iso":"eng"}],"intvolume":"      9035","month":"01","status":"public","page":"517 - 532","ec_funded":1,"type":"conference","oa":1,"article_processing_charge":"No","year":"2015","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2015-01-01T00:00:00Z","scopus_import":"1","department":[{"_id":"KrCh"}],"volume":9035,"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"doi":"10.1007/978-3-662-46681-0_50","citation":{"apa":"Bloem, R., Chatterjee, K., Jacobs, S., &#38; Könighofer, R. (2015). Assume-guarantee synthesis for concurrent reactive programs with partial information (Vol. 9035, pp. 517–532). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">https://doi.org/10.1007/978-3-662-46681-0_50</a>","ama":"Bloem R, Chatterjee K, Jacobs S, Könighofer R. Assume-guarantee synthesis for concurrent reactive programs with partial information. In: Vol 9035. Springer; 2015:517-532. doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">10.1007/978-3-662-46681-0_50</a>","ista":"Bloem R, Chatterjee K, Jacobs S, Könighofer R. 2015. Assume-guarantee synthesis for concurrent reactive programs with partial information. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9035, 517–532.","mla":"Bloem, Roderick, et al. <i>Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information</i>. Vol. 9035, Springer, 2015, pp. 517–32, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">10.1007/978-3-662-46681-0_50</a>.","ieee":"R. Bloem, K. Chatterjee, S. Jacobs, and R. Könighofer, “Assume-guarantee synthesis for concurrent reactive programs with partial information,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom, 2015, vol. 9035, pp. 517–532.","short":"R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp. 517–532.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Swen Jacobs, and Robert Könighofer. “Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information,” 9035:517–32. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">https://doi.org/10.1007/978-3-662-46681-0_50</a>."},"publist_id":"5264","_id":"1838","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1411.4604"}],"oa_version":"Preprint","acknowledgement":"This work was supported by the Austrian Science Fund (FWF) through the research network RiSE (S11406-N23, S11407-N23) and grant nr. P23499-N23, by the European Commission through an ERC Start grant (279307: Graph Games) and project STANCE (317753), as well as by the German Research Foundation (DFG) through SFB/TR 14 AVACS and project ASDPS(JA 2357/2-1).","day":"01","arxiv":1,"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"London, United Kingdom","start_date":"2015-04-11","end_date":"2015-04-18"},"external_id":{"arxiv":["1411.4604"]},"author":[{"full_name":"Bloem, Roderick","last_name":"Bloem","first_name":"Roderick"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Jacobs, Swen","first_name":"Swen","last_name":"Jacobs"},{"first_name":"Robert","last_name":"Könighofer","full_name":"Könighofer, Robert"}],"date_updated":"2025-06-11T07:09:03Z","title":"Assume-guarantee synthesis for concurrent reactive programs with partial information"},{"publisher":"Springer","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i) generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii) generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies."}],"date_created":"2018-12-11T11:54:18Z","intvolume":"      9035","language":[{"iso":"eng"}],"status":"public","month":"01","page":"181 - 187","oa":1,"type":"conference","ec_funded":1,"series_title":"Lecture Notes in Computer Science","year":"2015","article_processing_charge":"No","publication_status":"published","date_published":"2015-01-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":9035,"scopus_import":"1","department":[{"_id":"KrCh"}],"doi":"10.1007/978-3-662-46681-0_12","citation":{"ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives,” vol. 9035. Springer, pp. 181–187, 2015.","mla":"Brázdil, Tomáš, et al. <i>Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives</i>. Vol. 9035, Springer, 2015, pp. 181–87, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">10.1007/978-3-662-46681-0_12</a>.","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. 2015;9035:181-187. doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">10.1007/978-3-662-46681-0_12</a>","apa":"Brázdil, T., Chatterjee, K., Forejt, V., &#38; Kučera, A. (2015). Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">https://doi.org/10.1007/978-3-662-46681-0_12</a>","ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2015. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. 9035, 181–187.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">https://doi.org/10.1007/978-3-662-46681-0_12</a>.","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187."},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"main_file_link":[{"url":"http://arxiv.org/abs/1501.03093","open_access":"1"}],"quality_controlled":"1","oa_version":"Preprint","publist_id":"5263","_id":"1839","arxiv":1,"day":"01","external_id":{"arxiv":["1501.03093"]},"conference":{"end_date":"2015-04-18","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"London, United Kingdom","start_date":"2015-04-11"},"author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"full_name":"Kučera, Antonín","first_name":"Antonín","last_name":"Kučera"}],"date_updated":"2025-06-11T07:09:21Z","title":"Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives"},{"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium on Automata, Languages, and Programming</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd International Colloquium on Automata, Languages, and Programming</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium on Automata, Languages, and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium on Automata, Languages, and Programming</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium on Automata, Languages, and Programming</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium on Automata, Languages, and Programming</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium on Automata, Languages, and Programming, Springer Nature, 2015, pp. 121–133."},"doi":"10.1007/978-3-662-47666-6_10","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","volume":9135,"_id":"1610","publist_id":"5556","oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.08259"}],"pubrep_id":"321","conference":{"location":"Kyoto, Japan","name":"ICALP: Automata, Languages and Programming","start_date":"2015-07-06","end_date":"2015-07-10"},"OA_place":"repository","external_id":{"isi":["000364317900010"],"arxiv":["1504.08259"]},"day":"01","acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects\r\nS11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499-\r\nN23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph\r\nGames), and MSR faculty fellows award.","related_material":{"record":[{"relation":"earlier_version","id":"5438","status":"public"},{"relation":"later_version","id":"465","status":"public"}]},"publication_identifier":{"isbn":["978-3-662-47665-9"]},"arxiv":1,"title":"Edit distance for pushdown automata","date_updated":"2026-07-06T13:27:53Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"}],"language":[{"iso":"eng"}],"OA_type":"green","intvolume":"      9135","date_created":"2018-12-11T11:53:01Z","abstract":[{"lang":"eng","text":"The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k."}],"alternative_title":["LNCS"],"publisher":"Springer Nature","status":"public","month":"07","publication":"42nd International Colloquium on Automata, Languages, and Programming","issue":"Part II","type":"conference","isi":1,"ec_funded":1,"oa":1,"page":"121 - 133","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2015-07-01T00:00:00Z","publication_status":"published","year":"2015","article_processing_charge":"No"},{"ec_funded":1,"type":"conference","isi":1,"oa":1,"page":"244 - 256","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2015-07-01T00:00:00Z","year":"2015","article_processing_charge":"No","publication_status":"published","series_title":"LICS","language":[{"iso":"eng"}],"OA_type":"green","alternative_title":["LICS"],"date_created":"2018-12-11T11:53:18Z","abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. ","lang":"eng"}],"publisher":"IEEE","status":"public","month":"07","OA_place":"repository","conference":{"end_date":"2015-07-10","name":"LICS: Logic in Computer Science","location":"Kyoto, Japan","start_date":"2015-07-06"},"external_id":{"isi":["000380427100024"]},"related_material":{"record":[{"status":"public","id":"5429","relation":"earlier_version"},{"relation":"earlier_version","id":"5435","status":"public"},{"status":"public","relation":"later_version","id":"466"}]},"acknowledgement":"A Technical Report of this paper is available at DOI: 10.15479/AT:IST-2015-318-v1-1\r\n","day":"01","date_updated":"2026-07-06T13:26:26Z","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"full_name":"Komárková, Zuzana","last_name":"Komárková","first_name":"Zuzana"},{"first_name":"Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"}],"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"doi":"10.1109/LICS.2015.32","citation":{"short":"K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.","chicago":"Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>.","apa":"Chatterjee, K., Komárková, Z., &#38; Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>","ama":"Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>","ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.","mla":"Chatterjee, Krishnendu, et al. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IEEE, 2015, pp. 244–56, doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>.","ieee":"K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015."},"scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publist_id":"5493","_id":"1657","main_file_link":[{"open_access":"1","url":"https://doi.org/10.15479/AT:IST-2015-318-v1-1"}],"quality_controlled":"1","oa_version":"Preprint"},{"oa":1,"type":"technical_report","page":"51","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5429"},{"status":"public","id":"1657","relation":"later_version"},{"relation":"later_version","id":"466","status":"public"}]},"publication_identifier":{"issn":["2664-1690"]},"file_date_updated":"2020-07-14T12:46:53Z","day":"23","date_published":"2015-02-23T00:00:00Z","date_updated":"2026-07-06T13:26:26Z","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"IST-2015-318-v2+1_main.pdf","creator":"system","checksum":"75284adec80baabdfe71ff9ebbc27445","date_created":"2018-12-12T11:54:03Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_size":717630,"file_id":"5525","date_updated":"2020-07-14T12:46:53Z"}],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Komarkova","first_name":"Zuzana","full_name":"Komarkova, Zuzana"},{"orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"}],"year":"2015","publication_status":"published","citation":{"chicago":"Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-318-v2-1\">https://doi.org/10.15479/AT:IST-2015-318-v2-1</a>.","short":"K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.","ieee":"K. Chatterjee, Z. Komarkova, and J. Kretinsky, <i>Unifying two views on multiple mean-payoff objectives in Markov decision processes</i>. IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-318-v2-1\">10.15479/AT:IST-2015-318-v2-1</a>.","ama":"Chatterjee K, Komarkova Z, Kretinsky J. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-318-v2-1\">10.15479/AT:IST-2015-318-v2-1</a>","ista":"Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 51p.","apa":"Chatterjee, K., Komarkova, Z., &#38; Kretinsky, J. (2015). <i>Unifying two views on multiple mean-payoff objectives in Markov decision processes</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-318-v2-1\">https://doi.org/10.15479/AT:IST-2015-318-v2-1</a>"},"doi":"10.15479/AT:IST-2015-318-v2-1","language":[{"iso":"eng"}],"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. \r\nThere have been two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector.  \r\nWe consider the problem where the goal is to optimize the expectation under the constraint that the satisfaction semantics is ensured, and thus consider a generalization that unifies the existing semantics. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensures certain probabilistic guarantee).\r\nOur main results are algorithms for the decision problem which are always polynomial in the size of the MDP.\r\nWe also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Finally, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem.","lang":"eng"}],"department":[{"_id":"KrCh"}],"date_created":"2018-12-12T11:39:19Z","has_accepted_license":"1","status":"public","month":"02","oa_version":"Published Version","ddc":["004"],"_id":"5435","pubrep_id":"327"},{"_id":"5429","oa_version":"Published Version","status":"public","month":"01","ddc":["004"],"pubrep_id":"318","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2015-318-v1-1","citation":{"ieee":"K. Chatterjee, Z. Komarkova, and J. Kretinsky, <i>Unifying two views on multiple mean-payoff objectives in Markov decision processes</i>. IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-318-v1-1\">10.15479/AT:IST-2015-318-v1-1</a>.","ista":"Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 41p.","ama":"Chatterjee K, Komarkova Z, Kretinsky J. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-318-v1-1\">10.15479/AT:IST-2015-318-v1-1</a>","apa":"Chatterjee, K., Komarkova, Z., &#38; Kretinsky, J. (2015). <i>Unifying two views on multiple mean-payoff objectives in Markov decision processes</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-318-v1-1\">https://doi.org/10.15479/AT:IST-2015-318-v1-1</a>","chicago":"Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-318-v1-1\">https://doi.org/10.15479/AT:IST-2015-318-v1-1</a>.","short":"K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015."},"date_created":"2018-12-12T11:39:17Z","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. \r\nThere have been two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector.  \r\nWe consider the problem where the goal is to optimize the expectation under the constraint that the satisfaction semantics is ensured, and thus consider a generalization that unifies the existing semantics.\r\nOur problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensures certain probabilistic guarantee).\r\nOur main results are algorithms for the decision problem which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions.\r\nFinally, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem."}],"department":[{"_id":"KrCh"}],"has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","date_published":"2015-01-12T00:00:00Z","date_updated":"2026-07-06T13:26:26Z","publication_status":"published","year":"2015","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Zuzana","last_name":"Komarkova","full_name":"Komarkova, Zuzana"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"file":[{"file_id":"5533","date_updated":"2020-07-14T12:46:52Z","file_name":"IST-2015-318-v1+1_main.pdf","checksum":"e4869a584567c506349abda9c8ec7db3","creator":"system","date_created":"2018-12-12T11:54:11Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_size":689863}],"type":"technical_report","oa":1,"day":"12","file_date_updated":"2020-07-14T12:46:52Z","publication_identifier":{"issn":["2664-1690"]},"related_material":{"record":[{"id":"5435","relation":"later_version","status":"public"},{"status":"public","relation":"later_version","id":"1657"},{"relation":"later_version","id":"466","status":"public"}]},"page":"41"},{"publication_status":"published","year":"2015","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"file":[{"content_type":"application/pdf","access_level":"open_access","file_size":422573,"file_name":"IST-2015-334-v1+1_report.pdf","checksum":"8a5f2d77560e552af87eb1982437a43b","creator":"system","relation":"main_file","date_created":"2018-12-12T11:53:56Z","date_updated":"2020-07-14T12:46:55Z","file_id":"5518"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Edit distance for pushdown automata","date_published":"2015-05-05T00:00:00Z","date_updated":"2026-07-06T13:27:53Z","day":"05","related_material":{"record":[{"status":"public","relation":"later_version","id":"1610"},{"status":"public","relation":"later_version","id":"465"}]},"file_date_updated":"2020-07-14T12:46:55Z","publication_identifier":{"issn":["2664-1690"]},"page":"15","type":"technical_report","oa":1,"pubrep_id":"334","_id":"5438","oa_version":"Published Version","status":"public","ddc":["004"],"month":"05","date_created":"2018-12-12T11:39:20Z","has_accepted_license":"1","abstract":[{"text":"The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1, L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses.\r\nThe problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k. ","lang":"eng"}],"department":[{"_id":"KrCh"}],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2015-334-v1-1","citation":{"apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). <i>Edit distance for pushdown automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">https://doi.org/10.15479/AT:IST-2015-334-v1-1</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. <i>Edit Distance for Pushdown Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">10.15479/AT:IST-2015-334-v1-1</a>","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata, IST Austria, 15p.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, <i>Edit distance for pushdown automata</i>. IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. <i>Edit Distance for Pushdown Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">10.15479/AT:IST-2015-334-v1-1</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Edit Distance for Pushdown Automata, IST Austria, 2015.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. <i>Edit Distance for Pushdown Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">https://doi.org/10.15479/AT:IST-2015-334-v1-1</a>."}},{"month":"07","publication":"Proceedings - Symposium on Logic in Computer Science","status":"public","abstract":[{"text":"The computation of the winning set for one-pair Streett objectives and for k-pair Streett objectives in (standard) graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formed ness of specifications, and the synthesis of reactive systems. We give faster algorithms for the computation of the winning set for (1) one-pair Streett objectives (aka parity-3 problem) in game graphs and (2) for k-pair Streett objectives in graphs. For both problems this represents the first improvement in asymptotic running time in 15 years.","lang":"eng"}],"date_created":"2018-12-11T11:53:19Z","publisher":"IEEE","language":[{"iso":"eng"}],"year":"2015","article_processing_charge":"No","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2015-07-01T00:00:00Z","article_number":"7174888","isi":1,"type":"conference","ec_funded":1,"oa":1,"publist_id":"5489","_id":"1661","main_file_link":[{"url":"https://eprints.cs.univie.ac.at/4368/","open_access":"1"}],"oa_version":"Submitted Version","quality_controlled":"1","scopus_import":"1","department":[{"_id":"KrCh"}],"volume":"2015-July","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"citation":{"chicago":"Chatterjee, Krishnendu, Monika Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for One-Pair and k-Pair Streett Objectives.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.34\">https://doi.org/10.1109/LICS.2015.34</a>.","short":"K. Chatterjee, M. Henzinger, V. Loitzenbauer, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","mla":"Chatterjee, Krishnendu, et al. “Improved Algorithms for One-Pair and k-Pair Streett Objectives.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174888, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.34\">10.1109/LICS.2015.34</a>.","ieee":"K. Chatterjee, M. Henzinger, and V. Loitzenbauer, “Improved algorithms for one-pair and k-pair Streett objectives,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","ista":"Chatterjee K, Henzinger M, Loitzenbauer V. 2015. Improved algorithms for one-pair and k-pair Streett objectives. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174888.","apa":"Chatterjee, K., Henzinger, M., &#38; Loitzenbauer, V. (2015). Improved algorithms for one-pair and k-pair Streett objectives. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.34\">https://doi.org/10.1109/LICS.2015.34</a>","ama":"Chatterjee K, Henzinger M, Loitzenbauer V. Improved algorithms for one-pair and k-pair Streett objectives. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.34\">10.1109/LICS.2015.34</a>"},"doi":"10.1109/LICS.2015.34","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H"},{"full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer","first_name":"Veronika"}],"date_updated":"2026-07-06T13:28:05Z","title":"Improved algorithms for one-pair and k-pair Streett objectives","related_material":{"record":[{"id":"464","relation":"later_version","status":"public"}]},"acknowledgement":"K. C. is supported by the Austrian Science Fund (FWF): P23499-N23 and S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games), and a Microsoft Faculty Fellows Award. M. H. is supported by the Austrian Science Fund (FWF): P23499-N23 and the Vienna Science and Technology Fund (WWTF) grant ICT10-002. V. L. is supported by the Vienna Science and Technology Fund (WWTF) grant ICT10-002. The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement no. 340506.","day":"01","conference":{"end_date":"2015-07-10","start_date":"2015-07-06","name":"LICS: Logic in Computer Science","location":"Kyoto, Japan"},"external_id":{"isi":["000380427100026"]}},{"type":"journal_article","ec_funded":1,"isi":1,"oa":1,"page":"52 - 59","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2015-01-01T00:00:00Z","publication_status":"published","article_processing_charge":"No","year":"2015","language":[{"iso":"eng"}],"intvolume":"       115","abstract":[{"text":"Opacity is a generic security property, that has been defined on (non-probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a subset of runs, and a function describing the view of an external observer, the value of interest for opacity is a measure of the set of runs disclosing the secret. We extend this definition to the richer framework of Markov decision processes, where non-deterministicchoice is combined with probabilistic transitions, and we study related decidability problems with partial or complete observation hypotheses for the schedulers. We prove that all questions are decidable with complete observation and ω-regular secrets. With partial observation, we prove that all quantitative questions are undecidable but the question whether a system is almost surely non-opaquebecomes decidable for a restricted class of ω-regular secrets, as well as for all ω-regular secrets under finite-memory schedulers.","lang":"eng"}],"date_created":"2018-12-11T11:55:20Z","publisher":"Elsevier","das_tickbox":"1","status":"public","publication":"Information Processing Letters","month":"01","issue":"1","external_id":{"arxiv":["1407.4225"],"isi":["000345478700010"]},"day":"01","arxiv":1,"title":"Probabilistic opacity for Markov decision processes","date_updated":"2026-07-07T13:10:27Z","author":[{"last_name":"Bérard","first_name":"Béatrice","full_name":"Bérard, Béatrice"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Nathalie","last_name":"Sznajder","full_name":"Sznajder, Nathalie"}],"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.1016/j.ipl.2014.09.001","citation":{"chicago":"Bérard, Béatrice, Krishnendu Chatterjee, and Nathalie Sznajder. “Probabilistic Opacity for Markov Decision Processes.” <i>Information Processing Letters</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">https://doi.org/10.1016/j.ipl.2014.09.001</a>.","short":"B. Bérard, K. Chatterjee, N. Sznajder, Information Processing Letters 115 (2015) 52–59.","mla":"Bérard, Béatrice, et al. “Probabilistic Opacity for Markov Decision Processes.” <i>Information Processing Letters</i>, vol. 115, no. 1, Elsevier, 2015, pp. 52–59, doi:<a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">10.1016/j.ipl.2014.09.001</a>.","ieee":"B. Bérard, K. Chatterjee, and N. Sznajder, “Probabilistic opacity for Markov decision processes,” <i>Information Processing Letters</i>, vol. 115, no. 1. Elsevier, pp. 52–59, 2015.","ista":"Bérard B, Chatterjee K, Sznajder N. 2015. Probabilistic opacity for Markov decision processes. Information Processing Letters. 115(1), 52–59.","apa":"Bérard, B., Chatterjee, K., &#38; Sznajder, N. (2015). Probabilistic opacity for Markov decision processes. <i>Information Processing Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">https://doi.org/10.1016/j.ipl.2014.09.001</a>","ama":"Bérard B, Chatterjee K, Sznajder N. Probabilistic opacity for Markov decision processes. <i>Information Processing Letters</i>. 2015;115(1):52-59. doi:<a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">10.1016/j.ipl.2014.09.001</a>"},"department":[{"_id":"KrCh"}],"scopus_import":"1","volume":115,"_id":"2034","publist_id":"5025","oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1407.4225"}]},{"isi":1,"type":"conference","ec_funded":1,"oa":1,"year":"2015","article_processing_charge":"No","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_number":"7174926","date_published":"2015-07-31T00:00:00Z","date_created":"2018-12-11T11:53:17Z","abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}],"publisher":"IEEE","OA_type":"green","language":[{"iso":"eng"}],"corr_author":"1","status":"public","publication":"Proceedings - Symposium on Logic in Computer Science","month":"07","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.\r\nA Technical Report of the paper is available at: \r\nhttps://repository.ist.ac.at/331/\r\n","related_material":{"record":[{"relation":"earlier_version","id":"5415","status":"public"},{"status":"public","relation":"earlier_version","id":"5436"},{"status":"public","id":"467","relation":"later_version"}]},"day":"31","arxiv":1,"OA_place":"repository","conference":{"end_date":"2015-07-10","name":"LICS: Logic in Computer Science","location":"Kyoto, Japan","start_date":"2015-07-06"},"external_id":{"isi":["000380427100064"],"arxiv":["1606.03598"]},"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2026-07-07T14:01:10Z","title":"Nested weighted automata","scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":"2015-July","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174926, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). Nested weighted automata. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174926.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>"},"doi":"10.1109/LICS.2015.72","publist_id":"5494","_id":"1656","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1606.03598"}],"oa_version":"Preprint","quality_controlled":"1"},{"pubrep_id":"331","_id":"5436","ddc":["000"],"oa_version":"Published Version","status":"public","month":"04","alternative_title":["IST Austria Technical Report"],"date_created":"2018-12-12T11:39:19Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"abstract":[{"text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time.\r\nIn nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.","lang":"eng"}],"has_accepted_license":"1","publisher":"IST Austria","language":[{"iso":"eng"}],"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria, 29p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2015."},"doi":"10.15479/AT:IST-2015-170-v2-2","year":"2015","publication_status":"published","file":[{"date_updated":"2020-07-14T12:46:54Z","file_id":"5541","access_level":"open_access","content_type":"application/pdf","file_size":569991,"creator":"system","file_name":"IST-2015-170-v2+2_report.pdf","checksum":"3c402f47d3669c28d04d1af405a08e3f","date_created":"2018-12-12T11:54:19Z","relation":"main_file"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2015-04-24T00:00:00Z","date_updated":"2026-07-07T14:01:10Z","title":"Nested weighted automata","publication_identifier":{"issn":["2664-1690"]},"file_date_updated":"2020-07-14T12:46:54Z","related_material":{"record":[{"status":"public","id":"5415","relation":"earlier_version"},{"status":"public","relation":"later_version","id":"1656"},{"relation":"later_version","id":"467","status":"public"}]},"day":"24","page":"29","type":"technical_report","oa":1},{"main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4528522/","open_access":"1"}],"quality_controlled":"1","oa_version":"Submitted Version","publist_id":"5425","_id":"1709","doi":"10.1098/rspb.2015.1041","citation":{"chicago":"Reiter, Johannes, Ayush Kanodia, Raghav Gupta, Martin Nowak, and Krishnendu Chatterjee. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society, 2015. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>.","short":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of the Royal Society of London Series B Biological Sciences 282 (2015).","mla":"Reiter, Johannes, et al. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812, Royal Society, 2015, doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>.","ieee":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, and K. Chatterjee, “Biological auctions with multiple rewards,” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812. Royal Society, 2015.","ista":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. 2015. Biological auctions with multiple rewards. Proceedings of the Royal Society of London Series B Biological Sciences. 282(1812).","apa":"Reiter, J., Kanodia, A., Gupta, R., Nowak, M., &#38; Chatterjee, K. (2015). Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>","ama":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. 2015;282(1812). doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>"},"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"volume":282,"department":[{"_id":"KrCh"}],"scopus_import":"1","date_updated":"2026-07-29T10:15:25Z","title":"Biological auctions with multiple rewards","author":[{"full_name":"Reiter, Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","orcid":"0000-0002-0170-7353","first_name":"Johannes"},{"full_name":"Kanodia, Ayush","last_name":"Kanodia","first_name":"Ayush"},{"last_name":"Gupta","first_name":"Raghav","full_name":"Gupta, Raghav"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"external_id":{"pmid":["26180069"],"isi":["000362305500021"]},"acknowledgement":"This work was supported by grants from the John Templeton Foundation, ERC Start Grant (279307: Graph Games), FWF NFN Grant (No S11407N23 RiSE/SHiNE), FWF Grant (No P23499N23) and a Microsoft faculty fellows award.","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1400"}]},"article_type":"original","day":"15","corr_author":"1","month":"07","status":"public","publication":"Proceedings of the Royal Society of London Series B Biological Sciences","issue":"1812","intvolume":"       282","language":[{"iso":"eng"}],"publisher":"Royal Society","pmid":1,"date_created":"2018-12-11T11:53:35Z","abstract":[{"lang":"eng","text":"The competition for resources among cells, individuals or species is a fundamental characteristic of evolution. Biological all-pay auctions have been used to model situations where multiple individuals compete for a single resource. However, in many situations multiple resources with various values exist and single reward auctions are not applicable. We generalize the model to multiple rewards and study the evolution of strategies. In biological all-pay auctions the bid of an individual corresponds to its strategy and is equivalent to its payment in the auction. The decreasingly ordered rewards are distributed according to the decreasingly ordered bids of the participating individuals. The reproductive success of an individual is proportional to its fitness given by the sum of the rewards won minus its payments. Hence, successful bidding strategies spread in the population. We find that the results for the multiple reward case are very different from the single reward case. While the mixed strategy equilibrium in the single reward case with more than two players consists of mostly low-bidding individuals, we show that the equilibrium can convert to many high-bidding individuals and a few low-bidding individuals in the multiple reward case. Some reward values lead to a specialization among the individuals where one subpopulation competes for the rewards and the other subpopulation largely avoids costly competitions. Whether the mixed strategy equilibrium is an evolutionarily stable strategy (ESS) depends on the specific values of the rewards."}],"date_published":"2015-07-15T00:00:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2015","article_processing_charge":"No","publication_status":"published","oa":1,"isi":1,"type":"journal_article"},{"month":"04","status":"public","corr_author":"1","oa_version":"None","doi_confirm":"1","publist_id":"5807","_id":"1400","degree_awarded":"PhD","citation":{"mla":"Reiter, Johannes. <i>The Subclonal Evolution of Cancer</i>. Institute of Science and Technology Austria, 2015.","ieee":"J. Reiter, “The subclonal evolution of cancer,” Institute of Science and Technology Austria, 2015.","apa":"Reiter, J. (2015). <i>The subclonal evolution of cancer</i>. Institute of Science and Technology Austria.","ama":"Reiter J. The subclonal evolution of cancer. 2015.","ista":"Reiter J. 2015. The subclonal evolution of cancer. Institute of Science and Technology Austria.","chicago":"Reiter, Johannes. “The Subclonal Evolution of Cancer.” Institute of Science and Technology Austria, 2015.","short":"J. Reiter, The Subclonal Evolution of Cancer, Institute of Science and Technology Austria, 2015."},"language":[{"iso":"eng"}],"supervisor":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"}],"publisher":"Institute of Science and Technology Austria","alternative_title":["ISTA Thesis"],"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"date_created":"2018-12-11T11:51:48Z","abstract":[{"text":"Cancer results from an uncontrolled growth of abnormal cells. Sequentially accumulated genetic and epigenetic alterations decrease cell death and increase cell replication. We used mathematical models to quantify the effect of driver gene mutations. The recently developed targeted therapies can lead to dramatic regressions. However, in solid cancers, clinical responses are often short-lived because resistant cancer cells evolve. We estimated that approximately 50 different mutations can confer resistance to a typical targeted therapeutic agent. We find that resistant cells are likely to be present in expanded subclones before the start of the treatment. The dominant strategy to prevent the evolution of resistance is combination therapy. Our analytical results suggest that in most patients, dual therapy, but not monotherapy, can result in long-term disease control. However, long-term control can only occur if there are no possible mutations in the genome that can cause cross-resistance to both drugs. Furthermore, we showed that simultaneous therapy with two drugs is much more likely to result in long-term disease control than sequential therapy with the same drugs. To improve our understanding of the underlying subclonal evolution we reconstruct the evolutionary history of a patient's cancer from next-generation sequencing data of spatially-distinct DNA samples. Using a quantitative measure of genetic relatedness, we found that pancreatic cancers and their metastases demonstrated a higher level of relatedness than that expected for any two cells randomly taken from a normal tissue. This minimal amount of genetic divergence among advanced lesions indicates that genetic heterogeneity, when quantitatively defined, is not a fundamental feature of the natural history of untreated pancreatic cancers. Our newly developed, phylogenomic tool Treeomics finds evidence for seeding patterns of metastases and can directly be used to discover rules governing the evolution of solid malignancies to transform cancer into a more predictable disease.","lang":"eng"}],"date_updated":"2026-07-29T10:15:25Z","date_published":"2015-04-01T00:00:00Z","title":"The subclonal evolution of cancer","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"full_name":"Reiter, Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","first_name":"Johannes","last_name":"Reiter","orcid":"0000-0002-0170-7353"}],"year":"2015","article_processing_charge":"No","publication_status":"published","type":"dissertation","OA_place":"publisher","page":"183","publication_identifier":{"issn":["2663-337X"]},"related_material":{"record":[{"id":"2000","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"1709"},{"status":"public","id":"2858","relation":"part_of_dissertation"},{"status":"public","id":"2816","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"2247"},{"id":"3260","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"3157","relation":"part_of_dissertation"}]},"day":"01"},{"_id":"1820","publist_id":"5286","quality_controlled":"1","oa_version":"Preprint","main_file_link":[{"url":"http://arxiv.org/abs/1411.3880","open_access":"1"}],"department":[{"_id":"KrCh"}],"scopus_import":"1","volume":5,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"citation":{"ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure reachability in POMDPs,” in <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>, Austin, TX, USA, 2015, vol. 5, pp. 3496–3502.","mla":"Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.” <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>, vol. 5, AAAI Press, 2015, pp. 3496–502, doi:<a href=\"https://doi.org/10.1609/aaai.v29i1.9683\">10.1609/aaai.v29i1.9683</a>.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability in POMDPs. In: <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>. Vol 5. AAAI Press; 2015:3496-3502. doi:<a href=\"https://doi.org/10.1609/aaai.v29i1.9683\">10.1609/aaai.v29i1.9683</a>","apa":"Chatterjee, K., Chmelik, M., Gupta, R., &#38; Kanodia, A. (2015). Optimal cost almost-sure reachability in POMDPs. In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i> (Vol. 5, pp. 3496–3502). Austin, TX, USA: AAAI Press. <a href=\"https://doi.org/10.1609/aaai.v29i1.9683\">https://doi.org/10.1609/aaai.v29i1.9683</a>","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Optimal cost almost-sure reachability in POMDPs. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence . IAAI: Innovative Applications of Artificial Intelligence, Artifical Intelligence, vol. 5, 3496–3502.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Optimal Cost Almost-Sure Reachability in POMDPs.” In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>, 5:3496–3502. AAAI Press, 2015. <a href=\"https://doi.org/10.1609/aaai.v29i1.9683\">https://doi.org/10.1609/aaai.v29i1.9683</a>.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , AAAI Press, 2015, pp. 3496–3502."},"doi":"10.1609/aaai.v29i1.9683","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"last_name":"Gupta","first_name":"Raghav","full_name":"Gupta, Raghav"},{"full_name":"Kanodia, Ayush","last_name":"Kanodia","first_name":"Ayush"}],"title":"Optimal cost almost-sure reachability in POMDPs","date_updated":"2026-08-19T09:31:47Z","day":"01","related_material":{"record":[{"status":"public","id":"1529","relation":"later_version"}]},"acknowledgement":" The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","arxiv":1,"conference":{"location":"Austin, TX, USA","name":"IAAI: Innovative Applications of Artificial Intelligence","start_date":"2015-01-25","end_date":"2015-01-30"},"external_id":{"isi":["000372683700002"],"arxiv":["1411.3880"]},"publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence ","corr_author":"1","status":"public","month":"06","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with a set of target states and every transition is associated with an integer cost. The optimization objec- tive we study asks to minimize the expected total cost till the target set is reached, while ensuring that the target set is reached almost-surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost and the bound is double exponential; (ii) we show that the problem of approximating the optimal cost is decidable and present ap- proximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst- case running time of our algorithm is double exponential, we present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples.","lang":"eng"}],"date_created":"2018-12-11T11:54:11Z","alternative_title":["Artifical Intelligence"],"publisher":"AAAI Press","language":[{"iso":"eng"}],"intvolume":"         5","publication_status":"published","year":"2015","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2015-06-01T00:00:00Z","page":"3496-3502","ec_funded":1,"isi":1,"type":"conference","oa":1},{"publication_status":"published","article_processing_charge":"No","year":"2014","date_published":"2014-01-30T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"262-281","oa":1,"type":"conference","ec_funded":1,"month":"01","status":"public","publication":"Verification, Model Checking, and Abstract Interpretation","publisher":"Springer Nature","date_created":"2022-03-18T13:01:22Z","abstract":[{"lang":"eng","text":"We revisit the parameterized model checking problem for token-passing systems and specifications in indexed CTL  ∗ \\X. Emerson and Namjoshi (1995, 2003) have shown that parameterized model checking of indexed CTL  ∗ \\X in uni-directional token rings can be reduced to checking rings up to some cutoff size. Clarke et al. (2004) have shown a similar result for general topologies and indexed LTL \\X, provided processes cannot choose the directions for sending or receiving the token.\r\nWe unify and substantially extend these results by systematically exploring fragments of indexed CTL  ∗ \\X with respect to general topologies. For each fragment we establish whether a cutoff exists, and for some concrete topologies, such as rings, cliques and stars, we infer small cutoffs. Finally, we show that the problem becomes undecidable, and thus no cutoffs exist, if processes are allowed to choose the directions in which they send or from which they receive the token."}],"alternative_title":["LNCS"],"intvolume":"      8318","language":[{"iso":"eng"}],"author":[{"last_name":"Aminof","first_name":"Benjamin","full_name":"Aminof, Benjamin","id":"4A55BD00-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jacobs, Swen","first_name":"Swen","last_name":"Jacobs"},{"full_name":"Khalimov, Ayrat","last_name":"Khalimov","first_name":"Ayrat"},{"id":"2EC51194-F248-11E8-B48F-1D18A9856A87","full_name":"Rubin, Sasha","last_name":"Rubin","first_name":"Sasha"}],"title":"Parameterized model checking of token-passing systems","date_updated":"2025-04-15T06:29:59Z","arxiv":1,"day":"30","acknowledgement":"This work was supported by the Austrian Science Fund through grant P23499-N23\r\nand through the RiSE network (S11403, S11405, S11406, S11407-N23); ERC Starting Grant (279307: Graph Games); Vienna Science and Technology Fund (WWTF)\r\ngrants PROSEED, ICT12-059, and VRG11-005.","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642540127"],"eisbn":["9783642540134"],"eissn":["1611-3349"]},"external_id":{"arxiv":["1311.4425"]},"conference":{"end_date":"2014-01-21","start_date":"2014-01-19","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","location":"San Diego, CA, United States"},"quality_controlled":"1","oa_version":"Preprint","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.1311.4425","open_access":"1"}],"_id":"10884","volume":8318,"scopus_import":"1","department":[{"_id":"KrCh"}],"doi":"10.1007/978-3-642-54013-4_15","citation":{"apa":"Aminof, B., Jacobs, S., Khalimov, A., &#38; Rubin, S. (2014). Parameterized model checking of token-passing systems. In <i>Verification, Model Checking, and Abstract Interpretation</i> (Vol. 8318, pp. 262–281). San Diego, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">https://doi.org/10.1007/978-3-642-54013-4_15</a>","ama":"Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized model checking of token-passing systems. In: <i>Verification, Model Checking, and Abstract Interpretation</i>. Vol 8318. Springer Nature; 2014:262-281. doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">10.1007/978-3-642-54013-4_15</a>","ista":"Aminof B, Jacobs S, Khalimov A, Rubin S. 2014. Parameterized model checking of token-passing systems. Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 262–281.","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Token-Passing Systems.” <i>Verification, Model Checking, and Abstract Interpretation</i>, vol. 8318, Springer Nature, 2014, pp. 262–81, doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">10.1007/978-3-642-54013-4_15</a>.","ieee":"B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, “Parameterized model checking of token-passing systems,” in <i>Verification, Model Checking, and Abstract Interpretation</i>, San Diego, CA, United States, 2014, vol. 8318, pp. 262–281.","short":"B. Aminof, S. Jacobs, A. Khalimov, S. Rubin, in:, Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 262–281.","chicago":"Aminof, Benjamin, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. “Parameterized Model Checking of Token-Passing Systems.” In <i>Verification, Model Checking, and Abstract Interpretation</i>, 8318:262–81. Springer Nature, 2014. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">https://doi.org/10.1007/978-3-642-54013-4_15</a>."},"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}]},{"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"full_name":"Filiot, Emmanuel","last_name":"Filiot","first_name":"Emmanuel"},{"first_name":"Jean-François","last_name":"Raskin","full_name":"Raskin, Jean-François"}],"title":"Doomsday equilibria for omega-regular games","date_updated":"2026-04-16T10:00:03Z","arxiv":1,"day":"30","acknowledgement":" Supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No\r\nS11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","related_material":{"record":[{"status":"public","relation":"later_version","id":"681"}]},"publication_identifier":{"eisbn":["9783642540134"],"isbn":["9783642540127"],"issn":["0302-9743"],"eissn":["1611-3349"]},"external_id":{"arxiv":["1311.3238"]},"OA_place":"repository","conference":{"end_date":"2014-01-21","start_date":"2014-01-19","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","location":"San Diego, CA, United States"},"oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1311.3238","open_access":"1"}],"_id":"10885","volume":8318,"scopus_import":"1","department":[{"_id":"KrCh"}],"doi":"10.1007/978-3-642-54013-4_5","citation":{"ista":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. 2014. Doomsday equilibria for omega-regular games. VMCAI 2014: Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 78–97.","apa":"Chatterjee, K., Doyen, L., Filiot, E., &#38; Raskin, J.-F. (2014). Doomsday equilibria for omega-regular games. In <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i> (Vol. 8318, pp. 78–97). San Diego, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">https://doi.org/10.1007/978-3-642-54013-4_5</a>","ama":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. Doomsday equilibria for omega-regular games. In: <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>. Vol 8318. Springer Nature; 2014:78-97. doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">10.1007/978-3-642-54013-4_5</a>","ieee":"K. Chatterjee, L. Doyen, E. Filiot, and J.-F. Raskin, “Doomsday equilibria for omega-regular games,” in <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>, San Diego, CA, United States, 2014, vol. 8318, pp. 78–97.","mla":"Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.” <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>, vol. 8318, Springer Nature, 2014, pp. 78–97, doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">10.1007/978-3-642-54013-4_5</a>.","short":"K. Chatterjee, L. Doyen, E. Filiot, J.-F. Raskin, in:, VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 78–97.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean-François Raskin. “Doomsday Equilibria for Omega-Regular Games.” In <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>, 8318:78–97. Springer Nature, 2014. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">https://doi.org/10.1007/978-3-642-54013-4_5</a>."},"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publication_status":"published","year":"2014","article_processing_charge":"No","date_published":"2014-01-30T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"78-97","oa":1,"ec_funded":1,"type":"conference","publication":"VMCAI 2014: Verification, Model Checking, and Abstract Interpretation","month":"01","status":"public","publisher":"Springer Nature","abstract":[{"lang":"eng","text":"Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\r\nIn this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\r\nWe present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games."}],"date_created":"2022-03-18T13:03:15Z","alternative_title":["LNCS"],"intvolume":"      8318","language":[{"iso":"eng"}],"OA_type":"green"}]