[{"oa":1,"isi":1,"ec_funded":1,"type":"journal_article","date_published":"2017-09-13T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_size":279071,"access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:14:37Z","relation":"main_file","creator":"system","file_name":"IST-2015-321-v1+1_main.pdf","checksum":"08041379ba408d40664f449eb5907a8f","date_updated":"2020-07-14T12:46:33Z","file_id":"5090"},{"date_updated":"2020-07-14T12:46:33Z","file_id":"5091","access_level":"open_access","content_type":"application/pdf","file_size":279071,"creator":"system","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","checksum":"08041379ba408d40664f449eb5907a8f","date_created":"2018-12-12T10:14:38Z","relation":"main_file"}],"publication_status":"published","year":"2017","article_processing_charge":"No","intvolume":"        13","language":[{"iso":"eng"}],"publisher":"International Federation for Computational Logic","has_accepted_license":"1","date_created":"2018-12-11T11:46:37Z","abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 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 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 the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"publication":"Logical Methods in Computer Science","corr_author":"1","status":"public","ddc":["004"],"month":"09","das_tickbox":"1","issue":"3","external_id":{"isi":["000419163000005"]},"license":"https://creativecommons.org/licenses/by-nd/4.0/","day":"13","file_date_updated":"2020-07-14T12:46:33Z","related_material":{"record":[{"status":"public","id":"5438","relation":"earlier_version"},{"status":"public","id":"1610","relation":"earlier_version"}]},"publication_identifier":{"issn":["1860-5974"]},"title":"Edit distance for pushdown automata","date_updated":"2026-07-06T13:27:53Z","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"},{"first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan"}],"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation for Computational Logic, 2017.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation for Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017)."},"tmp":{"image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"doi":"10.23638/LMCS-13(3:23)2017","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"volume":13,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","oa_version":"Published Version","quality_controlled":"1","_id":"465","publist_id":"7356","pubrep_id":"955"},{"external_id":{"arxiv":["1410.0833"],"isi":["000419163000001"]},"file_date_updated":"2020-07-14T12:46:32Z","publication_identifier":{"issn":["1860-5974"]},"related_material":{"record":[{"relation":"earlier_version","id":"1661","status":"public"}]},"day":"26","arxiv":1,"date_updated":"2026-07-06T13:28:05Z","title":"Improved algorithms for parity and Streett objectives","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","orcid":"0000-0002-5008-6530","first_name":"Monika H","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"first_name":"Veronika","last_name":"Loitzenbauer","full_name":"Loitzenbauer, Veronika"}],"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"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"tmp":{"image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"citation":{"short":"K. Chatterjee, M. Henzinger, V. Loitzenbauer, Logical Methods in Computer Science 13 (2017).","chicago":"Chatterjee, Krishnendu, Monika Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for Parity and Streett Objectives.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">https://doi.org/10.23638/LMCS-13(3:26)2017</a>.","ama":"Chatterjee K, Henzinger M, Loitzenbauer V. Improved algorithms for parity and Streett objectives. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">10.23638/LMCS-13(3:26)2017</a>","ista":"Chatterjee K, Henzinger M, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.","apa":"Chatterjee, K., Henzinger, M., &#38; Loitzenbauer, V. (2017). Improved algorithms for parity and Streett objectives. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">https://doi.org/10.23638/LMCS-13(3:26)2017</a>","ieee":"K. Chatterjee, M. Henzinger, and V. Loitzenbauer, “Improved algorithms for parity and Streett objectives,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation for Computational Logic, 2017.","mla":"Chatterjee, Krishnendu, et al. “Improved Algorithms for Parity and Streett Objectives.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, 26, International Federation for Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">10.23638/LMCS-13(3:26)2017</a>."},"doi":"10.23638/LMCS-13(3:26)2017","department":[{"_id":"KrCh"}],"scopus_import":"1","volume":13,"publist_id":"7357","_id":"464","oa_version":"Published Version","quality_controlled":"1","pubrep_id":"956","isi":1,"type":"journal_article","ec_funded":1,"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_number":"26","date_published":"2017-09-26T00:00:00Z","article_processing_charge":"No","year":"2017","publication_status":"published","file":[{"content_type":"application/pdf","access_level":"open_access","file_size":582940,"checksum":"12d469ae69b80361333d7dead965cf5d","creator":"system","file_name":"IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf","relation":"main_file","date_created":"2018-12-12T10:13:27Z","date_updated":"2020-07-14T12:46:32Z","file_id":"5010"}],"language":[{"iso":"eng"}],"intvolume":"        13","date_created":"2018-12-11T11:46:37Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"The computation of the winning set for parity objectives and for Streett objectives in 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-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs in time O(n2+nklogn). For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years."}],"publisher":"International Federation for Computational Logic","das_tickbox":"1","ddc":["004"],"corr_author":"1","month":"09","status":"public","publication":"Logical Methods in Computer Science","issue":"3"},{"author":[{"first_name":"Tadeas","last_name":"Priklopil","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","full_name":"Priklopil, Tadeas"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"date_updated":"2026-07-07T13:11:54Z","title":"Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma","file_date_updated":"2020-07-14T12:47:58Z","article_type":"original","publication_identifier":{"issn":["0022-5193"]},"day":"21","external_id":{"pmid":["28867224"],"isi":["000412039800007"]},"oa_version":"Submitted Version","quality_controlled":"1","publist_id":"6923","_id":"744","volume":433,"department":[{"_id":"KrCh"}],"scopus_import":"1","citation":{"chicago":"Priklopil, Tadeas, Krishnendu Chatterjee, and Martin Nowak. “Optional Interactions and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.” <i>Journal of Theoretical Biology</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">https://doi.org/10.1016/j.jtbi.2017.08.025</a>.","short":"T. Priklopil, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 433 (2017) 64–72.","mla":"Priklopil, Tadeas, et al. “Optional Interactions and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.” <i>Journal of Theoretical Biology</i>, vol. 433, Elsevier, 2017, pp. 64–72, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">10.1016/j.jtbi.2017.08.025</a>.","ieee":"T. Priklopil, K. Chatterjee, and M. Nowak, “Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma,” <i>Journal of Theoretical Biology</i>, vol. 433. Elsevier, pp. 64–72, 2017.","ama":"Priklopil T, Chatterjee K, Nowak M. Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma. <i>Journal of Theoretical Biology</i>. 2017;433:64-72. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">10.1016/j.jtbi.2017.08.025</a>","apa":"Priklopil, T., Chatterjee, K., &#38; Nowak, M. (2017). Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma. <i>Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">https://doi.org/10.1016/j.jtbi.2017.08.025</a>","ista":"Priklopil T, Chatterjee K, Nowak M. 2017. Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma. Journal of Theoretical Biology. 433, 64–72."},"tmp":{"image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)"},"doi":"10.1016/j.jtbi.2017.08.025","project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"file":[{"file_id":"7047","date_updated":"2020-07-14T12:47:58Z","date_created":"2019-11-19T07:57:39Z","relation":"main_file","creator":"dernst","checksum":"4b43af1615ebf1a861840cb03d8a320c","file_name":"2017_JournTheoretBio_Priklopil.pdf","file_size":537323,"access_level":"open_access","content_type":"application/pdf"}],"article_processing_charge":"No","year":"2017","publication_status":"published","date_published":"2017-11-21T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"64 - 72","oa":1,"ec_funded":1,"isi":1,"type":"journal_article","ddc":["000","570"],"corr_author":"1","month":"11","publication":"Journal of Theoretical Biology","status":"public","das_tickbox":"1","publisher":"Elsevier","has_accepted_license":"1","abstract":[{"text":"In evolutionary game theory interactions between individuals are often assumed obligatory. However, in many real-life situations, individuals can decide to opt out of an interaction depending on the information they have about the opponent. We consider a simple evolutionary game theoretic model to study such a scenario, where at each encounter between two individuals the type of the opponent (cooperator/defector) is known with some probability, and where each individual either accepts or opts out of the interaction. If the type of the opponent is unknown, a trustful individual accepts the interaction, whereas a suspicious individual opts out of the interaction. If either of the two individuals opt out both individuals remain without an interaction. We show that in the prisoners dilemma optional interactions along with suspicious behaviour facilitates the emergence of trustful cooperation.","lang":"eng"}],"date_created":"2018-12-11T11:48:16Z","pmid":1,"intvolume":"       433","language":[{"iso":"eng"}]},{"title":"Nested weighted automata","date_updated":"2026-07-07T14:01:10Z","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"external_id":{"arxiv":["1606.03598"],"isi":["000419237100006"]},"day":"01","related_material":{"record":[{"id":"5415","relation":"earlier_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5436"},{"id":"1656","relation":"earlier_version","status":"public"}]},"publication_identifier":{"issn":["1529-3785"]},"arxiv":1,"_id":"467","publist_id":"7354","oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-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"}],"doi":"10.1145/3152769","citation":{"mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 4. ACM, 2017.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic. 18(4), 31.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic</i>. 2017;18(4). doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic 18 (2017)."},"scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":18,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2017-12-01T00:00:00Z","article_number":"31","publication_status":"published","year":"2017","article_processing_charge":"No","ec_funded":1,"isi":1,"type":"journal_article","oa":1,"das_tickbox":"1","publication":"ACM Transactions on Computational Logic","month":"12","status":"public","corr_author":"1","issue":"4","language":[{"iso":"eng"}],"intvolume":"        18","date_created":"2018-12-11T11:46:38Z","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 or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.","lang":"eng"}],"publisher":"ACM"},{"_id":"949","publist_id":"6468","oa_version":"Submitted Version","quality_controlled":"1","pubrep_id":"845","project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"doi":"10.1007/978-3-319-68167-2_4","citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “JTDec: A Tool for Tree Decompositions in Soot.” edited by Deepak D’Souza, 10482:59–66. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">https://doi.org/10.1007/978-3-319-68167-2_4</a>.","short":"K. Chatterjee, A.K. Goharshady, A. Pavlogiannis, in:, D. D’Souza (Ed.), Springer, 2017, pp. 59–66.","mla":"Chatterjee, Krishnendu, et al. <i>JTDec: A Tool for Tree Decompositions in Soot</i>. Edited by Deepak D’Souza, vol. 10482, Springer, 2017, pp. 59–66, doi:<a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">10.1007/978-3-319-68167-2_4</a>.","ieee":"K. Chatterjee, A. K. Goharshady, and A. Pavlogiannis, “JTDec: A tool for tree decompositions in soot,” presented at the ATVA: Automated Technology for Verification and Analysis, Pune, India, 2017, vol. 10482, pp. 59–66.","apa":"Chatterjee, K., Goharshady, A. K., &#38; Pavlogiannis, A. (2017). JTDec: A tool for tree decompositions in soot. In D. D’Souza (Ed.) (Vol. 10482, pp. 59–66). Presented at the ATVA: Automated Technology for Verification and Analysis, Pune, India: Springer. <a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">https://doi.org/10.1007/978-3-319-68167-2_4</a>","ama":"Chatterjee K, Goharshady AK, Pavlogiannis A. JTDec: A tool for tree decompositions in soot. In: D’Souza D, ed. Vol 10482. Springer; 2017:59-66. doi:<a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">10.1007/978-3-319-68167-2_4</a>","ista":"Chatterjee K, Goharshady AK, Pavlogiannis A. 2017. JTDec: A tool for tree decompositions in soot. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 10482, 59–66."},"scopus_import":"1","department":[{"_id":"KrCh"}],"volume":10482,"title":"JTDec: A tool for tree decompositions in soot","date_updated":"2026-09-02T22:30:59Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas"}],"conference":{"name":"ATVA: Automated Technology for Verification and Analysis","location":"Pune, India","start_date":"2017-10-03","end_date":"2017-10-06"},"external_id":{"isi":["000723567800004"]},"day":"01","publication_identifier":{"issn":["0302-9743"]},"file_date_updated":"2020-07-14T12:48:16Z","related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"month":"01","status":"public","corr_author":"1","ddc":["005"],"language":[{"iso":"eng"}],"intvolume":"     10482","abstract":[{"text":"The notion of treewidth of graphs has been exploited for faster algorithms for several problems arising in verification and program analysis. Moreover, various notions of balanced tree decompositions have been used for improved algorithms supporting dynamic updates and analysis of concurrent programs. In this work, we present a tool for constructing tree-decompositions of CFGs obtained from Java methods, which is implemented as an extension to the widely used Soot framework. The experimental results show that our implementation on real-world Java benchmarks is very efficient. Our tool also provides the first implementation for balancing tree-decompositions. In summary, we present the first tool support for exploiting treewidth in the static analysis problems on Java programs.","lang":"eng"}],"date_created":"2018-12-11T11:49:22Z","has_accepted_license":"1","alternative_title":["LNCS"],"publisher":"Springer","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","date_published":"2017-01-01T00:00:00Z","publication_status":"published","article_processing_charge":"No","year":"2017","file":[{"content_type":"application/pdf","access_level":"open_access","file_size":948514,"file_name":"IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf","creator":"system","checksum":"a0d9f5f94dc594c4e71e78525c9942f1","relation":"main_file","date_created":"2018-12-12T10:10:45Z","date_updated":"2020-07-14T12:48:16Z","file_id":"4835"}],"isi":1,"type":"conference","ec_funded":1,"oa":1,"editor":[{"full_name":"D'Souza, Deepak","last_name":"D'Souza","first_name":"Deepak"}],"page":"59 - 66"},{"publication_identifier":{"isbn":["978-331963389-3"]},"related_material":{"record":[{"status":"public","id":"7014","relation":"later_version"},{"relation":"dissertation_contains","id":"8934","status":"public"}]},"day":"01","arxiv":1,"conference":{"end_date":"2017-07-28","start_date":"2017-07-24","name":"CAV: Computer Aided Verification","location":"Heidelberg, Germany"},"external_id":{"arxiv":["1705.00317"],"isi":["000431900900003"]},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir","first_name":"Amir","orcid":"0000-0003-1702-6584","last_name":"Goharshady"}],"date_updated":"2026-09-02T22:30:58Z","title":"Non-polynomial worst case analysis of recursive programs","department":[{"_id":"KrCh"}],"scopus_import":"1","volume":10427,"project":[{"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.1007/978-3-319-63390-9_3","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Non-Polynomial Worst Case Analysis of Recursive Programs</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 41–63, doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">10.1007/978-3-319-63390-9_3</a>.","ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst case analysis of recursive programs,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 41–63.","ama":"Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst case analysis of recursive programs. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:41-63. doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">10.1007/978-3-319-63390-9_3</a>","apa":"Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2017). Non-polynomial worst case analysis of recursive programs. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10427, pp. 41–63). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">https://doi.org/10.1007/978-3-319-63390-9_3</a>","ista":"Chatterjee K, Fu H, Goharshady AK. 2017. Non-polynomial worst case analysis of recursive programs. CAV: Computer Aided Verification, LNCS, vol. 10427, 41–63.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst Case Analysis of Recursive Programs.” edited by Rupak Majumdar and Viktor Kunčak, 10427:41–63. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">https://doi.org/10.1007/978-3-319-63390-9_3</a>.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 41–63."},"publist_id":"7149","_id":"639","main_file_link":[{"url":"https://arxiv.org/abs/1705.00317","open_access":"1"}],"quality_controlled":"1","oa_version":"Submitted Version","page":"41 - 63","editor":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"full_name":"Kunčak, Viktor","last_name":"Kunčak","first_name":"Viktor"}],"isi":1,"type":"conference","ec_funded":1,"oa":1,"year":"2017","article_processing_charge":"No","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2017-01-01T00:00:00Z","alternative_title":["LNCS"],"abstract":[{"text":"We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to recursion, resulting in measure functions, and show that they provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in non-polynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas’ Lemma, and Handelman’s Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form O(n log n) as well as O(nr) where r is not an integer. We present experimental results to demonstrate that our approach can efficiently obtain worst-case bounds of classical recursive algorithms such as Merge-Sort, Closest-Pair, Karatsuba’s algorithm and Strassen’s algorithm.","lang":"eng"}],"date_created":"2018-12-11T11:47:39Z","publisher":"Springer","language":[{"iso":"eng"}],"intvolume":"     10427","month":"01","status":"public"},{"doi":"10.4230/LIPIcs.MFCS.2016.24","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 58, 24.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science, Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Limit-Average Automata of Bounded Width</i>. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average automata of bounded width,” presented at the MFCS: Mathematical Foundations of Computer Science, Krakow; Poland, 2016, vol. 58.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>."},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"volume":58,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","quality_controlled":"1","oa_version":"Published Version","_id":"1090","publist_id":"6286","pubrep_id":"795","conference":{"location":"Krakow; Poland","name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2016-08-22","end_date":"2016-08-26"},"day":"01","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under grant 2014/15/D/ST6/04543.","file_date_updated":"2018-12-12T10:17:31Z","title":"Nested weighted limit-average automata of bounded width","date_updated":"2025-07-10T11:50:02Z","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","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"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"intvolume":"        58","language":[{"iso":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2018-12-11T11:50:05Z","abstract":[{"lang":"eng","text":" While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness."}],"has_accepted_license":"1","alternative_title":["LIPIcs"],"month":"08","ddc":["004"],"status":"public","oa":1,"type":"conference","ec_funded":1,"article_number":"24","date_published":"2016-08-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_updated":"2018-12-12T10:17:31Z","file_id":"5286","file_size":564560,"access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:17:31Z","relation":"main_file","creator":"system","file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf"}],"publication_status":"published","article_processing_charge":"No","year":"2016"},{"volume":59,"scopus_import":1,"department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"citation":{"mla":"Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016."},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.4230/LIPIcs.CONCUR.2016.20","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"pubrep_id":"794","oa_version":"Published Version","quality_controlled":"1","_id":"1093","publist_id":"6283","day":"01","file_date_updated":"2018-12-12T10:11:39Z","related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","conference":{"end_date":"2016-08-26","start_date":"2016-08-23","name":"CONCUR: Concurrency Theory","location":"Quebec City; Canada"},"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"},{"full_name":"Petrov, Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana","last_name":"Petrov","orcid":"0000-0002-9041-0905"}],"title":"Linear distances between Markov chains","date_updated":"2026-04-15T10:02:12Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2018-12-11T11:50:06Z","has_accepted_license":"1","abstract":[{"text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. ","lang":"eng"}],"alternative_title":["LIPIcs"],"intvolume":"        59","language":[{"iso":"eng"}],"ddc":["004"],"month":"08","status":"public","oa":1,"type":"conference","ec_funded":1,"file":[{"date_created":"2018-12-12T10:11:39Z","relation":"main_file","creator":"system","file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","file_size":501827,"access_level":"open_access","content_type":"application/pdf","file_id":"4895","date_updated":"2018-12-12T10:11:39Z"}],"publication_status":"published","year":"2016","date_published":"2016-08-01T00:00:00Z","article_number":"20","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"article_processing_charge":"No","year":"2016","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2016-07-05T00:00:00Z","page":"197 - 206","isi":1,"type":"conference","oa":1,"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science","month":"07","status":"public","alternative_title":["Proceedings Symposium on Logic in Computer Science"],"date_created":"2018-12-11T11:50:22Z","abstract":[{"text":"Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental -regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical -regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. © 2016 ACM.","lang":"eng"}],"publisher":"IEEE","language":[{"iso":"eng"}],"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Wolfgang","last_name":"Dvoák","full_name":"Dvoák, Wolfgang"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"}],"date_updated":"2025-09-22T14:12:05Z","title":"Model and objective separation with conditional lower bounds: disjunction is harder than conjunction","acknowledgement":"K.  C.,  M.  H.,  and  W.  D.  are  partially  supported  by  the  Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003.\r\nK. C. is partially supported by the Austrian Science Fund (FWF)\r\nNFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Start grant\r\n(279307: Graph Games). For W. D., M. H., and V. L. the research\r\nleading to these results has received funding from the European\r\nResearch Council under the European Union’s Seventh Framework\r\nProgramme (FP/2007-2013) / ERC Grant Agreement no. 340506.","day":"05","arxiv":1,"conference":{"end_date":"2016-07-08","location":"New York, NY, USA","name":"LICS: Logic in Computer Science","start_date":"2016-07-05"},"external_id":{"arxiv":["1602.02670"],"isi":["000387609200020"]},"publist_id":"6219","_id":"1140","main_file_link":[{"url":"https://arxiv.org/abs/1602.02670","open_access":"1"}],"oa_version":"Preprint","quality_controlled":"1","department":[{"_id":"KrCh"}],"scopus_import":"1","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"citation":{"chicago":"Chatterjee, Krishnendu, Wolfgang Dvoák, Monika Henzinger, and Veronika Loitzenbauer. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 197–206. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2935304\">https://doi.org/10.1145/2933575.2935304</a>.","short":"K. Chatterjee, W. Dvoák, M. Henzinger, V. Loitzenbauer, in:, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016, pp. 197–206.","mla":"Chatterjee, Krishnendu, et al. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2016, pp. 197–206, doi:<a href=\"https://doi.org/10.1145/2933575.2935304\">10.1145/2933575.2935304</a>.","ieee":"K. Chatterjee, W. Dvoák, M. Henzinger, and V. Loitzenbauer, “Model and objective separation with conditional lower bounds: disjunction is harder than conjunction,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, New York, NY, USA, 2016, pp. 197–206.","apa":"Chatterjee, K., Dvoák, W., Henzinger, M., &#38; Loitzenbauer, V. (2016). Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 197–206). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2935304\">https://doi.org/10.1145/2933575.2935304</a>","ista":"Chatterjee K, Dvoák W, Henzinger M, Loitzenbauer V. 2016. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science, , 197–206.","ama":"Chatterjee K, Dvoák W, Henzinger M, Loitzenbauer V. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2016:197-206. doi:<a href=\"https://doi.org/10.1145/2933575.2935304\">10.1145/2933575.2935304</a>"},"doi":"10.1145/2933575.2935304"},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":2016,"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":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-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"}],"doi":"10.1609/aaai.v30i1.10422","citation":{"short":"K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in POMDPs.” In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, 2016:3225–32. AAAI Press, 2016. <a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">https://doi.org/10.1609/aaai.v30i1.10422</a>.","ista":"Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232.","apa":"Chatterjee, K., Chmelik, M., &#38; Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i> (Vol. 2016, pp. 3225–3232). Phoenix, AZ, United States: AAAI Press. <a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">https://doi.org/10.1609/aaai.v30i1.10422</a>","ama":"Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. In: <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>. Vol 2016. AAAI Press; 2016:3225-3232. doi:<a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">10.1609/aaai.v30i1.10422</a>","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs,” in <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, Phoenix, AZ, United States, 2016, vol. 2016, pp. 3225–3232.","mla":"Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in POMDPs.” <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, vol. 2016, AAAI Press, 2016, pp. 3225–32, doi:<a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">10.1609/aaai.v30i1.10422</a>."},"publist_id":"6191","_id":"1166","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1511.08456","open_access":"1"}],"oa_version":"Preprint","quality_controlled":"1","related_material":{"link":[{"relation":"table_of_contents","url":"https://dl.acm.org/citation.cfm?id=3016355"}],"record":[{"status":"public","relation":"earlier_version","id":"5443"}]},"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.","day":"02","arxiv":1,"OA_place":"repository","conference":{"location":"Phoenix, AZ, United States","name":"AAAI: Conference on Artificial Intelligence","start_date":"2016-02-12","end_date":"2016-02-17"},"external_id":{"arxiv":["1511.08456"]},"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin"},{"first_name":"Jessica","last_name":"Davies","full_name":"Davies, Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2025-06-25T11:52:14Z","title":"A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs","date_created":"2018-12-11T11:50:30Z","abstract":[{"text":"POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.","lang":"eng"}],"publisher":"AAAI Press","OA_type":"green","language":[{"iso":"eng"}],"intvolume":"      2016","publication":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence","month":"12","corr_author":"1","status":"public","page":"3225 - 3232","ec_funded":1,"type":"conference","oa":1,"year":"2016","article_processing_charge":"No","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2016-12-02T00:00:00Z"},{"ec_funded":1,"type":"conference","oa":1,"page":"172 - 179","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2016-01-01T00:00:00Z","publication_status":"published","article_processing_charge":"No","year":"2016","language":[{"iso":"eng"}],"date_created":"2018-12-11T11:50:35Z","abstract":[{"text":"Balanced knockout tournaments are ubiquitous in sports competitions and are also used in decisionmaking and elections. The traditional computational question, that asks to compute a draw (optimal draw) that maximizes the winning probability for a distinguished player, has received a lot of attention. Previous works consider the problem where the pairwise winning probabilities are known precisely, while we study how robust is the winning probability with respect to small errors in the pairwise winning probabilities. First, we present several illuminating examples to establish: (a) there exist deterministic tournaments (where the pairwise winning probabilities are 0 or 1) where one optimal draw is much more robust than the other; and (b) in general, there exist tournaments with slightly suboptimal draws that are more robust than all the optimal draws. The above examples motivate the study of the computational problem of robust draws that guarantee a specified winning probability. Second, we present a polynomial-time algorithm for approximating the robustness of a draw for sufficiently small errors in pairwise winning probabilities, and obtain that the stated computational problem is NP-complete. We also show that two natural cases of deterministic tournaments where the optimal draw could be computed in polynomial time also admit polynomial-time algorithms to compute robust optimal draws.","lang":"eng"}],"publisher":"AAAI Press","month":"01","status":"public","corr_author":"1","conference":{"end_date":"2016-07-15","name":"IJCAI: International Joint Conference on Artificial Intelligence","location":"New York, NY, USA","start_date":"2016-07-09"},"external_id":{"arxiv":["1604.05090"]},"day":"01","related_material":{"link":[{"relation":"table_of_contents","url":"https://www.ijcai.org/proceedings/2016"}]},"arxiv":1,"title":"Robust draws in balanced knockout tournaments","date_updated":"2025-04-22T13:42:22Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","first_name":"Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_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"}],"citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Tkadlec J. Robust draws in balanced knockout tournaments. In: Vol 2016-January. AAAI Press; 2016:172-179.","ista":"Chatterjee K, Ibsen-Jensen R, Tkadlec J. 2016. Robust draws in balanced knockout tournaments. IJCAI: International Joint Conference on Artificial Intelligence vol. 2016–January, 172–179.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Tkadlec, J. (2016). Robust draws in balanced knockout tournaments (Vol. 2016–January, pp. 172–179). Presented at the IJCAI: International Joint Conference on Artificial Intelligence, New York, NY, USA: AAAI Press.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and J. Tkadlec, “Robust draws in balanced knockout tournaments,” presented at the IJCAI: International Joint Conference on Artificial Intelligence, New York, NY, USA, 2016, vol. 2016–January, pp. 172–179.","mla":"Chatterjee, Krishnendu, et al. <i>Robust Draws in Balanced Knockout Tournaments</i>. Vol. 2016–January, AAAI Press, 2016, pp. 172–79.","short":"K. Chatterjee, R. Ibsen-Jensen, J. Tkadlec, in:, AAAI Press, 2016, pp. 172–179.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Josef Tkadlec. “Robust Draws in Balanced Knockout Tournaments,” 2016–January:172–79. AAAI Press, 2016."},"department":[{"_id":"KrCh"}],"scopus_import":"1","volume":"2016-January","_id":"1182","publist_id":"6171","oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.05090"}]},{"ddc":["530"],"publication":"Physics of Life Reviews","month":"12","status":"public","date_created":"2018-12-11T11:50:40Z","has_accepted_license":"1","publisher":"Elsevier","language":[{"iso":"eng"}],"intvolume":"        19","year":"2016","article_processing_charge":"No","publication_status":"published","file":[{"date_created":"2018-12-12T10:11:02Z","relation":"main_file","creator":"system","checksum":"95e6dc78278334b99dacbf8822509364","file_name":"IST-2017-798-v1+1_comment_adami.pdf","file_size":171352,"access_level":"open_access","content_type":"application/pdf","file_id":"4855","date_updated":"2020-07-14T12:44:39Z"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2016-12-01T00:00:00Z","page":"29 - 31","isi":1,"type":"journal_article","ec_funded":1,"oa":1,"pubrep_id":"798","publist_id":"6150","_id":"1200","quality_controlled":"1","oa_version":"Submitted Version","department":[{"_id":"KrCh"}],"scopus_import":"1","volume":19,"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"citation":{"chicago":"Hilbe, Christian, and Arne Traulsen. “Only the Combination of Mathematics and Agent Based Simulations Can Leverage the Full Potential of Evolutionary Modeling: Comment on ‘Evolutionary Game Theory Using Agent-Based Methods’ by C. Adami, J. Schossau and A. Hintze.” <i>Physics of Life Reviews</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">https://doi.org/10.1016/j.plrev.2016.10.004</a>.","short":"C. Hilbe, A. Traulsen, Physics of Life Reviews 19 (2016) 29–31.","mla":"Hilbe, Christian, and Arne Traulsen. “Only the Combination of Mathematics and Agent Based Simulations Can Leverage the Full Potential of Evolutionary Modeling: Comment on ‘Evolutionary Game Theory Using Agent-Based Methods’ by C. Adami, J. Schossau and A. Hintze.” <i>Physics of Life Reviews</i>, vol. 19, Elsevier, 2016, pp. 29–31, doi:<a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">10.1016/j.plrev.2016.10.004</a>.","ieee":"C. Hilbe and A. Traulsen, “Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on ‘Evolutionary game theory using agent-based methods’ by C. Adami, J. Schossau and A. Hintze,” <i>Physics of Life Reviews</i>, vol. 19. Elsevier, pp. 29–31, 2016.","ista":"Hilbe C, Traulsen A. 2016. Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze. Physics of Life Reviews. 19, 29–31.","apa":"Hilbe, C., &#38; Traulsen, A. (2016). Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze. <i>Physics of Life Reviews</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">https://doi.org/10.1016/j.plrev.2016.10.004</a>","ama":"Hilbe C, Traulsen A. Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze. <i>Physics of Life Reviews</i>. 2016;19:29-31. doi:<a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">10.1016/j.plrev.2016.10.004</a>"},"tmp":{"image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)"},"doi":"10.1016/j.plrev.2016.10.004","author":[{"orcid":"0000-0001-5116-955X","last_name":"Hilbe","first_name":"Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian"},{"last_name":"Traulsen","first_name":"Arne","full_name":"Traulsen, Arne"}],"date_updated":"2025-09-22T09:42:11Z","title":"Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze","file_date_updated":"2020-07-14T12:44:39Z","acknowledgement":"C.H. acknowledges generous support from the ISTFELLOW program.","day":"01","external_id":{"isi":["000390640200003"]}},{"publist_id":"6083","_id":"1245","oa_version":"None","quality_controlled":"1","scopus_import":"1","department":[{"_id":"KrCh"}],"volume":26,"project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"doi":"10.1145/2818052.2869122","citation":{"ista":"Pandey V, Chatterjee K. 2016. Game-theoretic models identify useful principles for peer collaboration in online learning platforms. Proceedings of the ACM Conference on Computer Supported Cooperative Work. CSCW: Computer Supported Cooperative Work and Social Computing vol. 26, 365–368.","ama":"Pandey V, Chatterjee K. Game-theoretic models identify useful principles for peer collaboration in online learning platforms. In: <i>Proceedings of the ACM Conference on Computer Supported Cooperative Work</i>. Vol 26. ACM; 2016:365-368. doi:<a href=\"https://doi.org/10.1145/2818052.2869122\">10.1145/2818052.2869122</a>","apa":"Pandey, V., &#38; Chatterjee, K. (2016). Game-theoretic models identify useful principles for peer collaboration in online learning platforms. In <i>Proceedings of the ACM Conference on Computer Supported Cooperative Work</i> (Vol. 26, pp. 365–368). San Francisco, CA, USA: ACM. <a href=\"https://doi.org/10.1145/2818052.2869122\">https://doi.org/10.1145/2818052.2869122</a>","mla":"Pandey, Vineet, and Krishnendu Chatterjee. “Game-Theoretic Models Identify Useful Principles for Peer Collaboration in Online Learning Platforms.” <i>Proceedings of the ACM Conference on Computer Supported Cooperative Work</i>, vol. 26, no. Februar-2016, ACM, 2016, pp. 365–68, doi:<a href=\"https://doi.org/10.1145/2818052.2869122\">10.1145/2818052.2869122</a>.","ieee":"V. Pandey and K. Chatterjee, “Game-theoretic models identify useful principles for peer collaboration in online learning platforms,” in <i>Proceedings of the ACM Conference on Computer Supported Cooperative Work</i>, San Francisco, CA, USA, 2016, vol. 26, no. Februar-2016, pp. 365–368.","short":"V. Pandey, K. Chatterjee, in:, Proceedings of the ACM Conference on Computer Supported Cooperative Work, ACM, 2016, pp. 365–368.","chicago":"Pandey, Vineet, and Krishnendu Chatterjee. “Game-Theoretic Models Identify Useful Principles for Peer Collaboration in Online Learning Platforms.” In <i>Proceedings of the ACM Conference on Computer Supported Cooperative Work</i>, 26:365–68. ACM, 2016. <a href=\"https://doi.org/10.1145/2818052.2869122\">https://doi.org/10.1145/2818052.2869122</a>."},"author":[{"full_name":"Pandey, Vineet","last_name":"Pandey","first_name":"Vineet"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2025-09-22T09:14:46Z","title":"Game-theoretic models identify useful principles for peer collaboration in online learning platforms","acknowledgement":"ERC Start Grant Graph Games 279307 supported this  research. ","day":"27","conference":{"end_date":"2016-03-02","start_date":"2016-02-26","location":"San Francisco, CA, USA","name":"CSCW: Computer Supported Cooperative Work and Social Computing"},"external_id":{"isi":["000468137600088"]},"issue":"Februar-2016","month":"02","publication":"Proceedings of the ACM Conference on Computer Supported Cooperative Work","status":"public","date_created":"2018-12-11T11:50:55Z","abstract":[{"text":"To facilitate collaboration in massive online classrooms, instructors must make many decisions. For instance, the following parameters need to be decided when designing a peer-feedback system where students review each others' essays: the number of students each student must provide feedback to, an algorithm to map feedback providers to receivers, constraints that ensure students do not become free-riders (receiving feedback but not providing it), the best times to receive feedback to improve learning etc. While instructors can answer these questions by running experiments or invoking past experience, game-theoretic models with data from online learning platforms can identify better initial designs for further improvements. As an example, we explore the design space of a peer feedback system by modeling it using game theory. Our simulations show that incentivizing students to provide feedback requires the value obtained from receiving a feedback to exceed the cost of providing it by a large factor (greater than 7). Furthermore, hiding feedback from low-effort students incentivizes them to provide more feedback.","lang":"eng"}],"publisher":"ACM","language":[{"iso":"eng"}],"intvolume":"        26","year":"2016","article_processing_charge":"No","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2016-02-27T00:00:00Z","page":"365 - 368","isi":1,"type":"conference","ec_funded":1},{"department":[{"_id":"KrCh"}],"scopus_import":"1","volume":11,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"short":"C. Hilbe, K. Hagel, M. Milinski, PLoS One 11 (2016).","chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Asymmetric Power Boosts Extortion in an Economic Experiment.” <i>PLoS One</i>. Public Library of Science, 2016. <a href=\"https://doi.org/10.1371/journal.pone.0163867\">https://doi.org/10.1371/journal.pone.0163867</a>.","ista":"Hilbe C, Hagel K, Milinski M. 2016. Asymmetric power boosts extortion in an economic experiment. PLoS One. 11(10), e0163867.","ama":"Hilbe C, Hagel K, Milinski M. Asymmetric power boosts extortion in an economic experiment. <i>PLoS One</i>. 2016;11(10). doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867\">10.1371/journal.pone.0163867</a>","apa":"Hilbe, C., Hagel, K., &#38; Milinski, M. (2016). Asymmetric power boosts extortion in an economic experiment. <i>PLoS One</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0163867\">https://doi.org/10.1371/journal.pone.0163867</a>","mla":"Hilbe, Christian, et al. “Asymmetric Power Boosts Extortion in an Economic Experiment.” <i>PLoS One</i>, vol. 11, no. 10, e0163867, Public Library of Science, 2016, doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867\">10.1371/journal.pone.0163867</a>.","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Asymmetric power boosts extortion in an economic experiment,” <i>PLoS One</i>, vol. 11, no. 10. Public Library of Science, 2016."},"doi":"10.1371/journal.pone.0163867","pubrep_id":"716","publist_id":"5948","_id":"1322","quality_controlled":"1","oa_version":"Published Version","related_material":{"record":[{"status":"public","relation":"research_data","id":"9867"},{"relation":"research_data","id":"9868","status":"public"}]},"file_date_updated":"2020-07-14T12:44:44Z","acknowledgement":"CH was funded by the Schrödinger program of the Austrian Science Fund (FWF) J3475. ","day":"04","external_id":{"isi":["000385696900024"]},"author":[{"last_name":"Hilbe","orcid":"0000-0001-5116-955X","first_name":"Christian","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hagel, Kristin","last_name":"Hagel","first_name":"Kristin"},{"full_name":"Milinski, Manfred","last_name":"Milinski","first_name":"Manfred"}],"date_updated":"2025-09-22T08:27:01Z","title":"Asymmetric power boosts extortion in an economic experiment","date_created":"2018-12-11T11:51:22Z","abstract":[{"lang":"eng","text":"Direct reciprocity is a major mechanism for the evolution of cooperation. Several classical studies have suggested that humans should quickly learn to adopt reciprocal strategies to establish mutual cooperation in repeated interactions. On the other hand, the recently discovered theory of ZD strategies has found that subjects who use extortionate strategies are able to exploit and subdue cooperators. Although such extortioners have been predicted to succeed in any population of adaptive opponents, theoretical follow-up studies questioned whether extortion can evolve in reality. However, most of these studies presumed that individuals have similar strategic possibilities and comparable outside options, whereas asymmetries are ubiquitous in real world applications. Here we show with a model and an economic experiment that extortionate strategies readily emerge once subjects differ in their strategic power. Our experiment combines a repeated social dilemma with asymmetric partner choice. In our main treatment there is one randomly chosen group member who is unilaterally allowed to exchange one of the other group members after every ten rounds of the social dilemma. We find that this asymmetric replacement opportunity generally promotes cooperation, but often the resulting payoff distribution reflects the underlying power structure. Almost half of the subjects in a better strategic position turn into extortioners, who quickly proceed to exploit their peers. By adapting their cooperation probabilities consistent with ZD theory, extortioners force their co-players to cooperate without being similarly cooperative themselves. Comparison to non-extortionate players under the same conditions indicates a substantial net gain to extortion. Our results thus highlight how power asymmetries can endanger mutually beneficial interactions, and transform them into exploitative relationships. In particular, our results indicate that the extortionate strategies predicted from ZD theory could play a more prominent role in our daily interactions than previously thought."}],"has_accepted_license":"1","publisher":"Public Library of Science","language":[{"iso":"eng"}],"intvolume":"        11","issue":"10","publication":"PLoS One","month":"10","corr_author":"1","status":"public","ddc":["004","006"],"isi":1,"type":"journal_article","oa":1,"year":"2016","article_processing_charge":"No","publication_status":"published","file":[{"date_created":"2018-12-12T10:08:08Z","relation":"main_file","creator":"system","checksum":"6b33e394003dfe8b4ca6be1858aaa8e3","file_name":"IST-2016-716-v1+1_journal.pone.0163867.PDF","file_size":2077905,"access_level":"open_access","content_type":"application/pdf","file_id":"4668","date_updated":"2020-07-14T12:44:44Z"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2016-10-04T00:00:00Z","article_number":"e0163867"},{"oa":1,"type":"conference","ec_funded":1,"page":"88 - 96","date_published":"2016-01-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","year":"2016","article_processing_charge":"No","intvolume":"      2016","language":[{"iso":"eng"}],"publisher":"AAAI Press","date_created":"2018-12-11T11:51:22Z","abstract":[{"text":"DEC-POMDPs extend POMDPs to a multi-agent setting, where several agents operate in an uncertain environment independently to achieve a joint objective. DEC-POMDPs have been studied with finite-horizon and infinite-horizon discounted-sum objectives, and there exist solvers both for exact and approximate solutions. In this work we consider Goal-DEC-POMDPs, where given a set of target states, the objective is to ensure that the target set is reached with minimal cost. We consider the indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present a new and novel method to solve the problem that extends methods for finite-horizon DEC-POMDPs and the RTDP-Bel approach for POMDPs. We present experimental results on several examples, and show that our approach presents promising results. Copyright ","lang":"eng"}],"publication":"Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling","month":"01","corr_author":"1","status":"public","conference":{"start_date":"2016-06-12","name":"ICAPS: International Conference on Automated Planning and Scheduling","location":"London, United Kingdom","end_date":"2016-06-17"},"day":"01","title":"Indefinite-horizon reachability in Goal-DEC-POMDPs","date_updated":"2025-05-19T11:03:49Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik"}],"doi":"10.1609/icaps.v26i1.13737","citation":{"chicago":"Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” In <i>Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling</i>, 2016:88–96. AAAI Press, 2016. <a href=\"https://doi.org/10.1609/icaps.v26i1.13737\">https://doi.org/10.1609/icaps.v26i1.13737</a>.","short":"K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling, AAAI Press, 2016, pp. 88–96.","ieee":"K. Chatterjee and M. Chmelik, “Indefinite-horizon reachability in Goal-DEC-POMDPs,” in <i>Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling</i>, London, United Kingdom, 2016, vol. 2016, pp. 88–96.","mla":"Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” <i>Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling</i>, vol. 2016, AAAI Press, 2016, pp. 88–96, doi:<a href=\"https://doi.org/10.1609/icaps.v26i1.13737\">10.1609/icaps.v26i1.13737</a>.","ama":"Chatterjee K, Chmelik M. Indefinite-horizon reachability in Goal-DEC-POMDPs. In: <i>Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling</i>. Vol 2016. AAAI Press; 2016:88-96. doi:<a href=\"https://doi.org/10.1609/icaps.v26i1.13737\">10.1609/icaps.v26i1.13737</a>","apa":"Chatterjee, K., &#38; Chmelik, M. (2016). Indefinite-horizon reachability in Goal-DEC-POMDPs. In <i>Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling</i> (Vol. 2016, pp. 88–96). London, United Kingdom: AAAI Press. <a href=\"https://doi.org/10.1609/icaps.v26i1.13737\">https://doi.org/10.1609/icaps.v26i1.13737</a>","ista":"Chatterjee K, Chmelik M. 2016. Indefinite-horizon reachability in Goal-DEC-POMDPs. Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 2016, 88–96."},"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"volume":2016,"department":[{"_id":"KrCh"}],"scopus_import":"1","quality_controlled":"1","oa_version":"None","main_file_link":[{"url":"http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/12999","open_access":"1"}],"_id":"1324","publist_id":"5946"},{"pubrep_id":"665","oa_version":"Published Version","quality_controlled":"1","_id":"1325","publist_id":"5944","volume":59,"department":[{"_id":"KrCh"}],"scopus_import":1,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"ieee":"T. Brázdil, V. Forejt, A. Kučera, and P. Novotný, “Stability in graphs and games,” presented at the CONCUR: Concurrency Theory, Quebec City, Canada, 2016, vol. 59.","mla":"Brázdil, Tomáš, et al. <i>Stability in Graphs and Games</i>. Vol. 59, 10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">10.4230/LIPIcs.CONCUR.2016.10</a>.","ista":"Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.","apa":"Brázdil, T., Forejt, V., Kučera, A., &#38; Novotný, P. (2016). Stability in graphs and games (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.10</a>","ama":"Brázdil T, Forejt V, Kučera A, Novotný P. Stability in graphs and games. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">10.4230/LIPIcs.CONCUR.2016.10</a>","chicago":"Brázdil, Tomáš, Vojtěch Forejt, Antonín Kučera, and Petr Novotný. “Stability in Graphs and Games,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.10</a>.","short":"T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016."},"doi":"10.4230/LIPIcs.CONCUR.2016.10","project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"author":[{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"full_name":"Forejt, Vojtěch","last_name":"Forejt","first_name":"Vojtěch"},{"last_name":"Kučera","first_name":"Antonín","full_name":"Kučera, Antonín"},{"first_name":"Petr","last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"title":"Stability in graphs and games","date_updated":"2024-10-09T20:57:03Z","day":"01","acknowledgement":"The work has been supported by the Czech Science Foundation, grant No. 15-17564S, by EPSRC grant\r\nEP/M023656/1, and by the People Programme (Marie Curie Actions) of the European Union’s Seventh\r\nFramework Programme (FP7/2007-2013) under REA grant agreement no [291734]","file_date_updated":"2020-07-14T12:44:44Z","conference":{"start_date":"2016-08-23","name":"CONCUR: Concurrency Theory","location":"Quebec City, Canada","end_date":"2016-08-26"},"status":"public","ddc":["004"],"corr_author":"1","month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","has_accepted_license":"1","abstract":[{"text":"We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system.","lang":"eng"}],"date_created":"2018-12-11T11:51:23Z","alternative_title":["LIPIcs"],"intvolume":"        59","language":[{"iso":"eng"}],"file":[{"date_updated":"2020-07-14T12:44:44Z","file_id":"5229","access_level":"open_access","content_type":"application/pdf","file_size":553648,"file_name":"IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf","checksum":"3c2dc6ab0358f8aa8f7aa7d6c1293159","creator":"system","date_created":"2018-12-12T10:16:40Z","relation":"main_file"}],"publication_status":"published","year":"2016","article_number":"10","date_published":"2016-08-01T00:00:00Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa":1,"type":"conference","ec_funded":1},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2016-09-22T00:00:00Z","publication_status":"published","article_processing_charge":"No","year":"2016","ec_funded":1,"type":"conference","isi":1,"oa":1,"page":"32 - 49","corr_author":"1","status":"public","month":"09","language":[{"iso":"eng"}],"intvolume":"      9938","abstract":[{"lang":"eng","text":"Energy Markov Decision Processes (EMDPs) are finite-state Markov decision processes where each transition is assigned an integer counter update and a rational payoff. An EMDP configuration is a pair s(n), where s is a control state and n is the current counter value. The configurations are changed by performing transitions in the standard way. We consider the problem of computing a safe strategy (i.e., a strategy that keeps the counter non-negative) which maximizes the expected mean payoff. "}],"date_created":"2018-12-11T11:51:23Z","alternative_title":["LNCS"],"publisher":"Springer","title":"Optimizing the expected mean payoff in Energy Markov Decision Processes","date_updated":"2025-09-22T08:25:26Z","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"full_name":"Kučera, Antonín","last_name":"Kučera","first_name":"Antonín"},{"last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr"}],"conference":{"end_date":"2016-10-20","location":"Chiba, Japan","name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2016-10-17"},"external_id":{"isi":["000389808100003"],"arxiv":["1607.00678"]},"day":"22","acknowledgement":"The research was funded by the Czech Science Foundation Grant No. P202/12/G061 and by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].","arxiv":1,"_id":"1326","publist_id":"5943","quality_controlled":"1","oa_version":"Preprint","main_file_link":[{"url":"https://arxiv.org/abs/1607.00678","open_access":"1"}],"project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"doi":"10.1007/978-3-319-46520-3_3","citation":{"ama":"Brázdil T, Kučera A, Novotný P. Optimizing the expected mean payoff in Energy Markov Decision Processes. In: Vol 9938. Springer; 2016:32-49. doi:<a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">10.1007/978-3-319-46520-3_3</a>","apa":"Brázdil, T., Kučera, A., &#38; Novotný, P. (2016). Optimizing the expected mean payoff in Energy Markov Decision Processes (Vol. 9938, pp. 32–49). Presented at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan: Springer. <a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">https://doi.org/10.1007/978-3-319-46520-3_3</a>","ista":"Brázdil T, Kučera A, Novotný P. 2016. Optimizing the expected mean payoff in Energy Markov Decision Processes. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 9938, 32–49.","ieee":"T. Brázdil, A. Kučera, and P. Novotný, “Optimizing the expected mean payoff in Energy Markov Decision Processes,” presented at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan, 2016, vol. 9938, pp. 32–49.","mla":"Brázdil, Tomáš, et al. <i>Optimizing the Expected Mean Payoff in Energy Markov Decision Processes</i>. Vol. 9938, Springer, 2016, pp. 32–49, doi:<a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">10.1007/978-3-319-46520-3_3</a>.","short":"T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.","chicago":"Brázdil, Tomáš, Antonín Kučera, and Petr Novotný. “Optimizing the Expected Mean Payoff in Energy Markov Decision Processes,” 9938:32–49. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">https://doi.org/10.1007/978-3-319-46520-3_3</a>."},"department":[{"_id":"KrCh"}],"scopus_import":"1","volume":9938},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2016-01-01T00:00:00Z","publication_status":"published","article_processing_charge":"No","year":"2016","ec_funded":1,"type":"conference","oa":1,"page":"1465 - 1466","publication":"Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems","month":"01","status":"public","language":[{"iso":"eng"}],"date_created":"2018-12-11T11:51:23Z","abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs) with a set of target states and positive integer costs associated with every transition. The traditional optimization objective (stochastic shortest path) asks to minimize the expected total cost until the target set is reached. We extend the traditional framework of POMDPs to model energy consumption, which represents a hard constraint. The energy levels may increase and decrease with transitions, and the hard constraint requires that the energy level must remain positive in all steps till the target is reached. First, we present a novel algorithm for solving POMDPs with energy levels, developing on existing POMDP solvers and using RTDP as its main method. Our second contribution is related to policy representation. For larger POMDP instances the policies computed by existing solvers are too large to be understandable. We present an automated procedure based on machine learning techniques that automatically extracts important decisions of the policy allowing us to compute succinct human readable policies. Finally, we show experimentally that our algorithm performs well and computes succinct policies on a number of POMDP instances from the literature that were naturally enhanced with energy levels. "}],"publisher":"ACM","title":"Stochastic shortest path with energy constraints in POMDPs","date_updated":"2025-06-04T10:26:23Z","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"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"full_name":"Gupta, Anchit","first_name":"Anchit","last_name":"Gupta"},{"last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr"}],"conference":{"start_date":"2016-05-09","name":"AAMAS: Autonomous Agents & Multiagent Systems","location":"Singapore","end_date":"2016-05-13"},"external_id":{"arxiv":["1602.07565"]},"day":"01","arxiv":1,"_id":"1327","publist_id":"5942","oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"url":"https://arxiv.org/abs/1602.07565","open_access":"1"}],"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":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"citation":{"chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>, 1465–66. ACM, 2016.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–1466.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic shortest path with energy constraints in POMDPs,” in <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>, Singapore, 2016, pp. 1465–1466.","mla":"Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in POMDPs.” <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>, ACM, 2016, pp. 1465–66.","ista":"Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic shortest path with energy constraints in POMDPs. Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents &#38; Multiagent Systems, 1465–1466.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., &#38; Novotný, P. (2016). Stochastic shortest path with energy constraints in POMDPs. In <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i> (pp. 1465–1466). Singapore: ACM.","ama":"Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest path with energy constraints in POMDPs. In: <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>. ACM; 2016:1465-1466."},"department":[{"_id":"KrCh"}],"scopus_import":"1"},{"intvolume":"         7","language":[{"iso":"eng"}],"publisher":"Nature Publishing Group","date_created":"2018-12-11T11:51:25Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"Social dilemmas force players to balance between personal and collective gain. In many dilemmas, such as elected governments negotiating climate-change mitigation measures, the decisions are made not by individual players but by their representatives. However, the behaviour of representatives in social dilemmas has not been investigated experimentally. Here inspired by the negotiations for greenhouse-gas emissions reductions, we experimentally study a collective-risk social dilemma that involves representatives deciding on behalf of their fellow group members. Representatives can be re-elected or voted out after each consecutive collective-risk game. Selfish players are preferentially elected and are hence found most frequently in the &quot;representatives&quot; treatment. Across all treatments, we identify the selfish players as extortioners. As predicted by our mathematical model, their steadfast strategies enforce cooperation from fair players who finally compensate almost completely the deficit caused by the extortionate co-players. Everybody gains, but the extortionate representatives and their groups gain the most."}],"corr_author":"1","ddc":["519","530","599"],"month":"03","publication":"Nature Communications","status":"public","oa":1,"isi":1,"type":"journal_article","article_number":"10915","date_published":"2016-03-07T00:00:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"relation":"main_file","date_created":"2018-12-12T10:10:44Z","file_name":"IST-2016-661-v1+1_ncomms10915.pdf","checksum":"9ea0d7ce59a555a1cb8353d5559407cb","creator":"system","file_size":1432577,"content_type":"application/pdf","access_level":"open_access","file_id":"4834","date_updated":"2020-07-14T12:44:44Z"}],"year":"2016","article_processing_charge":"No","publication_status":"published","doi":"10.1038/ncomms10915","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"ieee":"M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, and J. Marotzke, “Humans choose representatives who enforce cooperation in social dilemmas through extortion,” <i>Nature Communications</i>, vol. 7. Nature Publishing Group, 2016.","mla":"Milinski, Manfred, et al. “Humans Choose Representatives Who Enforce Cooperation in Social Dilemmas through Extortion.” <i>Nature Communications</i>, vol. 7, 10915, Nature Publishing Group, 2016, doi:<a href=\"https://doi.org/10.1038/ncomms10915\">10.1038/ncomms10915</a>.","ista":"Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. 2016. Humans choose representatives who enforce cooperation in social dilemmas through extortion. Nature Communications. 7, 10915.","apa":"Milinski, M., Hilbe, C., Semmann, D., Sommerfeld, R., &#38; Marotzke, J. (2016). Humans choose representatives who enforce cooperation in social dilemmas through extortion. <i>Nature Communications</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/ncomms10915\">https://doi.org/10.1038/ncomms10915</a>","ama":"Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. Humans choose representatives who enforce cooperation in social dilemmas through extortion. <i>Nature Communications</i>. 2016;7. doi:<a href=\"https://doi.org/10.1038/ncomms10915\">10.1038/ncomms10915</a>","chicago":"Milinski, Manfred, Christian Hilbe, Dirk Semmann, Ralf Sommerfeld, and Jochem Marotzke. “Humans Choose Representatives Who Enforce Cooperation in Social Dilemmas through Extortion.” <i>Nature Communications</i>. Nature Publishing Group, 2016. <a href=\"https://doi.org/10.1038/ncomms10915\">https://doi.org/10.1038/ncomms10915</a>.","short":"M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, J. Marotzke, Nature Communications 7 (2016)."},"volume":7,"scopus_import":"1","department":[{"_id":"KrCh"}],"oa_version":"Published Version","quality_controlled":"1","publist_id":"5935","_id":"1333","pubrep_id":"661","external_id":{"isi":["000371720200001"]},"file_date_updated":"2020-07-14T12:44:44Z","acknowledgement":"We thank the students for participation; H.-J. Krambeck for writing the software for the game; H. Arndt, T. Bakker, L. Becks, H. Brendelberger, S. Dobler and T. Reusch for support; and the Max Planck Society for the Advancement of Science for funding.","day":"07","date_updated":"2025-09-22T08:21:34Z","title":"Humans choose representatives who enforce cooperation in social dilemmas through extortion","author":[{"first_name":"Manfred","last_name":"Milinski","full_name":"Milinski, Manfred"},{"full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe","orcid":"0000-0001-5116-955X","first_name":"Christian"},{"last_name":"Semmann","first_name":"Dirk","full_name":"Semmann, Dirk"},{"full_name":"Sommerfeld, Ralf","last_name":"Sommerfeld","first_name":"Ralf"},{"full_name":"Marotzke, Jochem","last_name":"Marotzke","first_name":"Jochem"}]},{"status":"public","corr_author":"1","month":"08","language":[{"iso":"eng"}],"intvolume":"      9837","alternative_title":["LNCS"],"date_created":"2018-12-11T11:51:26Z","abstract":[{"lang":"eng","text":"In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted ω-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted ω-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted ω-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties."}],"publisher":"Springer","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2016-08-31T00:00:00Z","year":"2016","article_processing_charge":"No","publication_status":"published","isi":1,"type":"conference","ec_funded":1,"oa":1,"page":"23 - 38","publist_id":"5932","_id":"1335","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"quality_controlled":"1","oa_version":"Preprint","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"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":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"doi":"10.1007/978-3-662-53413-7_2","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Monitor Automata,” 9837:23–38. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.","mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Monitor Automata</i>. Vol. 9837, Springer, 2016, pp. 23–38, doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,” presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016, vol. 9837, pp. 23–38.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>"},"scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":9837,"date_updated":"2025-09-22T08:19:49Z","title":"Quantitative monitor automata","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"}],"conference":{"name":"SAS: Static Analysis Symposium","location":"Edinburgh, United Kingdom","start_date":"2016-09-08","end_date":"2016-09-10"},"external_id":{"arxiv":["1604.06764"],"isi":["000388924600002"]},"day":"31","arxiv":1}]