[{"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"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.","lang":"eng"}],"publication_status":"published","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.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57, Springer, 2021, pp. 401–28, doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. 2021;57:401-428. doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>. Springer, 2021. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System Design</i>, vol. 57. Springer, pp. 401–428, 2021.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>"},"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.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"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"}],"quality_controlled":"1","oa_version":"Preprint","_id":"9393","publication_identifier":{"eissn":["1572-8102"],"issn":["0925-9856"]},"volume":57,"oa":1,"date_updated":"2023-10-10T11:13:20Z","article_processing_charge":"No","arxiv":1,"title":"Faster algorithms for quantitative verification in bounded treewidth graphs","external_id":{"isi":["000645490300001"],"arxiv":["1504.07384"]},"ec_funded":1,"doi":"10.1007/s10703-021-00373-5","year":"2021","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.07384"}],"isi":1,"status":"public","intvolume":"        57","type":"journal_article","day":"01","page":"401-428","publication":"Formal Methods in System Design","language":[{"iso":"eng"}],"publisher":"Springer","scopus_import":"1","article_type":"original","date_published":"2021-09-01T00:00:00Z","month":"09","date_created":"2021-05-16T22:01:47Z","department":[{"_id":"KrCh"}]},{"language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1","date_published":"2021-06-29T00:00:00Z","article_type":"original","month":"06","date_created":"2021-07-11T22:01:15Z","file":[{"content_type":"application/pdf","relation":"main_file","creator":"cziletti","file_id":"9692","success":1,"date_updated":"2021-07-19T13:02:20Z","access_level":"open_access","file_name":"2021_NatCoom_Tkadlec.pdf","file_size":628992,"date_created":"2021-07-19T13:02:20Z","checksum":"5767418926a7f7fb76151de29473dae0"}],"department":[{"_id":"KrCh"}],"has_accepted_license":"1","status":"public","intvolume":"        12","type":"journal_article","day":"29","file_date_updated":"2021-07-19T13:02:20Z","issue":"1","publication":"Nature Communications","title":"Fast and strong amplifiers of natural selection","external_id":{"isi":["000671752100003"],"pmid":["34188036"]},"ec_funded":1,"doi":"10.1038/s41467-021-24271-w","year":"2021","ddc":["510"],"article_number":"4009","isi":1,"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"author":[{"first_name":"Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"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."}],"publication_status":"published","citation":{"chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Fast and Strong Amplifiers of Natural Selection.” <i>Nature Communications</i>. Springer Nature, 2021. <a href=\"https://doi.org/10.1038/s41467-021-24271-w\">https://doi.org/10.1038/s41467-021-24271-w</a>.","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2021). Fast and strong amplifiers of natural selection. <i>Nature Communications</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41467-021-24271-w\">https://doi.org/10.1038/s41467-021-24271-w</a>","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Fast and strong amplifiers of natural selection,” <i>Nature Communications</i>, vol. 12, no. 1. Springer Nature, 2021.","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Nature Communications 12 (2021).","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2021. Fast and strong amplifiers of natural selection. Nature Communications. 12(1), 4009.","mla":"Tkadlec, Josef, et al. “Fast and Strong Amplifiers of Natural Selection.” <i>Nature Communications</i>, vol. 12, no. 1, 4009, Springer Nature, 2021, doi:<a href=\"https://doi.org/10.1038/s41467-021-24271-w\">10.1038/s41467-021-24271-w</a>.","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Fast and strong amplifiers of natural selection. <i>Nature Communications</i>. 2021;12(1). doi:<a href=\"https://doi.org/10.1038/s41467-021-24271-w\">10.1038/s41467-021-24271-w</a>"},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","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.","project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"}],"quality_controlled":"1","oa_version":"Published Version","pmid":1,"_id":"9640","publication_identifier":{"eissn":["20411723"]},"date_updated":"2025-07-14T09:10:05Z","volume":12,"oa":1,"article_processing_charge":"No"},{"status":"public","supervisor":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"type":"dissertation","day":"17","page":"171","file_date_updated":"2022-12-20T23:30:08Z","language":[{"iso":"eng"}],"publisher":"Institute of Science and Technology Austria","date_published":"2021-11-17T00:00:00Z","month":"11","date_created":"2021-11-15T17:12:57Z","file":[{"creator":"lschmid","file_id":"10305","content_type":"application/zip","relation":"source_file","date_created":"2021-11-18T12:41:46Z","checksum":"86a05b430756ca12ae8107b6e6f3c1e5","file_name":"submission_new.zip","file_size":29703124,"date_updated":"2022-12-20T23:30:08Z","access_level":"closed","embargo_to":"open_access"},{"relation":"main_file","content_type":"application/pdf","creator":"lschmid","file_id":"10306","access_level":"open_access","date_updated":"2022-12-20T23:30:08Z","embargo":"2022-10-18","file_size":8320985,"file_name":"thesis_new_upload.pdf","checksum":"d940af042e94660c6b6a7b4f0b184d47","date_created":"2021-11-18T12:59:15Z"}],"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"degree_awarded":"PhD","has_accepted_license":"1","author":[{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6978-7329","last_name":"Schmid","full_name":"Schmid, Laura","first_name":"Laura"}],"abstract":[{"text":"Indirect reciprocity in evolutionary game theory is a prominent mechanism for explaining the evolution of cooperation among unrelated individuals. In contrast to direct reciprocity, which is based on individuals meeting repeatedly, and conditionally cooperating by using their own experiences, indirect reciprocity is based on individuals’ reputations. If a player helps another, this increases the helper’s public standing, benefitting them in the future. This lets cooperation in the population emerge without individuals having to meet more than once. While the two modes of reciprocity are intertwined, they are difficult to compare. Thus, they are usually studied in isolation. Direct reciprocity can maintain cooperation with simple strategies, and is robust against noise even when players do not remember more\r\nthan their partner’s last action. Meanwhile, indirect reciprocity requires its successful strategies, or social norms, to be more complex. Exhaustive search previously identified eight such norms, called the “leading eight”, which excel at maintaining cooperation. However, as the first result of this thesis, we show that the leading eight break down once we remove the fundamental assumption that information is synchronized and public, such that everyone agrees on reputations. Once we consider a more realistic scenario of imperfect information, where reputations are private, and individuals occasionally misinterpret or miss observations, the leading eight do not promote cooperation anymore. Instead, minor initial disagreements can proliferate, fragmenting populations into subgroups. In a next step, we consider ways to mitigate this issue. We first explore whether introducing “generosity” can stabilize cooperation when players use the leading eight strategies in noisy environments. This approach of modifying strategies to include probabilistic elements for coping with errors is known to work well in direct reciprocity. However, as we show here, it fails for the more complex norms of indirect reciprocity. Imperfect information still prevents cooperation from evolving. On the other hand, we succeeded to show in this thesis that modifying the leading eight to use “quantitative assessment”, i.e. tracking reputation scores on a scale beyond good and bad, and making overall judgments of others based on a threshold, is highly successful, even when noise increases in the environment. Cooperation can flourish when reputations\r\nare more nuanced, and players have a broader understanding what it means to be “good.” Finally, we present a single theoretical framework that unites the two modes of reciprocity despite their differences. Within this framework, we identify a novel simple and successful strategy for indirect reciprocity, which can cope with noisy environments and has an analogue in direct reciprocity. We can also analyze decision making when different sources of information are available. Our results help highlight that for sustaining cooperation, already the most simple rules of reciprocity can be sufficient.","lang":"eng"}],"citation":{"chicago":"Schmid, Laura. “Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/at:ista:10293\">https://doi.org/10.15479/at:ista:10293</a>.","ieee":"L. Schmid, “Evolution of cooperation via (in)direct reciprocity under imperfect information,” Institute of Science and Technology Austria, 2021.","apa":"Schmid, L. (2021). <i>Evolution of cooperation via (in)direct reciprocity under imperfect information</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:10293\">https://doi.org/10.15479/at:ista:10293</a>","short":"L. Schmid, Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information, Institute of Science and Technology Austria, 2021.","ista":"Schmid L. 2021. Evolution of cooperation via (in)direct reciprocity under imperfect information. Institute of Science and Technology Austria.","ama":"Schmid L. Evolution of cooperation via (in)direct reciprocity under imperfect information. 2021. doi:<a href=\"https://doi.org/10.15479/at:ista:10293\">10.15479/at:ista:10293</a>","mla":"Schmid, Laura. <i>Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/at:ista:10293\">10.15479/at:ista:10293</a>."},"publication_status":"published","oa_version":"Published Version","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"},{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"issn":["2663-337X"]},"_id":"10293","article_processing_charge":"No","date_updated":"2025-07-14T09:10:09Z","oa":1,"title":"Evolution of cooperation via (in)direct reciprocity under imperfect information","ec_funded":1,"year":"2021","doi":"10.15479/at:ista:10293","ddc":["519","576"],"related_material":{"record":[{"status":"public","id":"9997","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"2"},{"id":"9402","relation":"part_of_dissertation","status":"public"}]},"alternative_title":["ISTA Thesis"]},{"doi":"10.1007/978-3-030-45237-7_5","year":"2020","title":"How many bits does it take to quantize your neural network?","alternative_title":["LNCS"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"related_material":{"record":[{"id":"11362","relation":"dissertation_contains","status":"public"}]},"ddc":["000"],"publication_status":"published","citation":{"chicago":"Giacobbe, Mirco, Thomas A Henzinger, and Mathias Lechner. “How Many Bits Does It Take to Quantize Your Neural Network?” In <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 12079:79–97. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">https://doi.org/10.1007/978-3-030-45237-7_5</a>.","apa":"Giacobbe, M., Henzinger, T. A., &#38; Lechner, M. (2020). How many bits does it take to quantize your neural network? In <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 12079, pp. 79–97). Dublin, Ireland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">https://doi.org/10.1007/978-3-030-45237-7_5</a>","ieee":"M. Giacobbe, T. A. Henzinger, and M. Lechner, “How many bits does it take to quantize your neural network?,” in <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Dublin, Ireland, 2020, vol. 12079, pp. 79–97.","ista":"Giacobbe M, Henzinger TA, Lechner M. 2020. How many bits does it take to quantize your neural network? International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 12079, 79–97.","short":"M. Giacobbe, T.A. Henzinger, M. Lechner, in:, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2020, pp. 79–97.","mla":"Giacobbe, Mirco, et al. “How Many Bits Does It Take to Quantize Your Neural Network?” <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 12079, Springer Nature, 2020, pp. 79–97, doi:<a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">10.1007/978-3-030-45237-7_5</a>.","ama":"Giacobbe M, Henzinger TA, Lechner M. How many bits does it take to quantize your neural network? In: <i>International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 12079. Springer Nature; 2020:79-97. doi:<a href=\"https://doi.org/10.1007/978-3-030-45237-7_5\">10.1007/978-3-030-45237-7_5</a>"},"abstract":[{"lang":"eng","text":"Quantization converts neural networks into low-bit fixed-point computations which can be carried out by efficient integer-only hardware, and is standard practice for the deployment of neural networks on real-time embedded devices. However, like their real-numbered counterpart, quantized networks are not immune to malicious misclassification caused by adversarial attacks. We investigate how quantization affects a network’s robustness to adversarial attacks, which is a formal verification question. We show that neither robustness nor non-robustness are monotonic with changing the number of bits for the representation and, also, neither are preserved by quantization from a real-numbered network. For this reason, we introduce a verification method for quantized neural networks which, using SMT solving over bit-vectors, accounts for their exact, bit-precise semantics. We built a tool and analyzed the effect of quantization on a classifier for the MNIST dataset. We demonstrate that, compared to our method, existing methods for the analysis of real-numbered networks often derive false conclusions about their quantizations, both when determining robustness and when detecting attacks, and that existing methods for quantized networks often miss attacks. Furthermore, we applied our method beyond robustness, showing how the number of bits in quantization enlarges the gender bias of a predictor for students’ grades."}],"author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","last_name":"Giacobbe"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"}],"volume":12079,"oa":1,"date_updated":"2023-06-23T07:01:11Z","article_processing_charge":"No","_id":"7808","publication_identifier":{"eissn":["16113349"],"isbn":["9783030452360"],"issn":["03029743"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"}],"quality_controlled":"1","oa_version":"Published Version","month":"04","date_published":"2020-04-17T00:00:00Z","publisher":"Springer Nature","scopus_import":1,"language":[{"iso":"eng"}],"has_accepted_license":"1","department":[{"_id":"ToHe"}],"conference":{"start_date":"2020-04-25","end_date":"2020-04-30","location":"Dublin, Ireland","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_created":"2020-05-10T22:00:49Z","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"7893","creator":"dernst","date_updated":"2020-07-14T12:48:03Z","access_level":"open_access","file_name":"2020_TACAS_Giacobbe.pdf","file_size":2744030,"date_created":"2020-05-26T12:48:15Z","checksum":"f19905a42891fe5ce93d69143fa3f6fb"}],"day":"17","type":"conference","intvolume":"     12079","status":"public","publication":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","file_date_updated":"2020-07-14T12:48:03Z","page":"79-97"},{"article_processing_charge":"No","volume":12075,"date_updated":"2025-06-02T08:53:42Z","oa":1,"quality_controlled":"1","oa_version":"Published Version","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_identifier":{"eissn":["16113349"],"isbn":["9783030449131"],"issn":["03029743"]},"_id":"7810","citation":{"apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2020). Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In <i>European Symposium on Programming</i> (Vol. 12075, pp. 112–140). Dublin, Ireland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">https://doi.org/10.1007/978-3-030-44914-8_5</a>","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal and perfectly parallel algorithms for on-demand data-flow analysis,” in <i>European Symposium on Programming</i>, Dublin, Ireland, 2020, vol. 12075, pp. 112–140.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” In <i>European Symposium on Programming</i>, 12075:112–40. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">https://doi.org/10.1007/978-3-030-44914-8_5</a>.","mla":"Chatterjee, Krishnendu, et al. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” <i>European Symposium on Programming</i>, vol. 12075, Springer Nature, 2020, pp. 112–40, doi:<a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">10.1007/978-3-030-44914-8_5</a>.","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In: <i>European Symposium on Programming</i>. Vol 12075. Springer Nature; 2020:112-140. doi:<a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">10.1007/978-3-030-44914-8_5</a>","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.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 112–140."},"publication_status":"published","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar"},{"first_name":"Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"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."}],"isi":1,"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"alternative_title":["LNCS"],"ddc":["000"],"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"doi":"10.1007/978-3-030-44914-8_5","year":"2020","title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","external_id":{"isi":["000681656800005"]},"page":"112-140","file_date_updated":"2020-07-14T12:48:03Z","publication":"European Symposium on Programming","type":"conference","day":"18","status":"public","intvolume":"     12075","department":[{"_id":"KrCh"}],"has_accepted_license":"1","date_created":"2020-05-10T22:00:50Z","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:48:03Z","file_size":651250,"file_name":"2020_LNCS_Chatterjee.pdf","checksum":"8618b80f4cf7b39a60e61a6445ad9807","date_created":"2020-05-26T13:34:48Z","relation":"main_file","content_type":"application/pdf","creator":"dernst","file_id":"7895"}],"conference":{"start_date":"2020-04-25","location":"Dublin, Ireland","end_date":"2020-04-30","name":"ESOP: Programming Languages and Systems"},"date_published":"2020-04-18T00:00:00Z","month":"04","language":[{"iso":"eng"}],"scopus_import":"1","publisher":"Springer Nature"},{"citation":{"apa":"Chatterjee, K., Fu, H., Goharshady, A. K., &#38; Goharshady, E. K. (2020). Polynomial invariant generation for non-deterministic recursive programs. In <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i> (pp. 672–687). London, United Kingdom: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3385412.3385969\">https://doi.org/10.1145/3385412.3385969</a>","ieee":"K. Chatterjee, H. Fu, A. K. Goharshady, and E. K. Goharshady, “Polynomial invariant generation for non-deterministic recursive programs,” in <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, London, United Kingdom, 2020, pp. 672–687.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. “Polynomial Invariant Generation for Non-Deterministic Recursive Programs.” In <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, 672–87. Association for Computing Machinery, 2020. <a href=\"https://doi.org/10.1145/3385412.3385969\">https://doi.org/10.1145/3385412.3385969</a>.","mla":"Chatterjee, Krishnendu, et al. “Polynomial Invariant Generation for Non-Deterministic Recursive Programs.” <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2020, pp. 672–87, doi:<a href=\"https://doi.org/10.1145/3385412.3385969\">10.1145/3385412.3385969</a>.","ama":"Chatterjee K, Fu H, Goharshady AK, Goharshady EK. Polynomial invariant generation for non-deterministic recursive programs. In: <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2020:672-687. doi:<a href=\"https://doi.org/10.1145/3385412.3385969\">10.1145/3385412.3385969</a>","ista":"Chatterjee K, Fu H, Goharshady AK, Goharshady EK. 2020. Polynomial invariant generation for non-deterministic recursive programs. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 672–687.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, E.K. Goharshady, in:, Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2020, pp. 672–687."},"publication_status":"published","abstract":[{"lang":"eng","text":"We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set.\r\n\r\nOn the theoretical side, the worst-case complexity of our approach is subexponential, whereas the worst-case complexity of the previous complete method (Kapur, ACA 2004) is doubly-exponential. Even when restricted to linear invariants, the best previous complexity for complete invariant generation is exponential (Colon et al, CAV 2003). On the practical side, we reduce the invariant generation problem to quadratic programming (QCLP), which is a classical optimization problem with many industrial solvers. We demonstrate the applicability of our approach by providing experimental results on several academic benchmarks. To the best of our knowledge, the only previous invariant generation method that provides completeness guarantees for invariants consisting of polynomial inequalities is (Kapur, ACA 2004), which relies on quantifier elimination and cannot even handle toy programs such as our running example."}],"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ehsan Kafshdar","full_name":"Goharshady, Ehsan Kafshdar","last_name":"Goharshady"}],"arxiv":1,"article_processing_charge":"No","date_updated":"2025-06-02T08:53:42Z","oa":1,"publication_identifier":{"isbn":["9781450376136"]},"_id":"8089","quality_controlled":"1","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1145/3385412.3385969","year":"2020","title":"Polynomial invariant generation for non-deterministic recursive programs","external_id":{"arxiv":["1902.04373"],"isi":["000614622300045"]},"isi":1,"main_file_link":[{"url":"https://arxiv.org/abs/1902.04373","open_access":"1"}],"related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"day":"11","type":"conference","status":"public","publication":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation","page":"672-687","month":"06","date_published":"2020-06-11T00:00:00Z","scopus_import":"1","publisher":"Association for Computing Machinery","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"conference":{"end_date":"2020-06-20","location":"London, United Kingdom","name":"PLDI: Programming Language Design and Implementation","start_date":"2020-06-15"},"date_created":"2020-07-05T22:00:45Z"},{"article_processing_charge":"No","oa":1,"date_updated":"2023-08-22T13:27:32Z","arxiv":1,"oa_version":"Preprint","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25C5A090-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z00312"},{"call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411"}],"quality_controlled":"1","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"8287","citation":{"ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability analysis of linear hybrid systems via block decomposition,” in <i>Proceedings of the International Conference on Embedded Software</i>, Virtual , 2020.","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., &#38; Schilling, C. (2020). Reachability analysis of linear hybrid systems via block decomposition. In <i>Proceedings of the International Conference on Embedded Software</i>. Virtual .","chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” In <i>Proceedings of the International Conference on Embedded Software</i>, 2020.","mla":"Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” <i>Proceedings of the International Conference on Embedded Software</i>, 2020.","ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis of linear hybrid systems via block decomposition. In: <i>Proceedings of the International Conference on Embedded Software</i>. ; 2020.","short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the International Conference on Embedded Software, 2020.","ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2020. Reachability analysis of linear hybrid systems via block decomposition. Proceedings of the International Conference on Embedded Software. EMSOFT: International Conference on Embedded Software."},"publication_status":"published","keyword":["reachability","hybrid systems","decomposition"],"author":[{"first_name":"Sergiy","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov"},{"first_name":"Marcelo","full_name":"Forets, Marcelo","last_name":"Forets"},{"first_name":"Goran","full_name":"Frehse, Goran","last_name":"Frehse"},{"last_name":"Potomkin","full_name":"Potomkin, Kostiantyn","first_name":"Kostiantyn"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","last_name":"Schilling","full_name":"Schilling, Christian","first_name":"Christian"}],"abstract":[{"text":"Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this paper, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.","lang":"eng"}],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"related_material":{"record":[{"status":"public","id":"8790","relation":"later_version"}]},"ec_funded":1,"year":"2020","title":"Reachability analysis of linear hybrid systems via block decomposition","external_id":{"arxiv":["1905.02458"]},"file_date_updated":"2020-08-24T12:53:15Z","publication":"Proceedings of the International Conference on Embedded Software","type":"conference","status":"public","department":[{"_id":"ToHe"}],"has_accepted_license":"1","date_created":"2020-08-24T12:56:20Z","file":[{"date_updated":"2020-08-24T12:53:15Z","access_level":"open_access","date_created":"2020-08-24T12:53:15Z","checksum":"d19e97d0f8a3a441dc078ec812297d75","file_name":"2020EMSOFT.pdf","file_size":696384,"creator":"cschilli","file_id":"8288","content_type":"application/pdf","relation":"main_file","success":1}],"conference":{"end_date":"2020-09-25","name":"EMSOFT: International Conference on Embedded Software","location":"Virtual ","start_date":"2020-09-20"},"date_published":"2020-01-01T00:00:00Z","language":[{"iso":"eng"}]},{"intvolume":"       171","status":"public","day":"06","type":"conference","publication":"31st International Conference on Concurrency Theory","file_date_updated":"2020-10-05T14:04:25Z","scopus_import":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","language":[{"iso":"eng"}],"month":"08","date_published":"2020-08-06T00:00:00Z","conference":{"name":"CONCUR: Conference on Concurrency Theory","end_date":"2020-09-04","location":"Virtual","start_date":"2020-09-01"},"date_created":"2020-10-04T22:01:36Z","file":[{"success":1,"creator":"dernst","file_id":"8610","content_type":"application/pdf","relation":"main_file","date_created":"2020-10-05T14:04:25Z","checksum":"5039752f644c4b72b9361d21a5e31baf","file_name":"2020_LIPIcsCONCUR_Chatterjee.pdf","file_size":601231,"date_updated":"2020-10-05T14:04:25Z","access_level":"open_access"}],"has_accepted_license":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"abstract":[{"text":"A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.","lang":"eng"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan"}],"citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2020). Multi-dimensional long-run average problems for vector addition systems with states. In <i>31st International Conference on Concurrency Theory</i> (Vol. 171). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Multi-dimensional long-run average problems for vector addition systems with states,” in <i>31st International Conference on Concurrency Theory</i>, Virtual, 2020, vol. 171.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” In <i>31st International Conference on Concurrency Theory</i>, Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Multi-dimensional long-run average problems for vector addition systems with states. In: <i>31st International Conference on Concurrency Theory</i>. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>","mla":"Chatterjee, Krishnendu, et al. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” <i>31st International Conference on Concurrency Theory</i>, vol. 171, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2020. Multi-dimensional long-run average problems for vector addition systems with states. 31st International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 171, 23.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020."},"publication_status":"published","publication_identifier":{"isbn":["9783959771603"],"issn":["18688969"]},"_id":"8600","quality_controlled":"1","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"article_processing_charge":"No","date_updated":"2021-01-12T08:20:15Z","volume":171,"oa":1,"external_id":{"arxiv":["2007.08917"]},"title":"Multi-dimensional long-run average problems for vector addition systems with states","doi":"10.4230/LIPIcs.CONCUR.2020.23","year":"2020","ddc":["000"],"tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","short":"CC BY (3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"alternative_title":["LIPIcs"],"article_number":"23"},{"date_published":"2020-10-12T00:00:00Z","month":"10","language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1","department":[{"_id":"KrCh"}],"has_accepted_license":"1","file":[{"date_updated":"2020-11-06T07:41:03Z","access_level":"open_access","file_name":"2020_LNCS_ATVA_Asadi_accepted.pdf","file_size":726648,"date_created":"2020-11-06T07:41:03Z","checksum":"ae83f27e5b189d5abc2e7514f1b7e1b5","content_type":"application/pdf","relation":"main_file","file_id":"8729","creator":"dernst","success":1}],"date_created":"2020-11-06T07:30:05Z","conference":{"start_date":"2020-10-19","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2020-10-23","location":"Hanoi, Vietnam"},"type":"conference","day":"12","status":"public","intvolume":"     12302","file_date_updated":"2020-11-06T07:41:03Z","page":"253-270","publication":"Automated Technology for Verification and Analysis","year":"2020","doi":"10.1007/978-3-030-59152-6_14","title":"Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth","external_id":{"isi":["000723555700014"]},"isi":1,"alternative_title":["LNCS"],"ddc":["000"],"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"publication_status":"published","citation":{"ama":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In: <i>Automated Technology for Verification and Analysis</i>. Vol 12302. Springer Nature; 2020:253-270. doi:<a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">10.1007/978-3-030-59152-6_14</a>","mla":"Asadi, Ali, et al. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” <i>Automated Technology for Verification and Analysis</i>, vol. 12302, Springer Nature, 2020, pp. 253–70, doi:<a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">10.1007/978-3-030-59152-6_14</a>.","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.","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.","apa":"Asadi, A., Chatterjee, K., Goharshady, A. K., Mohammadi, K., &#38; Pavlogiannis, A. (2020). Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In <i>Automated Technology for Verification and Analysis</i> (Vol. 12302, pp. 253–270). Hanoi, Vietnam: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">https://doi.org/10.1007/978-3-030-59152-6_14</a>","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 <i>Automated Technology for Verification and Analysis</i>, Hanoi, Vietnam, 2020, vol. 12302, pp. 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 <i>Automated Technology for Verification and Analysis</i>, 12302:253–70. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-59152-6_14\">https://doi.org/10.1007/978-3-030-59152-6_14</a>."},"author":[{"first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar"},{"last_name":"Mohammadi","full_name":"Mohammadi, Kiarash","first_name":"Kiarash"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"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"}],"volume":12302,"date_updated":"2025-06-02T08:53:43Z","oa":1,"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","oa_version":"Submitted Version","_id":"8728","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030591519"],"eisbn":["9783030591526"],"eissn":["1611-3349"]}},{"isi":1,"title":"Precedence-aware automated competitive analysis of real-time scheduling","external_id":{"isi":["000587712700069"]},"doi":"10.1109/TCAD.2020.3012803","year":"2020","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","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. ","quality_controlled":"1","oa_version":"None","project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"_id":"8788","publication_identifier":{"eissn":["19374151"],"issn":["02780070"]},"volume":39,"date_updated":"2023-08-22T13:27:05Z","article_processing_charge":"No","author":[{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Schaumberger, Nico","last_name":"Schaumberger","first_name":"Nico"},{"full_name":"Schmid, Ulrich","last_name":"Schmid","first_name":"Ulrich"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"abstract":[{"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.","lang":"eng"}],"publication_status":"published","citation":{"ieee":"A. Pavlogiannis, N. Schaumberger, U. Schmid, and K. Chatterjee, “Precedence-aware automated competitive analysis of real-time scheduling,” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11. IEEE, pp. 3981–3992, 2020.","apa":"Pavlogiannis, A., Schaumberger, N., Schmid, U., &#38; Chatterjee, K. (2020). Precedence-aware automated competitive analysis of real-time scheduling. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE. <a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">https://doi.org/10.1109/TCAD.2020.3012803</a>","chicago":"Pavlogiannis, Andreas, Nico Schaumberger, Ulrich Schmid, and Krishnendu Chatterjee. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE, 2020. <a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">https://doi.org/10.1109/TCAD.2020.3012803</a>.","ama":"Pavlogiannis A, Schaumberger N, Schmid U, Chatterjee K. Precedence-aware automated competitive analysis of real-time scheduling. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. 2020;39(11):3981-3992. doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">10.1109/TCAD.2020.3012803</a>","mla":"Pavlogiannis, Andreas, et al. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11, IEEE, 2020, pp. 3981–92, doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">10.1109/TCAD.2020.3012803</a>.","short":"A. Pavlogiannis, N. Schaumberger, U. Schmid, K. Chatterjee, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 3981–3992.","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."},"date_created":"2020-11-22T23:01:24Z","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"publisher":"IEEE","scopus_import":"1","article_type":"original","date_published":"2020-11-01T00:00:00Z","month":"11","page":"3981-3992","issue":"11","publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","status":"public","intvolume":"        39","type":"journal_article","day":"01"},{"main_file_link":[{"url":"https://arxiv.org/abs/1905.02458","open_access":"1"}],"isi":1,"related_material":{"record":[{"id":"8287","relation":"earlier_version","status":"public"}]},"ec_funded":1,"year":"2020","doi":"10.1109/TCAD.2020.3012859","title":"Reachability analysis of linear hybrid systems via block decomposition","external_id":{"isi":["000587712700072"],"arxiv":["1905.02458"]},"date_updated":"2023-08-22T13:27:33Z","volume":39,"oa":1,"article_processing_charge":"No","arxiv":1,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 754411, and the Air Force Office of Scientific Research under award number FA2386-17-1-4065. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the United States Air Force. ","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa_version":"Preprint","quality_controlled":"1","project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411"}],"_id":"8790","publication_identifier":{"eissn":["19374151"],"issn":["02780070"]},"publication_status":"published","citation":{"short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 4018–4029.","ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2020. Reachability analysis of linear hybrid systems via block decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 39(11), 4018–4029.","mla":"Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11, IEEE, 2020, pp. 4018–29, doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012859\">10.1109/TCAD.2020.3012859</a>.","ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis of linear hybrid systems via block decomposition. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. 2020;39(11):4018-4029. doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012859\">10.1109/TCAD.2020.3012859</a>","chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE, 2020. <a href=\"https://doi.org/10.1109/TCAD.2020.3012859\">https://doi.org/10.1109/TCAD.2020.3012859</a>.","ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability analysis of linear hybrid systems via block decomposition,” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11. IEEE, pp. 4018–4029, 2020.","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., &#38; Schilling, C. (2020). Reachability analysis of linear hybrid systems via block decomposition. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE. <a href=\"https://doi.org/10.1109/TCAD.2020.3012859\">https://doi.org/10.1109/TCAD.2020.3012859</a>"},"author":[{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov"},{"first_name":"Marcelo","full_name":"Forets, Marcelo","last_name":"Forets"},{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"last_name":"Potomkin","full_name":"Potomkin, Kostiantyn","first_name":"Kostiantyn"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","last_name":"Schilling"}],"abstract":[{"lang":"eng","text":"Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks."}],"department":[{"_id":"ToHe"}],"date_created":"2020-11-22T23:01:25Z","date_published":"2020-11-01T00:00:00Z","article_type":"original","month":"11","language":[{"iso":"eng"}],"publisher":"IEEE","scopus_import":"1","page":"4018-4029","issue":"11","publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","type":"journal_article","day":"01","status":"public","intvolume":"        39"},{"publication":"Proceedings of the 23rd International Conference on Principles of Distributed Systems","file_date_updated":"2020-07-14T12:47:56Z","intvolume":"       153","status":"public","day":"10","type":"conference","conference":{"name":"OPODIS: International Conference on Principles of Distributed Systems","end_date":"2019-12-19","location":"Neuchâtel, Switzerland","start_date":"2019-12-17"},"date_created":"2020-01-21T16:00:26Z","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"7608","creator":"dernst","file_size":630752,"file_name":"2019_LIPIcS_Schmid.pdf","checksum":"9a91916ac2c21ab42458fcda39ef0b8d","date_created":"2020-03-23T09:14:06Z","access_level":"open_access","date_updated":"2020-07-14T12:47:56Z"}],"has_accepted_license":"1","department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":"1","language":[{"iso":"eng"}],"month":"02","date_published":"2020-02-10T00:00:00Z","_id":"7346","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"}],"quality_controlled":"1","oa_version":"Preprint","arxiv":1,"date_updated":"2023-02-23T13:05:49Z","volume":153,"oa":1,"article_processing_charge":"No","abstract":[{"text":"The Price of Anarchy (PoA) is a well-established game-theoretic concept to shed light on coordination issues arising in open distributed systems. Leaving agents to selfishly optimize comes with the risk of ending up in sub-optimal states (in terms of performance and/or costs), compared to a centralized system design. However, the PoA relies on strong assumptions about agents' rationality (e.g., resources and information) and interactions, whereas in many distributed systems agents interact locally with bounded resources. They do so repeatedly over time (in contrast to \"one-shot games\"), and their strategies may evolve. Using a more realistic evolutionary game model, this paper introduces a realized evolutionary Price of Anarchy (ePoA). The ePoA allows an exploration of equilibrium selection in dynamic distributed systems with multiple equilibria, based on local interactions of simple memoryless agents. Considering a fundamental game related to virus propagation on networks, we present analytical bounds on the ePoA in basic network topologies and for different strategy update dynamics. In particular, deriving stationary distributions of the stochastic evolutionary process, we find that the Nash equilibria are not always the most abundant states, and that different processes can feature significant off-equilibrium behavior, leading to a significantly higher ePoA compared to the PoA studied traditionally in the literature. ","lang":"eng"}],"author":[{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","first_name":"Laura","orcid":"0000-0002-6978-7329","full_name":"Schmid, Laura","last_name":"Schmid"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Schmid","full_name":"Schmid, Stefan","first_name":"Stefan"}],"publication_status":"published","citation":{"short":"L. Schmid, K. Chatterjee, S. Schmid, in:, Proceedings of the 23rd International Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","ista":"Schmid L, Chatterjee K, Schmid S. 2020. The evolutionary price of anarchy: Locally bounded agents in a dynamic virus game. Proceedings of the 23rd International Conference on Principles of Distributed Systems. OPODIS: International Conference on Principles of Distributed Systems, LIPIcs, vol. 153, 21.","mla":"Schmid, Laura, et al. “The Evolutionary Price of Anarchy: Locally Bounded Agents in a Dynamic Virus Game.” <i>Proceedings of the 23rd International Conference on Principles of Distributed Systems</i>, vol. 153, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2019.21\">10.4230/LIPIcs.OPODIS.2019.21</a>.","ama":"Schmid L, Chatterjee K, Schmid S. The evolutionary price of anarchy: Locally bounded agents in a dynamic virus game. In: <i>Proceedings of the 23rd International Conference on Principles of Distributed Systems</i>. Vol 153. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2019.21\">10.4230/LIPIcs.OPODIS.2019.21</a>","chicago":"Schmid, Laura, Krishnendu Chatterjee, and Stefan Schmid. “The Evolutionary Price of Anarchy: Locally Bounded Agents in a Dynamic Virus Game.” In <i>Proceedings of the 23rd International Conference on Principles of Distributed Systems</i>, Vol. 153. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2019.21\">https://doi.org/10.4230/LIPIcs.OPODIS.2019.21</a>.","ieee":"L. Schmid, K. Chatterjee, and S. Schmid, “The evolutionary price of anarchy: Locally bounded agents in a dynamic virus game,” in <i>Proceedings of the 23rd International Conference on Principles of Distributed Systems</i>, Neuchâtel, Switzerland, 2020, vol. 153.","apa":"Schmid, L., Chatterjee, K., &#38; Schmid, S. (2020). The evolutionary price of anarchy: Locally bounded agents in a dynamic virus game. In <i>Proceedings of the 23rd International Conference on Principles of Distributed Systems</i> (Vol. 153). Neuchâtel, Switzerland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2019.21\">https://doi.org/10.4230/LIPIcs.OPODIS.2019.21</a>"},"ddc":["000"],"alternative_title":["LIPIcs"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"article_number":"21","external_id":{"arxiv":["1906.00110"]},"title":"The evolutionary price of anarchy: Locally bounded agents in a dynamic virus game","doi":"10.4230/LIPIcs.OPODIS.2019.21","year":"2020"},{"abstract":[{"text":"Neural networks have demonstrated unmatched performance in a range of classification tasks. Despite numerous efforts of the research community, novelty detection remains one of the significant limitations of neural networks. The ability to identify previously unseen inputs as novel is crucial for our understanding of the decisions made by neural networks. At runtime, inputs not falling into any of the categories learned during training cannot be classified correctly by the neural network. Existing approaches treat the neural network as a black box and try to detect novel inputs based on the confidence of the output predictions. However, neural networks are not trained to reduce their confidence for novel inputs, which limits the effectiveness of these approaches. We propose a framework to monitor a neural network by observing the hidden layers. We employ a common abstraction from program analysis - boxes - to identify novel behaviors in the monitored layers, i.e., inputs that cause behaviors outside the box. For each neuron, the boxes range over the values seen in training. The framework is efficient and flexible to achieve a desired trade-off between raising false warnings and detecting novel inputs. We illustrate the performance and the robustness to variability in the unknown classes on popular image-classification benchmarks.","lang":"eng"}],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"first_name":"Anna","full_name":"Lukina, Anna","last_name":"Lukina","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425"},{"last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","citation":{"apa":"Henzinger, T. A., Lukina, A., &#38; Schilling, C. (2020). Outside the box: Abstraction-based monitoring of neural networks. In <i>24th European Conference on Artificial Intelligence</i> (Vol. 325, pp. 2433–2440). Santiago de Compostela, Spain: IOS Press. <a href=\"https://doi.org/10.3233/FAIA200375\">https://doi.org/10.3233/FAIA200375</a>","ieee":"T. A. Henzinger, A. Lukina, and C. Schilling, “Outside the box: Abstraction-based monitoring of neural networks,” in <i>24th European Conference on Artificial Intelligence</i>, Santiago de Compostela, Spain, 2020, vol. 325, pp. 2433–2440.","chicago":"Henzinger, Thomas A, Anna Lukina, and Christian Schilling. “Outside the Box: Abstraction-Based Monitoring of Neural Networks.” In <i>24th European Conference on Artificial Intelligence</i>, 325:2433–40. IOS Press, 2020. <a href=\"https://doi.org/10.3233/FAIA200375\">https://doi.org/10.3233/FAIA200375</a>.","ama":"Henzinger TA, Lukina A, Schilling C. Outside the box: Abstraction-based monitoring of neural networks. In: <i>24th European Conference on Artificial Intelligence</i>. Vol 325. IOS Press; 2020:2433-2440. doi:<a href=\"https://doi.org/10.3233/FAIA200375\">10.3233/FAIA200375</a>","mla":"Henzinger, Thomas A., et al. “Outside the Box: Abstraction-Based Monitoring of Neural Networks.” <i>24th European Conference on Artificial Intelligence</i>, vol. 325, IOS Press, 2020, pp. 2433–40, doi:<a href=\"https://doi.org/10.3233/FAIA200375\">10.3233/FAIA200375</a>.","ista":"Henzinger TA, Lukina A, Schilling C. 2020. Outside the box: Abstraction-based monitoring of neural networks. 24th European Conference on Artificial Intelligence. ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 325, 2433–2440.","short":"T.A. Henzinger, A. Lukina, C. Schilling, in:, 24th European Conference on Artificial Intelligence, IOS Press, 2020, pp. 2433–2440."},"_id":"7505","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","acknowledgement":"We thank Christoph Lampert and Nikolaus Mayer for fruitful discussions. This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award) and the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie grant agreement No. 754411.","oa_version":"Published Version","quality_controlled":"1","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"arxiv":1,"volume":325,"oa":1,"date_updated":"2023-08-18T06:38:16Z","article_processing_charge":"No","external_id":{"arxiv":["1911.09032"],"isi":["000650971303002"]},"title":"Outside the box: Abstraction-based monitoring of neural networks","year":"2020","doi":"10.3233/FAIA200375","ec_funded":1,"ddc":["000"],"alternative_title":["Frontiers in Artificial Intelligence and Applications"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)"},"isi":1,"intvolume":"       325","status":"public","day":"24","type":"conference","publication":"24th European Conference on Artificial Intelligence","page":"2433-2440","file_date_updated":"2020-09-21T07:12:32Z","publisher":"IOS Press","language":[{"iso":"eng"}],"month":"02","date_published":"2020-02-24T00:00:00Z","conference":{"name":"ECAI: European Conference on Artificial Intelligence","end_date":"2020-09-08","location":"Santiago de Compostela, Spain","start_date":"2020-08-29"},"date_created":"2020-02-21T16:44:03Z","file":[{"success":1,"creator":"dernst","file_id":"8540","content_type":"application/pdf","relation":"main_file","date_created":"2020-09-21T07:12:32Z","checksum":"80642fa0b6cd7da95dcd87d63789ad5e","file_name":"2020_ECAI_Henzinger.pdf","file_size":1692214,"date_updated":"2020-09-21T07:12:32Z","access_level":"open_access"}],"has_accepted_license":"1","department":[{"_id":"ToHe"}]},{"title":"Social dilemmas among unequals","external_id":{"isi":["000482219600045"]},"year":"2019","doi":"10.1038/s41586-019-1488-5","ec_funded":1,"related_material":{"link":[{"url":"https://ist.ac.at/en/news/too-much-inequality-impedes-support-for-public-goods-according-to-research-published-in-nature/","description":"News on IST Homepage","relation":"press_release"}]},"ddc":["000"],"isi":1,"abstract":[{"text":"Direct reciprocity is a powerful mechanism for the evolution of cooperation on the basis of repeated interactions1,2,3,4. It requires that interacting individuals are sufficiently equal, such that everyone faces similar consequences when they cooperate or defect. Yet inequality is ubiquitous among humans5,6 and is generally considered to undermine cooperation and welfare7,8,9,10. Most previous models of reciprocity do not include inequality11,12,13,14,15. These models assume that individuals are the same in all relevant aspects. Here we introduce a general framework to study direct reciprocity among unequal individuals. Our model allows for multiple sources of inequality. Subjects can differ in their endowments, their productivities and in how much they benefit from public goods. We find that extreme inequality prevents cooperation. But if subjects differ in productivity, some endowment inequality can be necessary for cooperation to prevail. Our mathematical predictions are supported by a behavioural experiment in which we vary the endowments and productivities of the subjects. We observe that overall welfare is maximized when the two sources of heterogeneity are aligned, such that more productive individuals receive higher endowments. By contrast, when endowments and productivities are misaligned, cooperation quickly breaks down. Our findings have implications for policy-makers concerned with equity, efficiency and the provisioning of public goods.","lang":"eng"}],"author":[{"full_name":"Hauser, Oliver P.","last_name":"Hauser","first_name":"Oliver P."},{"first_name":"Christian","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"publication_status":"published","citation":{"ama":"Hauser OP, Hilbe C, Chatterjee K, Nowak MA. Social dilemmas among unequals. <i>Nature</i>. 2019;572(7770):524-527. doi:<a href=\"https://doi.org/10.1038/s41586-019-1488-5\">10.1038/s41586-019-1488-5</a>","mla":"Hauser, Oliver P., et al. “Social Dilemmas among Unequals.” <i>Nature</i>, vol. 572, no. 7770, Springer Nature, 2019, pp. 524–27, doi:<a href=\"https://doi.org/10.1038/s41586-019-1488-5\">10.1038/s41586-019-1488-5</a>.","short":"O.P. Hauser, C. Hilbe, K. Chatterjee, M.A. Nowak, Nature 572 (2019) 524–527.","ista":"Hauser OP, Hilbe C, Chatterjee K, Nowak MA. 2019. Social dilemmas among unequals. Nature. 572(7770), 524–527.","ieee":"O. P. Hauser, C. Hilbe, K. Chatterjee, and M. A. Nowak, “Social dilemmas among unequals,” <i>Nature</i>, vol. 572, no. 7770. Springer Nature, pp. 524–527, 2019.","apa":"Hauser, O. P., Hilbe, C., Chatterjee, K., &#38; Nowak, M. A. (2019). Social dilemmas among unequals. <i>Nature</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41586-019-1488-5\">https://doi.org/10.1038/s41586-019-1488-5</a>","chicago":"Hauser, Oliver P., Christian Hilbe, Krishnendu Chatterjee, and Martin A. Nowak. “Social Dilemmas among Unequals.” <i>Nature</i>. Springer Nature, 2019. <a href=\"https://doi.org/10.1038/s41586-019-1488-5\">https://doi.org/10.1038/s41586-019-1488-5</a>."},"_id":"6836","publication_identifier":{"eissn":["14764687"],"issn":["00280836"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","quality_controlled":"1","oa_version":"Submitted Version","project":[{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"oa":1,"volume":572,"date_updated":"2023-08-29T07:42:54Z","article_processing_charge":"No","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"month":"08","article_type":"letter_note","date_published":"2019-08-22T00:00:00Z","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:47:42Z","checksum":"a6e0e3168bf62de624e7772cdfaeb26f","date_created":"2020-05-14T10:00:32Z","file_size":18577756,"file_name":"2019_Nature_Hauser.pdf","creator":"dernst","file_id":"7828","relation":"main_file","content_type":"application/pdf"}],"date_created":"2019-09-01T22:00:56Z","has_accepted_license":"1","department":[{"_id":"KrCh"}],"intvolume":"       572","status":"public","day":"22","type":"journal_article","issue":"7770","publication":"Nature","page":"524-527","file_date_updated":"2020-07-14T12:47:42Z"},{"day":"01","type":"journal_article","intvolume":"        41","status":"public","publication":"ACM Transactions on Programming Languages and Systems","issue":"4","month":"10","date_published":"2019-10-01T00:00:00Z","article_type":"original","scopus_import":"1","publisher":"ACM","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"date_created":"2019-11-13T08:33:43Z","citation":{"short":"K. Chatterjee, H. Fu, A.K. Goharshady, ACM Transactions on Programming Languages and Systems 41 (2019).","ista":"Chatterjee K, Fu H, Goharshady AK. 2019. Non-polynomial worst-case analysis of recursive programs. ACM Transactions on Programming Languages and Systems. 41(4), 20.","ama":"Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href=\"https://doi.org/10.1145/3339984\">10.1145/3339984</a>","mla":"Chatterjee, Krishnendu, et al. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 20, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3339984\">10.1145/3339984</a>.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3339984\">https://doi.org/10.1145/3339984</a>.","apa":"Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2019). Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/3339984\">https://doi.org/10.1145/3339984</a>","ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst-case analysis of recursive programs,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019."},"publication_status":"published","abstract":[{"text":"We study the problem of developing efficient approaches for proving\r\nworst-case bounds of non-deterministic recursive programs. Ranking functions\r\nare sound and complete for proving termination and worst-case bounds of\r\nnonrecursive programs. First, we apply ranking functions to recursion,\r\nresulting in measure functions. We show that measure functions provide a sound\r\nand complete approach to prove worst-case bounds of non-deterministic recursive\r\nprograms. Our second contribution is the synthesis of measure functions in\r\nnonpolynomial forms. We show that non-polynomial measure functions with\r\nlogarithm and exponentiation can be synthesized through abstraction of\r\nlogarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem\r\nusing linear programming. While previous methods obtain worst-case polynomial\r\nbounds, our approach can synthesize bounds of the form $\\mathcal{O}(n\\log n)$\r\nas well as $\\mathcal{O}(n^r)$ where $r$ is not an integer. We present\r\nexperimental results to demonstrate that our approach can obtain efficiently\r\nworst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the\r\ndivide-and-conquer algorithm for the Closest-Pair problem, where we obtain\r\n$\\mathcal{O}(n \\log n)$ worst-case bound, and (ii) Karatsuba's algorithm for\r\npolynomial multiplication and Strassen's algorithm for matrix multiplication,\r\nwhere we obtain $\\mathcal{O}(n^r)$ bound such that $r$ is not an integer and\r\nclose to the best-known bounds for the respective algorithms.","lang":"eng"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584"}],"arxiv":1,"article_processing_charge":"No","volume":41,"oa":1,"date_updated":"2025-06-02T08:53:47Z","_id":"7014","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"quality_controlled":"1","oa_version":"Preprint","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","year":"2019","doi":"10.1145/3339984","ec_funded":1,"external_id":{"arxiv":["1705.00317"],"isi":["000564108400001"]},"title":"Non-polynomial worst-case analysis of recursive programs","isi":1,"main_file_link":[{"url":"https://arxiv.org/abs/1705.00317","open_access":"1"}],"article_number":"20","related_material":{"record":[{"relation":"earlier_version","id":"639","status":"public"},{"relation":"dissertation_contains","id":"8934","status":"public"}]}},{"issue":"3","publication":"Journal of the ACM","day":"01","type":"journal_article","intvolume":"        66","status":"public","department":[{"_id":"ToHe"}],"date_created":"2019-11-26T10:22:32Z","month":"05","article_type":"original","date_published":"2019-05-01T00:00:00Z","publisher":"ACM","scopus_import":"1","language":[{"iso":"eng"}],"volume":66,"date_updated":"2023-09-06T11:11:56Z","article_processing_charge":"No","_id":"7109","publication_identifier":{"issn":["0004-5411"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"None","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"quality_controlled":"1","publication_status":"published","citation":{"ista":"Ferrere T, Maler O, Ničković D, Pnueli A. 2019. From real-time logic to timed automata. Journal of the ACM. 66(3), 19.","short":"T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019).","ama":"Ferrere T, Maler O, Ničković D, Pnueli A. From real-time logic to timed automata. <i>Journal of the ACM</i>. 2019;66(3). doi:<a href=\"https://doi.org/10.1145/3286976\">10.1145/3286976</a>","mla":"Ferrere, Thomas, et al. “From Real-Time Logic to Timed Automata.” <i>Journal of the ACM</i>, vol. 66, no. 3, 19, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3286976\">10.1145/3286976</a>.","chicago":"Ferrere, Thomas, Oded Maler, Dejan Ničković, and Amir Pnueli. “From Real-Time Logic to Timed Automata.” <i>Journal of the ACM</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3286976\">https://doi.org/10.1145/3286976</a>.","ieee":"T. Ferrere, O. Maler, D. Ničković, and A. Pnueli, “From real-time logic to timed automata,” <i>Journal of the ACM</i>, vol. 66, no. 3. ACM, 2019.","apa":"Ferrere, T., Maler, O., Ničković, D., &#38; Pnueli, A. (2019). From real-time logic to timed automata. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3286976\">https://doi.org/10.1145/3286976</a>"},"abstract":[{"text":"We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.","lang":"eng"}],"author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"first_name":"Dejan","full_name":"Ničković, Dejan","last_name":"Ničković"},{"first_name":"Amir","full_name":"Pnueli, Amir","last_name":"Pnueli"}],"article_number":"19","isi":1,"year":"2019","doi":"10.1145/3286976","title":"From real-time logic to timed automata","external_id":{"isi":["000495406300005"]}},{"publication":"International Symposium on Automated Technology for Verification and Analysis","page":"462-478","day":"21","type":"conference","intvolume":"     11781","status":"public","department":[{"_id":"KrCh"}],"conference":{"location":"Taipei, Taiwan","name":"ATVA: Automated TEchnology for Verification and Analysis","end_date":"2019-10-31","start_date":"2019-10-28"},"date_created":"2019-12-15T23:00:44Z","month":"10","date_published":"2019-10-21T00:00:00Z","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"arxiv":1,"oa":1,"volume":11781,"date_updated":"2023-09-06T12:40:58Z","article_processing_charge":"No","_id":"7183","publication_identifier":{"issn":["03029743"],"isbn":["9783030317836"],"eissn":["16113349"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"}],"quality_controlled":"1","oa_version":"Preprint","publication_status":"published","citation":{"ieee":"T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, and D. Velan, “Deciding fast termination for probabilistic VASS with nondeterminism,” in <i>International Symposium on Automated Technology for Verification and Analysis</i>, Taipei, Taiwan, 2019, vol. 11781, pp. 462–478.","apa":"Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P., &#38; Velan, D. (2019). Deciding fast termination for probabilistic VASS with nondeterminism. In <i>International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 11781, pp. 462–478). Taipei, Taiwan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">https://doi.org/10.1007/978-3-030-31784-3_27</a>","chicago":"Brázdil, Tomás, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and Dominik Velan. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.” In <i>International Symposium on Automated Technology for Verification and Analysis</i>, 11781:462–78. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">https://doi.org/10.1007/978-3-030-31784-3_27</a>.","mla":"Brázdil, Tomás, et al. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.” <i>International Symposium on Automated Technology for Verification and Analysis</i>, vol. 11781, Springer Nature, 2019, pp. 462–78, doi:<a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">10.1007/978-3-030-31784-3_27</a>.","ama":"Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. Deciding fast termination for probabilistic VASS with nondeterminism. In: <i>International Symposium on Automated Technology for Verification and Analysis</i>. Vol 11781. Springer Nature; 2019:462-478. doi:<a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">10.1007/978-3-030-31784-3_27</a>","short":"T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, D. Velan, in:, International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2019, pp. 462–478.","ista":"Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. 2019. Deciding fast termination for probabilistic VASS with nondeterminism. International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated TEchnology for Verification and Analysis, LNCS, vol. 11781, 462–478."},"abstract":[{"lang":"eng","text":"A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in Ω(n2)."}],"author":[{"first_name":"Tomás","full_name":"Brázdil, Tomás","last_name":"Brázdil"},{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kucera, Antonín","last_name":"Kucera","first_name":"Antonín"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","full_name":"Novotný, Petr","first_name":"Petr"},{"full_name":"Velan, Dominik","last_name":"Velan","first_name":"Dominik"}],"alternative_title":["LNCS"],"isi":1,"main_file_link":[{"url":"https://arxiv.org/abs/1907.11010","open_access":"1"}],"doi":"10.1007/978-3-030-31784-3_27","year":"2019","external_id":{"arxiv":["1907.11010"],"isi":["000723515700027"]},"title":"Deciding fast termination for probabilistic VASS with nondeterminism"},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Published Version","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"quality_controlled":"1","pmid":1,"_id":"7210","publication_identifier":{"issn":["2399-3642"]},"volume":2,"date_updated":"2023-09-07T13:19:22Z","oa":1,"article_processing_charge":"No","author":[{"first_name":"Josef","full_name":"Tkadlec, Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"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"}],"publication_status":"published","citation":{"mla":"Tkadlec, Josef, et al. “Population Structure Determines the Tradeoff between Fixation Probability and Fixation Time.” <i>Communications Biology</i>, vol. 2, 138, Springer Nature, 2019, doi:<a href=\"https://doi.org/10.1038/s42003-019-0373-y\">10.1038/s42003-019-0373-y</a>.","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Population structure determines the tradeoff between fixation probability and fixation time. <i>Communications Biology</i>. 2019;2. doi:<a href=\"https://doi.org/10.1038/s42003-019-0373-y\">10.1038/s42003-019-0373-y</a>","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Communications Biology 2 (2019).","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.","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2019). Population structure determines the tradeoff between fixation probability and fixation time. <i>Communications Biology</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s42003-019-0373-y\">https://doi.org/10.1038/s42003-019-0373-y</a>","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Population structure determines the tradeoff between fixation probability and fixation time,” <i>Communications Biology</i>, vol. 2. Springer Nature, 2019.","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Population Structure Determines the Tradeoff between Fixation Probability and Fixation Time.” <i>Communications Biology</i>. Springer Nature, 2019. <a href=\"https://doi.org/10.1038/s42003-019-0373-y\">https://doi.org/10.1038/s42003-019-0373-y</a>."},"ddc":["000"],"related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"7196"}]},"article_number":"138","isi":1,"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"title":"Population structure determines the tradeoff between fixation probability and fixation time","external_id":{"pmid":["31044163"],"isi":["000465425700006"]},"ec_funded":1,"doi":"10.1038/s42003-019-0373-y","year":"2019","file_date_updated":"2020-07-14T12:47:53Z","publication":"Communications Biology","status":"public","intvolume":"         2","type":"journal_article","day":"23","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"7211","creator":"dernst","file_size":1670274,"file_name":"2019_CommBio_Tkadlec.pdf","checksum":"d1a69bfe73767e4246f0a38e4e1554dd","date_created":"2019-12-23T13:39:30Z","access_level":"open_access","date_updated":"2020-07-14T12:47:53Z"}],"date_created":"2019-12-23T13:36:50Z","department":[{"_id":"KrCh"}],"has_accepted_license":"1","language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1","article_type":"original","date_published":"2019-04-23T00:00:00Z","month":"04"},{"abstract":[{"text":"Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature.","lang":"eng"}],"author":[{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui","full_name":"Kong, Hui","last_name":"Kong","orcid":"0000-0002-3066-6941"},{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"citation":{"apa":"Kong, H., Bartocci, E., Jiang, Y., &#38; Henzinger, T. A. (2019). Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>","ieee":"H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 123–141.","chicago":"Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:123–41. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>.","ama":"Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:123-141. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>","mla":"Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>.","ista":"Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11750, 123–141.","short":"H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141."},"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-0302-9661-2"],"eissn":["1611-3349"]},"_id":"7231","quality_controlled":"1","oa_version":"Preprint","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407"},{"grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","arxiv":1,"article_processing_charge":"No","oa":1,"volume":11750,"date_updated":"2023-09-06T14:55:15Z","title":"Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty","external_id":{"isi":["000611677700008"],"arxiv":["1907.11514"]},"doi":"10.1007/978-3-030-29662-9_8","year":"2019","alternative_title":["LNCS"],"isi":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1907.11514"}],"intvolume":"     11750","status":"public","day":"13","type":"conference","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","page":"123-141","scopus_import":"1","publisher":"Springer Nature","language":[{"iso":"eng"}],"month":"08","date_published":"2019-08-13T00:00:00Z","conference":{"start_date":"2019-08-27","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","end_date":"2019-08-29","location":"Amsterdam, The Netherlands"},"date_created":"2020-01-05T23:00:47Z","department":[{"_id":"ToHe"}]},{"language":[{"iso":"eng"}],"scopus_import":"1","publisher":"Springer Nature","date_published":"2019-08-13T00:00:00Z","month":"08","date_created":"2020-01-05T23:00:48Z","conference":{"start_date":"2019-08-27","end_date":"2019-08-29","location":"Amsterdam, The Netherlands","name":"FORMATS: Formal Modeling and Anaysis of Timed Systems"},"department":[{"_id":"ToHe"}],"status":"public","intvolume":"     11750","type":"conference","day":"13","page":"59-75","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","title":"Mixed-time signal temporal logic","external_id":{"isi":["000611677700004"]},"year":"2019","doi":"10.1007/978-3-030-29662-9_4","isi":1,"alternative_title":["LNCS"],"author":[{"first_name":"Thomas","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"}],"abstract":[{"text":"We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. ","lang":"eng"}],"citation":{"chicago":"Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal Logic.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:59–75. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>.","ieee":"T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.","apa":"Ferrere, T., Maler, O., &#38; Nickovic, D. (2019). Mixed-time signal temporal logic. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>","short":"T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.","ista":"Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.","mla":"Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 59–75, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>.","ama":"Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:59-75. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>"},"publication_status":"published","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"}],"oa_version":"None","quality_controlled":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"isbn":["978-3-0302-9661-2"],"issn":["0302-9743"],"eissn":["1611-3349"]},"_id":"7232","article_processing_charge":"No","date_updated":"2023-09-06T14:57:17Z","volume":11750}]