[{"language":[{"iso":"eng"}],"publication":"Proceedings of the ACM on Programming Languages","title":"Data-centric dynamic partial order reduction","oa":1,"date_updated":"2023-02-23T12:27:16Z","issue":"POPL","article_processing_charge":"No","scopus_import":"1","intvolume":"         2","status":"public","type":"journal_article","author":[{"first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"},{"last_name":"Sinha","full_name":"Sinha, Nishant","first_name":"Nishant"},{"last_name":"Vaidya","first_name":"Kapil","full_name":"Vaidya, Kapil"}],"arxiv":1,"oa_version":"Published Version","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158119","open_access":"1"}],"day":"27","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","conference":{"start_date":"2018-01-07","name":"POPL: Programming Languages","end_date":"2018-01-13","location":"Los Angeles, CA, United States"},"month":"12","publication_identifier":{"eissn":["2475-1421"]},"_id":"10417","article_type":"original","doi":"10.1145/3158119","citation":{"apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., &#38; Vaidya, K. (2017). Data-centric dynamic partial order reduction. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158119\">https://doi.org/10.1145/3158119</a>","mla":"Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 31, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158119\">10.1145/3158119</a>.","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. 2(POPL), 31.","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158119\">https://doi.org/10.1145/3158119</a>.","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic partial order reduction. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158119\">10.1145/3158119</a>","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric dynamic partial order reduction,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings of the ACM on Programming Languages 2 (2017)."},"date_created":"2021-12-05T23:01:49Z","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061.","year":"2017","ec_funded":1,"article_number":"31","related_material":{"record":[{"id":"5448","relation":"earlier_version","status":"public"},{"status":"public","id":"5456","relation":"earlier_version"}]},"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":2,"publisher":"Association for Computing Machinery","date_published":"2017-12-27T00:00:00Z","publication_status":"published","external_id":{"arxiv":["1610.01188"]},"abstract":[{"lang":"eng","text":"We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.\r\n\r\nWe introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence."}]},{"status":"public","type":"journal_article","month":"12","publication_identifier":{"eissn":["2475-1421"]},"conference":{"location":"Los Angeles, CA, United States","end_date":"2018-01-13","name":"POPL: Programming Languages","start_date":"2018-01-07"},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","day":"07","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158121","open_access":"1"}],"oa_version":"Published Version","arxiv":1,"author":[{"full_name":"Mciver, Annabelle","first_name":"Annabelle","last_name":"Mciver"},{"full_name":"Morgan, Carroll","first_name":"Carroll","last_name":"Morgan"},{"full_name":"Kaminski, Benjamin Lucien","first_name":"Benjamin Lucien","last_name":"Kaminski"},{"first_name":"Joost P","full_name":"Katoen, Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87","last_name":"Katoen"}],"publication":"Proceedings of the ACM on Programming Languages","language":[{"iso":"eng"}],"intvolume":"         2","scopus_import":"1","issue":"POPL","article_processing_charge":"No","date_updated":"2021-12-07T08:04:14Z","oa":1,"title":"A new proof rule for almost-sure termination","date_published":"2017-12-07T00:00:00Z","publisher":"Association for Computing Machinery","quality_controlled":"1","volume":2,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"abstract":[{"lang":"eng","text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains."}],"external_id":{"arxiv":["1711.03588"]},"publication_status":"published","doi":"10.1145/3158121","article_type":"original","_id":"10418","article_number":"33","year":"2017","acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","date_created":"2021-12-05T23:01:49Z","citation":{"short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>","chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>.","ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.","mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>.","apa":"Mciver, A., Morgan, C., Kaminski, B. L., &#38; Katoen, J. P. (2017). A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>"}},{"title":"Pushdown reachability with constant treewidth","oa":1,"pubrep_id":"991","date_updated":"2023-09-20T12:08:18Z","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1","intvolume":"       122","isi":1,"language":[{"iso":"eng"}],"publication":"Information Processing Letters","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Georg F","full_name":"Osang, Georg F","last_name":"Osang","id":"464B40D6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8882-5116"}],"day":"01","oa_version":"Submitted Version","file":[{"file_name":"IST-2018-991-v1+2_2018_Chatterjee_Pushdown_PREPRINT.pdf","file_id":"4998","date_created":"2018-12-12T10:13:17Z","date_updated":"2019-10-15T07:44:51Z","creator":"system","relation":"main_file","file_size":247657,"content_type":"application/pdf","access_level":"open_access"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"issn":["00200190"]},"month":"06","status":"public","type":"journal_article","date_created":"2018-12-11T11:49:57Z","citation":{"apa":"Chatterjee, K., &#38; Osang, G. F. (2017). Pushdown reachability with constant treewidth. <i>Information Processing Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">https://doi.org/10.1016/j.ipl.2017.02.003</a>","ama":"Chatterjee K, Osang GF. Pushdown reachability with constant treewidth. <i>Information Processing Letters</i>. 2017;122:25-29. doi:<a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">10.1016/j.ipl.2017.02.003</a>","ieee":"K. Chatterjee and G. F. Osang, “Pushdown reachability with constant treewidth,” <i>Information Processing Letters</i>, vol. 122. Elsevier, pp. 25–29, 2017.","short":"K. Chatterjee, G.F. Osang, Information Processing Letters 122 (2017) 25–29.","mla":"Chatterjee, Krishnendu, and Georg F. Osang. “Pushdown Reachability with Constant Treewidth.” <i>Information Processing Letters</i>, vol. 122, Elsevier, 2017, pp. 25–29, doi:<a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">10.1016/j.ipl.2017.02.003</a>.","chicago":"Chatterjee, Krishnendu, and Georg F Osang. “Pushdown Reachability with Constant Treewidth.” <i>Information Processing Letters</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">https://doi.org/10.1016/j.ipl.2017.02.003</a>.","ista":"Chatterjee K, Osang GF. 2017. Pushdown reachability with constant treewidth. Information Processing Letters. 122, 25–29."},"publist_id":"6323","year":"2017","ec_funded":1,"file_date_updated":"2019-10-15T07:44:51Z","_id":"1065","doi":"10.1016/j.ipl.2017.02.003","publication_status":"published","external_id":{"isi":["000399506600005"]},"abstract":[{"text":"We consider the problem of reachability in pushdown graphs. We study the problem for pushdown graphs with constant treewidth. Even for pushdown graphs with treewidth 1, for the reachability problem we establish the following: (i) the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem would contradict the k-clique conjecture and imply faster combinatorial algorithms for cliques in graphs.","lang":"eng"}],"ddc":["000"],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"page":"25 - 29","department":[{"_id":"KrCh"},{"_id":"HeEd"}],"quality_controlled":"1","volume":122,"publisher":"Elsevier","date_published":"2017-06-01T00:00:00Z"},{"day":"01","oa_version":"None","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"06","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan"},{"first_name":"Yaron","full_name":"Velner, Yaron","last_name":"Velner"}],"type":"journal_article","status":"public","intvolume":"       254","scopus_import":"1","isi":1,"title":"Quantitative fair simulation games","date_updated":"2023-09-20T12:07:48Z","issue":"2","article_processing_charge":"No","publication":"Information and Computation","language":[{"iso":"eng"}],"external_id":{"isi":["000402025600002"]},"abstract":[{"lang":"eng","text":"Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms."}],"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"143 - 166","quality_controlled":"1","volume":254,"publisher":"Elsevier","date_published":"2017-06-01T00:00:00Z","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5428"}]},"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” <i>Information and Computation</i>, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. <i>Information and Computation</i>. 2017;254(2):143-166. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2017). Quantitative fair simulation games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>"},"publist_id":"6322","date_created":"2018-12-11T11:49:58Z","year":"2017","doi":"10.1016/j.ic.2016.10.006","_id":"1066"},{"isi":1,"has_accepted_license":"1","scopus_import":"1","intvolume":"         8","oa":1,"date_updated":"2023-09-20T11:55:31Z","pubrep_id":"786","article_processing_charge":"No","title":"Reconstructing metastatic seeding patterns of human cancers","publication":"Nature Communications","language":[{"iso":"eng"}],"publication_identifier":{"issn":["20411723"]},"month":"01","day":"31","oa_version":"Published Version","file":[{"file_id":"5133","file_name":"IST-2017-786-v1+1_ncomms14114.pdf","date_created":"2018-12-12T10:15:15Z","date_updated":"2018-12-12T10:15:15Z","creator":"system","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_size":897050}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"full_name":"Reiter, Johannes","first_name":"Johannes","orcid":"0000-0002-0170-7353","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Makohon Moore","first_name":"Alvin","full_name":"Makohon Moore, Alvin"},{"full_name":"Gerold, Jeffrey","first_name":"Jeffrey","last_name":"Gerold"},{"first_name":"Ivana","full_name":"Božić, Ivana","last_name":"Božić"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Iacobuzio Donahue, Christine","first_name":"Christine","last_name":"Iacobuzio Donahue"},{"last_name":"Vogelstein","first_name":"Bert","full_name":"Vogelstein, Bert"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"type":"journal_article","status":"public","ec_funded":1,"article_number":"14114","year":"2017","citation":{"mla":"Reiter, Johannes, et al. “Reconstructing Metastatic Seeding Patterns of Human Cancers.” <i>Nature Communications</i>, vol. 8, 14114, Nature Publishing Group, 2017, doi:<a href=\"https://doi.org/10.1038/ncomms14114\">10.1038/ncomms14114</a>.","ista":"Reiter J, Makohon Moore A, Gerold J, Božić I, Chatterjee K, Iacobuzio Donahue C, Vogelstein B, Nowak M. 2017. Reconstructing metastatic seeding patterns of human cancers. Nature Communications. 8, 14114.","chicago":"Reiter, Johannes, Alvin Makohon Moore, Jeffrey Gerold, Ivana Božić, Krishnendu Chatterjee, Christine Iacobuzio Donahue, Bert Vogelstein, and Martin Nowak. “Reconstructing Metastatic Seeding Patterns of Human Cancers.” <i>Nature Communications</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/ncomms14114\">https://doi.org/10.1038/ncomms14114</a>.","ama":"Reiter J, Makohon Moore A, Gerold J, et al. Reconstructing metastatic seeding patterns of human cancers. <i>Nature Communications</i>. 2017;8. doi:<a href=\"https://doi.org/10.1038/ncomms14114\">10.1038/ncomms14114</a>","ieee":"J. Reiter <i>et al.</i>, “Reconstructing metastatic seeding patterns of human cancers,” <i>Nature Communications</i>, vol. 8. Nature Publishing Group, 2017.","short":"J. Reiter, A. Makohon Moore, J. Gerold, I. Božić, K. Chatterjee, C. Iacobuzio Donahue, B. Vogelstein, M. Nowak, Nature Communications 8 (2017).","apa":"Reiter, J., Makohon Moore, A., Gerold, J., Božić, I., Chatterjee, K., Iacobuzio Donahue, C., … Nowak, M. (2017). Reconstructing metastatic seeding patterns of human cancers. <i>Nature Communications</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/ncomms14114\">https://doi.org/10.1038/ncomms14114</a>"},"date_created":"2018-12-11T11:50:02Z","publist_id":"6301","doi":"10.1038/ncomms14114","file_date_updated":"2018-12-12T10:15:15Z","_id":"1080","ddc":["004","006"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"isi":["000393096600001"]},"abstract":[{"text":"Reconstructing the evolutionary history of metastases is critical for understanding their basic biological principles and has profound clinical implications. Genome-wide sequencing data has enabled modern phylogenomic methods to accurately dissect subclones and their phylogenies from noisy and impure bulk tumour samples at unprecedented depth. However, existing methods are not designed to infer metastatic seeding patterns. Here we develop a tool, called Treeomics, to reconstruct the phylogeny of metastases and map subclones to their anatomic locations. Treeomics infers comprehensive seeding patterns for pancreatic, ovarian, and prostate cancers. Moreover, Treeomics correctly disambiguates true seeding patterns from sequencing artifacts; 7% of variants were misclassified by conventional statistical methods. These artifacts can skew phylogenies by creating illusory tumour heterogeneity among distinct samples. In silico benchmarking on simulated tumour phylogenies across a wide range of sample purities (15–95%) and sequencing depths (25-800 × ) demonstrates the accuracy of Treeomics compared with existing methods.","lang":"eng"}],"publication_status":"published","publisher":"Nature Publishing Group","date_published":"2017-01-31T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":8,"project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"}]},{"date_published":"2017-01-01T00:00:00Z","publisher":"Springer","quality_controlled":"1","volume":10482,"page":"59 - 66","department":[{"_id":"KrCh"}],"project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"ddc":["005"],"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"}],"external_id":{"isi":["000723567800004"]},"publication_status":"published","doi":"10.1007/978-3-319-68167-2_4","_id":"949","file_date_updated":"2020-07-14T12:48:16Z","related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"ec_funded":1,"year":"2017","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>.","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.","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>.","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>","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.","short":"K. Chatterjee, A.K. Goharshady, A. Pavlogiannis, in:, D. D’Souza (Ed.), Springer, 2017, 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>"},"publist_id":"6468","date_created":"2018-12-11T11:49:22Z","status":"public","type":"conference","alternative_title":["LNCS"],"publication_identifier":{"issn":["03029743"]},"month":"01","conference":{"start_date":"2017-10-03","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2017-10-06","location":"Pune, India"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"file_size":948514,"relation":"main_file","content_type":"application/pdf","access_level":"open_access","creator":"system","date_created":"2018-12-12T10:10:45Z","date_updated":"2020-07-14T12:48:16Z","file_id":"4835","checksum":"a0d9f5f94dc594c4e71e78525c9942f1","file_name":"IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf"}],"day":"01","oa_version":"Submitted Version","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","full_name":"Goharshady, Amir","first_name":"Amir"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"editor":[{"last_name":"D'Souza","full_name":"D'Souza, Deepak","first_name":"Deepak"}],"isi":1,"has_accepted_license":"1","intvolume":"     10482","scopus_import":"1","article_processing_charge":"No","date_updated":"2024-03-25T23:30:19Z","pubrep_id":"845","oa":1,"title":"JTDec: A tool for tree decompositions in soot"},{"doi":"10.4230/LIPIcs.CONCUR.2017.21","file_date_updated":"2020-07-14T12:48:16Z","_id":"950","related_material":{"record":[{"status":"public","id":"6752","relation":"later_version"}]},"article_number":"17","year":"2017","date_created":"2018-12-11T11:49:22Z","citation":{"apa":"Avni, G., Henzinger, T. A., &#38; Chonev, V. K. (2017). Infinite-duration bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>","mla":"Avni, Guy, et al. <i>Infinite-Duration Bidding Games</i>. Vol. 85, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">10.4230/LIPIcs.CONCUR.2017.21</a>.","ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17.","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>.","short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">10.4230/LIPIcs.CONCUR.2017.21</a>"},"publist_id":"6466","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2017-09-01T00:00:00Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","volume":85,"project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"arxiv":["1705.01433"]},"abstract":[{"text":"Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. \r\n","lang":"eng"}],"publication_status":"published","language":[{"iso":"eng"}],"has_accepted_license":"1","scopus_import":1,"intvolume":"        85","date_updated":"2023-08-29T07:02:13Z","pubrep_id":"844","oa":1,"title":"Infinite-duration bidding games","alternative_title":["LIPIcs"],"status":"public","type":"conference","conference":{"start_date":"2017-09-05","name":"CONCUR: Concurrency Theory","end_date":"2017-09-07","location":"Berlin, Germany"},"month":"09","publication_identifier":{"issn":["1868-8969"]},"day":"01","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_size":335170,"creator":"system","date_updated":"2020-07-14T12:48:16Z","date_created":"2018-12-12T10:18:00Z","checksum":"6d5cccf755207b91ccbef95d8275b013","file_name":"IST-2017-844-v1+1_concur-cr.pdf","file_id":"5318"}],"author":[{"first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Chonev","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","full_name":"Chonev, Ventsislav K","first_name":"Ventsislav K"}],"arxiv":1},{"publication_status":"published","external_id":{"isi":["000408311200013"]},"abstract":[{"text":"Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider the probabilistic behavior of the programs, the invariants are obtained completely ignoring the probabilistic aspect. In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We define the notion of {\\em stochastic invariants}, which are constraints along with a probability bound that the constraints hold. We introduce a concept of {\\em repulsing supermartingales}. First, we show that repulsing supermartingales can be used to obtain bounds on the probability of the stochastic invariants. Second, we show the effectiveness of repulsing supermartingales in the following three ways: (1)~With a combination of ranking and repulsing supermartingales we can compute lower bounds on the probability of termination; (2)~repulsing supermartingales provide witnesses for refutation of almost-sure termination; and (3)~with a combination of ranking and repulsing supermartingales we can establish persistence properties of probabilistic programs. We also present results on related computational problems and an experimental evaluation of our approach on academic examples. ","lang":"eng"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"publisher":"ACM","date_published":"2017-01-01T00:00:00Z","page":"145 - 160","department":[{"_id":"KrCh"}],"volume":52,"quality_controlled":"1","year":"2017","publist_id":"6157","date_created":"2018-12-11T11:50:39Z","citation":{"apa":"Chatterjee, K., Novotný, P., &#38; Zikelic, D. (2017). Stochastic invariants for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles of Programming Languages, Paris, France: ACM. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>","ieee":"K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic termination,” presented at the POPL: Principles of Programming Languages, Paris, France, 2017, vol. 52, no. 1, pp. 145–160.","ama":"Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic termination. In: Vol 52. ACM; 2017:145-160. doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>","short":"K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.","chicago":"Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Stochastic Invariants for Probabilistic Termination</i>. Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>.","ista":"Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 52, 145–160."},"ec_funded":1,"related_material":{"record":[{"relation":"dissertation_contains","id":"14539","status":"public"}]},"_id":"1194","doi":"10.1145/3009837.3009873","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Petr","full_name":"Novotny, Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zikelic","full_name":"Zikelic, Djordje","first_name":"Djordje"}],"conference":{"end_date":"2017-01-21","location":"Paris, France","start_date":"2017-01-15","name":"POPL: Principles of Programming Languages"},"month":"01","publication_identifier":{"issn":["07308566"]},"main_file_link":[{"url":"https://arxiv.org/abs/1611.01063","open_access":"1"}],"day":"01","oa_version":"Submitted Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","alternative_title":["ACM SIGPLAN Notices"],"type":"conference","status":"public","oa":1,"date_updated":"2025-07-14T09:09:58Z","issue":"1","article_processing_charge":"No","title":"Stochastic invariants for probabilistic termination","isi":1,"scopus_import":"1","intvolume":"        52","language":[{"iso":"eng"}]},{"file_date_updated":"2020-07-14T12:46:32Z","_id":"464","doi":"10.23638/LMCS-13(3:26)2017","citation":{"apa":"Chatterjee, K., Henzinger, M. H., &#38; Loitzenbauer, V. (2017). Improved algorithms for parity and Streett objectives. <i>Logical Methods in Computer Science</i>. International Federation of 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>","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 of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">10.23638/LMCS-13(3:26)2017</a>.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for Parity and Streett Objectives.” <i>Logical Methods in Computer Science</i>. International Federation of 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>.","ista":"Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.","ama":"Chatterjee K, Henzinger MH, 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>","ieee":"K. Chatterjee, M. H. Henzinger, and V. Loitzenbauer, “Improved algorithms for parity and Streett objectives,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","short":"K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, Logical Methods in Computer Science 13 (2017)."},"publist_id":"7357","date_created":"2018-12-11T11:46:37Z","year":"2017","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1661"}]},"article_number":"26","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":13,"publisher":"International Federation of Computational Logic","license":"https://creativecommons.org/licenses/by-nd/4.0/","date_published":"2017-09-26T00:00:00Z","publication_status":"published","external_id":{"arxiv":["1410.0833"]},"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."}],"ddc":["004"],"tmp":{"image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"language":[{"iso":"eng"}],"publication":"Logical Methods in Computer Science","title":"Improved algorithms for parity and Streett objectives","date_updated":"2025-06-02T08:53:41Z","oa":1,"pubrep_id":"956","issue":"3","article_processing_charge":"No","has_accepted_license":"1","intvolume":"        13","scopus_import":"1","type":"journal_article","status":"public","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Monika H","full_name":"Henzinger, Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530"},{"first_name":"Veronika","full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer"}],"arxiv":1,"day":"26","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_updated":"2020-07-14T12:46:32Z","date_created":"2018-12-12T10:13:27Z","file_name":"IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf","file_id":"5010","checksum":"12d469ae69b80361333d7dead965cf5d","content_type":"application/pdf","access_level":"open_access","file_size":582940,"relation":"main_file","creator":"system"}],"publication_identifier":{"issn":["1860-5974"]},"month":"09"},{"publisher":"International Federation of Computational Logic","date_published":"2017-09-13T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","volume":13,"project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"}],"ddc":["004"],"tmp":{"image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"abstract":[{"lang":"eng","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. "}],"publication_status":"published","doi":"10.23638/LMCS-13(3:23)2017","file_date_updated":"2020-07-14T12:46:33Z","_id":"465","ec_funded":1,"related_material":{"record":[{"id":"1610","relation":"earlier_version","status":"public"},{"status":"public","id":"5438","relation":"earlier_version"}]},"year":"2017","citation":{"short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","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>","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 of 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 of 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).","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 of 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>.","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 of 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>"},"date_created":"2018-12-11T11:46:37Z","publist_id":"7356","status":"public","type":"journal_article","publication_identifier":{"issn":["18605974"]},"month":"09","oa_version":"Published Version","day":"13","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","file_size":279071,"content_type":"application/pdf","access_level":"open_access","creator":"system","date_created":"2018-12-12T10:14:37Z","date_updated":"2020-07-14T12:46:33Z","file_id":"5090","checksum":"08041379ba408d40664f449eb5907a8f","file_name":"IST-2015-321-v1+1_main.pdf"},{"checksum":"08041379ba408d40664f449eb5907a8f","file_id":"5091","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:14:38Z","creator":"system","access_level":"open_access","file_size":279071,"relation":"main_file","content_type":"application/pdf"}],"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"publication":"Logical Methods in Computer Science","language":[{"iso":"eng"}],"intvolume":"        13","scopus_import":1,"has_accepted_license":"1","date_updated":"2023-02-23T12:26:25Z","oa":1,"pubrep_id":"955","issue":"3","title":"Edit distance for pushdown automata"},{"oa":1,"pubrep_id":"957","date_updated":"2023-02-23T12:26:16Z","issue":"2","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","scopus_import":1,"intvolume":"        13","has_accepted_license":"1","language":[{"iso":"eng"}],"publication":"Logical Methods in Computer Science","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Křetínská, Zuzana","first_name":"Zuzana","last_name":"Křetínská"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"}],"publication_identifier":{"issn":["18605974"]},"month":"07","oa_version":"Published Version","day":"03","file":[{"checksum":"bfa405385ec6229ad5ead89ab5751639","file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf","file_id":"5354","date_created":"2018-12-12T10:18:32Z","date_updated":"2020-07-14T12:46:33Z","creator":"system","relation":"main_file","file_size":511832,"content_type":"application/pdf","access_level":"open_access"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","status":"public","year":"2017","date_created":"2018-12-11T11:46:38Z","publist_id":"7355","citation":{"short":"K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017).","ama":"Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. 2017;13(2). doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>","ieee":"K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2. International Federation of Computational Logic, 2017.","chicago":"Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>.","ista":"Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15.","mla":"Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>.","apa":"Chatterjee, K., Křetínská, Z., &#38; Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>"},"ec_funded":1,"related_material":{"record":[{"status":"public","id":"1657","relation":"earlier_version"},{"id":"5429","relation":"earlier_version","status":"public"},{"id":"5435","relation":"earlier_version","status":"public"}]},"article_number":"15","file_date_updated":"2020-07-14T12:46:33Z","_id":"466","doi":"10.23638/LMCS-13(2:15)2017","publication_status":"published","ddc":["004"],"tmp":{"image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020)","call_identifier":"H2020","grant_number":"701309","_id":"2590DB08-B435-11E9-9278-68D0E5697425"}],"publisher":"International Federation of Computational Logic","date_published":"2017-07-03T00:00:00Z","department":[{"_id":"KrCh"}],"volume":13,"quality_controlled":"1"},{"year":"2017","date_created":"2018-12-11T11:46:38Z","publist_id":"7354","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 18(4), 31.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>"},"ec_funded":1,"article_number":"31","related_material":{"record":[{"status":"public","id":"1656","relation":"earlier_version"},{"relation":"earlier_version","id":"5415","status":"public"},{"id":"5436","relation":"earlier_version","status":"public"}]},"_id":"467","doi":"10.1145/3152769","publication_status":"published","external_id":{"arxiv":["1606.03598"]},"abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}],"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publisher":"ACM","date_published":"2017-12-01T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":18,"quality_controlled":"1","oa":1,"date_updated":"2023-02-23T12:26:19Z","issue":"4","title":"Nested weighted automata","scopus_import":1,"intvolume":"        18","language":[{"iso":"eng"}],"publication":"ACM Transactions on Computational Logic (TOCL)","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"arxiv":1,"publication_identifier":{"issn":["15293785"]},"month":"12","day":"01","main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}],"oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","status":"public"},{"date_published":"2017-03-06T00:00:00Z","publisher":"Nature Publishing Group","volume":7,"quality_controlled":"1","department":[{"_id":"KrCh"}],"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["004"],"abstract":[{"text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population. The fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure. Amplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade. In this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Cometswarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively. ","lang":"eng"}],"publication_status":"published","doi":"10.1038/s41598-017-00107-w","_id":"512","file_date_updated":"2020-07-14T12:46:36Z","related_material":{"record":[{"id":"5449","relation":"earlier_version","status":"public"}]},"article_number":"82","ec_funded":1,"year":"2017","date_created":"2018-12-11T11:46:53Z","publist_id":"7307","citation":{"apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2017). Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 7(1), 82.","mla":"Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>, vol. 7, no. 1, 82, Nature Publishing Group, 2017, doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification on undirected population structures: Comets beat stars,” <i>Scientific Reports</i>, vol. 7, no. 1. Nature Publishing Group, 2017.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. 2017;7(1). doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports 7 (2017)."},"status":"public","type":"journal_article","month":"03","publication_identifier":{"issn":["20452322"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","relation":"main_file","file_size":1536783,"content_type":"application/pdf","access_level":"open_access","checksum":"7d05cbdd914e194a019c0f91fb64e9a8","file_id":"5357","file_name":"IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf","date_created":"2018-12-12T10:18:35Z","date_updated":"2020-07-14T12:46:36Z"}],"oa_version":"Published Version","day":"06","author":[{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"publication":"Scientific Reports","language":[{"iso":"eng"}],"has_accepted_license":"1","intvolume":"         7","scopus_import":1,"article_processing_charge":"No","issue":"1","date_updated":"2023-02-23T12:26:57Z","pubrep_id":"938","oa":1,"title":"Amplification on undirected population structures: Comets beat stars"},{"abstract":[{"lang":"eng","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."}],"publication_status":"published","publisher":"ACM","date_published":"2016-02-27T00:00:00Z","department":[{"_id":"KrCh"}],"page":"365 - 368","volume":26,"quality_controlled":"1","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"ec_funded":1,"acknowledgement":"ERC Start Grant Graph Games 279307 supported this  research. ","year":"2016","date_created":"2018-12-11T11:50:55Z","citation":{"short":"V. Pandey, K. Chatterjee, in:, Proceedings of the ACM Conference on Computer Supported Cooperative Work, ACM, 2016, pp. 365–368.","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.","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>","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.","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>.","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>.","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>"},"publist_id":"6083","doi":"10.1145/2818052.2869122","_id":"1245","conference":{"location":"San Francisco, CA, USA","end_date":"2016-03-02","name":"CSCW: Computer Supported Cooperative Work and Social Computing","start_date":"2016-02-26"},"month":"02","day":"27","oa_version":"None","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Pandey","first_name":"Vineet","full_name":"Pandey, Vineet"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"type":"conference","status":"public","intvolume":"        26","scopus_import":1,"date_updated":"2021-01-12T06:49:22Z","issue":"Februar-2016","title":"Game-theoretic models identify useful principles for peer collaboration in online learning platforms","publication":"Proceedings of the ACM Conference on Computer Supported Cooperative Work","language":[{"iso":"eng"}]},{"title":"Asymmetric power boosts extortion in an economic experiment","oa":1,"pubrep_id":"716","date_updated":"2023-02-23T14:11:27Z","issue":"10","has_accepted_license":"1","scopus_import":1,"intvolume":"        11","language":[{"iso":"eng"}],"publication":"PLoS One","author":[{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe","orcid":"0000-0001-5116-955X","first_name":"Christian","full_name":"Hilbe, Christian"},{"first_name":"Kristin","full_name":"Hagel, Kristin","last_name":"Hagel"},{"full_name":"Milinski, Manfred","first_name":"Manfred","last_name":"Milinski"}],"day":"04","oa_version":"Published Version","file":[{"date_created":"2018-12-12T10:08:08Z","date_updated":"2020-07-14T12:44:44Z","file_id":"4668","checksum":"6b33e394003dfe8b4ca6be1858aaa8e3","file_name":"IST-2016-716-v1+1_journal.pone.0163867.PDF","relation":"main_file","file_size":2077905,"content_type":"application/pdf","access_level":"open_access","creator":"system"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"10","type":"journal_article","status":"public","date_created":"2018-12-11T11:51:22Z","publist_id":"5948","citation":{"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>","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>.","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>.","ista":"Hilbe C, Hagel K, Milinski M. 2016. Asymmetric power boosts extortion in an economic experiment. PLoS One. 11(10), e0163867.","short":"C. Hilbe, K. Hagel, M. Milinski, PLoS One 11 (2016).","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.","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>"},"acknowledgement":"CH was funded by the Schrödinger program of the Austrian Science Fund (FWF) J3475. ","year":"2016","related_material":{"record":[{"status":"public","relation":"research_data","id":"9867"},{"id":"9868","relation":"research_data","status":"public"}]},"article_number":"e0163867","file_date_updated":"2020-07-14T12:44:44Z","_id":"1322","doi":"10.1371/journal.pone.0163867","publication_status":"published","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."}],"ddc":["004","006"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":11,"publisher":"Public Library of Science","date_published":"2016-10-04T00:00:00Z"},{"date_updated":"2021-01-12T06:49:53Z","year":"2016","citation":{"ista":"Chatterjee K, Chmelik M. 2016. Indefinite-horizon reachability in Goal-DEC-POMDPs. Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 2016–January, 88–96.","chicago":"Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” In <i>Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling</i>, 2016–January:88–96. AAAI Press, 2016.","mla":"Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” <i>Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling</i>, vol. 2016–January, AAAI Press, 2016, pp. 88–96.","ama":"Chatterjee K, Chmelik M. Indefinite-horizon reachability in Goal-DEC-POMDPs. In: <i>Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling</i>. Vol 2016-January. AAAI Press; 2016: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 International Conference on Automated Planning and Scheduling</i>, London, United Kingdom, 2016, vol. 2016–January, pp. 88–96.","short":"K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, AAAI Press, 2016, pp. 88–96.","apa":"Chatterjee, K., &#38; Chmelik, M. (2016). Indefinite-horizon reachability in Goal-DEC-POMDPs. In <i>Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling</i> (Vol. 2016–January, pp. 88–96). London, United Kingdom: AAAI Press."},"title":"Indefinite-horizon reachability in Goal-DEC-POMDPs","date_created":"2018-12-11T11:51:22Z","publist_id":"5946","ec_funded":1,"scopus_import":1,"_id":"1324","language":[{"iso":"eng"}],"publication":"Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin"}],"publication_status":"published","conference":{"end_date":"2016-06-17","location":"London, United Kingdom","start_date":"2016-06-12","name":"ICAPS: International Conference on Automated Planning and Scheduling"},"month":"01","day":"01","main_file_link":[{"url":"http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/12999"}],"oa_version":"None","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","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 "}],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"publisher":"AAAI Press","status":"public","date_published":"2016-01-01T00:00:00Z","type":"conference","department":[{"_id":"KrCh"}],"page":"88 - 96","volume":"2016-January","quality_controlled":"1"},{"date_created":"2018-12-11T11:51:23Z","citation":{"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>","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.","short":"T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","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>.","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>"},"publist_id":"5944","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]","year":"2016","ec_funded":1,"article_number":"10","file_date_updated":"2020-07-14T12:44:44Z","_id":"1325","doi":"10.4230/LIPIcs.CONCUR.2016.10","publication_status":"published","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"}],"ddc":["004"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"project":[{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"KrCh"}],"volume":59,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2016-08-01T00:00:00Z","title":"Stability in graphs and games","date_updated":"2021-01-12T06:49:53Z","pubrep_id":"665","oa":1,"intvolume":"        59","has_accepted_license":"1","scopus_import":1,"language":[{"iso":"eng"}],"author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","full_name":"Novotny, Petr","first_name":"Petr"}],"day":"01","oa_version":"Published Version","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"file_size":553648,"access_level":"open_access","content_type":"application/pdf","relation":"main_file","creator":"system","date_updated":"2020-07-14T12:44:44Z","date_created":"2018-12-12T10:16:40Z","checksum":"3c2dc6ab0358f8aa8f7aa7d6c1293159","file_id":"5229","file_name":"IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf"}],"conference":{"name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","location":"Quebec City, Canada","end_date":"2016-08-26"},"month":"08","alternative_title":["LIPIcs"],"type":"conference","status":"public"},{"doi":"10.1007/978-3-319-46520-3_3","_id":"1326","ec_funded":1,"publist_id":"5943","citation":{"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>.","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>.","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.","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>","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.","short":"T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.","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>"},"date_created":"2018-12-11T11:51:23Z","year":"2016","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].","quality_controlled":"1","volume":9938,"department":[{"_id":"KrCh"}],"page":"32 - 49","date_published":"2016-09-22T00:00:00Z","publisher":"Springer","project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"abstract":[{"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. ","lang":"eng"}],"publication_status":"published","language":[{"iso":"eng"}],"scopus_import":1,"intvolume":"      9938","title":"Optimizing the expected mean payoff in Energy Markov Decision Processes","oa":1,"date_updated":"2021-01-12T06:49:53Z","status":"public","type":"conference","alternative_title":["LNCS"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1607.00678"}],"oa_version":"Preprint","day":"22","month":"09","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2016-10-17","location":"Chiba, Japan","end_date":"2016-10-20"},"author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"full_name":"Kučera, Antonín","first_name":"Antonín","last_name":"Kučera"},{"full_name":"Novotny, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny"}]},{"title":"Stochastic shortest path with energy constraints in POMDPs","date_created":"2018-12-11T11:51:23Z","publist_id":"5942","citation":{"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.","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.","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.","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.","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.","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."},"year":"2016","date_updated":"2021-01-12T06:49:54Z","oa":1,"scopus_import":1,"ec_funded":1,"_id":"1327","language":[{"iso":"eng"}],"publication":"Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems","author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik"},{"first_name":"Anchit","full_name":"Gupta, Anchit","last_name":"Gupta"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr"}],"publication_status":"published","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"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. ","lang":"eng"}],"day":"01","oa_version":"Preprint","main_file_link":[{"url":"https://arxiv.org/abs/1602.07565","open_access":"1"}],"month":"01","conference":{"name":"AAMAS: Autonomous Agents & Multiagent Systems","start_date":"2016-05-09","location":"Singapore","end_date":"2016-05-13"},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"1465 - 1466","status":"public","type":"conference","date_published":"2016-01-01T00:00:00Z","publisher":"ACM"},{"status":"public","type":"journal_article","month":"03","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","file_size":1432577,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_name":"IST-2016-661-v1+1_ncomms10915.pdf","checksum":"9ea0d7ce59a555a1cb8353d5559407cb","file_id":"4834","date_created":"2018-12-12T10:10:44Z","date_updated":"2020-07-14T12:44:44Z"}],"oa_version":"Published Version","day":"07","author":[{"first_name":"Manfred","full_name":"Milinski, Manfred","last_name":"Milinski"},{"orcid":"0000-0001-5116-955X","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian","first_name":"Christian"},{"full_name":"Semmann, Dirk","first_name":"Dirk","last_name":"Semmann"},{"last_name":"Sommerfeld","full_name":"Sommerfeld, Ralf","first_name":"Ralf"},{"last_name":"Marotzke","first_name":"Jochem","full_name":"Marotzke, Jochem"}],"publication":"Nature Communications","language":[{"iso":"eng"}],"scopus_import":1,"has_accepted_license":"1","intvolume":"         7","pubrep_id":"661","oa":1,"date_updated":"2021-01-12T06:49:57Z","title":"Humans choose representatives who enforce cooperation in social dilemmas through extortion","date_published":"2016-03-07T00:00:00Z","publisher":"Nature Publishing Group","volume":7,"quality_controlled":"1","department":[{"_id":"KrCh"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["519","530","599"],"abstract":[{"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.","lang":"eng"}],"publication_status":"published","doi":"10.1038/ncomms10915","_id":"1333","file_date_updated":"2020-07-14T12:44:44Z","article_number":"10915","year":"2016","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.","date_created":"2018-12-11T11:51:25Z","publist_id":"5935","citation":{"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>.","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>.","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.","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>","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.","short":"M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, J. Marotzke, Nature Communications 7 (2016).","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>"}}]