[{"quality_controlled":"1","isi":1,"publication":"Formal Methods in System Design","month":"09","oa":1,"status":"public","ec_funded":1,"article_type":"original","abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","publisher":"Springer","_id":"9393","page":"401-428","scopus_import":"1","date_created":"2021-05-16T22:01:47Z","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"volume":57,"title":"Faster algorithms for quantitative verification in bounded treewidth graphs","citation":{"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>.","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>","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>","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.","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>.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://arxiv.org/abs/1504.07384","open_access":"1"}],"article_processing_charge":"No","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"date_published":"2021-09-01T00:00:00Z","type":"journal_article","publication_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"year":"2021","day":"01","date_updated":"2025-04-15T07:23:30Z","intvolume":"        57","publication_status":"published","arxiv":1,"external_id":{"isi":["000645490300001"],"arxiv":["1504.07384"]},"oa_version":"Preprint","doi":"10.1007/s10703-021-00373-5","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"}]},{"pmid":1,"external_id":{"isi":["000671752100003"],"pmid":["34188036"]},"oa_version":"Published Version","file":[{"content_type":"application/pdf","file_id":"9692","file_size":628992,"access_level":"open_access","relation":"main_file","checksum":"5767418926a7f7fb76151de29473dae0","creator":"cziletti","file_name":"2021_NatCoom_Tkadlec.pdf","date_updated":"2021-07-19T13:02:20Z","success":1,"date_created":"2021-07-19T13:02:20Z"}],"author":[{"first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","full_name":"Tkadlec, Josef"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"doi":"10.1038/s41467-021-24271-w","intvolume":"        12","article_number":"4009","publication_status":"published","issue":"1","citation":{"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>.","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Nature Communications 12 (2021).","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>","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.","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>."},"title":"Fast and strong amplifiers of natural selection","volume":12,"project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"article_processing_charge":"No","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","language":[{"iso":"eng"}],"date_published":"2021-06-29T00:00:00Z","department":[{"_id":"KrCh"}],"has_accepted_license":"1","date_updated":"2026-04-02T14:04:10Z","day":"29","file_date_updated":"2021-07-19T13:02:20Z","type":"journal_article","publication_identifier":{"eissn":["2041-1723"]},"year":"2021","ddc":["510"],"quality_controlled":"1","status":"public","oa":1,"publication":"Nature Communications","month":"06","isi":1,"publisher":"Springer Nature","article_type":"original","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.","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."}],"ec_funded":1,"scopus_import":"1","date_created":"2021-07-11T22:01:15Z","_id":"9640","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"}},{"alternative_title":["ISTA Thesis"],"publication_status":"published","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"9997"},{"relation":"part_of_dissertation","status":"public","id":"9402"},{"relation":"part_of_dissertation","status":"public","id":"2"}]},"doi":"10.15479/at:ista:10293","file":[{"file_name":"submission_new.zip","creator":"lschmid","date_updated":"2022-12-20T23:30:08Z","date_created":"2021-11-18T12:41:46Z","embargo_to":"open_access","checksum":"86a05b430756ca12ae8107b6e6f3c1e5","content_type":"application/zip","file_size":29703124,"file_id":"10305","relation":"source_file","access_level":"closed"},{"access_level":"open_access","relation":"main_file","file_id":"10306","content_type":"application/pdf","file_size":8320985,"checksum":"d940af042e94660c6b6a7b4f0b184d47","embargo":"2022-10-18","creator":"lschmid","file_name":"thesis_new_upload.pdf","date_updated":"2022-12-20T23:30:08Z","date_created":"2021-11-18T12:59:15Z"}],"author":[{"full_name":"Schmid, Laura","last_name":"Schmid","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","first_name":"Laura"}],"oa_version":"Published Version","corr_author":"1","month":"11","status":"public","oa":1,"ddc":["519","576"],"degree_awarded":"PhD","OA_place":"publisher","_id":"10293","date_created":"2021-11-15T17:12:57Z","page":"171","ec_funded":1,"abstract":[{"lang":"eng","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."}],"publisher":"Institute of Science and Technology Austria","supervisor":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"title":"Evolution of cooperation via (in)direct reciprocity under imperfect information","citation":{"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>","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>","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>.","short":"L. Schmid, Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information, Institute of Science and Technology Austria, 2021.","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>.","ista":"Schmid L. 2021. Evolution of cooperation via (in)direct reciprocity under imperfect information. Institute of Science and Technology Austria."},"year":"2021","publication_identifier":{"issn":["2663-337X"]},"type":"dissertation","file_date_updated":"2022-12-20T23:30:08Z","date_updated":"2026-04-08T07:11:20Z","day":"17","has_accepted_license":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"date_published":"2021-11-17T00:00:00Z"},{"alternative_title":["LNCS"],"publication_status":"published","intvolume":"     12079","doi":"10.1007/978-3-030-45237-7_5","author":[{"first_name":"Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","last_name":"Giacobbe","full_name":"Giacobbe, Mirco"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","full_name":"Lechner, Mathias","last_name":"Lechner"}],"file":[{"creator":"dernst","file_name":"2020_TACAS_Giacobbe.pdf","date_updated":"2020-07-14T12:48:03Z","date_created":"2020-05-26T12:48:15Z","content_type":"application/pdf","file_id":"7893","file_size":2744030,"relation":"main_file","access_level":"open_access","checksum":"f19905a42891fe5ce93d69143fa3f6fb"}],"oa_version":"Published Version","external_id":{"isi":["001288734300005"]},"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"11362"}]},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"_id":"7808","scopus_import":"1","date_created":"2020-05-10T22:00:49Z","page":"79-97","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."}],"publisher":"Springer Nature","corr_author":"1","isi":1,"month":"04","publication":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","status":"public","oa":1,"ddc":["000"],"quality_controlled":"1","type":"conference","year":"2020","publication_identifier":{"isbn":["9783030452360"],"issn":["0302-9743"],"eissn":["1611-3349"]},"file_date_updated":"2020-07-14T12:48:03Z","day":"17","date_updated":"2026-04-16T09:46:07Z","has_accepted_license":"1","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"date_published":"2020-04-17T00:00:00Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","conference":{"location":"Dublin, Ireland","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2020-04-30","start_date":"2020-04-25"},"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"volume":12079,"title":"How many bits does it take to quantize your neural network?","citation":{"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.","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>.","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.","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.","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>"}},{"ec_funded":1,"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 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."}],"_id":"8287","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"date_created":"2020-08-24T12:56:20Z","keyword":["reachability","hybrid systems","decomposition"],"ddc":["000"],"quality_controlled":"1","month":"10","publication":"Proceedings of the International Conference on Embedded Software","status":"public","oa":1,"isi":1,"language":[{"iso":"eng"}],"date_published":"2020-10-01T00:00:00Z","has_accepted_license":"1","department":[{"_id":"ToHe"}],"file_date_updated":"2020-08-24T12:53:15Z","day":"01","date_updated":"2026-04-03T09:32:00Z","type":"conference","year":"2020","title":"Reachability analysis of linear hybrid systems via block decomposition","citation":{"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.","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: Embedded Software.","short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the International Conference on Embedded Software, 2020.","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.","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.","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 .","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."},"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z00312","name":"Synaptic communication in neuronal microcircuits","_id":"25C5A090-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"article_processing_charge":"No","conference":{"location":"Virtual ","end_date":"2020-09-25","name":"EMSOFT: Embedded Software","start_date":"2020-09-20"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","arxiv":1,"publication_status":"published","oa_version":"Preprint","author":[{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"first_name":"Marcelo","last_name":"Forets","full_name":"Forets, Marcelo"},{"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","first_name":"Christian","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling"}],"file":[{"creator":"cschilli","file_name":"2020EMSOFT.pdf","date_updated":"2020-08-24T12:53:15Z","date_created":"2020-08-24T12:53:15Z","success":1,"checksum":"d19e97d0f8a3a441dc078ec812297d75","content_type":"application/pdf","file_size":696384,"file_id":"8288","access_level":"open_access","relation":"main_file"}],"related_material":{"record":[{"id":"8790","status":"public","relation":"later_version"}]},"external_id":{"arxiv":["1905.02458"],"isi":["000587712700072"]}},{"external_id":{"arxiv":["2007.08917"]},"oa_version":"Published Version","doi":"10.4230/LIPIcs.CONCUR.2020.23","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"file":[{"date_created":"2020-10-05T14:04:25Z","success":1,"date_updated":"2020-10-05T14:04:25Z","creator":"dernst","file_name":"2020_LIPIcsCONCUR_Chatterjee.pdf","checksum":"5039752f644c4b72b9361d21a5e31baf","file_id":"8610","file_size":601231,"content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"intvolume":"       171","article_number":"23","publication_status":"published","alternative_title":["LIPIcs"],"arxiv":1,"volume":171,"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"citation":{"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>","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>.","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>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","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."},"title":"Multi-dimensional long-run average problems for vector addition systems with states","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2020-09-01","location":"Virtual","end_date":"2020-09-04","name":"CONCUR: Conference on Concurrency Theory"},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"has_accepted_license":"1","date_published":"2020-08-06T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","year":"2020","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959771603"]},"day":"06","date_updated":"2025-07-10T11:57:10Z","file_date_updated":"2020-10-05T14:04:25Z","ddc":["000"],"quality_controlled":"1","license":"https://creativecommons.org/licenses/by/3.0/","corr_author":"1","oa":1,"status":"public","month":"08","publication":"31st International Conference on Concurrency Theory","abstract":[{"lang":"eng","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."}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":"1","date_created":"2020-10-04T22:01:36Z","tmp":{"short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"_id":"8600"},{"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"volume":39,"title":"Precedence-aware automated competitive analysis of real-time scheduling","citation":{"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.","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>.","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>.","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>","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>","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."},"year":"2020","type":"journal_article","publication_identifier":{"issn":["0278-0070"],"eissn":["1937-4151"]},"day":"01","date_updated":"2026-04-02T14:37:50Z","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"date_published":"2020-11-01T00:00:00Z","isi":1,"publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","month":"11","status":"public","quality_controlled":"1","_id":"8788","page":"3981-3992","date_created":"2020-11-22T23:01:24Z","scopus_import":"1","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"}],"article_type":"original","acknowledgement":"This work was supported by the Austrian Science Foundation (FWF) under the NFN RiSE/SHiNE under Grant S11405 and Grant S11407. This article was presented in the International Conference on Embedded Software 2020 and appears as part of the ESWEEK-TCAD special issue. ","publisher":"IEEE","external_id":{"isi":["000587712700069"]},"doi":"10.1109/TCAD.2020.3012803","author":[{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"first_name":"Nico","full_name":"Schaumberger, Nico","last_name":"Schaumberger"},{"full_name":"Schmid, Ulrich","last_name":"Schmid","first_name":"Ulrich"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"oa_version":"None","issue":"11","publication_status":"published","intvolume":"        39"},{"quality_controlled":"1","oa":1,"status":"public","month":"11","publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","isi":1,"publisher":"IEEE","article_type":"original","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 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.","lang":"eng"}],"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. ","ec_funded":1,"date_created":"2020-11-22T23:01:25Z","scopus_import":"1","page":"4018-4029","OA_place":"publisher","_id":"8790","citation":{"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>.","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.","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>","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>","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.","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>."},"title":"Reachability analysis of linear hybrid systems via block decomposition","volume":39,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1905.02458"}],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","OA_type":"hybrid","language":[{"iso":"eng"}],"date_published":"2020-11-01T00:00:00Z","department":[{"_id":"ToHe"}],"day":"01","date_updated":"2026-04-03T09:32:00Z","year":"2020","type":"journal_article","publication_identifier":{"issn":["0278-0070"],"eissn":["1937-4151"]},"intvolume":"        39","publication_status":"published","issue":"11","arxiv":1,"related_material":{"record":[{"id":"8287","relation":"earlier_version","status":"public"}]},"external_id":{"arxiv":["1905.02458"],"isi":["000587712700072"]},"oa_version":"Preprint","author":[{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365"},{"first_name":"Marcelo","last_name":"Forets","full_name":"Forets, Marcelo"},{"last_name":"Frehse","full_name":"Frehse, Goran","first_name":"Goran"},{"first_name":"Kostiantyn","full_name":"Potomkin, Kostiantyn","last_name":"Potomkin"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","full_name":"Schilling, Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065"}],"doi":"10.1109/TCAD.2020.3012859"},{"external_id":{"arxiv":["1906.00110"]},"author":[{"full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","last_name":"Schmid","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","first_name":"Laura"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Schmid","full_name":"Schmid, Stefan","first_name":"Stefan"}],"file":[{"date_created":"2020-03-23T09:14:06Z","date_updated":"2020-07-14T12:47:56Z","file_name":"2019_LIPIcS_Schmid.pdf","creator":"dernst","checksum":"9a91916ac2c21ab42458fcda39ef0b8d","relation":"main_file","access_level":"open_access","file_id":"7608","content_type":"application/pdf","file_size":630752}],"doi":"10.4230/LIPIcs.OPODIS.2019.21","oa_version":"Preprint","article_number":"21","publication_status":"published","alternative_title":["LIPIcs"],"intvolume":"       153","arxiv":1,"conference":{"end_date":"2019-12-19","name":"OPODIS: International Conference on Principles of Distributed Systems","location":"Neuchâtel, Switzerland","start_date":"2019-12-17"},"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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>","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>","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.","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>.","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.","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>.","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."},"title":"The evolutionary price of anarchy: Locally bounded agents in a dynamic virus game","volume":153,"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"day":"10","date_updated":"2025-04-15T08:10:32Z","file_date_updated":"2020-07-14T12:47:56Z","year":"2020","type":"conference","language":[{"iso":"eng"}],"date_published":"2020-02-10T00:00:00Z","has_accepted_license":"1","department":[{"_id":"KrCh"}],"status":"public","oa":1,"month":"02","publication":"Proceedings of the 23rd International Conference on Principles of Distributed Systems","ddc":["000"],"quality_controlled":"1","date_created":"2020-01-21T16:00:26Z","scopus_import":"1","_id":"7346","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","abstract":[{"lang":"eng","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. "}]},{"corr_author":"1","isi":1,"month":"02","publication":"24th European Conference on Artificial Intelligence","status":"public","oa":1,"ddc":["000"],"quality_controlled":"1","_id":"7505","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)","image":"/images/cc_by_nc.png"},"date_created":"2020-02-21T16:44:03Z","scopus_import":"1","page":"2433-2440","ec_funded":1,"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.","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"}],"publisher":"IOS Press","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","article_processing_charge":"No","conference":{"location":"Santiago de Compostela, Spain","end_date":"2020-09-08","name":"ECAI: European Conference on Artificial Intelligence","start_date":"2020-08-29"},"project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"volume":325,"title":"Outside the box: Abstraction-based monitoring of neural networks","citation":{"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>","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>.","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.","short":"T.A. Henzinger, A. Lukina, C. Schilling, in:, 24th European Conference on Artificial Intelligence, IOS Press, 2020, pp. 2433–2440.","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.","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>."},"type":"conference","year":"2020","file_date_updated":"2020-09-21T07:12:32Z","day":"24","date_updated":"2025-04-15T06:26:13Z","has_accepted_license":"1","department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"date_published":"2020-02-24T00:00:00Z","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"publication_status":"published","intvolume":"       325","arxiv":1,"external_id":{"arxiv":["1911.09032"],"isi":["000650971303002"]},"doi":"10.3233/FAIA200375","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"first_name":"Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425","last_name":"Lukina","full_name":"Lukina, Anna"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"}],"file":[{"file_name":"2020_ECAI_Henzinger.pdf","creator":"dernst","success":1,"date_created":"2020-09-21T07:12:32Z","date_updated":"2020-09-21T07:12:32Z","relation":"main_file","access_level":"open_access","file_id":"8540","content_type":"application/pdf","file_size":1692214,"checksum":"80642fa0b6cd7da95dcd87d63789ad5e"}],"oa_version":"Published Version"},{"publication_status":"published","alternative_title":["LNCS"],"intvolume":"     12302","external_id":{"isi":["000723555700014"]},"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"doi":"10.1007/978-3-030-59152-6_14","file":[{"creator":"dernst","file_name":"2020_LNCS_ATVA_Asadi_accepted.pdf","date_updated":"2020-11-06T07:41:03Z","success":1,"date_created":"2020-11-06T07:41:03Z","checksum":"ae83f27e5b189d5abc2e7514f1b7e1b5","relation":"main_file","access_level":"open_access","file_size":726648,"file_id":"8729","content_type":"application/pdf"}],"author":[{"full_name":"Asadi, Ali","last_name":"Asadi","first_name":"Ali"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar"},{"full_name":"Mohammadi, Kiarash","last_name":"Mohammadi","first_name":"Kiarash"},{"orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Submitted Version","isi":1,"status":"public","oa":1,"publication":"Automated Technology for Verification and Analysis","month":"10","quality_controlled":"1","ddc":["000"],"page":"253-270","scopus_import":"1","date_created":"2020-11-06T07:30:05Z","_id":"8728","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"}],"publisher":"Springer Nature","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","conference":{"location":"Hanoi, Vietnam","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2020-10-23","start_date":"2020-10-19"},"article_processing_charge":"No","volume":12302,"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","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"}],"citation":{"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>","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>","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>.","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.","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>.","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.","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."},"title":"Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth","year":"2020","publication_identifier":{"eisbn":["9783030591526"],"eissn":["1611-3349"],"isbn":["9783030591519"],"issn":["0302-9743"]},"type":"conference","date_updated":"2026-09-04T22:31:00Z","day":"12","file_date_updated":"2020-11-06T07:41:03Z","has_accepted_license":"1","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"date_published":"2020-10-12T00:00:00Z"},{"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"title":"Polynomial invariant generation for non-deterministic recursive programs","citation":{"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.","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>.","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.","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>.","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.","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>","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>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://arxiv.org/abs/1902.04373","open_access":"1"}],"article_processing_charge":"No","conference":{"start_date":"2020-06-15","name":"PLDI: Programming Language Design and Implementation","end_date":"2020-06-20","location":"London, United Kingdom"},"department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"date_published":"2020-06-11T00:00:00Z","publication_identifier":{"isbn":["9781450376136"]},"year":"2020","type":"conference","date_updated":"2026-09-04T22:31:00Z","day":"11","quality_controlled":"1","isi":1,"publication":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation","month":"06","status":"public","oa":1,"abstract":[{"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.","lang":"eng"}],"publisher":"Association for Computing Machinery","_id":"8089","date_created":"2020-07-05T22:00:45Z","page":"672-687","scopus_import":"1","related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"external_id":{"arxiv":["1902.04373"],"isi":["000614622300045"]},"oa_version":"Preprint","doi":"10.1145/3385412.3385969","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu","full_name":"Fu, Hongfei"},{"last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ehsan Kafshdar","full_name":"Goharshady, Ehsan Kafshdar","last_name":"Goharshady"}],"publication_status":"published","arxiv":1},{"alternative_title":["LNCS"],"publication_status":"published","intvolume":"     12075","external_id":{"isi":["000681656800005"]},"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"doi":"10.1007/978-3-030-44914-8_5","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar"},{"last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"}],"file":[{"date_updated":"2020-07-14T12:48:03Z","date_created":"2020-05-26T13:34:48Z","file_name":"2020_LNCS_Chatterjee.pdf","creator":"dernst","content_type":"application/pdf","file_size":651250,"file_id":"7895","relation":"main_file","access_level":"open_access","checksum":"8618b80f4cf7b39a60e61a6445ad9807"}],"oa_version":"Published Version","corr_author":"1","isi":1,"month":"04","publication":"European Symposium on Programming","status":"public","oa":1,"quality_controlled":"1","ddc":["000"],"_id":"7810","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"page":"112-140","date_created":"2020-05-10T22:00:50Z","scopus_import":"1","abstract":[{"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.","lang":"eng"}],"publisher":"Springer Nature","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","conference":{"name":"ESOP: Programming Languages and Systems","end_date":"2020-04-30","location":"Dublin, Ireland","start_date":"2020-04-25"},"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies"}],"volume":12075,"title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","citation":{"short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 112–140.","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>.","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.","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>.","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>","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>"},"year":"2020","publication_identifier":{"isbn":["9783030449131"],"issn":["0302-9743"],"eissn":["1611-3349"]},"type":"conference","file_date_updated":"2020-07-14T12:48:03Z","date_updated":"2026-09-04T22:31:01Z","day":"18","has_accepted_license":"1","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"date_published":"2020-04-18T00:00:00Z"},{"intvolume":"     11388","alternative_title":["LNCS"],"publication_status":"published","arxiv":1,"external_id":{"arxiv":["1701.02944"],"isi":["000931943000022"]},"oa_version":"Preprint","doi":"10.1007/978-3-030-11245-5_22","author":[{"first_name":"Hongfei","full_name":"Fu, Hongfei","last_name":"Fu"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"quality_controlled":"1","isi":1,"month":"01","publication":"International Conference on Verification, Model Checking, and Abstract Interpretation","oa":1,"status":"public","abstract":[{"text":"We study the termination problem for nondeterministic probabilistic programs. We consider the bounded termination problem that asks whether the supremum of the expected termination time over all schedulers is bounded. First, we show that ranking supermartingales (RSMs) are both sound and complete for proving bounded termination over nondeterministic probabilistic programs. For nondeterministic probabilistic programs a previous result claimed that RSMs are not complete for bounded termination, whereas our result corrects the previous flaw and establishes completeness with a rigorous proof. Second, we present the first sound approach to establish lower bounds on expected termination time through RSMs.","lang":"eng"}],"publisher":"Springer Nature","OA_place":"repository","_id":"5948","page":"468-490","scopus_import":"1","date_created":"2019-02-10T22:59:17Z","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"volume":11388,"title":"Termination of nondeterministic probabilistic programs","citation":{"apa":"Fu, H., &#38; Chatterjee, K. (2019). Termination of nondeterministic probabilistic programs. In <i>International Conference on Verification, Model Checking, and Abstract Interpretation</i> (Vol. 11388, pp. 468–490). Cascais, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-11245-5_22\">https://doi.org/10.1007/978-3-030-11245-5_22</a>","chicago":"Fu, Hongfei, and Krishnendu Chatterjee. “Termination of Nondeterministic Probabilistic Programs.” In <i>International Conference on Verification, Model Checking, and Abstract Interpretation</i>, 11388:468–90. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-11245-5_22\">https://doi.org/10.1007/978-3-030-11245-5_22</a>.","ama":"Fu H, Chatterjee K. Termination of nondeterministic probabilistic programs. In: <i>International Conference on Verification, Model Checking, and Abstract Interpretation</i>. Vol 11388. Springer Nature; 2019:468-490. doi:<a href=\"https://doi.org/10.1007/978-3-030-11245-5_22\">10.1007/978-3-030-11245-5_22</a>","ieee":"H. Fu and K. Chatterjee, “Termination of nondeterministic probabilistic programs,” in <i>International Conference on Verification, Model Checking, and Abstract Interpretation</i>, Cascais, Portugal, 2019, vol. 11388, pp. 468–490.","short":"H. Fu, K. Chatterjee, in:, International Conference on Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2019, pp. 468–490.","mla":"Fu, Hongfei, and Krishnendu Chatterjee. “Termination of Nondeterministic Probabilistic Programs.” <i>International Conference on Verification, Model Checking, and Abstract Interpretation</i>, vol. 11388, Springer Nature, 2019, pp. 468–90, doi:<a href=\"https://doi.org/10.1007/978-3-030-11245-5_22\">10.1007/978-3-030-11245-5_22</a>.","ista":"Fu H, Chatterjee K. 2019. Termination of nondeterministic probabilistic programs. International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 11388, 468–490."},"OA_type":"green","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.02944"}],"article_processing_charge":"No","conference":{"start_date":"2019-01-13","location":"Cascais, Portugal","end_date":"2019-01-15","name":"VMCAI: Verification, Model Checking, and Abstract Interpretation"},"department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"date_published":"2019-01-11T00:00:00Z","type":"conference","year":"2019","day":"11","date_updated":"2025-07-03T11:45:45Z"},{"arxiv":1,"intvolume":"        22","publication_status":"published","oa_version":"Submitted Version","author":[{"first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy"},{"first_name":"Marcelo","full_name":"Forets, Marcelo","last_name":"Forets"},{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"full_name":"Potomkin, Kostiantyn","last_name":"Potomkin","first_name":"Kostiantyn"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","last_name":"Schilling","full_name":"Schilling, Christian"}],"file":[{"file_name":"hscc19.pdf","creator":"cschilli","date_created":"2019-03-05T09:27:18Z","date_updated":"2020-07-14T12:47:17Z","access_level":"open_access","relation":"main_file","file_size":3784414,"content_type":"application/pdf","file_id":"6067","checksum":"28ed56439aea5991c3122d4730fd828f"}],"doi":"10.1145/3302504.3311804","external_id":{"arxiv":["1901.10736"],"isi":["000516713900005"]},"publisher":"ACM","ec_funded":1,"abstract":[{"text":"We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.","lang":"eng"}],"_id":"6035","page":"39-44","date_created":"2019-02-18T14:43:28Z","scopus_import":"1","keyword":["reachability analysis","hybrid systems","lazy computation"],"ddc":["000"],"quality_controlled":"1","month":"04","publication":"Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control","status":"public","oa":1,"isi":1,"language":[{"iso":"eng"}],"date_published":"2019-04-16T00:00:00Z","department":[{"_id":"ToHe"}],"has_accepted_license":"1","file_date_updated":"2020-07-14T12:47:17Z","day":"16","date_updated":"2025-07-10T11:53:09Z","publication_identifier":{"isbn":["9781450362825"]},"type":"conference","year":"2019","title":"JuliaReach: A toolbox for set-based reachability","citation":{"short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 39–44.","mla":"Bogomolov, Sergiy, et al. “JuliaReach: A Toolbox for Set-Based Reachability.” <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>, vol. 22, ACM, 2019, pp. 39–44, doi:<a href=\"https://doi.org/10.1145/3302504.3311804\">10.1145/3302504.3311804</a>.","ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2019. JuliaReach: A toolbox for set-based reachability. Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control vol. 22, 39–44.","ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach: A toolbox for set-based reachability,” in <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>, Montreal, QC, Canada, 2019, vol. 22, pp. 39–44.","chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “JuliaReach: A Toolbox for Set-Based Reachability.” In <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>, 22:39–44. ACM, 2019. <a href=\"https://doi.org/10.1145/3302504.3311804\">https://doi.org/10.1145/3302504.3311804</a>.","ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. JuliaReach: A toolbox for set-based reachability. In: <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>. Vol 22. ACM; 2019:39-44. doi:<a href=\"https://doi.org/10.1145/3302504.3311804\">10.1145/3302504.3311804</a>","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., &#38; Schilling, C. (2019). JuliaReach: A toolbox for set-based reachability. In <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i> (Vol. 22, pp. 39–44). Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/3302504.3311804\">https://doi.org/10.1145/3302504.3311804</a>"},"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"}],"volume":22,"article_processing_charge":"No","conference":{"start_date":"2019-04-16","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2019-04-18","location":"Montreal, QC, Canada"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"oa_version":"Published Version","doi":"10.1007/978-3-030-17462-0_13","file":[{"date_created":"2019-05-10T14:16:05Z","date_updated":"2020-07-14T12:47:17Z","file_name":"2019_LNCS_Christakis.pdf","creator":"dernst","relation":"main_file","access_level":"open_access","file_id":"6408","file_size":773083,"content_type":"application/pdf","checksum":"9998496f6fe202c0a19124b4209154c6"}],"author":[{"full_name":"Christakis, Maria","last_name":"Christakis","first_name":"Maria"},{"first_name":"Matthias","last_name":"Heizmann","full_name":"Heizmann, Matthias"},{"first_name":"Muhammad Numair","full_name":"Mansur, Muhammad Numair","last_name":"Mansur"},{"last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Wüstholz, Valentin","last_name":"Wüstholz","first_name":"Valentin"}],"external_id":{"isi":["000681166500013"]},"intvolume":"     11427","alternative_title":["LNCS"],"publication_status":"published","department":[{"_id":"ToHe"}],"has_accepted_license":"1","language":[{"iso":"eng"}],"date_published":"2019-04-04T00:00:00Z","type":"conference","year":"2019","file_date_updated":"2020-07-14T12:47:17Z","date_updated":"2025-04-15T06:26:12Z","day":"04","project":[{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"volume":11427,"title":"Semantic fault localization and suspiciousness ranking","citation":{"ieee":"M. Christakis, M. Heizmann, M. N. Mansur, C. Schilling, and V. Wüstholz, “Semantic fault localization and suspiciousness ranking,” in <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, Prague, Czech Republic, 2019, vol. 11427, pp. 226–243.","chicago":"Christakis, Maria, Matthias Heizmann, Muhammad Numair Mansur, Christian Schilling, and Valentin Wüstholz. “Semantic Fault Localization and Suspiciousness Ranking.” In <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, 11427:226–43. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">https://doi.org/10.1007/978-3-030-17462-0_13</a>.","ama":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. Semantic fault localization and suspiciousness ranking. In: <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 11427. Springer Nature; 2019:226-243. doi:<a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">10.1007/978-3-030-17462-0_13</a>","apa":"Christakis, M., Heizmann, M., Mansur, M. N., Schilling, C., &#38; Wüstholz, V. (2019). Semantic fault localization and suspiciousness ranking. In <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i> (Vol. 11427, pp. 226–243). Prague, Czech Republic: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">https://doi.org/10.1007/978-3-030-17462-0_13</a>","ista":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. 2019. Semantic fault localization and suspiciousness ranking. 25th 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. 11427, 226–243.","mla":"Christakis, Maria, et al. “Semantic Fault Localization and Suspiciousness Ranking.” <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, vol. 11427, Springer Nature, 2019, pp. 226–43, doi:<a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">10.1007/978-3-030-17462-0_13</a>.","short":"M. Christakis, M. Heizmann, M.N. Mansur, C. Schilling, V. Wüstholz, in:, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2019, pp. 226–243."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","article_processing_charge":"No","conference":{"start_date":"2019-04-06","location":"Prague, Czech Republic","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2019-04-11"},"ec_funded":1,"abstract":[{"text":"Static program analyzers are increasingly effective in checking correctness properties of programs and reporting any errors found, often in the form of error traces. However, developers still spend a significant amount of time on debugging. This involves processing long error traces in an effort to localize a bug to a relatively small part of the program and to identify its cause. In this paper, we present a technique for automated fault localization that, given a program and an error trace, efficiently narrows down the cause of the error to a few statements. These statements are then ranked in terms of their suspiciousness. Our technique relies only on the semantics of the given program and does not require any test cases or user guidance. In experiments on a set of C benchmarks, we show that our technique is effective in quickly isolating the cause of error while out-performing other state-of-the-art fault-localization techniques.","lang":"eng"}],"publisher":"Springer Nature","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"_id":"6042","page":"226-243","scopus_import":"1","date_created":"2019-02-18T16:44:06Z","ddc":["000"],"quality_controlled":"1","isi":1,"month":"04","publication":"25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ","status":"public","oa":1},{"keyword":["safety","risk","reliability and quality","software"],"date_created":"2021-10-27T14:57:06Z","scopus_import":"1","OA_place":"publisher","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"_id":"10190","abstract":[{"text":"The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning.","lang":"eng"}],"acknowledgement":"The authors would also like to thank anonymous referees for their valuable comments and helpful suggestions. This work is supported by the Austrian Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE), by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian Science Fund (FWF) Schrodinger grant J-4220.\r\n","publisher":"ACM","corr_author":"1","status":"public","oa":1,"publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","month":"10","ddc":["000"],"quality_controlled":"1","publication_identifier":{"eissn":["2475-1421"]},"type":"conference","year":"2019","day":"10","date_updated":"2026-04-08T07:00:31Z","file_date_updated":"2021-11-12T11:41:56Z","has_accepted_license":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"date_published":"2019-10-10T00:00:00Z","language":[{"iso":"eng"}],"OA_type":"hybrid","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2019-10-23","end_date":"2019-10-25","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","location":"Athens, Greece"},"article_processing_charge":"No","volume":3,"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"}],"citation":{"apa":"Chatterjee, K., Pavlogiannis, A., &#38; Toman, V. (2019). Value-centric dynamic partial order reduction. In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i> (Vol. 3). Athens, Greece: ACM. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric Dynamic Partial Order Reduction.” In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Vol. 3. ACM, 2019. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Athens, Greece, 2019, vol. 3.","ama":"Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>. Vol 3. ACM; 2019. doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>","mla":"Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, vol. 3, 124, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>.","ista":"Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124.","short":"K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019."},"title":"Value-centric dynamic partial order reduction","arxiv":1,"publication_status":"published","article_number":"124","intvolume":"         3","doi":"10.1145/3360550","file":[{"checksum":"2149979c46964c4d117af06ccb6c0834","file_id":"10278","content_type":"application/pdf","file_size":570829,"relation":"main_file","access_level":"open_access","creator":"cchlebak","file_name":"2019_ACM_Chatterjee.pdf","success":1,"date_created":"2021-11-12T11:41:56Z","date_updated":"2021-11-12T11:41:56Z"}],"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"oa_version":"Published Version","external_id":{"arxiv":["1909.00989"]},"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"10199"}]}},{"oa_version":"Submitted Version","author":[{"first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","last_name":"Ferrere","full_name":"Ferrere, Thomas"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Donzé","full_name":"Donzé, Alexandre","first_name":"Alexandre"},{"first_name":"Hisahiro","full_name":"Ito, Hisahiro","last_name":"Ito"},{"first_name":"James","last_name":"Kapinski","full_name":"Kapinski, James"}],"file":[{"checksum":"b8e967081e051d1c55ca5d18fb187890","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"8633","file_size":1055421,"date_created":"2020-10-08T17:25:45Z","date_updated":"2020-10-08T17:25:45Z","success":1,"creator":"dernst","file_name":"2019_ACM_Ferrere.pdf"}],"doi":"10.1145/3302504.3311800","external_id":{"isi":["000516713900007"]},"publication_status":"published","date_published":"2019-04-16T00:00:00Z","language":[{"iso":"eng"}],"has_accepted_license":"1","department":[{"_id":"ToHe"}],"file_date_updated":"2020-10-08T17:25:45Z","date_updated":"2025-07-10T11:53:22Z","day":"16","year":"2019","publication_identifier":{"isbn":["9781450362825"]},"type":"conference","title":"Interface-aware signal temporal logic","citation":{"short":"T. Ferrere, D. Nickovic, A. Donzé, H. Ito, J. Kapinski, in:, Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 57–66.","ista":"Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. 2019. Interface-aware signal temporal logic. Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 57–66.","mla":"Ferrere, Thomas, et al. “Interface-Aware Signal Temporal Logic.” <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2019, pp. 57–66, doi:<a href=\"https://doi.org/10.1145/3302504.3311800\">10.1145/3302504.3311800</a>.","chicago":"Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James Kapinski. “Interface-Aware Signal Temporal Logic.” In <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, 57–66. ACM, 2019. <a href=\"https://doi.org/10.1145/3302504.3311800\">https://doi.org/10.1145/3302504.3311800</a>.","apa":"Ferrere, T., Nickovic, D., Donzé, A., Ito, H., &#38; Kapinski, J. (2019). Interface-aware signal temporal logic. In <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i> (pp. 57–66). Montreal, Canada: ACM. <a href=\"https://doi.org/10.1145/3302504.3311800\">https://doi.org/10.1145/3302504.3311800</a>","ieee":"T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware signal temporal logic,” in <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, Montreal, Canada, 2019, pp. 57–66.","ama":"Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. Interface-aware signal temporal logic. In: <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2019:57-66. doi:<a href=\"https://doi.org/10.1145/3302504.3311800\">10.1145/3302504.3311800</a>"},"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"article_processing_charge":"No","conference":{"start_date":"2019-04-16","location":"Montreal, Canada","end_date":"2019-04-18","name":"HSCC: Hybrid Systems - Computation and Control"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"ACM","abstract":[{"lang":"eng","text":"Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system."}],"_id":"6428","page":"57-66","date_created":"2019-05-13T08:13:46Z","scopus_import":"1","quality_controlled":"1","ddc":["000"],"month":"04","publication":"Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control","oa":1,"status":"public","isi":1},{"volume":11561,"project":[{"_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"citation":{"ieee":"G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger, “Run-time optimization for learned controllers through quantitative games,” in <i>31st International Conference on Computer-Aided Verification</i>, New York, NY, United States, 2019, vol. 11561, pp. 630–649.","apa":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., &#38; Pranger, S. (2019). Run-time optimization for learned controllers through quantitative games. In <i>31st International Conference on Computer-Aided Verification</i> (Vol. 11561, pp. 630–649). New York, NY, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">https://doi.org/10.1007/978-3-030-25540-4_36</a>","chicago":"Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers through Quantitative Games.” In <i>31st International Conference on Computer-Aided Verification</i>, 11561:630–49. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">https://doi.org/10.1007/978-3-030-25540-4_36</a>.","ama":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time optimization for learned controllers through quantitative games. In: <i>31st International Conference on Computer-Aided Verification</i>. Vol 11561. Springer; 2019:630-649. doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">10.1007/978-3-030-25540-4_36</a>","mla":"Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative Games.” <i>31st International Conference on Computer-Aided Verification</i>, vol. 11561, Springer, 2019, pp. 630–49, doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">10.1007/978-3-030-25540-4_36</a>.","ista":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019. Run-time optimization for learned controllers through quantitative games. 31st International Conference on Computer-Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 11561, 630–649.","short":"G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 630–649."},"title":"Run-time optimization for learned controllers through quantitative games","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","conference":{"name":"CAV: Computer Aided Verification","end_date":"2019-07-18","location":"New York, NY, United States","start_date":"2019-07-13"},"article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"has_accepted_license":"1","date_published":"2019-07-12T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"year":"2019","date_updated":"2025-04-15T06:26:05Z","day":"12","file_date_updated":"2020-07-14T12:47:31Z","ddc":["000"],"quality_controlled":"1","isi":1,"corr_author":"1","status":"public","oa":1,"month":"07","publication":"31st International Conference on Computer-Aided Verification","abstract":[{"lang":"eng","text":"A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive  synthesis.  First,  we  abstract  the  plant  by  building  a  stochastic  model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles."}],"publisher":"Springer","page":"630-649","scopus_import":"1","date_created":"2019-05-16T11:22:30Z","_id":"6462","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000491468000036"]},"oa_version":"Published Version","doi":"10.1007/978-3-030-25540-4_36","author":[{"first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","last_name":"Avni","full_name":"Avni, Guy"},{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"first_name":"Bettina","full_name":"Konighofer, Bettina","last_name":"Konighofer"},{"last_name":"Pranger","full_name":"Pranger, Stefan","first_name":"Stefan"}],"file":[{"creator":"dernst","file_name":"2019_CAV_Avni.pdf","date_created":"2019-08-14T09:35:24Z","date_updated":"2020-07-14T12:47:31Z","checksum":"c231579f2485c6fd4df17c9443a4d80b","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"6816","file_size":659766}],"intvolume":"     11561","publication_status":"published","alternative_title":["LNCS"]},{"citation":{"short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.","ista":"Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. 2019. Membership-based synthesis of linear hybrid automata. 31st International Conference on Computer-Aided Verification. CAV: Computer-Aided Verification, LNCS, vol. 11561, 297–314.","mla":"Garcia Soto, Miriam, et al. “Membership-Based Synthesis of Linear Hybrid Automata.” <i>31st International Conference on Computer-Aided Verification</i>, vol. 11561, Springer, 2019, pp. 297–314, doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">10.1007/978-3-030-25540-4_16</a>.","ieee":"M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based synthesis of linear hybrid automata,” in <i>31st International Conference on Computer-Aided Verification</i>, New York City, NY, USA, 2019, vol. 11561, pp. 297–314.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In <i>31st International Conference on Computer-Aided Verification</i>, 11561:297–314. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">https://doi.org/10.1007/978-3-030-25540-4_16</a>.","apa":"Garcia Soto, M., Henzinger, T. A., Schilling, C., &#38; Zeleznik, L. (2019). Membership-based synthesis of linear hybrid automata. In <i>31st International Conference on Computer-Aided Verification</i> (Vol. 11561, pp. 297–314). New York City, NY, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">https://doi.org/10.1007/978-3-030-25540-4_16</a>","ama":"Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis of linear hybrid automata. In: <i>31st International Conference on Computer-Aided Verification</i>. Vol 11561. Springer; 2019:297-314. doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">10.1007/978-3-030-25540-4_16</a>"},"title":"Membership-based synthesis of linear hybrid automata","volume":11561,"project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"conference":{"start_date":"2019-07-15","location":"New York City, NY, USA","name":"CAV: Computer-Aided Verification","end_date":"2019-07-18"},"article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","language":[{"iso":"eng"}],"date_published":"2019-07-12T00:00:00Z","department":[{"_id":"ToHe"}],"has_accepted_license":"1","date_updated":"2025-04-15T06:26:13Z","day":"12","file_date_updated":"2020-07-14T12:47:32Z","type":"conference","year":"2019","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"quality_controlled":"1","ddc":["000"],"oa":1,"status":"public","month":"07","publication":"31st International Conference on Computer-Aided Verification","isi":1,"corr_author":"1","publisher":"Springer","abstract":[{"text":"We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements.","lang":"eng"}],"ec_funded":1,"date_created":"2019-05-27T07:09:53Z","scopus_import":"1","page":"297-314","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"_id":"6493","keyword":["Synthesis","Linear hybrid automaton","Membership"],"external_id":{"isi":["000491468000016"]},"oa_version":"Published Version","file":[{"date_updated":"2020-07-14T12:47:32Z","date_created":"2019-08-14T11:05:30Z","creator":"dernst","file_name":"2019_CAV_GarciaSoto.pdf","file_id":"6817","content_type":"application/pdf","file_size":674795,"relation":"main_file","access_level":"open_access","checksum":"1f1d61b83a151031745ef70a501da3d6"}],"author":[{"first_name":"Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","orcid":"0000−0003−2936−5719","full_name":"Garcia Soto, Miriam"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","last_name":"Schilling","full_name":"Schilling, Christian"},{"first_name":"Luka","id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87","last_name":"Zeleznik","full_name":"Zeleznik, Luka"}],"doi":"10.1007/978-3-030-25540-4_16","intvolume":"     11561","publication_status":"published","alternative_title":["LNCS"]}]