[{"_id":"10731","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"article_type":"original","type":"journal_article","status":"public","date_updated":"2023-08-02T14:13:07Z","ddc":["570"],"department":[{"_id":"KrCh"}],"file_date_updated":"2022-02-07T14:57:59Z","abstract":[{"lang":"eng","text":"Motivated by COVID-19, we develop and analyze a simple stochastic model for the spread of disease in human population. We track how the number of infected and critically ill people develops over time in order to estimate the demand that is imposed on the hospital system. To keep this demand under control, we consider a class of simple policies for slowing down and reopening society and we compare their efficiency in mitigating the spread of the virus from several different points of view. We find that in order to avoid overwhelming of the hospital system, a policy must impose a harsh lockdown or it must react swiftly (or both). While reacting swiftly is universally beneficial, being harsh pays off only when the country is patient about reopening and when the neighboring countries coordinate their mitigation efforts. Our work highlights the importance of acting decisively when closing down and the importance of patience and coordination between neighboring countries when reopening."}],"oa_version":"Published Version","scopus_import":"1","intvolume":" 12","month":"01","publication_status":"published","publication_identifier":{"eissn":["2045-2322"]},"language":[{"iso":"eng"}],"file":[{"creator":"alisjak","date_updated":"2022-02-07T14:57:59Z","file_size":2971922,"date_created":"2022-02-07T14:57:59Z","file_name":"2022_ScientificReports_Svoboda.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"10744","checksum":"247afd30c173390940f099ead35a28ed","success":1}],"ec_funded":1,"issue":"1","volume":12,"article_number":"1526","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"citation":{"chicago":"Svoboda, Jakub, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” Scientific Reports. Springer Nature, 2022. https://doi.org/10.1038/s41598-022-05333-5.","ista":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2022. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 12(1), 1526.","mla":"Svoboda, Jakub, et al. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” Scientific Reports, vol. 12, no. 1, 1526, Springer Nature, 2022, doi:10.1038/s41598-022-05333-5.","ama":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 2022;12(1). doi:10.1038/s41598-022-05333-5","apa":"Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K., & Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. Springer Nature. https://doi.org/10.1038/s41598-022-05333-5","ieee":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Infection dynamics of COVID-19 virus under lockdown and reopening,” Scientific Reports, vol. 12, no. 1. Springer Nature, 2022.","short":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Scientific Reports 12 (2022)."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","external_id":{"isi":["000749198000039"],"arxiv":["2012.15155"]},"article_processing_charge":"No","author":[{"first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","full_name":"Svoboda, Jakub"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","first_name":"Josef"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Nowak, Martin A.","last_name":"Nowak","first_name":"Martin A."}],"title":"Infection dynamics of COVID-19 virus under lockdown and reopening","acknowledgement":"K.C. acknowledges support from ERC Consolidator Grant No. (863818: ForM-SMart). A.P. acknowledges support from FWF Grant No. J-4220. M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","oa":1,"publisher":"Springer Nature","quality_controlled":"1","year":"2022","isi":1,"has_accepted_license":"1","publication":"Scientific Reports","day":"27","date_created":"2022-02-06T23:01:30Z","doi":"10.1038/s41598-022-05333-5","date_published":"2022-01-27T00:00:00Z"},{"date_updated":"2023-08-04T09:50:44Z","department":[{"_id":"KrCh"}],"_id":"12257","status":"public","type":"journal_article","article_type":"original","language":[{"iso":"eng"}],"publication_identifier":{"eissn":["2470-0053"],"issn":["2470-0045"]},"publication_status":"published","volume":106,"issue":"3","ec_funded":1,"oa_version":"Preprint","abstract":[{"text":"Structural balance theory is an established framework for studying social relationships of friendship and enmity. These relationships are modeled by a signed network whose energy potential measures the level of imbalance, while stochastic dynamics drives the network toward a state of minimum energy that captures social balance. It is known that this energy landscape has local minima that can trap socially aware dynamics, preventing it from reaching balance. Here we first study the robustness and attractor properties of these local minima. We show that a stochastic process can reach them from an abundance of initial states and that some local minima cannot be escaped by mild perturbations of the network. Motivated by these anomalies, we introduce best-edge dynamics (BED), a new plausible stochastic process. We prove that BED always reaches balance and that it does so fast in various interesting settings.","lang":"eng"}],"month":"09","intvolume":" 106","scopus_import":"1","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2210.02394","open_access":"1"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ista":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. 2022. Social balance on networks: Local minima and best-edge dynamics. Physical Review E. 106(3), 034321.","chicago":"Chatterjee, Krishnendu, Jakub Svoboda, Dorde Zikelic, Andreas Pavlogiannis, and Josef Tkadlec. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” Physical Review E. American Physical Society, 2022. https://doi.org/10.1103/physreve.106.034321.","ieee":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, and J. Tkadlec, “Social balance on networks: Local minima and best-edge dynamics,” Physical Review E, vol. 106, no. 3. American Physical Society, 2022.","short":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, J. Tkadlec, Physical Review E 106 (2022).","ama":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. Social balance on networks: Local minima and best-edge dynamics. Physical Review E. 2022;106(3). doi:10.1103/physreve.106.034321","apa":"Chatterjee, K., Svoboda, J., Zikelic, D., Pavlogiannis, A., & Tkadlec, J. (2022). Social balance on networks: Local minima and best-edge dynamics. Physical Review E. American Physical Society. https://doi.org/10.1103/physreve.106.034321","mla":"Chatterjee, Krishnendu, et al. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” Physical Review E, vol. 106, no. 3, 034321, American Physical Society, 2022, doi:10.1103/physreve.106.034321."},"title":"Social balance on networks: Local minima and best-edge dynamics","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","last_name":"Svoboda"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef"}],"external_id":{"isi":["000870243100001"],"arxiv":["2210.02394"]},"article_processing_charge":"No","article_number":"034321","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_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","grant_number":"S11407","name":"Game Theory"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"665385","name":"International IST Doctoral Program"}],"day":"29","publication":"Physical Review E","isi":1,"year":"2022","date_published":"2022-09-29T00:00:00Z","doi":"10.1103/physreve.106.034321","date_created":"2023-01-16T09:57:57Z","acknowledgement":"K.C. acknowledges support from ERC Start Grant No. (279307: Graph Games), ERC Consolidator Grant No. (863818: ForM-SMart), and Austrian Science Fund (FWF)\r\nGrants No. P23499-N23 and No. S11407-N23 (RiSE). This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie\r\nSkłodowska-Curie Grant Agreement No. 665385.","quality_controlled":"1","publisher":"American Physical Society","oa":1},{"status":"public","type":"conference","conference":{"name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","location":"Virtual","end_date":"2021-12-17","start_date":"2021-12-15"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"10629","file_date_updated":"2022-01-17T10:36:08Z","department":[{"_id":"KrCh"}],"ddc":["000"],"date_updated":"2022-01-17T10:39:40Z","month":"11","intvolume":" 213","scopus_import":"1","alternative_title":["LIPIcs"],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Product graphs arise naturally in formal verification and program analysis. For example, the analysis of two concurrent threads requires the product of two component control-flow graphs, and for language inclusion of deterministic automata the product of two automata is constructed. In many cases, the component graphs have constant treewidth, e.g., when the input contains control-flow graphs of programs. We consider the algorithmic analysis of products of two constant-treewidth graphs with respect to three classic specification languages, namely, (a) algebraic properties, (b) mean-payoff properties, and (c) initial credit for energy properties.\r\nOur main contributions are as follows. Consider a graph G that is the product of two constant-treewidth graphs of size n each. First, given an idempotent semiring, we present an algorithm that computes the semiring transitive closure of G in time Õ(n⁴). Since the output has size Θ(n⁴), our algorithm is optimal (up to polylog factors). Second, given a mean-payoff objective, we present an O(n³)-time algorithm for deciding whether the value of a starting state is non-negative, improving the previously known O(n⁴) bound. Third, given an initial credit for energy objective, we present an O(n⁵)-time algorithm for computing the minimum initial credit for all nodes of G, improving the previously known O(n⁸) bound. At the heart of our approach lies an algorithm for the efficient construction of strongly-balanced tree decompositions of constant-treewidth graphs. Given a constant-treewidth graph G' of n nodes and a positive integer λ, our algorithm constructs a binary tree decomposition of G' of width O(λ) with the property that the size of each subtree decreases geometrically with rate (1/2 + 2^{-λ})."}],"volume":213,"file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"71141acdeffa9056f24d6dbef952d254","file_id":"10633","success":1,"creator":"cchlebak","date_updated":"2022-01-17T10:36:08Z","file_size":891566,"date_created":"2022-01-17T10:36:08Z","file_name":"2021_LIPIcs_Chatterjee.pdf"}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-3-9597-7215-0"],"issn":["1868-8969"]},"publication_status":"published","article_number":"42","title":"Quantitative verification on product graphs of small treewidth","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"article_processing_charge":"No","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Quantitative verification on product graphs of small treewidth. 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 213, 42.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Quantitative Verification on Product Graphs of Small Treewidth.” In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Vol. 213. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Quantitative verification on product graphs of small treewidth. In: 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Vol 213. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2021. doi:10.4230/LIPIcs.FSTTCS.2021.42","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2021). Quantitative verification on product graphs of small treewidth. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 213). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Quantitative verification on product graphs of small treewidth,” in 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Virtual, 2021, vol. 213.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Verification on Product Graphs of Small Treewidth.” 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 213, 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, doi:10.4230/LIPIcs.FSTTCS.2021.42."},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","oa":1,"doi":"10.4230/LIPIcs.FSTTCS.2021.42","date_published":"2021-11-29T00:00:00Z","date_created":"2022-01-16T23:01:28Z","day":"29","publication":"41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","has_accepted_license":"1","year":"2021"},{"publication":"Nature Communications","day":"29","year":"2021","has_accepted_license":"1","isi":1,"date_created":"2021-07-11T22:01:15Z","date_published":"2021-06-29T00:00:00Z","doi":"10.1038/s41467-021-24271-w","acknowledgement":"K.C. acknowledges support from ERC Start grant no. (279307: Graph Games), ERC Consolidator grant no. (863818: ForM-SMart), Austrian Science Fund (FWF) grant no. P23499-N23 and S11407-N23 (RiSE). M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","oa":1,"publisher":"Springer Nature","quality_controlled":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Fast and strong amplifiers of natural selection,” Nature Communications, vol. 12, no. 1. Springer Nature, 2021.","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Nature Communications 12 (2021).","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., & Nowak, M. A. (2021). Fast and strong amplifiers of natural selection. Nature Communications. Springer Nature. https://doi.org/10.1038/s41467-021-24271-w","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Fast and strong amplifiers of natural selection. Nature Communications. 2021;12(1). doi:10.1038/s41467-021-24271-w","mla":"Tkadlec, Josef, et al. “Fast and Strong Amplifiers of Natural Selection.” Nature Communications, vol. 12, no. 1, 4009, Springer Nature, 2021, doi:10.1038/s41467-021-24271-w.","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2021. Fast and strong amplifiers of natural selection. Nature Communications. 12(1), 4009.","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Fast and Strong Amplifiers of Natural Selection.” Nature Communications. Springer Nature, 2021. https://doi.org/10.1038/s41467-021-24271-w."},"title":"Fast and strong amplifiers of natural selection","article_processing_charge":"No","external_id":{"isi":["000671752100003"],"pmid":["34188036"]},"author":[{"last_name":"Tkadlec","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"article_number":"4009","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"language":[{"iso":"eng"}],"file":[{"success":1,"checksum":"5767418926a7f7fb76151de29473dae0","file_id":"9692","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2021_NatCoom_Tkadlec.pdf","date_created":"2021-07-19T13:02:20Z","creator":"cziletti","file_size":628992,"date_updated":"2021-07-19T13:02:20Z"}],"publication_status":"published","publication_identifier":{"eissn":["20411723"]},"ec_funded":1,"volume":12,"issue":"1","oa_version":"Published Version","pmid":1,"abstract":[{"lang":"eng","text":"Selection and random drift determine the probability that novel mutations fixate in a population. Population structure is known to affect the dynamics of the evolutionary process. Amplifiers of selection are population structures that increase the fixation probability of beneficial mutants compared to well-mixed populations. Over the past 15 years, extensive research has produced remarkable structures called strong amplifiers which guarantee that every beneficial mutation fixates with high probability. But strong amplification has come at the cost of considerably delaying the fixation event, which can slow down the overall rate of evolution. However, the precise relationship between fixation probability and time has remained elusive. Here we characterize the slowdown effect of strong amplification. First, we prove that all strong amplifiers must delay the fixation event at least to some extent. Second, we construct strong amplifiers that delay the fixation event only marginally as compared to the well-mixed populations. Our results thus establish a tight relationship between fixation probability and time: Strong amplification always comes at a cost of a slowdown, but more than a marginal slowdown is not needed."}],"intvolume":" 12","month":"06","scopus_import":"1","ddc":["510"],"date_updated":"2023-08-10T14:05:09Z","file_date_updated":"2021-07-19T13:02:20Z","department":[{"_id":"KrCh"}],"_id":"9640","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"article_type":"original","type":"journal_article"},{"citation":{"ista":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In 33rd International Conference on Computer-Aided Verification , 12759:341–66. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-81685-8_16.","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in 33rd International Conference on Computer-Aided Verification , Virtual, 2021, vol. 12759, pp. 341–366.","short":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, V. Toman, in:, 33rd International Conference on Computer-Aided Verification , Springer Nature, 2021, pp. 341–366.","ama":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: 33rd International Conference on Computer-Aided Verification . Vol 12759. Springer Nature; 2021:341-366. doi:10.1007/978-3-030-81685-8_16","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., & Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In 33rd International Conference on Computer-Aided Verification (Vol. 12759, pp. 341–366). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-81685-8_16","mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” 33rd International Conference on Computer-Aided Verification , vol. 12759, Springer Nature, 2021, pp. 341–66, doi:10.1007/978-3-030-81685-8_16."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","author":[{"first_name":"Pratyush","last_name":"Agarwal","full_name":"Agarwal, Pratyush"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Shreya","full_name":"Pathak, Shreya","last_name":"Pathak"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"article_processing_charge":"Yes","external_id":{"arxiv":["2105.06424"],"isi":["000698732400016"]},"title":"Stateless model checking under a reads-value-from equivalence","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"isi":1,"has_accepted_license":"1","year":"2021","day":"15","publication":"33rd International Conference on Computer-Aided Verification ","page":"341-366","doi":"10.1007/978-3-030-81685-8_16","date_published":"2021-07-15T00:00:00Z","date_created":"2021-09-05T22:01:24Z","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.","publisher":"Springer Nature","quality_controlled":"1","oa":1,"date_updated":"2023-09-07T13:30:27Z","ddc":["000"],"department":[{"_id":"KrCh"}],"file_date_updated":"2022-05-13T07:00:20Z","_id":"9987","type":"conference","conference":{"start_date":"2021-07-20","end_date":"2021-07-23","location":"Virtual","name":"CAV: Computer Aided Verification "},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","publication_identifier":{"isbn":["978-3-030-81684-1"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["978-3-030-81685-8"]},"publication_status":"published","file":[{"file_id":"11368","checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2022-05-13T07:00:20Z","file_name":"2021_LNCS_Agarwal.pdf","creator":"dernst","date_updated":"2022-05-13T07:00:20Z","file_size":1516756}],"language":[{"iso":"eng"}],"volume":"12759 ","related_material":{"record":[{"status":"public","id":"10199","relation":"dissertation_contains"}]},"ec_funded":1,"abstract":[{"text":"Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["LNCS"],"scopus_import":"1","month":"07"},{"scopus_import":"1","month":"10","intvolume":" 5","abstract":[{"lang":"eng","text":"In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of n events over k threads and d variables, we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k· d) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when k is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.\r\n\r\n"}],"oa_version":"Published Version","issue":"OOPSLA","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"10199"}]},"volume":5,"ec_funded":1,"publication_identifier":{"eissn":["2475-1421"]},"publication_status":"published","file":[{"file_name":"2021_ProcACMPL_Bui.pdf","date_created":"2021-11-04T07:24:48Z","creator":"cchlebak","file_size":2903485,"date_updated":"2021-11-04T07:24:48Z","success":1,"checksum":"9d6dce7b611853c529bb7b1915ac579e","file_id":"10215","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"type":"journal_article","article_type":"original","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","keyword":["safety","risk","reliability and quality","software"],"_id":"10191","file_date_updated":"2021-11-04T07:24:48Z","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"date_updated":"2023-09-07T13:30:27Z","ddc":["000"],"quality_controlled":"1","publisher":"Association for Computing Machinery","oa":1,"acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003.","doi":"10.1145/3485541","date_published":"2021-10-15T00:00:00Z","date_created":"2021-10-27T15:05:34Z","has_accepted_license":"1","year":"2021","day":"15","publication":"Proceedings of the ACM on Programming Languages","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"article_number":"164","author":[{"full_name":"Bui, Truc Lam","last_name":"Bui","first_name":"Truc Lam"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Tushar","last_name":"Gautam","full_name":"Gautam, Tushar"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","last_name":"Toman","first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"external_id":{"arxiv":["2011.11763"]},"article_processing_charge":"No","title":"The reads-from equivalence for the TSO and PSO memory models","citation":{"chicago":"Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2021. https://doi.org/10.1145/3485541.","ista":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 5(OOPSLA), 164.","mla":"Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA, 164, Association for Computing Machinery, 2021, doi:10.1145/3485541.","apa":"Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., & Toman, V. (2021). The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3485541","ama":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 2021;5(OOPSLA). doi:10.1145/3485541","ieee":"T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from equivalence for the TSO and PSO memory models,” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021)."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9"},{"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_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","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"external_id":{"isi":["000645490300001"],"arxiv":["1504.07384"]},"article_processing_charge":"No","title":"Faster algorithms for quantitative verification in bounded treewidth graphs","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 57, 401–428.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design. Springer, 2021. https://doi.org/10.1007/s10703-021-00373-5.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” Formal Methods in System Design, vol. 57. Springer, pp. 401–428, 2021.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 2021;57:401-428. doi:10.1007/s10703-021-00373-5","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-021-00373-5","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design, vol. 57, Springer, 2021, pp. 401–28, doi:10.1007/s10703-021-00373-5."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","publisher":"Springer","oa":1,"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","page":"401-428","doi":"10.1007/s10703-021-00373-5","date_published":"2021-09-01T00:00:00Z","date_created":"2021-05-16T22:01:47Z","isi":1,"year":"2021","day":"01","publication":"Formal Methods in System Design","article_type":"original","type":"journal_article","status":"public","_id":"9393","department":[{"_id":"KrCh"}],"date_updated":"2023-10-10T11:13:20Z","scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/1504.07384","open_access":"1"}],"month":"09","intvolume":" 57","abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"oa_version":"Preprint","volume":57,"ec_funded":1,"publication_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"publication_status":"published","language":[{"iso":"eng"}]},{"_id":"8788","status":"public","article_type":"original","type":"journal_article","date_updated":"2023-08-22T13:27:05Z","department":[{"_id":"KrCh"}],"oa_version":"None","abstract":[{"lang":"eng","text":"We consider a real-time setting where an environment releases sequences of firm-deadline tasks, and an online scheduler chooses on-the-fly the ones to execute on a single processor so as to maximize cumulated utility. The competitive ratio is a well-known performance measure for the scheduler: it gives the worst-case ratio, among all possible choices for the environment, of the cumulated utility of the online scheduler versus an offline scheduler that knows these choices in advance. Traditionally, competitive analysis is performed by hand, while automated techniques are rare and only handle static environments with independent tasks. We present a quantitative-verification framework for precedence-aware competitive analysis, where task releases may depend on preceding scheduling choices, i.e., the environment can respond to scheduling decisions dynamically . We consider two general classes of precedences: 1) follower precedences force the release of a dependent task upon the completion of a set of precursor tasks, while and 2) pairing precedences modify the characteristics of a dependent task provided the completion of a set of precursor tasks. Precedences make competitive analysis challenging, as the online and offline schedulers operate on diverging sequences. We make a formal presentation of our framework, and use a GPU-based implementation to analyze ten well-known schedulers on precedence-based application examples taken from the existing literature: 1) a handshake protocol (HP); 2) network packet-switching; 3) query scheduling (QS); and 4) a sporadic-interrupt setting. Our experimental results show that precedences and task parameters can vary drastically the best scheduler. Our framework thus supports application designers in choosing the best scheduler among a given set automatically."}],"intvolume":" 39","month":"11","scopus_import":"1","language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"eissn":["19374151"],"issn":["02780070"]},"issue":"11","volume":39,"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Pavlogiannis, Andreas, et al. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no. 11, IEEE, 2020, pp. 3981–92, doi:10.1109/TCAD.2020.3012803.","ieee":"A. Pavlogiannis, N. Schaumberger, U. Schmid, and K. Chatterjee, “Precedence-aware automated competitive analysis of real-time scheduling,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no. 11. IEEE, pp. 3981–3992, 2020.","short":"A. Pavlogiannis, N. Schaumberger, U. Schmid, K. Chatterjee, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 3981–3992.","apa":"Pavlogiannis, A., Schaumberger, N., Schmid, U., & Chatterjee, K. (2020). Precedence-aware automated competitive analysis of real-time scheduling. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. IEEE. https://doi.org/10.1109/TCAD.2020.3012803","ama":"Pavlogiannis A, Schaumberger N, Schmid U, Chatterjee K. Precedence-aware automated competitive analysis of real-time scheduling. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 2020;39(11):3981-3992. doi:10.1109/TCAD.2020.3012803","chicago":"Pavlogiannis, Andreas, Nico Schaumberger, Ulrich Schmid, and Krishnendu Chatterjee. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. IEEE, 2020. https://doi.org/10.1109/TCAD.2020.3012803.","ista":"Pavlogiannis A, Schaumberger N, Schmid U, Chatterjee K. 2020. Precedence-aware automated competitive analysis of real-time scheduling. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 39(11), 3981–3992."},"title":"Precedence-aware automated competitive analysis of real-time scheduling","article_processing_charge":"No","external_id":{"isi":["000587712700069"]},"author":[{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"full_name":"Schaumberger, Nico","last_name":"Schaumberger","first_name":"Nico"},{"first_name":"Ulrich","full_name":"Schmid, Ulrich","last_name":"Schmid"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"}],"acknowledgement":"This work was supported by the Austrian Science Foundation (FWF) under the NFN RiSE/SHiNE under Grant S11405 and Grant S11407. This article was presented in the International Conference on Embedded Software 2020 and appears as part of the ESWEEK-TCAD special issue. ","publisher":"IEEE","quality_controlled":"1","publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","day":"01","year":"2020","isi":1,"date_created":"2020-11-22T23:01:24Z","doi":"10.1109/TCAD.2020.3012803","date_published":"2020-11-01T00:00:00Z","page":"3981-3992"},{"date_published":"2020-01-17T00:00:00Z","doi":"10.1371/journal.pcbi.1007494","date_created":"2019-12-23T13:45:11Z","has_accepted_license":"1","isi":1,"year":"2020","day":"17","publication":"PLoS computational biology","publisher":"Public Library of Science","quality_controlled":"1","oa":1,"author":[{"orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","last_name":"Tkadlec","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin A.","full_name":"Nowak, Martin A.","last_name":"Nowak"}],"article_processing_charge":"No","external_id":{"arxiv":["1906.02785"],"isi":["000510916500025"]},"title":"Limits on amplifiers of natural selection under death-Birth updating","citation":{"short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, PLoS Computational Biology 16 (2020).","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Limits on amplifiers of natural selection under death-Birth updating,” PLoS computational biology, vol. 16. Public Library of Science, 2020.","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Limits on amplifiers of natural selection under death-Birth updating. PLoS computational biology. 2020;16. doi:10.1371/journal.pcbi.1007494","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., & Nowak, M. A. (2020). Limits on amplifiers of natural selection under death-Birth updating. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1007494","mla":"Tkadlec, Josef, et al. “Limits on Amplifiers of Natural Selection under Death-Birth Updating.” PLoS Computational Biology, vol. 16, e1007494, Public Library of Science, 2020, doi:10.1371/journal.pcbi.1007494.","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2020. Limits on amplifiers of natural selection under death-Birth updating. PLoS computational biology. 16, e1007494.","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Limits on Amplifiers of Natural Selection under Death-Birth Updating.” PLoS Computational Biology. Public Library of Science, 2020. https://doi.org/10.1371/journal.pcbi.1007494."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_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","grant_number":"S11407","name":"Game Theory"}],"article_number":"e1007494","related_material":{"record":[{"relation":"part_of_dissertation","id":"7196","status":"public"}]},"volume":16,"ec_funded":1,"publication_identifier":{"eissn":["15537358"]},"publication_status":"published","file":[{"file_name":"2020_PlosCompBio_Tkadlec.pdf","date_created":"2020-02-03T07:32:42Z","creator":"dernst","file_size":1817531,"date_updated":"2020-07-14T12:47:53Z","checksum":"ce32ee2d2f53aed832f78bbd47e882df","file_id":"7441","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"scopus_import":"1","month":"01","intvolume":" 16","abstract":[{"text":"The fixation probability of a single mutant invading a population of residents is among the most widely-studied quantities in evolutionary dynamics. Amplifiers of natural selection are population structures that increase the fixation probability of advantageous mutants, compared to well-mixed populations. Extensive studies have shown that many amplifiers exist for the Birth-death Moran process, some of them substantially increasing the fixation probability or even guaranteeing fixation in the limit of large population size. On the other hand, no amplifiers are known for the death-Birth Moran process, and computer-assisted exhaustive searches have failed to discover amplification. In this work we resolve this disparity, by showing that any amplification under death-Birth updating is necessarily bounded and transient. Our boundedness result states that even if a population structure does amplify selection, the resulting fixation probability is close to that of the well-mixed population. Our transience result states that for any population structure there exists a threshold r⋆ such that the population structure ceases to amplify selection if the mutant fitness advantage r is larger than r⋆. Finally, we also extend the above results to δ-death-Birth updating, which is a combination of Birth-death and death-Birth updating. On the positive side, we identify population structures that maintain amplification for a wide range of values r and δ. These results demonstrate that amplification of natural selection depends on the specific mechanisms of the evolutionary process.","lang":"eng"}],"oa_version":"Published Version","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:47:53Z","date_updated":"2023-10-17T12:29:47Z","ddc":["000"],"type":"journal_article","article_type":"original","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","_id":"7212"},{"article_processing_charge":"No","external_id":{"isi":["000681656800005"]},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","citation":{"mla":"Chatterjee, Krishnendu, et al. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” European Symposium on Programming, vol. 12075, Springer Nature, 2020, pp. 112–40, doi:10.1007/978-3-030-44914-8_5.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal and perfectly parallel algorithms for on-demand data-flow analysis,” in European Symposium on Programming, Dublin, Ireland, 2020, vol. 12075, pp. 112–140.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 112–140.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A. (2020). Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In European Symposium on Programming (Vol. 12075, pp. 112–140). Dublin, Ireland: Springer Nature. https://doi.org/10.1007/978-3-030-44914-8_5","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In: European Symposium on Programming. Vol 12075. Springer Nature; 2020:112-140. doi:10.1007/978-3-030-44914-8_5","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” In European Symposium on Programming, 12075:112–40. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-44914-8_5.","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2020. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. European Symposium on Programming. ESOP: Programming Languages and Systems, LNCS, vol. 12075, 112–140."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"page":"112-140","date_created":"2020-05-10T22:00:50Z","doi":"10.1007/978-3-030-44914-8_5","date_published":"2020-04-18T00:00:00Z","year":"2020","isi":1,"has_accepted_license":"1","publication":"European Symposium on Programming","day":"18","oa":1,"publisher":"Springer Nature","quality_controlled":"1","file_date_updated":"2020-07-14T12:48:03Z","department":[{"_id":"KrCh"}],"date_updated":"2024-03-27T23:30:33Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2020-04-25","end_date":"2020-04-30","location":"Dublin, Ireland","name":"ESOP: Programming Languages and Systems"},"type":"conference","status":"public","_id":"7810","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"volume":12075,"publication_status":"published","publication_identifier":{"issn":["03029743"],"isbn":["9783030449131"],"eissn":["16113349"]},"language":[{"iso":"eng"}],"file":[{"file_id":"7895","checksum":"8618b80f4cf7b39a60e61a6445ad9807","content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2020-05-26T13:34:48Z","file_name":"2020_LNCS_Chatterjee.pdf","date_updated":"2020-07-14T12:48:03Z","file_size":651250,"creator":"dernst"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 12075","month":"04","abstract":[{"lang":"eng","text":"Interprocedural data-flow analyses form an expressive and useful paradigm of numerous static analysis applications, such as live variables analysis, alias analysis and null pointers analysis. The most widely-used framework for interprocedural data-flow analysis is IFDS, which encompasses distributive data-flow functions over a finite domain. On-demand data-flow analyses restrict the focus of the analysis on specific program locations and data facts. This setting provides a natural split between (i) an offline (or preprocessing) phase, where the program is partially analyzed and analysis summaries are created, and (ii) an online (or query) phase, where analysis queries arrive on demand and the summaries are used to speed up answering queries.\r\nIn this work, we consider on-demand IFDS analyses where the queries concern program locations of the same procedure (aka same-context queries). We exploit the fact that flow graphs of programs have low treewidth to develop faster algorithms that are space and time optimal for many common data-flow analyses, in both the preprocessing and the query phase. We also use treewidth to develop query solutions that are embarrassingly parallelizable, i.e. the total work for answering each query is split to a number of threads such that each thread performs only a constant amount of work. Finally, we implement a static analyzer based on our algorithms, and perform a series of on-demand analysis experiments on standard benchmarks. Our experimental results show a drastic speed-up of the queries after only a lightweight preprocessing phase, which significantly outperforms existing techniques."}],"oa_version":"Published Version"},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ista":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. 2020. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 12302, 253–270.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” In Automated Technology for Verification and Analysis, 12302:253–70. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-59152-6_14.","ama":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In: Automated Technology for Verification and Analysis. Vol 12302. Springer Nature; 2020:253-270. doi:10.1007/978-3-030-59152-6_14","apa":"Asadi, A., Chatterjee, K., Goharshady, A. K., Mohammadi, K., & Pavlogiannis, A. (2020). Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In Automated Technology for Verification and Analysis (Vol. 12302, pp. 253–270). Hanoi, Vietnam: Springer Nature. https://doi.org/10.1007/978-3-030-59152-6_14","short":"A. Asadi, K. Chatterjee, A.K. Goharshady, K. Mohammadi, A. Pavlogiannis, in:, Automated Technology for Verification and Analysis, Springer Nature, 2020, pp. 253–270.","ieee":"A. Asadi, K. Chatterjee, A. K. Goharshady, K. Mohammadi, and A. Pavlogiannis, “Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth,” in Automated Technology for Verification and Analysis, Hanoi, Vietnam, 2020, vol. 12302, pp. 253–270.","mla":"Asadi, Ali, et al. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” Automated Technology for Verification and Analysis, vol. 12302, Springer Nature, 2020, pp. 253–70, doi:10.1007/978-3-030-59152-6_14."},"title":"Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth","author":[{"first_name":"Ali","full_name":"Asadi, Ali","last_name":"Asadi"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar"},{"first_name":"Kiarash","last_name":"Mohammadi","full_name":"Mohammadi, Kiarash"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"}],"article_processing_charge":"No","external_id":{"isi":["000723555700014"]},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"}],"day":"12","publication":"Automated Technology for Verification and Analysis","has_accepted_license":"1","isi":1,"year":"2020","date_published":"2020-10-12T00:00:00Z","doi":"10.1007/978-3-030-59152-6_14","date_created":"2020-11-06T07:30:05Z","page":"253-270","publisher":"Springer Nature","quality_controlled":"1","oa":1,"ddc":["000"],"date_updated":"2024-03-27T23:30:33Z","department":[{"_id":"KrCh"}],"file_date_updated":"2020-11-06T07:41:03Z","_id":"8728","status":"public","type":"conference","conference":{"start_date":"2020-10-19","location":"Hanoi, Vietnam","end_date":"2020-10-23","name":"ATVA: Automated Technology for Verification and Analysis"},"file":[{"file_name":"2020_LNCS_ATVA_Asadi_accepted.pdf","date_created":"2020-11-06T07:41:03Z","file_size":726648,"date_updated":"2020-11-06T07:41:03Z","creator":"dernst","success":1,"file_id":"8729","checksum":"ae83f27e5b189d5abc2e7514f1b7e1b5","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"publication_identifier":{"eisbn":["9783030591526"],"eissn":["1611-3349"],"isbn":["9783030591519"],"issn":["0302-9743"]},"publication_status":"published","volume":12302,"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"oa_version":"Submitted Version","abstract":[{"text":"Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in O((n+m)⋅t2) time, given a tree decomposition of the MC with width t. Our results also imply a bound of O(κ⋅(n+m)⋅t2) for each objective on MDPs, where κ is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude.","lang":"eng"}],"month":"10","intvolume":" 12302","alternative_title":["LNCS"],"scopus_import":"1"},{"ec_funded":1,"related_material":{"record":[{"status":"public","id":"7196","relation":"part_of_dissertation"}]},"volume":2,"publication_status":"published","publication_identifier":{"issn":["2399-3642"]},"language":[{"iso":"eng"}],"file":[{"file_name":"2019_CommBio_Tkadlec.pdf","date_created":"2019-12-23T13:39:30Z","file_size":1670274,"date_updated":"2020-07-14T12:47:53Z","creator":"dernst","checksum":"d1a69bfe73767e4246f0a38e4e1554dd","file_id":"7211","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"scopus_import":"1","intvolume":" 2","month":"04","abstract":[{"text":"The rate of biological evolution depends on the fixation probability and on the fixation time of new mutants. Intensive research has focused on identifying population structures that augment the fixation probability of advantageous mutants. But these amplifiers of natural selection typically increase fixation time. Here we study population structures that achieve a tradeoff between fixation probability and time. First, we show that no amplifiers can have an asymptotically lower absorption time than the well-mixed population. Then we design population structures that substantially augment the fixation probability with just a minor increase in fixation time. Finally, we show that those structures enable higher effective rate of evolution than the well-mixed population provided that the rate of generating advantageous mutants is relatively low. Our work sheds light on how population structure affects the rate of evolution. Moreover, our structures could be useful for lab-based, medical, or industrial applications of evolutionary optimization.","lang":"eng"}],"pmid":1,"oa_version":"Published Version","file_date_updated":"2020-07-14T12:47:53Z","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T13:19:22Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"article_type":"original","type":"journal_article","status":"public","_id":"7210","date_created":"2019-12-23T13:36:50Z","date_published":"2019-04-23T00:00:00Z","doi":"10.1038/s42003-019-0373-y","year":"2019","has_accepted_license":"1","isi":1,"publication":"Communications Biology","day":"23","oa":1,"quality_controlled":"1","publisher":"Springer Nature","article_processing_charge":"No","external_id":{"pmid":["31044163"],"isi":["000465425700006"]},"author":[{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"full_name":"Nowak, Martin A.","last_name":"Nowak","first_name":"Martin A."}],"title":"Population structure determines the tradeoff between fixation probability and fixation time","citation":{"chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Population Structure Determines the Tradeoff between Fixation Probability and Fixation Time.” Communications Biology. Springer Nature, 2019. https://doi.org/10.1038/s42003-019-0373-y.","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2019. Population structure determines the tradeoff between fixation probability and fixation time. Communications Biology. 2, 138.","mla":"Tkadlec, Josef, et al. “Population Structure Determines the Tradeoff between Fixation Probability and Fixation Time.” Communications Biology, vol. 2, 138, Springer Nature, 2019, doi:10.1038/s42003-019-0373-y.","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Population structure determines the tradeoff between fixation probability and fixation time,” Communications Biology, vol. 2. Springer Nature, 2019.","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Communications Biology 2 (2019).","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., & Nowak, M. A. (2019). Population structure determines the tradeoff between fixation probability and fixation time. Communications Biology. Springer Nature. https://doi.org/10.1038/s42003-019-0373-y","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Population structure determines the tradeoff between fixation probability and fixation time. Communications Biology. 2019;2. doi:10.1038/s42003-019-0373-y"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"article_number":"138"},{"project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"article_number":"124","title":"Value-centric dynamic partial order reduction","article_processing_charge":"No","external_id":{"arxiv":["1909.00989"]},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"ama":"Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. Vol 3. ACM; 2019. doi:10.1145/3360550","apa":"Chatterjee, K., Pavlogiannis, A., & Toman, V. (2019). Value-centric dynamic partial order reduction. In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Vol. 3). Athens, Greece: ACM. https://doi.org/10.1145/3360550","ieee":"K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Athens, Greece, 2019, vol. 3.","short":"K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019.","mla":"Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, vol. 3, 124, ACM, 2019, doi:10.1145/3360550.","ista":"Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric Dynamic Partial Order Reduction.” In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Vol. 3. ACM, 2019. https://doi.org/10.1145/3360550."},"oa":1,"quality_controlled":"1","publisher":"ACM","acknowledgement":"The authors would also like to thank anonymous referees for their valuable comments and helpful suggestions. This work is supported by the Austrian Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE), by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian Science Fund (FWF) Schrodinger grant J-4220.\r\n","date_created":"2021-10-27T14:57:06Z","date_published":"2019-10-10T00:00:00Z","doi":"10.1145/3360550","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","day":"10","year":"2019","has_accepted_license":"1","keyword":["safety","risk","reliability and quality","software"],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2019-10-23","location":"Athens, Greece","end_date":"2019-10-25","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications"},"type":"conference","_id":"10190","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"file_date_updated":"2021-11-12T11:41:56Z","ddc":["000"],"date_updated":"2023-09-07T13:30:27Z","intvolume":" 3","month":"10","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3360550","open_access":"1"}],"oa_version":"Published Version","abstract":[{"text":"The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning.","lang":"eng"}],"volume":3,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"10199"}]},"language":[{"iso":"eng"}],"file":[{"file_id":"10278","checksum":"2149979c46964c4d117af06ccb6c0834","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2021-11-12T11:41:56Z","file_name":"2019_ACM_Chatterjee.pdf","creator":"cchlebak","date_updated":"2021-11-12T11:41:56Z","file_size":570829}],"publication_status":"published","publication_identifier":{"eissn":["2475-1421"]}},{"quality_controlled":"1","publisher":"ACM","oa":1,"has_accepted_license":"1","year":"2019","day":"01","publication":"Proceedings of the ACM on Programming Languages","doi":"10.1145/3290366","date_published":"2019-01-01T00:00:00Z","date_created":"2019-05-06T12:18:17Z","article_number":"53","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"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","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis. “Efficient Parameterized Algorithms for Data Packing.” Proceedings of the ACM on Programming Languages. ACM, 2019. https://doi.org/10.1145/3290366.","ista":"Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. 2019. Efficient parameterized algorithms for data packing. Proceedings of the ACM on Programming Languages. 3(POPL), 53.","mla":"Chatterjee, Krishnendu, et al. “Efficient Parameterized Algorithms for Data Packing.” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 53, ACM, 2019, doi:10.1145/3290366.","apa":"Chatterjee, K., Goharshady, A. K., Okati, N., & Pavlogiannis, A. (2019). Efficient parameterized algorithms for data packing. Proceedings of the ACM on Programming Languages. ACM. https://doi.org/10.1145/3290366","ama":"Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. Efficient parameterized algorithms for data packing. Proceedings of the ACM on Programming Languages. 2019;3(POPL). doi:10.1145/3290366","ieee":"K. Chatterjee, A. K. Goharshady, N. Okati, and A. Pavlogiannis, “Efficient parameterized algorithms for data packing,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL. ACM, 2019.","short":"K. Chatterjee, A.K. Goharshady, N. Okati, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 3 (2019)."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady"},{"first_name":"Nastaran","full_name":"Okati, Nastaran","last_name":"Okati"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"title":"Efficient parameterized algorithms for data packing","abstract":[{"text":"There is a huge gap between the speeds of modern caches and main memories, and therefore cache misses account for a considerable loss of efficiency in programs. The predominant technique to address this issue has been Data Packing: data elements that are frequently accessed within time proximity are packed into the same cache block, thereby minimizing accesses to the main memory. We consider the algorithmic problem of Data Packing on a two-level memory system. Given a reference sequence R of accesses to data elements, the task is to partition the elements into cache blocks such that the number of cache misses on R is minimized. The problem is notoriously difficult: it is NP-hard even when the cache has size 1, and is hard to approximate for any cache size larger than 4. Therefore, all existing techniques for Data Packing are based on heuristics and lack theoretical guarantees. In this work, we present the first positive theoretical results for Data Packing, along with new and stronger negative results. We consider the problem under the lens of the underlying access hypergraphs, which are hypergraphs of affinities between the data elements, where the order of an access hypergraph corresponds to the size of the affinity group. We study the problem parameterized by the treewidth of access hypergraphs, which is a standard notion in graph theory to measure the closeness of a graph to a tree. Our main results are as follows: We show there is a number q* depending on the cache parameters such that (a) if the access hypergraph of order q* has constant treewidth, then there is a linear-time algorithm for Data Packing; (b)the Data Packing problem remains NP-hard even if the access hypergraph of order q*-1 has constant treewidth. Thus, we establish a fine-grained dichotomy depending on a single parameter, namely, the highest order among access hypegraphs that have constant treewidth; and establish the optimal value q* of this parameter. Finally, we present an experimental evaluation of a prototype implementation of our algorithm. Our results demonstrate that, in practice, access hypergraphs of many commonly-used algorithms have small treewidth. We compare our approach with several state-of-the-art heuristic-based algorithms and show that our algorithm leads to significantly fewer cache-misses. ","lang":"eng"}],"oa_version":"Published Version","month":"01","intvolume":" 3","publication_identifier":{"issn":["2475-1421"]},"publication_status":"published","file":[{"date_updated":"2020-07-14T12:47:29Z","file_size":1294962,"creator":"dernst","date_created":"2019-05-06T12:23:11Z","file_name":"2019_ACM_POPL_Chatterjee.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"6381","checksum":"c157752f96877b36685ad7063ada4524"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"volume":3,"issue":"POPL","ec_funded":1,"_id":"6380","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","pubrep_id":"1056","date_updated":"2024-03-27T23:30:33Z","ddc":["004"],"file_date_updated":"2020-07-14T12:47:29Z","department":[{"_id":"KrCh"}]},{"department":[{"_id":"KrCh"}],"file_date_updated":"2020-10-08T12:58:10Z","date_updated":"2024-03-27T23:30:34Z","ddc":["000"],"type":"journal_article","article_type":"original","status":"public","_id":"7158","ec_funded":1,"volume":41,"issue":"4","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"publication_status":"published","publication_identifier":{"issn":["0164-0925"]},"language":[{"iso":"eng"}],"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","success":1,"file_id":"8632","checksum":"291cc86a07bd010d4815e177dac57b70","creator":"dernst","file_size":667357,"date_updated":"2020-10-08T12:58:10Z","file_name":"2019_ACMTransactions_Chatterjee.pdf","date_created":"2020-10-08T12:58:10Z"}],"scopus_import":"1","intvolume":" 41","month":"11","abstract":[{"lang":"eng","text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, and so on. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in an important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect we consider is that the control flow graphs for most programs have constant treewidth.\r\n\r\nOur main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing but can answer subsequent queries significantly faster as compared to the current algorithmic solutions for interprocedural dataflow analysis. We have also implemented our algorithms and evaluated their performance for performing on-demand interprocedural dataflow analysis on various domains, such as for live variable analysis and reaching definitions, on a standard benchmark set. Our experimental results align with our theoretical statements and show that after a lightweight preprocessing, on-demand queries are answered much faster than the standard existing algorithmic approaches.\r\n"}],"oa_version":"Submitted Version","article_processing_charge":"No","external_id":{"isi":["000564108400004"]},"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goyal","full_name":"Goyal, Prateesh","first_name":"Prateesh"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"title":"Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth","citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” ACM Transactions on Programming Languages and Systems. ACM, 2019. https://doi.org/10.1145/3363525.","ista":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. 2019. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Transactions on Programming Languages and Systems. 41(4), 23.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” ACM Transactions on Programming Languages and Systems, vol. 41, no. 4, 23, ACM, 2019, doi:10.1145/3363525.","ieee":"K. Chatterjee, A. K. Goharshady, P. Goyal, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth,” ACM Transactions on Programming Languages and Systems, vol. 41, no. 4. ACM, 2019.","short":"K. Chatterjee, A.K. Goharshady, P. Goyal, R. Ibsen-Jensen, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 41 (2019).","apa":"Chatterjee, K., Goharshady, A. K., Goyal, P., Ibsen-Jensen, R., & Pavlogiannis, A. (2019). Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Transactions on Programming Languages and Systems. ACM. https://doi.org/10.1145/3363525","ama":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Transactions on Programming Languages and Systems. 2019;41(4). doi:10.1145/3363525"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"article_number":"23","date_created":"2019-12-09T08:33:33Z","doi":"10.1145/3363525","date_published":"2019-11-01T00:00:00Z","year":"2019","isi":1,"has_accepted_license":"1","publication":"ACM Transactions on Programming Languages and Systems","day":"01","oa":1,"publisher":"ACM","quality_controlled":"1"},{"date_created":"2018-12-11T11:48:14Z","doi":"10.1007/s11241-017-9293-4","date_published":"2018-01-01T00:00:00Z","page":"166 - 207","publication":"Real-Time Systems","day":"01","year":"2018","isi":1,"has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Springer","title":"Automated competitive analysis of real time scheduling with graph games","external_id":{"isi":["000419955500006"]},"article_processing_charge":"No","publist_id":"6929","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"last_name":"Kößler","full_name":"Kößler, Alexander","first_name":"Alexander"},{"full_name":"Schmid, Ulrich","last_name":"Schmid","first_name":"Ulrich"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2018. Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. 54(1), 166–207.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” Real-Time Systems. Springer, 2018. https://doi.org/10.1007/s11241-017-9293-4.","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “Automated competitive analysis of real time scheduling with graph games,” Real-Time Systems, vol. 54, no. 1. Springer, pp. 166–207, 2018.","short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54 (2018) 166–207.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2018). Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. Springer. https://doi.org/10.1007/s11241-017-9293-4","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. Automated competitive analysis of real time scheduling with graph games. Real-Time Systems. 2018;54(1):166-207. doi:10.1007/s11241-017-9293-4","mla":"Chatterjee, Krishnendu, et al. “Automated Competitive Analysis of Real Time Scheduling with Graph Games.” Real-Time Systems, vol. 54, no. 1, Springer, 2018, pp. 166–207, doi:10.1007/s11241-017-9293-4."},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"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"}],"ec_funded":1,"issue":"1","volume":54,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"2820"}]},"language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T10:17:14Z","file_name":"IST-2018-960-v1+1_2017_Chatterjee_Automated_competetive.pdf","date_updated":"2020-07-14T12:47:56Z","file_size":1163507,"creator":"system","checksum":"c2590ef160709d8054cf29ee173f1454","file_id":"5267","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"publication_status":"published","intvolume":" 54","month":"01","scopus_import":"1","oa_version":"Published Version","abstract":[{"text":"This paper is devoted to automatic competitive analysis of real-time scheduling algorithms for firm-deadline tasksets, where only completed tasks con- tribute some utility to the system. Given such a taskset T , the competitive ratio of an on-line scheduling algorithm A for T is the worst-case utility ratio of A over the utility achieved by a clairvoyant algorithm. We leverage the theory of quantitative graph games to address the competitive analysis and competitive synthesis problems. For the competitive analysis case, given any taskset T and any finite-memory on- line scheduling algorithm A , we show that the competitive ratio of A in T can be computed in polynomial time in the size of the state space of A . Our approach is flexible as it also provides ways to model meaningful constraints on the released task sequences that determine the competitive ratio. We provide an experimental study of many well-known on-line scheduling algorithms, which demonstrates the feasibility of our competitive analysis approach that effectively replaces human ingenuity (required Preliminary versions of this paper have appeared in Chatterjee et al. ( 2013 , 2014 ). B Andreas Pavlogiannis pavlogiannis@ist.ac.at Krishnendu Chatterjee krish.chat@ist.ac.at Alexander Kößler koe@ecs.tuwien.ac.at Ulrich Schmid s@ecs.tuwien.ac.at 1 IST Austria (Institute of Science and Technology Austria), Am Campus 1, 3400 Klosterneuburg, Austria 2 Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria 123 Real-Time Syst for finding worst-case scenarios) by computing power. For the competitive synthesis case, we are just given a taskset T , and the goal is to automatically synthesize an opti- mal on-line scheduling algorithm A , i.e., one that guarantees the largest competitive ratio possible for T . We show how the competitive synthesis problem can be reduced to a two-player graph game with partial information, and establish that the compu- tational complexity of solving this game is Np -complete. The competitive synthesis problem is hence in Np in the size of the state space of the non-deterministic labeled transition system encoding the taskset. Overall, the proposed framework assists in the selection of suitable scheduling algorithms for a given taskset, which is in fact the most common situation in real-time systems design. ","lang":"eng"}],"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:47:56Z","ddc":["000"],"date_updated":"2023-09-27T12:52:38Z","pubrep_id":"960","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","_id":"738"},{"date_created":"2018-12-18T13:22:58Z","date_published":"2018-06-14T00:00:00Z","doi":"10.1038/s42003-018-0078-7","year":"2018","has_accepted_license":"1","isi":1,"publication":"Communications Biology","day":"14","oa":1,"quality_controlled":"1","publisher":"Springer Nature","external_id":{"isi":["000461126500071"]},"article_processing_charge":"No","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","last_name":"Tkadlec","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"title":"Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory","citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin A. Nowak. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” Communications Biology. Springer Nature, 2018. https://doi.org/10.1038/s42003-018-0078-7.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. 2018. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. 1(1), 71.","mla":"Pavlogiannis, Andreas, et al. “Construction of Arbitrarily Strong Amplifiers of Natural Selection Using Evolutionary Graph Theory.” Communications Biology, vol. 1, no. 1, 71, Springer Nature, 2018, doi:10.1038/s42003-018-0078-7.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak MA. Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. 2018;1(1). doi:10.1038/s42003-018-0078-7","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. A. (2018). Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology. Springer Nature. https://doi.org/10.1038/s42003-018-0078-7","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M.A. Nowak, Communications Biology 1 (2018).","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. A. Nowak, “Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory,” Communications Biology, vol. 1, no. 1. Springer Nature, 2018."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"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":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"article_number":"71","ec_funded":1,"volume":1,"related_material":{"record":[{"id":"7196","status":"public","relation":"part_of_dissertation"},{"id":"5559","status":"public","relation":"popular_science"}]},"issue":"1","publication_status":"published","publication_identifier":{"issn":["2399-3642"]},"language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"a9db825fa3b64a51ff3de035ec973b3e","file_id":"5752","file_size":1804194,"date_updated":"2020-07-14T12:47:10Z","creator":"dernst","file_name":"2018_CommBiology_Pavlogiannis.pdf","date_created":"2018-12-18T13:37:04Z"}],"scopus_import":"1","intvolume":" 1","month":"06","abstract":[{"lang":"eng","text":"Because of the intrinsic randomness of the evolutionary process, a mutant with a fitness advantage has some chance to be selected but no certainty. Any experiment that searches for advantageous mutants will lose many of them due to random drift. It is therefore of great interest to find population structures that improve the odds of advantageous mutants. Such structures are called amplifiers of natural selection: they increase the probability that advantageous mutants are selected. Arbitrarily strong amplifiers guarantee the selection of advantageous mutants, even for very small fitness advantage. Despite intensive research over the past decade, arbitrarily strong amplifiers have remained rare. Here we show how to construct a large variety of them. Our amplifiers are so simple that they could be useful in biotechnology, when optimizing biological molecules, or as a diagnostic tool, when searching for faster dividing cells or viruses. They could also occur in natural population structures."}],"oa_version":"Published Version","file_date_updated":"2020-07-14T12:47:10Z","department":[{"_id":"KrCh"}],"date_updated":"2024-02-21T13:48:42Z","ddc":["004","519","576"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","pubrep_id":"1045","status":"public","_id":"5751"},{"date_updated":"2024-03-27T23:30:34Z","department":[{"_id":"KrCh"}],"_id":"6009","status":"public","type":"journal_article","language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"issn":["0164-0925"]},"ec_funded":1,"related_material":{"record":[{"id":"1437","status":"public","relation":"earlier_version"},{"status":"public","id":"5441","relation":"earlier_version"},{"id":"5442","status":"public","relation":"earlier_version"},{"relation":"dissertation_contains","status":"public","id":"8934"}]},"issue":"3","volume":40,"oa_version":"Preprint","abstract":[{"lang":"eng","text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n"}],"intvolume":" 40","month":"08","main_file_link":[{"url":"https://arxiv.org/abs/1510.07565","open_access":"1"}],"scopus_import":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"mla":"Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” ACM Transactions on Programming Languages and Systems, vol. 40, no. 3, 9, Association for Computing Machinery (ACM), 2018, doi:10.1145/3210257.","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” ACM Transactions on Programming Languages and Systems, vol. 40, no. 3. Association for Computing Machinery (ACM), 2018.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 2018;40(3). doi:10.1145/3210257","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A. (2018). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM). https://doi.org/10.1145/3210257","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3210257.","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 40(3), 9."},"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","article_processing_charge":"No","external_id":{"arxiv":["1510.07565"],"isi":["000444694800001"]},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"article_number":"9","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"publication":"ACM Transactions on Programming Languages and Systems","day":"01","year":"2018","isi":1,"date_created":"2019-02-14T14:31:52Z","date_published":"2018-08-01T00:00:00Z","doi":"10.1145/3210257","oa":1,"quality_controlled":"1","publisher":"Association for Computing Machinery (ACM)"},{"citation":{"ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 7(1), 82.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.” Scientific Reports. Nature Publishing Group, 2017. https://doi.org/10.1038/s41598-017-00107-w.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports 7 (2017).","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification on undirected population structures: Comets beat stars,” Scientific Reports, vol. 7, no. 1. Nature Publishing Group, 2017.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2017). Amplification on undirected population structures: Comets beat stars. Scientific Reports. Nature Publishing Group. https://doi.org/10.1038/s41598-017-00107-w","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 2017;7(1). doi:10.1038/s41598-017-00107-w","mla":"Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures: Comets Beat Stars.” Scientific Reports, vol. 7, no. 1, 82, Nature Publishing Group, 2017, doi:10.1038/s41598-017-00107-w."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"7307","author":[{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Tkadlec","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"article_processing_charge":"No","title":"Amplification on undirected population structures: Comets beat stars","article_number":"82","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","year":"2017","day":"06","publication":"Scientific Reports","doi":"10.1038/s41598-017-00107-w","date_published":"2017-03-06T00:00:00Z","date_created":"2018-12-11T11:46:53Z","quality_controlled":"1","publisher":"Nature Publishing Group","oa":1,"date_updated":"2023-02-23T12:26:57Z","ddc":["004"],"file_date_updated":"2020-07-14T12:46:36Z","department":[{"_id":"KrCh"}],"_id":"512","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","pubrep_id":"938","publication_identifier":{"issn":["20452322"]},"publication_status":"published","file":[{"checksum":"7d05cbdd914e194a019c0f91fb64e9a8","file_id":"5357","content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2018-12-12T10:18:35Z","file_name":"IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf","date_updated":"2020-07-14T12:46:36Z","file_size":1536783,"creator":"system"}],"language":[{"iso":"eng"}],"volume":7,"issue":"1","related_material":{"record":[{"relation":"earlier_version","id":"5449","status":"public"}]},"ec_funded":1,"abstract":[{"lang":"eng","text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population. The fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure. Amplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade. In this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Cometswarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively. "}],"oa_version":"Published Version","scopus_import":1,"month":"03","intvolume":" 7"},{"scopus_import":"1","intvolume":" 2","month":"12","abstract":[{"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.","lang":"eng"}],"oa_version":"Published Version","ec_funded":1,"issue":"POPL","related_material":{"record":[{"relation":"earlier_version","id":"5455","status":"public"}]},"volume":2,"publication_status":"published","publication_identifier":{"eissn":["2475-1421"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2021-12-07T08:06:28Z","file_name":"2017_ACMProgLang_Chatterjee.pdf","date_updated":"2021-12-07T08:06:28Z","file_size":460188,"creator":"cchlebak","checksum":"faa3f7b3fe8aab84b50ed805c26a0ee5","file_id":"10421","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2018-01-07","end_date":"2018-01-13","location":"Los Angeles, CA, United States","name":"POPL: Programming Languages"},"article_type":"original","type":"journal_article","status":"public","_id":"10416","department":[{"_id":"KrCh"}],"file_date_updated":"2021-12-07T08:06:28Z","date_updated":"2023-02-23T12:27:13Z","ddc":["000"],"oa":1,"quality_controlled":"1","publisher":"Association for Computing Machinery","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","date_created":"2021-12-05T23:01:48Z","doi":"10.1145/3158118","date_published":"2017-12-27T00:00:00Z","year":"2017","has_accepted_license":"1","publication":"Proceedings of the ACM on Programming Languages","day":"27","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_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":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"article_number":"30","article_processing_charge":"No","external_id":{"arxiv":["1910.00241"]},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Choudhary","full_name":"Choudhary, Bhavya","first_name":"Bhavya"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"title":"Optimal Dyck reachability for data-dependence and Alias analysis","citation":{"chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158118.","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.","mla":"Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 30, Association for Computing Machinery, 2017, doi:10.1145/3158118.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability for data-dependence and Alias analysis,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 2 (2017).","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158118","apa":"Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158118"},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9"},{"language":[{"iso":"eng"}],"file":[{"checksum":"177a84a46e3ac17e87b31534ad16a4c9","file_id":"5524","access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T11:54:02Z","file_name":"IST-2017-870-v1+1_main.pdf","creator":"system","date_updated":"2020-07-14T12:46:59Z","file_size":960491}],"publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"related_material":{"record":[{"id":"10416","status":"public","relation":"later_version"}]},"oa_version":"Published Version","abstract":[{"lang":"eng","text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graphwhere the edges are labeled with different types of opening and closing parentheses, and the reachabilityinformation is computed via paths whose parentheses are properly matched. We present new results for Dyckreachability 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 asfollows:First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph withnnodes andmedges, we present: (i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching lower bound that shows that our algorithm is optimalwrt to worst-case complexity; and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtainanalysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almostlinear 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 MatrixMultiplication, which is a long-standing open problem. Thus we establish that the existing combinatorialalgorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the samehardness holds for graphs of constant treewidth.Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependenceanalysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform allexisting methods on the two problems, over real-world benchmarks."}],"month":"10","alternative_title":["IST Austria Technical Report"],"ddc":["000"],"date_updated":"2023-02-21T15:54:10Z","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:59Z","_id":"5455","pubrep_id":"870","status":"public","type":"technical_report","day":"23","year":"2017","has_accepted_license":"1","date_created":"2018-12-12T11:39:26Z","doi":"10.15479/AT:IST-2017-870-v1-1","date_published":"2017-10-23T00:00:00Z","page":"37","oa":1,"publisher":"IST Austria","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and alias analysis, IST Austria, 37p.","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2017-870-v1-1.","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria; 2017. doi:10.15479/AT:IST-2017-870-v1-1","apa":"Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and alias analysis. IST Austria. https://doi.org/10.15479/AT:IST-2017-870-v1-1","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for Data-Dependence and Alias Analysis, IST Austria, 2017.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, Optimal Dyck reachability for data-dependence and alias analysis. IST Austria, 2017.","mla":"Chatterjee, Krishnendu, et al. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. IST Austria, 2017, doi:10.15479/AT:IST-2017-870-v1-1."},"title":"Optimal Dyck reachability for data-dependence and alias analysis","article_processing_charge":"No","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Bhavya","full_name":"Choudhary, Bhavya","last_name":"Choudhary"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}]},{"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"article_number":"31","external_id":{"arxiv":["1610.01188"]},"article_processing_charge":"No","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"first_name":"Nishant","last_name":"Sinha","full_name":"Sinha, Nishant"},{"last_name":"Vaidya","full_name":"Vaidya, Kapil","first_name":"Kapil"}],"title":"Data-centric dynamic partial order reduction","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.","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158119.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings of the ACM on Programming Languages 2 (2017).","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric dynamic partial order reduction,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.","apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K. (2017). Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158119","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158119","mla":"Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 31, Association for Computing Machinery, 2017, doi:10.1145/3158119."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa":1,"quality_controlled":"1","publisher":"Association for Computing Machinery","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.","date_created":"2021-12-05T23:01:49Z","doi":"10.1145/3158119","date_published":"2017-12-27T00:00:00Z","year":"2017","publication":"Proceedings of the ACM on Programming Languages","day":"27","conference":{"location":"Los Angeles, CA, United States","end_date":"2018-01-13","start_date":"2018-01-07","name":"POPL: Programming Languages"},"article_type":"original","type":"journal_article","status":"public","_id":"10417","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:27:16Z","main_file_link":[{"open_access":"1","url":"https://dl.acm.org/doi/10.1145/3158119"}],"scopus_import":"1","intvolume":" 2","month":"12","abstract":[{"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.","lang":"eng"}],"oa_version":"Published Version","ec_funded":1,"volume":2,"issue":"POPL","related_material":{"record":[{"relation":"earlier_version","id":"5448","status":"public"},{"id":"5456","status":"public","relation":"earlier_version"}]},"publication_status":"published","publication_identifier":{"eissn":["2475-1421"]},"language":[{"iso":"eng"}]},{"_id":"5456","type":"technical_report","status":"public","pubrep_id":"872","citation":{"mla":"Chalupa, Marek, et al. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2017, doi:10.15479/AT:IST-2017-872-v1-1.","apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K. (2017). Data-centric dynamic partial order reduction. IST Austria. https://doi.org/10.15479/AT:IST-2017-872-v1-1","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-Centric Dynamic Partial Order Reduction. IST Austria; 2017. doi:10.15479/AT:IST-2017-872-v1-1","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2017.","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, Data-centric dynamic partial order reduction. IST Austria, 2017.","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2017-872-v1-1.","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction, IST Austria, 36p."},"date_updated":"2023-02-23T12:26:54Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"first_name":"Nishant","full_name":"Sinha, Nishant","last_name":"Sinha"},{"last_name":"Vaidya","full_name":"Vaidya, Kapil","first_name":"Kapil"}],"title":"Data-centric dynamic partial order reduction","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:59Z","abstract":[{"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\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.\r\n1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence. \r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.","lang":"eng"}],"oa_version":"Published Version","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"month":"10","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","year":"2017","day":"23","file":[{"file_size":910347,"date_updated":"2020-07-14T12:46:59Z","creator":"system","file_name":"IST-2017-872-v1+1_main.pdf","date_created":"2018-12-12T11:53:26Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"5487","checksum":"d2635c4cf013000f0a1b09e80f9e4ab7"}],"language":[{"iso":"eng"}],"page":"36","doi":"10.15479/AT:IST-2017-872-v1-1","date_published":"2017-10-23T00:00:00Z","related_material":{"record":[{"id":"10417","status":"public","relation":"later_version"},{"status":"public","id":"5448","relation":"earlier_version"}]},"date_created":"2018-12-12T11:39:26Z"},{"publication_identifier":{"issn":["2663-337X"]},"publication_status":"published","degree_awarded":"PhD","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"3a3ec003f6ee73f41f82a544d63dfc77","file_id":"4900","date_updated":"2020-07-14T12:48:10Z","file_size":4103115,"creator":"system","date_created":"2018-12-12T10:11:44Z","file_name":"IST-2017-854-v1+1_Pavlogiannis_Thesis_PubRep.pdf"},{"file_id":"6201","checksum":"bd2facc45ff8a2e20c5ed313c2ccaa83","access_level":"closed","relation":"source_file","content_type":"application/zip","date_created":"2019-04-05T07:59:31Z","file_name":"2017_thesis_Pavlogiannis.zip","creator":"dernst","date_updated":"2020-07-14T12:48:10Z","file_size":14744374}],"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"1071","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","status":"public","id":"1437"},{"id":"1602","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"1604","status":"public"},{"id":"1607","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"1714","status":"public"}]},"ec_funded":1,"license":"https://creativecommons.org/licenses/by-nd/4.0/","abstract":[{"text":"This dissertation focuses on algorithmic aspects of program verification, and presents modeling and complexity advances on several problems related to the\r\nstatic analysis of programs, the stateless model checking of concurrent programs, and the competitive analysis of real-time scheduling algorithms.\r\nOur contributions can be broadly grouped into five categories.\r\n\r\nOur first contribution is a set of new algorithms and data structures for the quantitative and data-flow analysis of programs, based on the graph-theoretic notion of treewidth.\r\nIt has been observed that the control-flow graphs of typical programs have special structure, and are characterized as graphs of small treewidth.\r\nWe utilize this structural property to provide faster algorithms for the quantitative and data-flow analysis of recursive and concurrent programs.\r\nIn most cases we make an algebraic treatment of the considered problem,\r\nwhere several interesting analyses, such as the reachability, shortest path, and certain kind of data-flow analysis problems follow as special cases. \r\nWe exploit the constant-treewidth property to obtain algorithmic improvements for on-demand versions of the problems, \r\nand provide data structures with various tradeoffs between the resources spent in the preprocessing and querying phase.\r\nWe also improve on the algorithmic complexity of quantitative problems outside the algebraic path framework,\r\nnamely of the minimum mean-payoff, minimum ratio, and minimum initial credit for energy problems.\r\n\r\n\r\nOur second contribution is a set of algorithms for Dyck reachability with applications to data-dependence analysis and alias analysis.\r\nIn particular, we develop an optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous in context-insensitive, field-sensitive points-to analysis.\r\nAdditionally, we develop an efficient algorithm for context-sensitive data-dependence analysis via Dyck reachability,\r\nwhere the task is to obtain analysis summaries of library code in the presence of callbacks.\r\nOur algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is (i)~linear in the number of call sites and (ii)~only logarithmic in the size of the whole library, as opposed to linear in the size of the whole library.\r\nFinally, we prove that Dyck reachability is Boolean Matrix Multiplication-hard in general, and the hardness also holds for graphs of constant treewidth.\r\nThis hardness result strongly indicates that there exist no combinatorial algorithms for Dyck reachability with truly subcubic complexity.\r\n\r\n\r\nOur third contribution is the formalization and algorithmic treatment of the Quantitative Interprocedural Analysis framework.\r\nIn this framework, the transitions of a recursive program are annotated as good, bad or neutral, and receive a weight which measures\r\nthe magnitude of their respective effect.\r\nThe Quantitative Interprocedural Analysis problem asks to determine whether there exists an infinite run of the program where the long-run ratio of the bad weights over the good weights is above a given threshold.\r\nWe illustrate how several quantitative problems related to static analysis of recursive programs can be instantiated in this framework,\r\nand present some case studies to this direction.\r\n\r\n\r\nOur fourth contribution is a new dynamic partial-order reduction for the stateless model checking of concurrent programs. Traditional approaches rely on the standard Mazurkiewicz equivalence between traces, by means of partitioning the trace space into equivalence classes, and attempting to explore a few representatives from each class.\r\nWe present a new dynamic partial-order reduction method called the Data-centric Partial Order Reduction (DC-DPOR).\r\nOur algorithm is based on a new equivalence between traces, called the observation equivalence.\r\nDC-DPOR explores a coarser partitioning of the trace space than any exploration method based on the standard Mazurkiewicz equivalence.\r\nDepending on the program, the new partitioning can be even exponentially coarser.\r\nAdditionally, DC-DPOR spends only polynomial time in each explored class.\r\n\r\n\r\nOur fifth contribution is the use of automata and game-theoretic verification techniques in the competitive analysis and synthesis of real-time scheduling algorithms for firm-deadline tasks.\r\nOn the analysis side, we leverage automata on infinite words to compute the competitive ratio of real-time schedulers subject to various environmental constraints.\r\nOn the synthesis side, we introduce a new instance of two-player mean-payoff partial-information games, and show\r\nhow the synthesis of an optimal real-time scheduler can be reduced to computing winning strategies in this new type of games.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["ISTA Thesis"],"month":"08","supervisor":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2023-09-07T12:01:59Z","ddc":["000"],"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:48:10Z","_id":"821","type":"dissertation","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"status":"public","pubrep_id":"854","has_accepted_license":"1","year":"2017","day":"09","page":"418","date_published":"2017-08-09T00:00:00Z","doi":"10.15479/AT:ISTA:th_854","date_created":"2018-12-11T11:48:41Z","acknowledgement":"First, I am thankful to my advisor, Krishnendu Chatterjee, for offering me the opportunity to\r\nmaterialize my scientific curiosity in a remarkably wide range of interesting topics, as well as for his constant availability and continuous support throughout my doctoral studies. I have had the privilege of collaborating with, discussing and getting inspired by all members of my committee: Thomas A. Henzinger, Ulrich Schmid and Martin A. Nowak. The role of the above four people has been very instrumental both to the research carried out for this dissertation, and to the researcher I evolved to in the process.\r\nI have greatly enjoyed my numerous brainstorming sessions with Rasmus Ibsen-Jensen, many\r\nof which led to results on low-treewidth graphs presented here. I thank Alex Kößler for our\r\ndiscussions on modeling and analyzing real-time scheduling algorithms, Yaron Velner for our\r\ncollaboration on the Quantitative Interprocedural Analysis framework, and Nishant Sinha for our initial discussions on partial order reduction techniques in stateless model checking. I also thank Jan Otop, Ben Adlam, Bernhard Kragl and Josef Tkadlec for our fruitful collaborations on\r\ntopics outside the scope of this dissertation, as well as the interns Prateesh Goyal, Amir Kafshdar Goharshady, Samarth Mishra, Bhavya Choudhary and Marek Chalupa, with whom I have shared my excitement on various research topics. Together with my collaborators, I thank officemates and members of the Chatterjee and Henzinger groups throughout the years, Thorsten Tarrach, Ventsi Chonev, Roopsha Samanta, Przemek Daca, Mirco Giacobbe, Tanja Petrov, Ashutosh\r\nGupta, Arjun Radhakrishna, Petr Novontý, Christian Hilbe, Jakob Ruess, Martin Chmelik,\r\nCezara Dragoi, Johannes Reiter, Andrey Kupriyanov, Guy Avni, Sasha Rubin, Jessica Davies, Hongfei Fu, Thomas Ferrère, Pavol Cerný, Ali Sezgin, Jan Kretínský, Sergiy Bogomolov, Hui\r\nKong, Benjamin Aminof, Duc-Hiep Chu, and Damien Zufferey. Besides collaborations and office spaces, with many of the above people I have been fortunate to share numerous whiteboard\r\ndiscussions, as well as memorable long walks and amicable meals accompanied by stimulating\r\nconversations. I am highly indebted to Elisabeth Hacker for her continuous assistance in matters\r\nthat often exceeded her official duties, and who made my integration in Austria a smooth process.","publisher":"Institute of Science and Technology Austria","oa":1,"citation":{"ista":"Pavlogiannis A. 2017. Algorithmic advances in program analysis and their applications. Institute of Science and Technology Austria.","chicago":"Pavlogiannis, Andreas. “Algorithmic Advances in Program Analysis and Their Applications.” Institute of Science and Technology Austria, 2017. https://doi.org/10.15479/AT:ISTA:th_854.","ieee":"A. Pavlogiannis, “Algorithmic advances in program analysis and their applications,” Institute of Science and Technology Austria, 2017.","short":"A. Pavlogiannis, Algorithmic Advances in Program Analysis and Their Applications, Institute of Science and Technology Austria, 2017.","ama":"Pavlogiannis A. Algorithmic advances in program analysis and their applications. 2017. doi:10.15479/AT:ISTA:th_854","apa":"Pavlogiannis, A. (2017). Algorithmic advances in program analysis and their applications. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:th_854","mla":"Pavlogiannis, Andreas. Algorithmic Advances in Program Analysis and Their Applications. Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:th_854."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"6828","author":[{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"No","title":"Algorithmic advances in program analysis and their applications","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}]},{"month":"03","intvolume":" 10201","alternative_title":["LNCS"],"scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.04914"}],"oa_version":"Submitted Version","abstract":[{"lang":"eng","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."}],"volume":10201,"ec_funded":1,"language":[{"iso":"eng"}],"publication_identifier":{"issn":["03029743"]},"publication_status":"published","status":"public","type":"conference","conference":{"name":"ESOP: European Symposium on Programming","end_date":"2017-04-29","location":"Uppsala, Sweden","start_date":"2017-04-22"},"_id":"1011","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2023-09-22T09:44:50Z","publisher":"Springer","quality_controlled":"1","oa":1,"date_published":"2017-03-19T00:00:00Z","doi":"10.1007/978-3-662-54434-1_11","date_created":"2018-12-11T11:49:41Z","page":"287 - 313","day":"19","isi":1,"year":"2017","project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"title":"Faster algorithms for weighted recursive state machines","editor":[{"full_name":"Yang, Hongseok","last_name":"Yang","first_name":"Hongseok"}],"publist_id":"6384","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kragl","full_name":"Kragl, Bernhard","orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","first_name":"Bernhard"},{"last_name":"Mishra","full_name":"Mishra, Samarth","first_name":"Samarth"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"article_processing_charge":"No","external_id":{"isi":["000681702400011"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","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.","apa":"Chatterjee, K., Kragl, B., Mishra, S., & 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. https://doi.org/10.1007/978-3-662-54434-1_11","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:10.1007/978-3-662-54434-1_11","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:10.1007/978-3-662-54434-1_11.","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.","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. https://doi.org/10.1007/978-3-662-54434-1_11."}},{"_id":"5559","status":"public","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"keyword":["natural selection"],"type":"research_data","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["519"],"date_updated":"2024-02-21T13:48:42Z","citation":{"short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak , (2017).","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak , “Strong amplifiers of natural selection.” Institute of Science and Technology Austria, 2017.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Strong amplifiers of natural selection. 2017. doi:10.15479/AT:ISTA:51","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak , M. (2017). Strong amplifiers of natural selection. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:51","mla":"Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection. Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:51.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Strong amplifiers of natural selection, Institute of Science and Technology Austria, 10.15479/AT:ISTA:51.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak . “Strong Amplifiers of Natural Selection.” Institute of Science and Technology Austria, 2017. https://doi.org/10.15479/AT:ISTA:51."},"title":"Strong amplifiers of natural selection","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:47:02Z","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","last_name":"Nowak ","full_name":"Nowak , Martin"}],"article_processing_charge":"No","oa_version":"Published Version","abstract":[{"lang":"eng","text":"Strong amplifiers of natural selection"}],"month":"01","publisher":"Institute of Science and Technology Austria","oa":1,"file":[{"file_id":"5644","checksum":"b427dd46a30096a1911b245640c47af8","content_type":"video/mp4","relation":"main_file","access_level":"open_access","file_name":"IST-2017-51-v1+2_illustration.mp4","date_created":"2018-12-12T13:05:18Z","file_size":32987015,"date_updated":"2020-07-14T12:47:02Z","creator":"system"}],"day":"02","has_accepted_license":"1","year":"2017","datarep_id":"51","related_material":{"record":[{"status":"public","id":"5452","relation":"research_paper"},{"relation":"research_paper","status":"public","id":"5751"}]},"doi":"10.15479/AT:ISTA:51","date_published":"2017-01-02T00:00:00Z","date_created":"2018-12-12T12:31:32Z","ec_funded":1},{"oa_version":"Submitted Version","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."}],"month":"01","intvolume":" 10482","scopus_import":"1","alternative_title":["LNCS"],"file":[{"file_id":"4835","checksum":"a0d9f5f94dc594c4e71e78525c9942f1","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf","date_created":"2018-12-12T10:10:45Z","file_size":948514,"date_updated":"2020-07-14T12:48:16Z","creator":"system"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["03029743"]},"publication_status":"published","volume":10482,"related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"ec_funded":1,"_id":"949","status":"public","pubrep_id":"845","type":"conference","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2017-10-03","end_date":"2017-10-06","location":"Pune, India"},"ddc":["005"],"date_updated":"2024-03-27T23:30:34Z","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:48:16Z","publisher":"Springer","quality_controlled":"1","oa":1,"day":"01","has_accepted_license":"1","isi":1,"year":"2017","doi":"10.1007/978-3-319-68167-2_4","date_published":"2017-01-01T00:00:00Z","date_created":"2018-12-11T11:49:22Z","page":"59 - 66","project":[{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “JTDec: A Tool for Tree Decompositions in Soot.” edited by Deepak D’Souza, 10482:59–66. Springer, 2017. https://doi.org/10.1007/978-3-319-68167-2_4.","ista":"Chatterjee K, Goharshady AK, Pavlogiannis A. 2017. JTDec: A tool for tree decompositions in soot. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 10482, 59–66.","mla":"Chatterjee, Krishnendu, et al. JTDec: A Tool for Tree Decompositions in Soot. Edited by Deepak D’Souza, vol. 10482, Springer, 2017, pp. 59–66, doi:10.1007/978-3-319-68167-2_4.","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.","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:10.1007/978-3-319-68167-2_4","apa":"Chatterjee, K., Goharshady, A. K., & 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. https://doi.org/10.1007/978-3-319-68167-2_4"},"editor":[{"first_name":"Deepak","full_name":"D'Souza, Deepak","last_name":"D'Souza"}],"title":"JTDec: A tool for tree decompositions in soot","publist_id":"6468","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"article_processing_charge":"No","external_id":{"isi":["000723567800004"]}},{"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"}],"file_date_updated":"2020-07-14T12:46:58Z","title":"Quantitative interprocedural analysis","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T10:06:22Z","citation":{"ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2016. Quantitative interprocedural analysis, IST Austria, 33p.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. Quantitative Interprocedural Analysis. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-523-v1-1.","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative Interprocedural Analysis. IST Austria; 2016. doi:10.15479/AT:IST-2016-523-v1-1","apa":"Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2016). Quantitative interprocedural analysis. IST Austria. https://doi.org/10.15479/AT:IST-2016-523-v1-1","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Quantitative Interprocedural Analysis, IST Austria, 2016.","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, Quantitative interprocedural analysis. IST Austria, 2016.","mla":"Chatterjee, Krishnendu, et al. Quantitative Interprocedural Analysis. IST Austria, 2016, doi:10.15479/AT:IST-2016-523-v1-1."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["005"],"type":"technical_report","status":"public","pubrep_id":"523","_id":"5445","page":"33","doi":"10.15479/AT:IST-2016-523-v1-1","date_published":"2016-03-31T00:00:00Z","related_material":{"record":[{"id":"1604","status":"public","relation":"later_version"}]},"date_created":"2018-12-12T11:39:22Z","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2016","file":[{"file_name":"IST-2016-523-v1+1_main.pdf","date_created":"2018-12-12T11:53:52Z","file_size":1012204,"date_updated":"2020-07-14T12:46:58Z","creator":"system","file_id":"5513","checksum":"cef516fa091925b5868813e355268fb4","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"day":"31","language":[{"iso":"eng"}],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"03","abstract":[{"text":"We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs. ","lang":"eng"}],"oa_version":"Published Version"},{"file_date_updated":"2020-07-14T12:46:58Z","department":[{"_id":"KrCh"}],"title":"Amplification on undirected population structures: Comets beat stars","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","last_name":"Tkadlec","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"ddc":["519"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Pavlogiannis, Andreas, et al. Amplification on Undirected Population Structures: Comets Beat Stars. IST Austria, 2016, doi:10.15479/AT:IST-2016-648-v1-1.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on Undirected Population Structures: Comets Beat Stars. IST Austria; 2016. doi:10.15479/AT:IST-2016-648-v1-1","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Amplification on undirected population structures: Comets beat stars. IST Austria. https://doi.org/10.15479/AT:IST-2016-648-v1-1","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected Population Structures: Comets Beat Stars, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Amplification on undirected population structures: Comets beat stars. IST Austria, 2016.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Amplification on Undirected Population Structures: Comets Beat Stars. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-648-v1-1.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Amplification on undirected population structures: Comets beat stars, IST Austria, 22p."},"date_updated":"2023-02-23T12:22:21Z","pubrep_id":"648","status":"public","type":"technical_report","_id":"5449","date_created":"2018-12-12T11:39:24Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"512"}]},"date_published":"2016-11-09T00:00:00Z","doi":"10.15479/AT:IST-2016-648-v1-1","page":"22","language":[{"iso":"eng"}],"file":[{"creator":"system","file_size":1264221,"date_updated":"2020-07-14T12:46:58Z","file_name":"IST-2016-648-v1+1_tr.pdf","date_created":"2018-12-12T11:54:07Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"5529","checksum":"8345a8c1e7d7f0cd92516d182b7fc59e"}],"day":"09","year":"2016","publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","month":"11","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa_version":"Updated Version","abstract":[{"lang":"eng","text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population.\r\nThe fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure.\r\nAmplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade.\r\nIn this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively."}]},{"date_updated":"2023-02-23T12:27:07Z","citation":{"ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-749-v3-1","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-749-v3-1","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong amplifiers of natural selection. IST Austria, 2016.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016.","mla":"Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2017-749-v3-1.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 34p.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2017-749-v3-1."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"title":"Arbitrarily strong amplifiers of natural selection","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:59Z","_id":"5453","type":"technical_report","pubrep_id":"755","status":"public","publication_status":"published","year":"2016","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"day":"30","file":[{"file_name":"IST-2017-749-v3+1_main.pdf","date_created":"2018-12-12T11:53:13Z","file_size":1015647,"date_updated":"2020-07-14T12:46:59Z","creator":"system","file_id":"5474","checksum":"83b0313dab3bff4bdb6ac38695026fda","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"page":"34","date_created":"2018-12-12T11:39:25Z","doi":"10.15479/AT:IST-2017-749-v3-1","date_published":"2016-12-30T00:00:00Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5452"}]},"oa_version":"Published Version","oa":1,"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"month":"12"},{"date_updated":"2023-02-23T12:27:05Z","citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-728-v1-1.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers of natural selection, IST Austria, 34p.","mla":"Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2016-728-v1-1.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of Natural Selection, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Strong amplifiers of natural selection. IST Austria, 2016.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2016-728-v1-1","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2016-728-v1-1"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"file_date_updated":"2020-07-14T12:46:59Z","title":"Strong amplifiers of natural selection","department":[{"_id":"KrCh"}],"_id":"5451","type":"technical_report","pubrep_id":"728","status":"public","year":"2016","publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","language":[{"iso":"eng"}],"file":[{"file_name":"IST-2016-728-v1+1_main.pdf","date_created":"2018-12-12T11:53:04Z","creator":"system","file_size":1014732,"date_updated":"2020-07-14T12:46:59Z","checksum":"7b8bb17c322c0556acba6ac169fa71c1","file_id":"5465","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"day":"30","page":"34","date_created":"2018-12-12T11:39:24Z","doi":"10.15479/AT:IST-2016-728-v1-1","date_published":"2016-12-30T00:00:00Z","oa_version":"Published Version","oa":1,"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"month":"12"},{"publist_id":"6312","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"title":"Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs","citation":{"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. https://doi.org/10.4230/LIPIcs.ESA.2016.28.","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. Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs. Vol. 57, 28, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:10.4230/LIPIcs.ESA.2016.28.","apa":"Chatterjee, K., Ibsen-Jensen, R., & 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. https://doi.org/10.4230/LIPIcs.ESA.2016.28","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:10.4230/LIPIcs.ESA.2016.28","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."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"article_number":"28","date_published":"2016-08-01T00:00:00Z","doi":"10.4230/LIPIcs.ESA.2016.28","date_created":"2018-12-11T11:49:59Z","has_accepted_license":"1","year":"2016","day":"01","publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","quality_controlled":"1","oa":1,"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).","file_date_updated":"2018-12-12T10:14:31Z","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T12:01:58Z","ddc":["004","006"],"type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2016-08-22","location":"Aarhus, Denmark","end_date":"2016-08-24","name":"ESA: European Symposium on Algorithms"},"status":"public","pubrep_id":"777","_id":"1071","volume":57,"related_material":{"record":[{"status":"public","id":"821","relation":"dissertation_contains"}]},"ec_funded":1,"publication_status":"published","file":[{"creator":"system","date_updated":"2018-12-12T10:14:31Z","file_size":579225,"date_created":"2018-12-12T10:14:31Z","file_name":"IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"5084"}],"language":[{"iso":"eng"}],"scopus_import":1,"alternative_title":["LIPIcs"],"month":"08","intvolume":" 57","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"}],"oa_version":"Published Version"},{"date_updated":"2024-02-21T13:48:42Z","ddc":["000"],"file_date_updated":"2020-07-14T12:46:59Z","department":[{"_id":"KrCh"}],"_id":"5452","type":"technical_report","status":"public","pubrep_id":"750","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5460","checksum":"58e895f26c82f560c0f0989bf8b08599","date_updated":"2020-07-14T12:46:59Z","file_size":811558,"creator":"system","date_created":"2018-12-12T11:52:59Z","file_name":"IST-2017-728-v2+1_main.pdf"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"5453","status":"public","relation":"later_version"},{"relation":"popular_science","status":"public","id":"5559"}]},"ec_funded":1,"oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"month":"12","citation":{"mla":"Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2017-728-v2-1.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong amplifiers of natural selection. IST Austria, 2016.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-728-v2-1","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-728-v2-1","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2017-728-v2-1.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 32p."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","last_name":"Tkadlec","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"article_processing_charge":"No","title":"Arbitrarily strong amplifiers of natural selection","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","year":"2016","day":"30","page":"32","doi":"10.15479/AT:IST-2017-728-v2-1","date_published":"2016-12-30T00:00:00Z","date_created":"2018-12-12T11:39:25Z","publisher":"IST Austria","oa":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"}],"citation":{"ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2016. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. POPL: Principles of Programming Languages, POPL, vol. 20–22, 733–747.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components,” 20–22:733–47. ACM, 2016. https://doi.org/10.1145/2837614.2837624.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 733–747.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, ACM, 2016, pp. 733–747.","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: Vol 20-22. ACM; 2016:733-747. doi:10.1145/2837614.2837624","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A. (2016). Algorithms for algebraic path properties in concurrent systems of constant treewidth components (Vol. 20–22, pp. 733–747). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837624","mla":"Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. Vol. 20–22, ACM, 2016, pp. 733–47, doi:10.1145/2837614.2837624."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["1510.07565"]},"publist_id":"5761","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","first_name":"Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","oa":1,"quality_controlled":"1","publisher":"ACM","year":"2016","day":"11","page":"733 - 747","date_created":"2018-12-11T11:52:01Z","doi":"10.1145/2837614.2837624","date_published":"2016-01-11T00:00:00Z","_id":"1437","conference":{"start_date":"2016-01-20","end_date":"2016-01-22","location":"St. Petersburg, FL, USA","name":"POPL: Principles of Programming Languages"},"type":"conference","status":"public","date_updated":"2024-03-27T23:30:32Z","department":[{"_id":"KrCh"}],"abstract":[{"text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.","lang":"eng"}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1510.07565"}],"alternative_title":["POPL"],"scopus_import":1,"month":"01","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5441"},{"status":"public","id":"5442","relation":"earlier_version"},{"relation":"dissertation_contains","id":"821","status":"public"},{"status":"public","id":"6009","relation":"later_version"},{"id":"8934","status":"public","relation":"dissertation_contains"}]},"volume":"20-22"},{"article_number":"17147","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Pavlogiannis, Andreas, Krishnendu Chatterjee, Ben Adlam, and Martin Nowak. “Cellular Cooperation with Shift Updating and Repulsion.” Scientific Reports. Nature Publishing Group, 2015. https://doi.org/10.1038/srep17147.","ista":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. 2015. Cellular cooperation with shift updating and repulsion. Scientific Reports. 5, 17147.","mla":"Pavlogiannis, Andreas, et al. “Cellular Cooperation with Shift Updating and Repulsion.” Scientific Reports, vol. 5, 17147, Nature Publishing Group, 2015, doi:10.1038/srep17147.","ama":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. Cellular cooperation with shift updating and repulsion. Scientific Reports. 2015;5. doi:10.1038/srep17147","apa":"Pavlogiannis, A., Chatterjee, K., Adlam, B., & Nowak, M. (2015). Cellular cooperation with shift updating and repulsion. Scientific Reports. Nature Publishing Group. https://doi.org/10.1038/srep17147","short":"A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).","ieee":"A. Pavlogiannis, K. Chatterjee, B. Adlam, and M. Nowak, “Cellular cooperation with shift updating and repulsion,” Scientific Reports, vol. 5. Nature Publishing Group, 2015."},"title":"Cellular cooperation with shift updating and repulsion","publist_id":"5536","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Ben","full_name":"Adlam, Ben","last_name":"Adlam"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"acknowledgement":"The research was supported by the Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft Faculty Fellows award. Support from the John Templeton foundation is gratefully acknowledged.","quality_controlled":"1","publisher":"Nature Publishing Group","oa":1,"day":"25","publication":"Scientific Reports","has_accepted_license":"1","year":"2015","date_published":"2015-11-25T00:00:00Z","doi":"10.1038/srep17147","date_created":"2018-12-11T11:53:06Z","_id":"1624","status":"public","pubrep_id":"466","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"date_updated":"2021-01-12T06:52:05Z","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:07Z","oa_version":"Published Version","abstract":[{"lang":"eng","text":"Population structure can facilitate evolution of cooperation. In a structured population, cooperators can form clusters which resist exploitation by defectors. Recently, it was observed that a shift update rule is an extremely strong amplifier of cooperation in a one dimensional spatial model. For the shift update rule, an individual is chosen for reproduction proportional to fecundity; the offspring is placed next to the parent; a random individual dies. Subsequently, the population is rearranged (shifted) until all individual cells are again evenly spaced out. For large population size and a one dimensional population structure, the shift update rule favors cooperation for any benefit-to-cost ratio greater than one. But every attempt to generalize shift updating to higher dimensions while maintaining its strong effect has failed. The reason is that in two dimensions the clusters are fragmented by the movements caused by rearranging the cells. Here we introduce the natural phenomenon of a repulsive force between cells of different types. After a birth and death event, the cells are being rearranged minimizing the overall energy expenditure. If the repulsive force is sufficiently high, shift becomes a strong promoter of cooperation in two dimensions."}],"month":"11","intvolume":" 5","scopus_import":1,"file":[{"creator":"system","date_updated":"2020-07-14T12:45:07Z","file_size":1021931,"date_created":"2018-12-12T10:12:29Z","file_name":"IST-2016-466-v1+1_srep17147.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"38e06d8310d2087cae5f6d4d4bfe082b","file_id":"4947"}],"language":[{"iso":"eng"}],"publication_status":"published","volume":5,"ec_funded":1},{"citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-330-v2-1.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 27p.","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-330-v2-1.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-330-v2-1","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-330-v2-1","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria, 2015."},"date_updated":"2023-02-23T12:26:05Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"file_date_updated":"2020-07-14T12:46:54Z","department":[{"_id":"KrCh"}],"title":"Faster algorithms for quantitative verification in constant treewidth graphs","_id":"5437","type":"technical_report","status":"public","pubrep_id":"333","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2015","day":"27","file":[{"date_updated":"2020-07-14T12:46:54Z","file_size":1072137,"creator":"system","date_created":"2018-12-12T11:53:12Z","file_name":"IST-2015-330-v2+1_main.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5473","checksum":"f5917c20f84018b362d385c000a2e123"}],"language":[{"iso":"eng"}],"page":"27","date_published":"2015-04-27T00:00:00Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"1607"},{"id":"5430","status":"public","relation":"earlier_version"}]},"doi":"10.15479/AT:IST-2015-330-v2-1","date_created":"2018-12-12T11:39:19Z","abstract":[{"text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. \r\nThe algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let $n$ denote the number of nodes of a graph, $m$ the number of edges (for constant treewidth graphs $m=O(n)$) and $W$ the largest absolute value of the weights.\r\nOur main theoretical results are as follows.\r\nFirst, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of $\\epsilon$ in time $O(n \\cdot \\log (n/\\epsilon))$ and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time $O(n \\cdot \\log (|a\\cdot b|))=O(n\\cdot\\log (n\\cdot W))$, when the output is $\\frac{a}{b}$, as compared to the previously best known algorithm with running time $O(n^2 \\cdot \\log (n\\cdot W))$. Third, for the minimum initial credit problem we show that (i)~for general graphs the problem can be solved in $O(n^2\\cdot m)$ time and the associated decision problem can be solved in $O(n\\cdot m)$ time, improving the previous known $O(n^3\\cdot m\\cdot \\log (n\\cdot W))$ and $O(n^2 \\cdot m)$ bounds, respectively; and (ii)~for constant treewidth graphs we present an algorithm that requires $O(n\\cdot \\log n)$ time, improving the previous known $O(n^4 \\cdot \\log (n \\cdot W))$ bound.\r\nWe have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks. ","lang":"eng"}],"oa_version":"Published Version","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"month":"04"},{"citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 31p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-319-v1-1.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria, 2015.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-319-v1-1","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-319-v1-1","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-319-v1-1."},"date_updated":"2023-02-23T12:26:22Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"}],"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:52Z","title":"Faster algorithms for quantitative verification in constant treewidth graphs","_id":"5430","type":"technical_report","status":"public","pubrep_id":"319","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2015","file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"62c6ea01e342553dcafb88a070fb1ad5","file_id":"5482","creator":"system","file_size":1089651,"date_updated":"2020-07-14T12:46:52Z","file_name":"IST-2015-319-v1+1_long.pdf","date_created":"2018-12-12T11:53:21Z"}],"day":"10","language":[{"iso":"eng"}],"page":"31","doi":"10.15479/AT:IST-2015-319-v1-1","date_published":"2015-02-10T00:00:00Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"1607"},{"relation":"later_version","id":"5437","status":"public"}]},"date_created":"2018-12-12T11:39:17Z","abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean- payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m = O ( n ) ) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a mul- tiplicative factor of ∊ in time O ( n · log( n/∊ )) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O ( n · log( | a · b · n | )) = O ( n · log( n · W )) , when the output is a b , as compared to the previously best known algorithm with running time O ( n 2 · log( n · W )) . Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O ( n 2 · m ) time and the associated decision problem can be solved in O ( n · m ) time, improving the previous known O ( n 3 · m · log( n · W )) and O ( n 2 · m ) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O ( n · log n ) time, improving the previous known O ( n 4 · log( n · W )) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"oa_version":"Published Version","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"month":"02"},{"oa":1,"publisher":"ACM","quality_controlled":"1","acknowledgement":"We thank anonymous reviewers for helpful comments to improve the presentation of the paper.","date_created":"2018-12-11T11:52:58Z","date_published":"2015-01-01T00:00:00Z","doi":"10.1145/2676726.2676979","page":"97 - 109","publication":"ACM SIGPLAN Notices","day":"01","year":"2015","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"title":"Faster algorithms for algebraic path properties in recursive state machines with constant treewidth","external_id":{"arxiv":["1410.7724"]},"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"first_name":"Prateesh","last_name":"Goyal","full_name":"Goyal, Prateesh"}],"publist_id":"5565","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” ACM SIGPLAN Notices, vol. 50, no. 1, ACM, 2015, pp. 97–109, doi:10.1145/2676726.2676979.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, and P. Goyal, “Faster algorithms for algebraic path properties in recursive state machines with constant treewidth,” ACM SIGPLAN Notices, vol. 50, no. 1. ACM, pp. 97–109, 2015.","apa":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., & Goyal, P. (2015). Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. Mumbai, India: ACM. https://doi.org/10.1145/2676726.2676979","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 2015;50(1):97-109. doi:10.1145/2676726.2676979","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” ACM SIGPLAN Notices. ACM, 2015. https://doi.org/10.1145/2676726.2676979.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. 2015. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 50(1), 97–109."},"intvolume":" 50","month":"01","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1410.7724"}],"scopus_import":1,"oa_version":"Preprint","abstract":[{"lang":"eng","text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks."}],"ec_funded":1,"issue":"1","volume":50,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"821"}]},"language":[{"iso":"eng"}],"publication_status":"published","status":"public","conference":{"end_date":"2015-01-17","location":"Mumbai, India","start_date":"2015-01-15","name":"SIGPLAN: Symposium on Principles of Programming Languages"},"type":"journal_article","_id":"1602","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T12:01:58Z"},{"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publication_status":"published","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5445"},{"relation":"dissertation_contains","status":"public","id":"821"}]},"volume":50,"issue":"1","ec_funded":1,"oa_version":"None","abstract":[{"text":"We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs.","lang":"eng"}],"month":"01","intvolume":" 50","scopus_import":1,"date_updated":"2023-09-07T12:01:59Z","department":[{"_id":"KrCh"}],"_id":"1604","status":"public","pubrep_id":"523","type":"journal_article","conference":{"name":"SIGPLAN: Symposium on Principles of Programming Languages","location":"Mumbai, India","end_date":"2015-01-17","start_date":"2015-01-15"},"day":"01","publication":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT ","year":"2015","date_published":"2015-01-01T00:00:00Z","doi":"10.1145/2676726.2676968","date_created":"2018-12-11T11:52:59Z","page":"539 - 551","quality_controlled":"1","publisher":"ACM","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . ACM, 2015. https://doi.org/10.1145/2676726.2676968.","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT 50 (2015) 539–551.","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural analysis,” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1. ACM, pp. 539–551, 2015.","apa":"Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2015). Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . Mumbai, India: ACM. https://doi.org/10.1145/2676726.2676968","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 2015;50(1):539-551. doi:10.1145/2676726.2676968","mla":"Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1, ACM, 2015, pp. 539–51, doi:10.1145/2676726.2676968."},"title":"Quantitative interprocedural analysis","publist_id":"5563","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"}],"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}]},{"abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"oa_version":"Preprint","alternative_title":["LNCS"],"scopus_import":1,"main_file_link":[{"url":"http://arxiv.org/abs/1504.07384","open_access":"1"}],"month":"07","intvolume":" 9206","publication_status":"published","language":[{"iso":"eng"}],"related_material":{"record":[{"relation":"earlier_version","id":"5430","status":"public"},{"id":"5437","status":"public","relation":"earlier_version"},{"status":"public","id":"821","relation":"dissertation_contains"}]},"volume":9206,"ec_funded":1,"_id":"1607","type":"conference","conference":{"end_date":"2015-07-24","location":"San Francisco, CA, USA","start_date":"2015-07-18","name":"CAV: Computer Aided Verification"},"status":"public","date_updated":"2023-09-07T12:01:59Z","department":[{"_id":"KrCh"}],"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","publisher":"Springer","quality_controlled":"1","oa":1,"year":"2015","day":"16","page":"140 - 157","date_published":"2015-07-16T00:00:00Z","doi":"10.1007/978-3-319-21690-4_9","date_created":"2018-12-11T11:52:59Z","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. Vol. 9206, Springer, 2015, pp. 140–57, doi:10.1007/978-3-319-21690-4_9.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157). Presented at the CAV: Computer Aided Verification, San Francisco, CA, USA: Springer. https://doi.org/10.1007/978-3-319-21690-4_9","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157. doi:10.1007/978-3-319-21690-4_9","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in constant treewidth graphs,” presented at the CAV: Computer Aided Verification, San Francisco, CA, USA, 2015, vol. 9206, pp. 140–157.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,” 9206:140–57. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_9.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification, LNCS, vol. 9206, 140–157."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publist_id":"5560","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"title":"Faster algorithms for quantitative verification in constant treewidth graphs"},{"quality_controlled":"1","publisher":"IEEE","day":"15","publication":"Real-Time Systems Symposium","year":"2015","date_published":"2015-01-15T00:00:00Z","doi":"10.1109/RTSS.2014.9","date_created":"2018-12-11T11:53:37Z","page":"118 - 127","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” Real-Time Systems Symposium, vol. 2015, no. January, IEEE, 2015, pp. 118–27, doi:10.1109/RTSS.2014.9.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2015). A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In Real-Time Systems Symposium (Vol. 2015, pp. 118–127). Rome, Italy: IEEE. https://doi.org/10.1109/RTSS.2014.9","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In: Real-Time Systems Symposium. Vol 2015. IEEE; 2015:118-127. doi:10.1109/RTSS.2014.9","short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, in:, Real-Time Systems Symposium, IEEE, 2015, pp. 118–127.","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks,” in Real-Time Systems Symposium, Rome, Italy, 2015, vol. 2015, no. January, pp. 118–127.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” In Real-Time Systems Symposium, 2015:118–27. IEEE, 2015. https://doi.org/10.1109/RTSS.2014.9.","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2015. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium vol. 2015, 118–127."},"title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Alexander","full_name":"Kößler, Alexander","last_name":"Kößler"},{"full_name":"Schmid, Ulrich","last_name":"Schmid","first_name":"Ulrich"}],"publist_id":"5417","article_processing_charge":"No","oa_version":"None","abstract":[{"lang":"eng","text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application."}],"month":"01","intvolume":" 2015","scopus_import":1,"language":[{"iso":"eng"}],"publication_status":"published","related_material":{"record":[{"status":"public","id":"5423","relation":"earlier_version"},{"relation":"dissertation_contains","id":"821","status":"public"}]},"issue":"January","volume":2015,"_id":"1714","status":"public","type":"conference","conference":{"end_date":"2014-12-05","location":"Rome, Italy","start_date":"2014-12-02","name":"RTSS: Real-Time Systems Symposium"},"date_updated":"2023-09-07T12:01:59Z","department":[{"_id":"KrCh"}]},{"citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-340-v1-1.","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2015. Algorithms for algebraic path properties in concurrent systems of constant treewidth components, IST Austria, 24p.","mla":"Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015, doi:10.15479/AT:IST-2015-340-v1-1.","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A. (2015). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria. https://doi.org/10.15479/AT:IST-2015-340-v1-1","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria; 2015. doi:10.15479/AT:IST-2015-340-v1-1","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria, 2015.","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria, 2015."},"date_updated":"2023-09-19T14:36:19Z","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"full_name":"Goharshady, Amir","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"file_date_updated":"2020-07-14T12:46:56Z","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","department":[{"_id":"KrCh"}],"_id":"5441","type":"technical_report","status":"public","pubrep_id":"340","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","year":"2015","day":"11","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"df383dc62c94d7b2ea639aba088a76c6","file_id":"5531","file_size":861396,"date_updated":"2020-07-14T12:46:56Z","creator":"system","file_name":"IST-2015-340-v1+1_main.pdf","date_created":"2018-12-12T11:54:09Z"}],"language":[{"iso":"eng"}],"page":"24","date_published":"2015-07-11T00:00:00Z","doi":"10.15479/AT:IST-2015-340-v1-1","related_material":{"record":[{"status":"public","id":"1437","relation":"later_version"},{"status":"public","id":"5442","relation":"earlier_version"},{"relation":"later_version","id":"6009","status":"public"}]},"date_created":"2018-12-12T11:39:21Z","abstract":[{"text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"07"},{"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2014","day":"14","file":[{"file_size":670031,"date_updated":"2020-07-14T12:46:50Z","creator":"system","file_name":"IST-2014-187-v1+1_main_full_tech.pdf","date_created":"2018-12-12T11:54:25Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"c608e66030a4bf51d2d99b451f539b99","file_id":"5548"}],"language":[{"iso":"eng"}],"page":"34","doi":"10.15479/AT:IST-2014-187-v1-1","date_published":"2014-04-14T00:00:00Z","date_created":"2018-12-12T11:39:13Z","abstract":[{"lang":"eng","text":"We consider the reachability and shortest path problems on low tree-width graphs, with n nodes, m edges, and tree-width t, on a standard RAM with wordsize W. We use O to hide polynomial factors of the inverse of the Ackermann function. Our main contributions are three fold:\r\n1. For reachability, we present an algorithm that requires O(n·t2·log(n/t)) preprocessing time, O(n·(t·log(n/t))/W) space, and O(t/W) time for pair queries and O((n·t)/W) time for single-source queries. Note that for constant t our algorithm uses O(n·logn) time for preprocessing; and O(n/W) time for single-source queries, which is faster than depth first search/breath first search (after the preprocessing).\r\n2. We present an algorithm for shortest path that requires O(n·t2) preprocessing time, O(n·t) space, and O(t2) time for pair queries and O(n·t) time single-source queries.\r\n3. We give a space versus query time trade-off algorithm for shortest path that, given any constant >0, requires O(n·t2) preprocessing time, O(n·t2) space, and O(n1−·t2) time for pair queries.\r\nOur algorithms improve all existing results, and use very simple data structures."}],"oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"04","date_updated":"2021-01-12T08:02:03Z","citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-187-v1-1","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2014). Improved algorithms for reachability and shortest path on low tree-width graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-187-v1-1","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs, IST Austria, 2014.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Improved algorithms for reachability and shortest path on low tree-width graphs. IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-187-v1-1.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Improved algorithms for reachability and shortest path on low tree-width graphs, IST Austria, 34p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-187-v1-1."},"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"department":[{"_id":"KrCh"}],"title":"Improved algorithms for reachability and shortest path on low tree-width graphs","file_date_updated":"2020-07-14T12:46:50Z","_id":"5419","type":"technical_report","status":"public","pubrep_id":"187"},{"related_material":{"record":[{"id":"1714","status":"public","relation":"later_version"}]},"doi":"10.15479/AT:IST-2014-300-v1-1","date_published":"2014-07-29T00:00:00Z","date_created":"2018-12-12T11:39:15Z","page":"14","day":"29","file":[{"date_updated":"2020-07-14T12:46:50Z","file_size":1270021,"creator":"system","date_created":"2018-12-12T11:53:53Z","file_name":"IST-2014-300-v1+1_main.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"4b8fde4d9ef6653837f6803921d83032","file_id":"5514"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","year":"2014","publication_status":"published","month":"07","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"oa_version":"Published Version","abstract":[{"text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm- deadline real-time tasks based on multi-objective graphs: Given a taskset and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. a clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including D(over), that have been proposed in the past, for various tasksets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are tasksets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application. ","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:50Z","department":[{"_id":"KrCh"}],"title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kössler","full_name":"Kössler, Alexander","first_name":"Alexander"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"first_name":"Ulrich","last_name":"Schmid","full_name":"Schmid, Ulrich"}],"ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:11:15Z","citation":{"mla":"Chatterjee, Krishnendu, et al. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria, 2014, doi:10.15479/AT:IST-2014-300-v1-1.","ieee":"K. Chatterjee, A. Kössler, A. Pavlogiannis, and U. Schmid, A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. IST Austria, 2014.","short":"K. Chatterjee, A. Kössler, A. Pavlogiannis, U. Schmid, A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks, IST Austria, 2014.","apa":"Chatterjee, K., Kössler, A., Pavlogiannis, A., & Schmid, U. (2014). A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. IST Austria. https://doi.org/10.15479/AT:IST-2014-300-v1-1","ama":"Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria; 2014. doi:10.15479/AT:IST-2014-300-v1-1","chicago":"Chatterjee, Krishnendu, Alexander Kössler, Andreas Pavlogiannis, and Ulrich Schmid. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-300-v1-1.","ista":"Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. 2014. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks, IST Austria, 14p."},"status":"public","pubrep_id":"300","type":"technical_report","_id":"5423"},{"page":"24","date_published":"2014-11-05T00:00:00Z","doi":"10.15479/AT:IST-2014-314-v1-1","date_created":"2018-12-12T11:39:16Z","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","year":"2014","publication_status":"published","day":"05","file":[{"date_created":"2018-12-12T11:53:10Z","file_name":"IST-2014-314-v1+1_long.pdf","creator":"system","date_updated":"2020-07-14T12:46:52Z","file_size":405561,"file_id":"5471","checksum":"9d3b90bf4fff74664f182f2d95ef727a","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"month":"11","abstract":[{"lang":"eng","text":"We consider graphs with n nodes together with their tree-decomposition that has b = O ( n ) bags and width t , on the standard RAM computational model with wordsize W = Θ (log n ) . Our contributions are two-fold: Our first contribution is an algorithm that given a graph and its tree-decomposition as input, computes a binary and balanced tree-decomposition of width at most 4 · t + 3 of the graph in O ( b ) time and space, improving a long-standing (from 1992) bound of O ( n · log n ) time for constant treewidth graphs. Our second contribution is on reachability queries for low treewidth graphs. We build on our tree-balancing algorithm and present a data-structure for graph reachability that requires O ( n · t 2 ) preprocessing time, O ( n · t ) space, and O ( d t/ log n e ) time for pair queries, and O ( n · t · log t/ log n ) time for single-source queries. For constant t our data-structure uses O ( n ) time for preprocessing, O (1) time for pair queries, and O ( n/ log n ) time for single-source queries. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries."}],"oa_version":"Published Version","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"}],"department":[{"_id":"KrCh"}],"title":"Optimal tree-decomposition balancing and reachability on low treewidth graphs","file_date_updated":"2020-07-14T12:46:52Z","date_updated":"2021-01-12T08:02:09Z","citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-314-v1-1.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Optimal tree-decomposition balancing and reachability on low treewidth graphs, IST Austria, 24p.","mla":"Chatterjee, Krishnendu, et al. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-314-v1-1.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Optimal tree-decomposition balancing and reachability on low treewidth graphs. IST Austria, 2014.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs, IST Austria, 2014.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2014). Optimal tree-decomposition balancing and reachability on low treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-314-v1-1","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-314-v1-1"},"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"technical_report","status":"public","pubrep_id":"314","_id":"5427"},{"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"article_number":"7p","title":"The time scale of evolutionary innovation","publist_id":"5012","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"last_name":"Adlam","full_name":"Adlam, Ben","first_name":"Ben"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology, vol. 10, no. 9, 7p, Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Nowak, PLoS Computational Biology 10 (2014).","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Nowak, “The time scale of evolutionary innovation,” PLoS Computational Biology, vol. 10, no. 9. Public Library of Science, 2014.","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. The time scale of evolutionary innovation. PLoS Computational Biology. 2014;10(9). doi:10.1371/journal.pcbi.1003818","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Nowak, M. (2014). The time scale of evolutionary innovation. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Nowak. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology. Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. 2014. The time scale of evolutionary innovation. PLoS Computational Biology. 10(9), 7p."},"oa":1,"publisher":"Public Library of Science","quality_controlled":"1","date_created":"2018-12-11T11:55:22Z","doi":"10.1371/journal.pcbi.1003818","date_published":"2014-09-11T00:00:00Z","publication":"PLoS Computational Biology","day":"11","year":"2014","has_accepted_license":"1","pubrep_id":"440","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","_id":"2039","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:26Z","ddc":["510"],"date_updated":"2023-02-23T14:06:36Z","intvolume":" 10","month":"09","scopus_import":1,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"A fundamental question in biology is the following: what is the time scale that is needed for evolutionary innovations? There are many results that characterize single steps in terms of the fixation time of new mutants arising in populations of certain size and structure. But here we ask a different question, which is concerned with the much longer time scale of evolutionary trajectories: how long does it take for a population exploring a fitness landscape to find target sequences that encode new biological functions? Our key variable is the length, (Formula presented.) of the genetic sequence that undergoes adaptation. In computer science there is a crucial distinction between problems that require algorithms which take polynomial or exponential time. The latter are considered to be intractable. Here we develop a theoretical approach that allows us to estimate the time of evolution as function of (Formula presented.) We show that adaptation on many fitness landscapes takes time that is exponential in (Formula presented.) even if there are broad selection gradients and many targets uniformly distributed in sequence space. These negative results lead us to search for specific mechanisms that allow evolution to work on polynomial time scales. We study a regeneration process and show that it enables evolution to work in polynomial time."}],"ec_funded":1,"issue":"9","volume":10,"related_material":{"record":[{"id":"9739","status":"public","relation":"research_data"}]},"language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T10:11:35Z","file_name":"IST-2016-440-v1+1_journal.pcbi.1003818.pdf","creator":"system","date_updated":"2020-07-14T12:45:26Z","file_size":1399093,"file_id":"4890","checksum":"712d4c5787ddf97809cfc962507f0738","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"publication_status":"published"},{"type":"research_data_reference","status":"public","_id":"9739","article_processing_charge":"No","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"first_name":"Ben","last_name":"Adlam","full_name":"Adlam, Ben"},{"full_name":"Novak, Martin","last_name":"Novak","first_name":"Martin"}],"department":[{"_id":"KrCh"}],"title":"Detailed proofs for “The time scale of evolutionary innovation”","date_updated":"2023-02-23T10:25:37Z","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Novak. “Detailed Proofs for ‘The Time Scale of Evolutionary Innovation.’” Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.s001.","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. 2014. Detailed proofs for “The time scale of evolutionary innovation”, Public Library of Science, 10.1371/journal.pcbi.1003818.s001.","mla":"Chatterjee, Krishnendu, et al. Detailed Proofs for “The Time Scale of Evolutionary Innovation.” Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.s001.","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Novak, M. (2014). Detailed proofs for “The time scale of evolutionary innovation.” Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818.s001","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. Detailed proofs for “The time scale of evolutionary innovation.” 2014. doi:10.1371/journal.pcbi.1003818.s001","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Novak, (2014).","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Novak, “Detailed proofs for ‘The time scale of evolutionary innovation.’” Public Library of Science, 2014."},"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","publisher":"Public Library of Science","month":"09","oa_version":"Published Version","date_created":"2021-07-28T08:13:57Z","doi":"10.1371/journal.pcbi.1003818.s001","date_published":"2014-09-11T00:00:00Z","related_material":{"record":[{"relation":"used_in_publication","id":"2039","status":"public"}]},"year":"2014","day":"11"},{"publist_id":"5835","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"title":"Distributed synthesis for LTL fragments","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"citation":{"ista":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL fragments. 13th International Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 18–25.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. “Distributed Synthesis for LTL Fragments.” In 13th International Conference on Formal Methods in Computer-Aided Design, 18–25. IEEE, 2013. https://doi.org/10.1109/FMCAD.2013.6679386.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, in:, 13th International Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, “Distributed synthesis for LTL fragments,” in 13th International Conference on Formal Methods in Computer-Aided Design, Portland, OR, United States, 2013, pp. 18–25.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013). Distributed synthesis for LTL fragments. In 13th International Conference on Formal Methods in Computer-Aided Design (pp. 18–25). Portland, OR, United States: IEEE. https://doi.org/10.1109/FMCAD.2013.6679386","ama":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed synthesis for LTL fragments. In: 13th International Conference on Formal Methods in Computer-Aided Design. IEEE; 2013:18-25. doi:10.1109/FMCAD.2013.6679386","mla":"Chatterjee, Krishnendu, et al. “Distributed Synthesis for LTL Fragments.” 13th International Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25, doi:10.1109/FMCAD.2013.6679386."},"date_updated":"2023-02-23T12:24:53Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"start_date":"2013-10-20","location":"Portland, OR, United States","end_date":"2013-10-23","name":"FMCAD: Formal Methods in Computer-Aided Design"},"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"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"status":"public","_id":"1376","page":"18 - 25","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5406"}]},"date_published":"2013-12-11T00:00:00Z","doi":"10.1109/FMCAD.2013.6679386","date_created":"2018-12-11T11:51:40Z","ec_funded":1,"publication_status":"published","year":"2013","day":"11","publication":"13th International Conference on Formal Methods in Computer-Aided Design","language":[{"iso":"eng"}],"quality_controlled":"1","publisher":"IEEE","month":"12","abstract":[{"text":"We consider the distributed synthesis problem for temporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTL and our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3) Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.","lang":"eng"}],"oa_version":"None"},{"oa":1,"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"month":"07","abstract":[{"text":"We consider the distributed synthesis problem fortemporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTLand our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3)Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.","lang":"eng"}],"oa_version":"Published Version","page":"11","date_created":"2018-12-12T11:39:09Z","doi":"10.15479/AT:IST-2013-130-v1-1","date_published":"2013-07-08T00:00:00Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"1376"}]},"publication_status":"published","year":"2013","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","language":[{"iso":"eng"}],"day":"08","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"5540","checksum":"855513ebaf6f72228800c5fdb522f93c","file_size":467895,"date_updated":"2020-07-14T12:46:45Z","creator":"system","file_name":"IST-2013-130-v1+1_Distributed_Synthesis.pdf","date_created":"2018-12-12T11:54:18Z"}],"type":"technical_report","pubrep_id":"130","status":"public","_id":"5406","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"file_date_updated":"2020-07-14T12:46:45Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Distributed synthesis for LTL Fragments","date_updated":"2023-02-21T17:01:26Z","citation":{"mla":"Chatterjee, Krishnendu, et al. Distributed Synthesis for LTL Fragments. IST Austria, 2013, doi:10.15479/AT:IST-2013-130-v1-1.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013). Distributed synthesis for LTL Fragments. IST Austria. https://doi.org/10.15479/AT:IST-2013-130-v1-1","ama":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed Synthesis for LTL Fragments. IST Austria; 2013. doi:10.15479/AT:IST-2013-130-v1-1","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed synthesis for LTL Fragments. IST Austria, 2013.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. Distributed Synthesis for LTL Fragments. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-130-v1-1.","ista":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL Fragments, IST Austria, 11p."},"ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"}]