[{"has_accepted_license":"1","publication":"Nature Genetics","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"}],"oa_version":"Submitted Version","month":"03","language":[{"iso":"eng"}],"type":"journal_article","date_published":"2017-03-01T00:00:00Z","publication_identifier":{"issn":["10614036"]},"oa":1,"publist_id":"7092","file":[{"access_level":"open_access","relation":"main_file","creator":"dernst","file_id":"7050","file_size":908099,"checksum":"e442dc3b7420a36ec805e9bb45cc1a2e","date_created":"2019-11-19T08:13:50Z","file_name":"2017_NatureGenetics_Makohon.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:33Z"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","pmid":1,"_id":"653","issue":"3","author":[{"first_name":"Alvin","last_name":"Makohon Moore","full_name":"Makohon Moore, Alvin"},{"last_name":"Zhang","first_name":"Ming","full_name":"Zhang, Ming"},{"orcid":"0000-0002-0170-7353","full_name":"Reiter, Johannes","first_name":"Johannes","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Božić, Ivana","first_name":"Ivana","last_name":"Božić"},{"first_name":"Benjamin","last_name":"Allen","full_name":"Allen, Benjamin"},{"id":"1d4c0f4f-e8a3-11ec-a351-e36772758c45","full_name":"Kundu, Deepanjan","first_name":"Deepanjan","last_name":"Kundu"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Wong, Fay","first_name":"Fay","last_name":"Wong"},{"first_name":"Yuchen","last_name":"Jiao","full_name":"Jiao, Yuchen"},{"full_name":"Kohutek, Zachary","first_name":"Zachary","last_name":"Kohutek"},{"last_name":"Hong","first_name":"Jungeui","full_name":"Hong, Jungeui"},{"first_name":"Marc","last_name":"Attiyeh","full_name":"Attiyeh, Marc"},{"first_name":"Breanna","last_name":"Javier","full_name":"Javier, Breanna"},{"full_name":"Wood, Laura","last_name":"Wood","first_name":"Laura"},{"full_name":"Hruban, Ralph","first_name":"Ralph","last_name":"Hruban"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"},{"last_name":"Papadopoulos","first_name":"Nickolas","full_name":"Papadopoulos, Nickolas"},{"last_name":"Kinzler","first_name":"Kenneth","full_name":"Kinzler, Kenneth"},{"full_name":"Vogelstein, Bert","last_name":"Vogelstein","first_name":"Bert"},{"full_name":"Iacobuzio Donahue, Christine","last_name":"Iacobuzio Donahue","first_name":"Christine"}],"article_processing_charge":"No","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:47:43Z","publication_status":"published","intvolume":"        49","title":"Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer","quality_controlled":"1","ec_funded":1,"page":"358 - 366","file_date_updated":"2020-07-14T12:47:33Z","publisher":"Nature Publishing Group","article_type":"original","citation":{"ista":"Makohon Moore A, Zhang M, Reiter J, Božić I, Allen B, Kundu D, Chatterjee K, Wong F, Jiao Y, Kohutek Z, Hong J, Attiyeh M, Javier B, Wood L, Hruban R, Nowak M, Papadopoulos N, Kinzler K, Vogelstein B, Iacobuzio Donahue C. 2017. Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer. Nature Genetics. 49(3), 358–366.","short":"A. Makohon Moore, M. Zhang, J. Reiter, I. Božić, B. Allen, D. Kundu, K. Chatterjee, F. Wong, Y. Jiao, Z. Kohutek, J. Hong, M. Attiyeh, B. Javier, L. Wood, R. Hruban, M. Nowak, N. Papadopoulos, K. Kinzler, B. Vogelstein, C. Iacobuzio Donahue, Nature Genetics 49 (2017) 358–366.","mla":"Makohon Moore, Alvin, et al. “Limited Heterogeneity of Known Driver Gene Mutations among the Metastases of Individual Patients with Pancreatic Cancer.” <i>Nature Genetics</i>, vol. 49, no. 3, Nature Publishing Group, 2017, pp. 358–66, doi:<a href=\"https://doi.org/10.1038/ng.3764\">10.1038/ng.3764</a>.","ieee":"A. Makohon Moore <i>et al.</i>, “Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer,” <i>Nature Genetics</i>, vol. 49, no. 3. Nature Publishing Group, pp. 358–366, 2017.","chicago":"Makohon Moore, Alvin, Ming Zhang, Johannes Reiter, Ivana Božić, Benjamin Allen, Deepanjan Kundu, Krishnendu Chatterjee, et al. “Limited Heterogeneity of Known Driver Gene Mutations among the Metastases of Individual Patients with Pancreatic Cancer.” <i>Nature Genetics</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/ng.3764\">https://doi.org/10.1038/ng.3764</a>.","ama":"Makohon Moore A, Zhang M, Reiter J, et al. Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer. <i>Nature Genetics</i>. 2017;49(3):358-366. doi:<a href=\"https://doi.org/10.1038/ng.3764\">10.1038/ng.3764</a>","apa":"Makohon Moore, A., Zhang, M., Reiter, J., Božić, I., Allen, B., Kundu, D., … Iacobuzio Donahue, C. (2017). Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer. <i>Nature Genetics</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/ng.3764\">https://doi.org/10.1038/ng.3764</a>"},"year":"2017","date_updated":"2022-06-10T09:55:08Z","external_id":{"pmid":["28092682"]},"day":"01","doi":"10.1038/ng.3764","abstract":[{"lang":"eng","text":"The extent of heterogeneity among driver gene mutations present in naturally occurring metastases - that is, treatment-naive metastatic disease - is largely unknown. To address this issue, we carried out 60× whole-genome sequencing of 26 metastases from four patients with pancreatic cancer. We found that identical mutations in known driver genes were present in every metastatic lesion for each patient studied. Passenger gene mutations, which do not have known or predicted functional consequences, accounted for all intratumoral heterogeneity. Even with respect to these passenger mutations, our analysis suggests that the genetic similarity among the founding cells of metastases was higher than that expected for any two cells randomly taken from a normal tissue. The uniformity of known driver gene mutations among metastases in the same patient has critical and encouraging implications for the success of future targeted therapies in advanced-stage disease."}],"acknowledgement":"We thank the Memorial Sloan Kettering Cancer Center Molecular Cytology core facility for immunohistochemistry staining. This work was supported by Office of Naval Research grant N00014-16-1-2914, the Bill and Melinda Gates Foundation (OPP1148627), and a gift from B. Wu and E. Larson (M.A.N.), National Institutes of Health grants CA179991 (C.A.I.-D. and I.B.), F31 CA180682 (A.P.M.-M.), CA43460 (B.V.), and P50 CA62924, the Monastra Foundation, the Virginia and D.K. Ludwig Fund for Cancer Research, the Lustgarten Foundation for Pancreatic Cancer Research, the Sol Goldman Center for Pancreatic Cancer Research, the Sol Goldman Sequencing Center, ERC Start grant 279307: Graph Games (J.G.R., D.K., and C.K.), Austrian Science Fund (FWF) grant P23499-N23 (J.G.R., D.K., and C.K.), and FWF NFN grant S11407-N23 RiSE/SHiNE (J.G.R., D.K., and C.K.).","volume":49,"ddc":["000"]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1701.05738"}],"oa":1,"publication_identifier":{"isbn":["9783662545768"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783662545775"]},"type":"conference","date_published":"2017-03-31T00:00:00Z","conference":{"location":"Uppsala, Sweden","end_date":"2017-04-29","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"language":[{"iso":"eng"}],"month":"03","oa_version":"Preprint","publication":"Tools and Algorithms for the Construction and Analysis of Systems","acknowledgement":"This work is partially funded by the DFG project “Verified Model Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.","volume":10205,"abstract":[{"text":"Transforming deterministic ω\r\n-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.","lang":"eng"}],"day":"31","doi":"10.1007/978-3-662-54577-5_26","arxiv":1,"external_id":{"arxiv":["1701.05738"]},"citation":{"chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 10205:443–60. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record for transforming Rabin automata into parity automata,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Uppsala, Sweden, 2017, vol. 10205, pp. 443–460.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record for transforming Rabin automata into parity automata. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 10205. Springer; 2017:443-460. doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 10205, pp. 443–460). Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance record for transforming Rabin automata into parity automata. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.","mla":"Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 10205, Springer, 2017, pp. 443–60, doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460."},"year":"2017","date_updated":"2023-06-21T13:29:46Z","publisher":"Springer","quality_controlled":"1","page":"443-460","intvolume":"     10205","alternative_title":["LNCS"],"title":"Index appearance record for transforming Rabin automata into parity automata","date_created":"2023-06-21T13:21:14Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"publication_status":"published","author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"},{"full_name":"Waldmann, Clara","first_name":"Clara","last_name":"Waldmann"},{"first_name":"Maximilian","last_name":"Weininger","full_name":"Weininger, Maximilian"}],"_id":"13160"},{"year":"2017","citation":{"ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23(2):230-253. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253."},"date_updated":"2023-09-20T09:43:09Z","external_id":{"isi":["000390637000014"],"arxiv":["1410.5387"]},"isi":1,"day":"01","arxiv":1,"doi":"10.1016/j.nahs.2016.04.006","abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study."}],"volume":23,"scopus_import":"1","_id":"1407","issue":"2","author":[{"last_name":"Svoreňová","first_name":"Mária","full_name":"Svoreňová, Mária"},{"first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ivana","last_name":"Cěrná","full_name":"Cěrná, Ivana"},{"last_name":"Belta","first_name":"Cǎlin","full_name":"Belta, Cǎlin"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2018-12-11T11:51:50Z","publication_status":"published","intvolume":"        23","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","ec_funded":1,"quality_controlled":"1","page":"230 - 253","publisher":"Elsevier","type":"journal_article","date_published":"2017-02-01T00:00:00Z","oa":1,"publist_id":"5800","main_file_link":[{"url":"http://arxiv.org/abs/1410.5387","open_access":"1"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","related_material":{"record":[{"status":"public","id":"1689","relation":"earlier_version"}]},"publication":"Nonlinear Analysis: Hybrid Systems","project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"}],"oa_version":"Preprint","month":"02","language":[{"iso":"eng"}]},{"ddc":["005"],"volume":10482,"abstract":[{"lang":"eng","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."}],"day":"01","doi":"10.1007/978-3-319-68167-2_4","external_id":{"isi":["000723567800004"]},"isi":1,"year":"2017","citation":{"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>","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>","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>.","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.","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>.","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."},"date_updated":"2024-03-25T23:30:19Z","editor":[{"first_name":"Deepak","last_name":"D'Souza","full_name":"D'Souza, Deepak"}],"publisher":"Springer","file_date_updated":"2020-07-14T12:48:16Z","ec_funded":1,"quality_controlled":"1","page":"59 - 66","intvolume":"     10482","alternative_title":["LNCS"],"title":"JTDec: A tool for tree decompositions in soot","pubrep_id":"845","date_created":"2018-12-11T11:49:22Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","publication_status":"published","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Amir","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","_id":"949","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","file":[{"access_level":"open_access","relation":"main_file","creator":"system","file_id":"4835","file_size":948514,"checksum":"a0d9f5f94dc594c4e71e78525c9942f1","date_created":"2018-12-12T10:10:45Z","content_type":"application/pdf","file_name":"IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf","date_updated":"2020-07-14T12:48:16Z"}],"oa":1,"publist_id":"6468","publication_identifier":{"issn":["03029743"]},"type":"conference","date_published":"2017-01-01T00:00:00Z","conference":{"start_date":"2017-10-03","name":"ATVA: Automated Technology for Verification and Analysis","location":"Pune, India","end_date":"2017-10-06"},"language":[{"iso":"eng"}],"month":"01","project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"oa_version":"Submitted Version","has_accepted_license":"1"},{"doi":"10.4230/LIPIcs.CONCUR.2017.21","arxiv":1,"day":"01","abstract":[{"lang":"eng","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"}],"date_updated":"2023-08-29T07:02:13Z","citation":{"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>","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>","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>.","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.","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>.","short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17."},"year":"2017","external_id":{"arxiv":["1705.01433"]},"volume":85,"ddc":["000"],"publication_status":"published","date_created":"2018-12-11T11:49:22Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"alternative_title":["LIPIcs"],"pubrep_id":"844","title":"Infinite-duration bidding games","intvolume":"        85","_id":"950","scopus_import":1,"author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Chonev, Ventsislav K","last_name":"Chonev","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","file_date_updated":"2020-07-14T12:48:16Z","publication_identifier":{"issn":["1868-8969"]},"oa":1,"publist_id":"6466","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2017-09-01T00:00:00Z","type":"conference","file":[{"access_level":"open_access","relation":"main_file","file_id":"5318","creator":"system","date_created":"2018-12-12T10:18:00Z","checksum":"6d5cccf755207b91ccbef95d8275b013","file_size":335170,"date_updated":"2020-07-14T12:48:16Z","file_name":"IST-2017-844-v1+1_concur-cr.pdf","content_type":"application/pdf"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"6752","relation":"later_version","status":"public"}]},"oa_version":"Published Version","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"month":"09","article_number":"17","has_accepted_license":"1","conference":{"start_date":"2017-09-05","name":"CONCUR: Concurrency Theory","end_date":"2017-09-07","location":"Berlin, Germany"},"language":[{"iso":"eng"}]},{"main_file_link":[{"url":"http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092","open_access":"1"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","oa":1,"publist_id":"6387","type":"conference","date_published":"2017-01-01T00:00:00Z","conference":{"start_date":"2017-02-04","name":"AAAI: Conference on Artificial Intelligence","end_date":"2017-02-10","location":"San Francisco, CA, United States"},"language":[{"iso":"eng"}],"project":[{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"oa_version":"Submitted Version","month":"01","publication":"Proceedings of the 31st AAAI Conference on Artificial Intelligence","volume":5,"acknowledgement":"he research leading to these results was supported by the Austrian Science Fund (FWF) NFN Grant no. S11407-N23 (RiSE/SHiNE); two ERC Starting grants (279307: Graph Games, 279499: inVEST); the Vienna Science and Tech- nology Fund (WWTF) through project ICT15-003; and the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. [291734].","day":"01","abstract":[{"text":"A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the “expectation” and “threshold” approaches and consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we are given a threshold t and the objective is to find a policy σ such that a) each possible outcome of σ yields a discounted-sum payoff of at least t, and b) the expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks.","lang":"eng"}],"citation":{"ista":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. 2017. Optimizing expectation with guarantees in POMDPs. Proceedings of the 31st AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 5, 3725–3732.","mla":"Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.” <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, vol. 5, AAAI Press, 2017, pp. 3725–32.","short":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, D. Zikelic, in:, Proceedings of the 31st AAAI Conference on Artificial Intelligence, AAAI Press, 2017, pp. 3725–3732.","chicago":"Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, 5:3725–32. AAAI Press, 2017.","ieee":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing expectation with guarantees in POMDPs,” in <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, San Francisco, CA, United States, 2017, vol. 5, pp. 3725–3732.","apa":"Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., &#38; Zikelic, D. (2017). Optimizing expectation with guarantees in POMDPs. In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i> (Vol. 5, pp. 3725–3732). San Francisco, CA, United States: AAAI Press.","ama":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation with guarantees in POMDPs. In: <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>. Vol 5. AAAI Press; 2017:3725-3732."},"year":"2017","date_updated":"2025-06-02T08:53:49Z","external_id":{"isi":["000485630703107"]},"isi":1,"publisher":"AAAI Press","ec_funded":1,"quality_controlled":"1","page":"3725 - 3732","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:49:40Z","article_processing_charge":"No","publication_status":"published","intvolume":"         5","title":"Optimizing expectation with guarantees in POMDPs","scopus_import":"1","_id":"1009","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Petr","last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pérez","first_name":"Guillermo","full_name":"Pérez, Guillermo"},{"full_name":"Raskin, Jean","last_name":"Raskin","first_name":"Jean"},{"first_name":"Djordje","last_name":"Zikelic","full_name":"Zikelic, Djordje"}]},{"project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa_version":"Submitted Version","month":"03","language":[{"iso":"eng"}],"conference":{"start_date":"2017-04-22","name":"ESOP: European Symposium on Programming","end_date":"2017-04-29","location":"Uppsala, Sweden"},"type":"conference","date_published":"2017-03-19T00:00:00Z","publication_identifier":{"issn":["03029743"]},"oa":1,"publist_id":"6384","main_file_link":[{"url":"https://arxiv.org/abs/1701.04914","open_access":"1"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","scopus_import":"1","_id":"1011","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mishra, Samarth","first_name":"Samarth","last_name":"Mishra"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-11T11:49:41Z","article_processing_charge":"No","publication_status":"published","intvolume":"     10201","title":"Faster algorithms for weighted recursive state machines","alternative_title":["LNCS"],"ec_funded":1,"quality_controlled":"1","page":"287 - 313","editor":[{"first_name":"Hongseok","last_name":"Yang","full_name":"Yang, Hongseok"}],"publisher":"Springer","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Weighted Recursive State Machines</i>. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>.","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","apa":"Chatterjee, K., Kragl, B., Mishra, S., &#38; Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>","ieee":"K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms for weighted recursive state machines,” presented at the ESOP: European Symposium on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.","chicago":"Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis. “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok Yang, 10201:287–313. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>."},"year":"2017","date_updated":"2023-09-22T09:44:50Z","external_id":{"isi":["000681702400011"]},"isi":1,"day":"19","doi":"10.1007/978-3-662-54434-1_11","abstract":[{"text":"Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.","lang":"eng"}],"volume":10201},{"oa":1,"publication_identifier":{"eissn":["2475-1421"]},"date_published":"2017-12-27T00:00:00Z","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","related_material":{"record":[{"relation":"earlier_version","id":"5455","status":"public"}]},"status":"public","file":[{"file_name":"2017_ACMProgLang_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2021-12-07T08:06:28Z","checksum":"faa3f7b3fe8aab84b50ed805c26a0ee5","file_size":460188,"date_created":"2021-12-07T08:06:28Z","creator":"cchlebak","file_id":"10421","relation":"main_file","success":1,"access_level":"open_access"}],"month":"12","article_number":"30","oa_version":"Published Version","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"publication":"Proceedings of the ACM on Programming Languages","has_accepted_license":"1","conference":{"name":"POPL: Programming Languages","start_date":"2018-01-07","end_date":"2018-01-13","location":"Los Angeles, CA, United States"},"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graph where the edges are labeled with different types of opening and closing parentheses, and the reachability information is computed via paths whose parentheses are properly matched. We present new results for Dyck reachability problems with applications to alias analysis and data-dependence analysis. Our main contributions, that include improved upper bounds as well as lower bounds that establish optimality guarantees, are as follows: First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph with n nodes and m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)), where α(n) is the inverse Ackermann function, improving the previously known O(n2) time bound; (ii) a matching lower bound that shows that our algorithm is optimal wrt to worst-case complexity; and (iii) an optimal average-case upper bound of O(m) time, improving the previously known O(m · logn) bound. Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtain analysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is only linear, and only wrt the number of call sites. Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean Matrix Multiplication, which is a long-standing open problem. Thus we establish that the existing combinatorial algorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the same hardness holds for graphs of constant treewidth. Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependence analysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform all existing methods on the two problems, over real-world benchmarks."}],"doi":"10.1145/3158118","arxiv":1,"day":"27","external_id":{"arxiv":["1910.00241"]},"date_updated":"2023-02-23T12:27:13Z","year":"2017","citation":{"apa":"Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and Alias analysis. <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/3158118\">https://doi.org/10.1145/3158118</a>","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence and Alias analysis. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158118\">10.1145/3158118</a>","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability for data-dependence and Alias analysis,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158118\">https://doi.org/10.1145/3158118</a>.","mla":"Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 30, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158118\">10.1145/3158118</a>.","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 2 (2017).","ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. 2(POPL), 30."},"ddc":["000"],"volume":2,"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant (279307: Graph Games).\r\n","title":"Optimal Dyck reachability for data-dependence and Alias analysis","intvolume":"         2","publication_status":"published","date_created":"2021-12-05T23:01:48Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Choudhary, Bhavya","last_name":"Choudhary","first_name":"Bhavya"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas"}],"issue":"POPL","_id":"10416","scopus_import":"1","article_type":"original","publisher":"Association for Computing Machinery","file_date_updated":"2021-12-07T08:06:28Z","ec_funded":1,"quality_controlled":"1"},{"publication_status":"published","date_created":"2021-12-05T23:01:49Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","title":"Data-centric dynamic partial order reduction","intvolume":"         2","_id":"10417","scopus_import":"1","author":[{"first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Sinha","first_name":"Nishant","full_name":"Sinha, Nishant"},{"full_name":"Vaidya, Kapil","last_name":"Vaidya","first_name":"Kapil"}],"issue":"POPL","publisher":"Association for Computing Machinery","article_type":"original","ec_funded":1,"quality_controlled":"1","doi":"10.1145/3158119","arxiv":1,"day":"27","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."}],"date_updated":"2023-02-23T12:27:16Z","year":"2017","citation":{"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.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings of the ACM on Programming Languages 2 (2017).","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>.","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>.","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.","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>","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>"},"external_id":{"arxiv":["1610.01188"]},"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.","volume":2,"oa_version":"Published Version","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"month":"12","article_number":"31","publication":"Proceedings of the ACM on Programming Languages","conference":{"location":"Los Angeles, CA, United States","end_date":"2018-01-13","start_date":"2018-01-07","name":"POPL: Programming Languages"},"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["2475-1421"]},"oa":1,"date_published":"2017-12-27T00:00:00Z","type":"journal_article","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158119","open_access":"1"}],"related_material":{"record":[{"relation":"earlier_version","id":"5448","status":"public"},{"status":"public","relation":"earlier_version","id":"5456"}]},"status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9"},{"language":[{"iso":"eng"}],"conference":{"name":"POPL: Programming Languages","start_date":"2018-01-07","end_date":"2018-01-13","location":"Los Angeles, CA, United States"},"publication":"Proceedings of the ACM on Programming Languages","month":"12","article_number":"33","oa_version":"Published Version","status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158121","open_access":"1"}],"date_published":"2017-12-07T00:00:00Z","type":"journal_article","oa":1,"publication_identifier":{"eissn":["2475-1421"]},"quality_controlled":"1","article_type":"original","publisher":"Association for Computing Machinery","author":[{"last_name":"Mciver","first_name":"Annabelle","full_name":"Mciver, Annabelle"},{"first_name":"Carroll","last_name":"Morgan","full_name":"Morgan, Carroll"},{"full_name":"Kaminski, Benjamin Lucien","first_name":"Benjamin Lucien","last_name":"Kaminski"},{"full_name":"Katoen, Joost P","last_name":"Katoen","first_name":"Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87"}],"issue":"POPL","_id":"10418","scopus_import":"1","title":"A new proof rule for almost-sure termination","intvolume":"         2","publication_status":"published","article_processing_charge":"No","date_created":"2021-12-05T23:01:49Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"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.","volume":2,"external_id":{"arxiv":["1711.03588"]},"date_updated":"2021-12-07T08:04:14Z","citation":{"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>","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>","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>.","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.","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","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>.","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."},"year":"2017","abstract":[{"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.","lang":"eng"}],"arxiv":1,"doi":"10.1145/3158121","day":"07"},{"date_published":"2017-06-01T00:00:00Z","type":"journal_article","oa":1,"publist_id":"6323","publication_identifier":{"issn":["00200190"]},"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"file_id":"4998","creator":"system","access_level":"open_access","relation":"main_file","date_updated":"2019-10-15T07:44:51Z","file_name":"IST-2018-991-v1+2_2018_Chatterjee_Pushdown_PREPRINT.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:13:17Z","file_size":247657}],"publication":"Information Processing Letters","has_accepted_license":"1","month":"06","oa_version":"Submitted Version","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"isi":1,"external_id":{"isi":["000399506600005"]},"date_updated":"2023-09-20T12:08:18Z","citation":{"ieee":"K. Chatterjee and G. F. Osang, “Pushdown reachability with constant treewidth,” <i>Information Processing Letters</i>, vol. 122. Elsevier, pp. 25–29, 2017.","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>.","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>","ista":"Chatterjee K, Osang GF. 2017. Pushdown reachability with constant treewidth. Information Processing Letters. 122, 25–29.","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>."},"year":"2017","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"}],"doi":"10.1016/j.ipl.2017.02.003","day":"01","ddc":["000"],"volume":122,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"464B40D6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8882-5116","full_name":"Osang, Georg F","first_name":"Georg F","last_name":"Osang"}],"_id":"1065","scopus_import":"1","title":"Pushdown reachability with constant treewidth","pubrep_id":"991","intvolume":"       122","publication_status":"published","date_created":"2018-12-11T11:49:57Z","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"HeEd"}],"file_date_updated":"2019-10-15T07:44:51Z","page":"25 - 29","quality_controlled":"1","ec_funded":1,"publisher":"Elsevier"},{"publisher":"ACM","page":"145 - 160","quality_controlled":"1","ec_funded":1,"title":"Stochastic invariants for probabilistic termination","alternative_title":["ACM SIGPLAN Notices"],"intvolume":"        52","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:50:39Z","article_processing_charge":"No","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zikelic, Djordje","last_name":"Zikelic","first_name":"Djordje"}],"issue":"1","_id":"1194","scopus_import":"1","volume":52,"abstract":[{"lang":"eng","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. "}],"doi":"10.1145/3009837.3009873","day":"01","isi":1,"external_id":{"isi":["000408311200013"]},"date_updated":"2025-07-14T09:09:58Z","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>","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>","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.","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>.","short":"K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.","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."},"year":"2017","conference":{"name":"POPL: Principles of Programming Languages","start_date":"2017-01-15","end_date":"2017-01-21","location":"Paris, France"},"language":[{"iso":"eng"}],"month":"01","oa_version":"Submitted Version","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"status":"public","id":"14539","relation":"dissertation_contains"}]},"status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1611.01063"}],"oa":1,"publist_id":"6157","publication_identifier":{"issn":["07308566"]},"date_published":"2017-01-01T00:00:00Z","type":"conference"},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","related_material":{"record":[{"status":"public","id":"2305","relation":"earlier_version"}]},"file":[{"date_updated":"2020-07-14T12:44:42Z","file_name":"IST-2016-717-v1+1_1-s2.0-S0022000016300897-main.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:11:30Z","checksum":"91271b23cf884d7c06d33bef0cd623b1","file_size":708657,"file_id":"4885","creator":"system","relation":"main_file","access_level":"open_access"}],"oa":1,"publist_id":"6009","type":"journal_article","date_published":"2017-03-01T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"language":[{"iso":"eng"}],"month":"03","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"Journal of Computer and System Sciences","ddc":["004","006"],"volume":84,"abstract":[{"text":"We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints.","lang":"eng"}],"day":"01","doi":"10.1016/j.jcss.2016.09.009","external_id":{"isi":["000388430000011"]},"isi":1,"citation":{"apa":"Brázdil, T., Chatterjee, K., Forejt, V., &#38; Kučera, A. (2017). Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. 2017;84:144-170. doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>","ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance for stability in Markov decision processes,” <i>Journal of Computer and System Sciences</i>, vol. 84. Elsevier, pp. 144–170, 2017.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>.","mla":"Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>, vol. 84, Elsevier, 2017, pp. 144–70, doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>.","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and System Sciences 84 (2017) 144–170.","ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2017. Trading performance for stability in Markov decision processes. Journal of Computer and System Sciences. 84, 144–170."},"year":"2017","date_updated":"2023-09-20T11:15:31Z","publisher":"Elsevier","file_date_updated":"2020-07-14T12:44:42Z","ec_funded":1,"quality_controlled":"1","page":"144 - 170","intvolume":"        84","pubrep_id":"717","title":"Trading performance for stability in Markov decision processes","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:51:12Z","article_processing_charge":"No","publication_status":"published","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"full_name":"Kučera, Antonín","last_name":"Kučera","first_name":"Antonín"}],"scopus_import":"1","_id":"1294"},{"scopus_import":"1","license":"https://creativecommons.org/licenses/by/3.0/","_id":"1068","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Dvorák","first_name":"Wolfgang","full_name":"Dvorák, Wolfgang"},{"first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"}],"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:49:58Z","article_processing_charge":"No","publication_status":"published","intvolume":"        58","alternative_title":["LIPIcs"],"title":"Conditionally optimal algorithms for generalized Büchi Games","pubrep_id":"779","ec_funded":1,"quality_controlled":"1","file_date_updated":"2018-12-12T10:16:02Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2016","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Conditionally Optimal Algorithms for Generalized Büchi Games</i>. Vol. 58, 25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">10.4230/LIPIcs.MFCS.2016.25</a>.","short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2016. Conditionally optimal algorithms for generalized Büchi Games. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 58, 25.","apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., &#38; Loitzenbauer, V. (2016). Conditionally optimal algorithms for generalized Büchi Games (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">https://doi.org/10.4230/LIPIcs.MFCS.2016.25</a>","ama":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Conditionally optimal algorithms for generalized Büchi Games. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">10.4230/LIPIcs.MFCS.2016.25</a>","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika Loitzenbauer. “Conditionally Optimal Algorithms for Generalized Büchi Games,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">https://doi.org/10.4230/LIPIcs.MFCS.2016.25</a>.","ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Conditionally optimal algorithms for generalized Büchi Games,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow, Poland, 2016, vol. 58."},"date_updated":"2025-06-02T08:53:50Z","day":"01","doi":"10.4230/LIPIcs.MFCS.2016.25","abstract":[{"lang":"eng","text":"Games on graphs provide the appropriate framework to study several central problems in computer science, such as verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k*n^2), improving the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1 k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m &gt; n^{1.5}. "}],"acknowledgement":"K. C., M. H., and W. D. are partially supported by the Vienna Science and Technology Fund (WWTF) through project ICT15-003. K. C. is partially supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Start grant (279307","volume":58,"ddc":["000","004","006"],"has_accepted_license":"1","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"oa_version":"Published Version","article_number":"25","month":"08","language":[{"iso":"eng"}],"conference":{"start_date":"2016-08-22","name":"MFCS: Mathematical Foundations of Computer Science (SG)","end_date":"2016-08-26","location":"Krakow, Poland"},"tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","short":"CC BY (3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"type":"conference","date_published":"2016-08-01T00:00:00Z","oa":1,"publist_id":"6317","file":[{"access_level":"open_access","relation":"main_file","creator":"system","file_id":"5187","file_size":632786,"date_created":"2018-12-12T10:16:02Z","file_name":"IST-2017-779-v1+1_LIPIcs-MFCS-2016-25.pdf","content_type":"application/pdf","date_updated":"2018-12-12T10:16:02Z"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"volume":55,"acknowledgement":"Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307:  Graph Games), and ERC Advanced Grant (267989: QUAREM).","ddc":["004","006"],"year":"2016","citation":{"mla":"Chonev, Ventsislav K., et al. <i>On the Skolem Problem for Continuous Linear Dynamical Systems</i>. Vol. 55, 100, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">10.4230/LIPIcs.ICALP.2016.100</a>.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 100.","apa":"Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On the skolem problem for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata, Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">https://doi.org/10.4230/LIPIcs.ICALP.2016.100</a>","ama":"Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear dynamical systems. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">10.4230/LIPIcs.ICALP.2016.100</a>","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016, vol. 55.","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">https://doi.org/10.4230/LIPIcs.ICALP.2016.100</a>."},"date_updated":"2021-01-12T06:48:03Z","day":"01","doi":"10.4230/LIPIcs.ICALP.2016.100","abstract":[{"lang":"eng","text":"The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differen-\r\ntial equation has a zero in a given interval of real numbers. This is a fundamental reachability\r\nproblem for continuous linear dynamical systems, such as linear hybrid automata and continuous-\r\ntime Markov chains. Decidability of the problem is currently open – indeed decidability is open\r\neven for the sub-problem in which a zero is sought in a bounded interval. In this paper we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture, a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse the unbounded problem in terms of the\r\nfrequencies of the differential equation, that is, the imaginary parts of the characteristic roots.\r\nWe show that the unbounded problem can be reduced to the bounded problem if there is at most\r\none rationally linearly independent frequency, or if there are two rationally linearly independent\r\nfrequencies and all characteristic roots are simple. We complete the picture by showing that de-\r\ncidability of the unbounded problem in the case of two (or more) rationally linearly independent\r\nfrequencies would entail a major new effectiveness result in Diophantine approximation, namely\r\ncomputability of the Diophantine-approximation types of all real algebraic numbers."}],"quality_controlled":"1","ec_funded":1,"file_date_updated":"2018-12-12T10:16:26Z","publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","scopus_import":1,"_id":"1069","author":[{"id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","full_name":"Chonev, Ventsislav K","first_name":"Ventsislav K","last_name":"Chonev"},{"first_name":"Joël","last_name":"Ouaknine","full_name":"Ouaknine, Joël"},{"last_name":"Worrell","first_name":"James","full_name":"Worrell, James"}],"date_created":"2018-12-11T11:49:59Z","department":[{"_id":"KrCh"}],"publication_status":"published","intvolume":"        55","title":"On the skolem problem for continuous linear dynamical systems","alternative_title":["LIPIcs"],"pubrep_id":"778","file":[{"creator":"system","file_id":"5213","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf","date_updated":"2018-12-12T10:16:26Z","file_size":521415,"date_created":"2018-12-12T10:16:26Z"}],"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2016-08-01T00:00:00Z","oa":1,"publist_id":"6314","language":[{"iso":"eng"}],"conference":{"location":"Rome, Italy","end_date":"2016-07-15","start_date":"2016-07-12","name":"ICALP: Automata, Languages and Programming"},"has_accepted_license":"1","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa_version":"Published Version","article_number":"100","month":"08"},{"date_updated":"2021-01-12T06:48:03Z","citation":{"chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Computation Tree Logic for Synchronization Properties,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>.","ieee":"K. Chatterjee and L. Doyen, “Computation tree logic for synchronization properties,” presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016, vol. 55.","apa":"Chatterjee, K., &#38; Doyen, L. (2016). Computation tree logic for synchronization properties (Vol. 55). Presented at the ICALP: Automata, Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>","ama":"Chatterjee K, Doyen L. Computation tree logic for synchronization properties. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">10.4230/LIPIcs.ICALP.2016.98</a>","ista":"Chatterjee K, Doyen L. 2016. Computation tree logic for synchronization properties. ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 98.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Computation Tree Logic for Synchronization Properties</i>. Vol. 55, 98, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">10.4230/LIPIcs.ICALP.2016.98</a>.","short":"K. Chatterjee, L. Doyen, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016."},"year":"2016","abstract":[{"text":"We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking. ","lang":"eng"}],"doi":"10.4230/LIPIcs.ICALP.2016.98","day":"01","ddc":["005"],"volume":55,"acknowledgement":"This research was partially supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003, and European project Cassting (FP7-601148).\r\n\r\nWe thank Stefan Göller and anonymous reviewers for their insightful\r\ncomments and suggestions.\r\n","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"}],"_id":"1070","scopus_import":1,"pubrep_id":"812","title":"Computation tree logic for synchronization properties","alternative_title":["LIPIcs"],"intvolume":"        55","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:49:59Z","file_date_updated":"2018-12-12T10:08:52Z","quality_controlled":"1","ec_funded":1,"publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","date_published":"2016-01-01T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publist_id":"6313","status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","access_level":"open_access","file_id":"4714","creator":"system","date_created":"2018-12-12T10:08:52Z","file_size":546133,"date_updated":"2018-12-12T10:08:52Z","file_name":"IST-2017-812-v1+1_LIPIcs-ICALP-2016-98.pdf","content_type":"application/pdf"}],"has_accepted_license":"1","month":"01","article_number":"98","oa_version":"Published Version","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"language":[{"iso":"eng"}],"conference":{"location":"Rome, Italy","end_date":"2016-07-15","start_date":"2016-07-12","name":"ICALP: Automata, Languages and Programming"}},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2016-08-01T00:00:00Z","publist_id":"6312","oa":1,"file":[{"file_name":"IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf","content_type":"application/pdf","date_updated":"2018-12-12T10:14:31Z","file_size":579225,"date_created":"2018-12-12T10:14:31Z","creator":"system","file_id":"5084","access_level":"open_access","relation":"main_file"}],"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"821"}]},"has_accepted_license":"1","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"oa_version":"Published Version","article_number":"28","month":"08","language":[{"iso":"eng"}],"conference":{"location":"Aarhus, Denmark","end_date":"2016-08-24","name":"ESA: European Symposium on Algorithms","start_date":"2016-08-22"},"year":"2016","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2016. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. ESA: European Symposium on Algorithms, LIPIcs, vol. 57, 28.","mla":"Chatterjee, Krishnendu, et al. <i>Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs</i>. Vol. 57, 28, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs,” presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark, 2016, vol. 57.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs,” Vol. 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2016). Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs (Vol. 57). Presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. In: Vol 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>"},"date_updated":"2023-09-07T12:01:58Z","day":"01","doi":"10.4230/LIPIcs.ESA.2016.28","abstract":[{"text":"We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity. ","lang":"eng"}],"volume":57,"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE) and ERC Start grant (279307: Graph Games).","ddc":["004","006"],"scopus_import":1,"_id":"1071","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:49:59Z","publication_status":"published","intvolume":"        57","title":"Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs","alternative_title":["LIPIcs"],"pubrep_id":"777","quality_controlled":"1","ec_funded":1,"file_date_updated":"2018-12-12T10:14:31Z","publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik"},{"_id":"1090","scopus_import":1,"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-11T11:50:05Z","title":"Nested weighted limit-average automata of bounded width","pubrep_id":"795","alternative_title":["LIPIcs"],"intvolume":"        58","quality_controlled":"1","ec_funded":1,"file_date_updated":"2018-12-12T10:17:31Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2021-01-12T06:48:12Z","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Limit-Average Automata of Bounded Width</i>. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 58, 24.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average automata of bounded width,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland, 2016, vol. 58.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>."},"year":"2016","doi":"10.4230/LIPIcs.MFCS.2016.24","day":"01","abstract":[{"lang":"eng","text":" While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness."}],"volume":58,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under grant 2014/15/D/ST6/04543.","ddc":["004"],"has_accepted_license":"1","oa_version":"Published Version","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"month":"08","article_number":"24","language":[{"iso":"eng"}],"conference":{"start_date":"2016-08-22","name":"MFCS: Mathematical Foundations of Computer Science (SG)","location":"Krakow; Poland","end_date":"2016-08-26"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2016-08-01T00:00:00Z","type":"conference","publist_id":"6286","oa":1,"file":[{"content_type":"application/pdf","file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf","date_updated":"2018-12-12T10:17:31Z","file_size":564560,"date_created":"2018-12-12T10:17:31Z","creator":"system","file_id":"5286","access_level":"open_access","relation":"main_file"}],"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"language":[{"iso":"eng"}],"conference":{"location":"Quebec City; Canada","end_date":"2016-08-26","name":"CONCUR: Concurrency Theory","start_date":"2016-08-23"},"has_accepted_license":"1","article_number":"20","month":"08","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"1155","relation":"dissertation_contains","status":"public"}]},"status":"public","file":[{"creator":"system","file_id":"4895","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","date_updated":"2018-12-12T10:11:39Z","file_size":501827,"date_created":"2018-12-12T10:11:39Z"}],"type":"conference","date_published":"2016-08-01T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publist_id":"6283","oa":1,"file_date_updated":"2018-12-12T10:11:39Z","quality_controlled":"1","ec_funded":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","author":[{"full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":1,"_id":"1093","intvolume":"        59","pubrep_id":"794","alternative_title":["LIPIcs"],"title":"Linear distances between Markov chains","date_created":"2018-12-11T11:50:06Z","department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"publication_status":"published","ddc":["004"],"volume":59,"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","citation":{"chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>."},"year":"2016","date_updated":"2023-09-07T11:58:33Z","abstract":[{"lang":"eng","text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. "}],"day":"01","doi":"10.4230/LIPIcs.CONCUR.2016.20"},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-11T11:50:21Z","publication_status":"published","title":"Quantitative automata under probabilistic semantics","scopus_import":1,"_id":"1138","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"publisher":"IEEE","quality_controlled":"1","ec_funded":1,"page":"76 - 85","day":"05","doi":"10.1145/2933575.2933588","arxiv":1,"abstract":[{"lang":"eng","text":"Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM."}],"citation":{"ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 76–85.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, IEEE, 2016, pp. 76–85, doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, 76–85. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, New York, NY, USA, 2016, pp. 76–85.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>. IEEE; 2016:76-85. doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative automata under probabilistic semantics. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i> (pp. 76–85). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>"},"year":"2016","date_updated":"2021-01-12T06:48:34Z","external_id":{"arxiv":["1604.06764"]},"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S114","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"oa_version":"Preprint","month":"07","publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","conference":{"start_date":"2016-07-05","name":"LICS: Logic in Computer Science","end_date":"2016-07-08","location":"New York, NY, USA"},"language":[{"iso":"eng"}],"publist_id":"6220","oa":1,"type":"conference","date_published":"2016-07-05T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public"}]