[{"language":[{"iso":"eng"}],"doi":"10.1098/rspb.2015.1041","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","oa":1,"external_id":{"pmid":["26180069"]},"main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4528522/","open_access":"1"}],"month":"07","volume":282,"date_updated":"2023-09-07T11:40:43Z","date_created":"2018-12-11T11:53:35Z","related_material":{"record":[{"id":"1400","relation":"dissertation_contains","status":"public"}]},"author":[{"last_name":"Reiter","first_name":"Johannes","orcid":"0000-0002-0170-7353","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","full_name":"Reiter, Johannes"},{"full_name":"Kanodia, Ayush","first_name":"Ayush","last_name":"Kanodia"},{"full_name":"Gupta, Raghav","first_name":"Raghav","last_name":"Gupta"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"department":[{"_id":"KrCh"}],"publisher":"Royal Society","publication_status":"published","pmid":1,"year":"2015","acknowledgement":"This work was supported by grants from the John Templeton Foundation, ERC Start Grant (279307: Graph Games), FWF NFN Grant (No S11407N23 RiSE/SHiNE), FWF Grant (No P23499N23) and a Microsoft faculty fellows award.","publist_id":"5425","date_published":"2015-07-15T00:00:00Z","article_type":"original","citation":{"apa":"Reiter, J., Kanodia, A., Gupta, R., Nowak, M., & Chatterjee, K. (2015). Biological auctions with multiple rewards. Proceedings of the Royal Society of London Series B Biological Sciences. Royal Society. https://doi.org/10.1098/rspb.2015.1041","ieee":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, and K. Chatterjee, “Biological auctions with multiple rewards,” Proceedings of the Royal Society of London Series B Biological Sciences, vol. 282, no. 1812. Royal Society, 2015.","ista":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. 2015. Biological auctions with multiple rewards. Proceedings of the Royal Society of London Series B Biological Sciences. 282(1812).","ama":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. Biological auctions with multiple rewards. Proceedings of the Royal Society of London Series B Biological Sciences. 2015;282(1812). doi:10.1098/rspb.2015.1041","chicago":"Reiter, Johannes, Ayush Kanodia, Raghav Gupta, Martin Nowak, and Krishnendu Chatterjee. “Biological Auctions with Multiple Rewards.” Proceedings of the Royal Society of London Series B Biological Sciences. Royal Society, 2015. https://doi.org/10.1098/rspb.2015.1041.","short":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of the Royal Society of London Series B Biological Sciences 282 (2015).","mla":"Reiter, Johannes, et al. “Biological Auctions with Multiple Rewards.” Proceedings of the Royal Society of London Series B Biological Sciences, vol. 282, no. 1812, Royal Society, 2015, doi:10.1098/rspb.2015.1041."},"publication":"Proceedings of the Royal Society of London Series B Biological Sciences","article_processing_charge":"No","day":"15","scopus_import":1,"oa_version":"Submitted Version","intvolume":" 282","title":"Biological auctions with multiple rewards","status":"public","_id":"1709","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"1812","abstract":[{"lang":"eng","text":"The competition for resources among cells, individuals or species is a fundamental characteristic of evolution. Biological all-pay auctions have been used to model situations where multiple individuals compete for a single resource. However, in many situations multiple resources with various values exist and single reward auctions are not applicable. We generalize the model to multiple rewards and study the evolution of strategies. In biological all-pay auctions the bid of an individual corresponds to its strategy and is equivalent to its payment in the auction. The decreasingly ordered rewards are distributed according to the decreasingly ordered bids of the participating individuals. The reproductive success of an individual is proportional to its fitness given by the sum of the rewards won minus its payments. Hence, successful bidding strategies spread in the population. We find that the results for the multiple reward case are very different from the single reward case. While the mixed strategy equilibrium in the single reward case with more than two players consists of mostly low-bidding individuals, we show that the equilibrium can convert to many high-bidding individuals and a few low-bidding individuals in the multiple reward case. Some reward values lead to a specialization among the individuals where one subpopulation competes for the rewards and the other subpopulation largely avoids costly competitions. Whether the mixed strategy equilibrium is an evolutionarily stable strategy (ESS) depends on the specific values of the rewards."}],"type":"journal_article"},{"date_published":"2015-04-01T00:00:00Z","supervisor":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"}],"degree_awarded":"PhD","language":[{"iso":"eng"}],"citation":{"ama":"Reiter J. The subclonal evolution of cancer. 2015.","ieee":"J. Reiter, “The subclonal evolution of cancer,” Institute of Science and Technology Austria, 2015.","apa":"Reiter, J. (2015). The subclonal evolution of cancer. Institute of Science and Technology Austria.","ista":"Reiter J. 2015. The subclonal evolution of cancer. Institute of Science and Technology Austria.","short":"J. Reiter, The Subclonal Evolution of Cancer, Institute of Science and Technology Austria, 2015.","mla":"Reiter, Johannes. The Subclonal Evolution of Cancer. Institute of Science and Technology Austria, 2015.","chicago":"Reiter, Johannes. “The Subclonal Evolution of Cancer.” Institute of Science and Technology Austria, 2015."},"page":"183","month":"04","day":"01","article_processing_charge":"No","publication_identifier":{"issn":["2663-337X"]},"author":[{"full_name":"Reiter, Johannes","first_name":"Johannes","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353"}],"related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"1709"},{"status":"public","relation":"part_of_dissertation","id":"2000"},{"status":"public","relation":"part_of_dissertation","id":"2247"},{"id":"2816","relation":"part_of_dissertation","status":"public"},{"id":"2858","status":"public","relation":"part_of_dissertation"},{"id":"3157","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"3260"}]},"date_created":"2018-12-11T11:51:48Z","date_updated":"2023-09-07T11:40:44Z","oa_version":"None","_id":"1400","year":"2015","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_status":"published","status":"public","title":"The subclonal evolution of cancer","department":[{"_id":"KrCh"}],"publisher":"Institute of Science and Technology Austria","abstract":[{"text":"Cancer results from an uncontrolled growth of abnormal cells. Sequentially accumulated genetic and epigenetic alterations decrease cell death and increase cell replication. We used mathematical models to quantify the effect of driver gene mutations. The recently developed targeted therapies can lead to dramatic regressions. However, in solid cancers, clinical responses are often short-lived because resistant cancer cells evolve. We estimated that approximately 50 different mutations can confer resistance to a typical targeted therapeutic agent. We find that resistant cells are likely to be present in expanded subclones before the start of the treatment. The dominant strategy to prevent the evolution of resistance is combination therapy. Our analytical results suggest that in most patients, dual therapy, but not monotherapy, can result in long-term disease control. However, long-term control can only occur if there are no possible mutations in the genome that can cause cross-resistance to both drugs. Furthermore, we showed that simultaneous therapy with two drugs is much more likely to result in long-term disease control than sequential therapy with the same drugs. To improve our understanding of the underlying subclonal evolution we reconstruct the evolutionary history of a patient's cancer from next-generation sequencing data of spatially-distinct DNA samples. Using a quantitative measure of genetic relatedness, we found that pancreatic cancers and their metastases demonstrated a higher level of relatedness than that expected for any two cells randomly taken from a normal tissue. This minimal amount of genetic divergence among advanced lesions indicates that genetic heterogeneity, when quantitatively defined, is not a fundamental feature of the natural history of untreated pancreatic cancers. Our newly developed, phylogenomic tool Treeomics finds evidence for seeding patterns of metastases and can directly be used to discover rules governing the evolution of solid malignancies to transform cancer into a more predictable disease.","lang":"eng"}],"publist_id":"5807","type":"dissertation","alternative_title":["ISTA Thesis"]},{"date_published":"2015-05-01T00:00:00Z","citation":{"chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. https://doi.org/10.1145/2737166.2737175.","mla":"Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory. ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.","short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","ista":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition operators for IOCO-testing theory. CBSE: Component-Based Software Engineering , Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering , , 101–110.","apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., & Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. https://doi.org/10.1145/2737166.2737175","ieee":"N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175"},"page":"101 - 110","day":"01","has_accepted_license":"1","scopus_import":1,"pubrep_id":"625","oa_version":"Submitted Version","file":[{"file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf","access_level":"open_access","content_type":"application/pdf","file_size":467561,"creator":"system","relation":"main_file","file_id":"5303","date_updated":"2020-07-14T12:44:59Z","date_created":"2018-12-12T10:17:46Z","checksum":"c6ce681035c163a158751f240cb7d389"}],"_id":"1502","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","ddc":["000"],"title":"Complete composition operators for IOCO-testing theory","abstract":[{"text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system.","lang":"eng"}],"type":"conference","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"conference":{"name":"CBSE: Component-Based Software Engineering ","location":"Montreal, QC, Canada","start_date":"2015-05-04","end_date":"2015-05-08"},"doi":"10.1145/2737166.2737175","language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"month":"05","publication_identifier":{"isbn":["978-1-4503-3471-6"]},"author":[{"full_name":"Beneš, Nikola","first_name":"Nikola","last_name":"Beneš"},{"first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan"},{"full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"}],"related_material":{"record":[{"id":"1155","status":"public","relation":"dissertation_contains"}]},"date_created":"2018-12-11T11:52:24Z","date_updated":"2023-09-07T11:58:33Z","year":"2015","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373 (nSafeCer). Jan Křetínský has been partially supported by the Czech Science Foundation, grant No. P202/12/G061. Nikola Beneš has been supported by the\r\nMEYS project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"ACM","file_date_updated":"2020-07-14T12:44:59Z","publist_id":"5676","ec_funded":1},{"publist_id":"5677","ec_funded":1,"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","year":"2015","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","date_created":"2018-12-11T11:52:23Z","date_updated":"2023-09-07T11:58:33Z","volume":47,"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","last_name":"Daca","full_name":"Daca, Przemyslaw"}],"related_material":{"record":[{"id":"1155","status":"public","relation":"dissertation_contains"}]},"month":"10","quality_controlled":"1","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1405.0835","open_access":"1"}],"language":[{"iso":"eng"}],"doi":"10.1007/s10703-015-0235-2","type":"journal_article","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. "}],"issue":"2","title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","status":"public","intvolume":" 47","_id":"1501","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","scopus_import":1,"day":"01","page":"230 - 264","publication":"Formal Methods in System Design","citation":{"ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 2015;47(2):230-264. doi:10.1007/s10703-015-0235-2","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” Formal Methods in System Design, vol. 47, no. 2. Springer, pp. 230–264, 2015.","apa":"Chatterjee, K., Chmelik, M., & Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-015-0235-2","mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” Formal Methods in System Design, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:10.1007/s10703-015-0235-2.","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” Formal Methods in System Design. Springer, 2015. https://doi.org/10.1007/s10703-015-0235-2."},"date_published":"2015-10-01T00:00:00Z"},{"volume":50,"date_updated":"2023-09-07T12:01:58Z","date_created":"2018-12-11T11:52:58Z","related_material":{"record":[{"id":"821","relation":"dissertation_contains","status":"public"}]},"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"},{"full_name":"Goyal, Prateesh","last_name":"Goyal","first_name":"Prateesh"}],"department":[{"_id":"KrCh"}],"publisher":"ACM","publication_status":"published","acknowledgement":"We thank anonymous reviewers for helpful comments to improve the presentation of the paper.","year":"2015","ec_funded":1,"publist_id":"5565","language":[{"iso":"eng"}],"doi":"10.1145/2676726.2676979","conference":{"end_date":"2015-01-17","start_date":"2015-01-15","location":"Mumbai, India","name":"SIGPLAN: Symposium on Principles of Programming Languages"},"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","external_id":{"arxiv":["1410.7724"]},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1410.7724"}],"month":"01","oa_version":"Preprint","intvolume":" 50","status":"public","title":"Faster algorithms for algebraic path properties in recursive state machines with constant treewidth","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1602","issue":"1","abstract":[{"text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks.","lang":"eng"}],"type":"journal_article","date_published":"2015-01-01T00:00:00Z","page":"97 - 109","citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” ACM SIGPLAN Notices. ACM, 2015. https://doi.org/10.1145/2676726.2676979.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” ACM SIGPLAN Notices, vol. 50, no. 1, ACM, 2015, pp. 97–109, doi:10.1145/2676726.2676979.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. 2015. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 50(1), 97–109.","apa":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., & Goyal, P. (2015). Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. Mumbai, India: ACM. https://doi.org/10.1145/2676726.2676979","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, and P. Goyal, “Faster algorithms for algebraic path properties in recursive state machines with constant treewidth,” ACM SIGPLAN Notices, vol. 50, no. 1. ACM, pp. 97–109, 2015.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 2015;50(1):97-109. doi:10.1145/2676726.2676979"},"publication":"ACM SIGPLAN Notices","day":"01","scopus_import":1},{"scopus_import":1,"day":"01","publication":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT ","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . ACM, 2015. https://doi.org/10.1145/2676726.2676968.","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT 50 (2015) 539–551.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1, ACM, 2015, pp. 539–51, doi:10.1145/2676726.2676968.","apa":"Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2015). Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . Mumbai, India: ACM. https://doi.org/10.1145/2676726.2676968","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural analysis,” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1. ACM, pp. 539–551, 2015.","ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 2015;50(1):539-551. doi:10.1145/2676726.2676968"},"page":"539 - 551","date_published":"2015-01-01T00:00:00Z","type":"journal_article","abstract":[{"text":"We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs.","lang":"eng"}],"issue":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1604","title":"Quantitative interprocedural analysis","status":"public","intvolume":" 50","pubrep_id":"523","oa_version":"None","month":"01","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"quality_controlled":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"conference":{"end_date":"2015-01-17","location":"Mumbai, India","start_date":"2015-01-15","name":"SIGPLAN: Symposium on Principles of Programming Languages"},"doi":"10.1145/2676726.2676968","language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"5563","year":"2015","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"ACM","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"related_material":{"record":[{"id":"5445","status":"public","relation":"earlier_version"},{"relation":"dissertation_contains","status":"public","id":"821"}]},"date_updated":"2023-09-07T12:01:59Z","date_created":"2018-12-11T11:52:59Z","volume":50},{"main_file_link":[{"url":"http://arxiv.org/abs/1504.07384","open_access":"1"}],"oa":1,"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","doi":"10.1007/978-3-319-21690-4_9","conference":{"start_date":"2015-07-18","location":"San Francisco, CA, USA","end_date":"2015-07-24","name":"CAV: Computer Aided Verification"},"language":[{"iso":"eng"}],"month":"07","year":"2015","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.","department":[{"_id":"KrCh"}],"publisher":"Springer","publication_status":"published","related_material":{"record":[{"id":"5430","status":"public","relation":"earlier_version"},{"id":"5437","status":"public","relation":"earlier_version"},{"relation":"dissertation_contains","status":"public","id":"821"}]},"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"}],"volume":9206,"date_created":"2018-12-11T11:52:59Z","date_updated":"2023-09-07T12:01:59Z","ec_funded":1,"publist_id":"5560","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. Vol. 9206, Springer, 2015, pp. 140–57, doi:10.1007/978-3-319-21690-4_9.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,” 9206:140–57. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_9.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157. doi:10.1007/978-3-319-21690-4_9","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in constant treewidth graphs,” presented at the CAV: Computer Aided Verification, San Francisco, CA, USA, 2015, vol. 9206, pp. 140–157.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157). Presented at the CAV: Computer Aided Verification, San Francisco, CA, USA: Springer. https://doi.org/10.1007/978-3-319-21690-4_9","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification, LNCS, vol. 9206, 140–157."},"page":"140 - 157","date_published":"2015-07-16T00:00:00Z","scopus_import":1,"day":"16","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1607","intvolume":" 9206","status":"public","title":"Faster algorithms for quantitative verification in constant treewidth graphs","oa_version":"Preprint","type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.","lang":"eng"}]},{"date_published":"2015-01-15T00:00:00Z","citation":{"short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, in:, Real-Time Systems Symposium, IEEE, 2015, pp. 118–127.","mla":"Chatterjee, Krishnendu, et al. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” Real-Time Systems Symposium, vol. 2015, no. January, IEEE, 2015, pp. 118–27, doi:10.1109/RTSS.2014.9.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” In Real-Time Systems Symposium, 2015:118–27. IEEE, 2015. https://doi.org/10.1109/RTSS.2014.9.","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In: Real-Time Systems Symposium. Vol 2015. IEEE; 2015:118-127. doi:10.1109/RTSS.2014.9","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks,” in Real-Time Systems Symposium, Rome, Italy, 2015, vol. 2015, no. January, pp. 118–127.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2015). A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In Real-Time Systems Symposium (Vol. 2015, pp. 118–127). Rome, Italy: IEEE. https://doi.org/10.1109/RTSS.2014.9","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2015. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium vol. 2015, 118–127."},"publication":"Real-Time Systems Symposium","page":"118 - 127","article_processing_charge":"No","day":"15","scopus_import":1,"oa_version":"None","_id":"1714","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 2015","title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","status":"public","issue":"January","abstract":[{"lang":"eng","text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application."}],"type":"conference","doi":"10.1109/RTSS.2014.9","conference":{"location":"Rome, Italy","start_date":"2014-12-02","end_date":"2014-12-05","name":"RTSS: Real-Time Systems Symposium"},"language":[{"iso":"eng"}],"quality_controlled":"1","month":"01","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5423"},{"id":"821","status":"public","relation":"dissertation_contains"}]},"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"full_name":"Kößler, Alexander","last_name":"Kößler","first_name":"Alexander"},{"first_name":"Ulrich","last_name":"Schmid","full_name":"Schmid, Ulrich"}],"volume":2015,"date_created":"2018-12-11T11:53:37Z","date_updated":"2023-09-07T12:01:59Z","year":"2015","publisher":"IEEE","department":[{"_id":"KrCh"}],"publication_status":"published","publist_id":"5417"},{"abstract":[{"lang":"eng","text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks."}],"file_date_updated":"2020-07-14T12:46:56Z","alternative_title":["IST Austria Technical Report"],"type":"technical_report","date_created":"2018-12-12T11:39:21Z","date_updated":"2023-09-19T14:36:19Z","file":[{"file_id":"5531","relation":"main_file","checksum":"df383dc62c94d7b2ea639aba088a76c6","date_created":"2018-12-12T11:54:09Z","date_updated":"2020-07-14T12:46:56Z","access_level":"open_access","file_name":"IST-2015-340-v1+1_main.pdf","creator":"system","file_size":861396,"content_type":"application/pdf"}],"oa_version":"Published Version","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","first_name":"Amir","last_name":"Goharshady","full_name":"Goharshady, Amir"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"pubrep_id":"340","related_material":{"record":[{"id":"1437","status":"public","relation":"later_version"},{"relation":"earlier_version","status":"public","id":"5442"},{"id":"6009","status":"public","relation":"later_version"}]},"status":"public","ddc":["000"],"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","publication_status":"published","publisher":"IST Austria","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5441","year":"2015","day":"11","month":"07","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2015-340-v1-1","date_published":"2015-07-11T00:00:00Z","page":"24","oa":1,"citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-340-v1-1.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015, doi:10.15479/AT:IST-2015-340-v1-1.","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A. (2015). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria. https://doi.org/10.15479/AT:IST-2015-340-v1-1","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria, 2015.","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2015. Algorithms for algebraic path properties in concurrent systems of constant treewidth components, IST Austria, 24p.","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria; 2015. doi:10.15479/AT:IST-2015-340-v1-1"}},{"abstract":[{"text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study.","lang":"eng"}],"ec_funded":1,"publist_id":"5456","type":"conference","author":[{"first_name":"Mária","last_name":"Svoreňová","full_name":"Svoreňová, Mária"},{"full_name":"Kretinsky, Jan","last_name":"Kretinsky","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Cěrná, Ivana","first_name":"Ivana","last_name":"Cěrná"},{"first_name":"Cǎlin","last_name":"Belta","full_name":"Belta, Cǎlin"}],"related_material":{"record":[{"id":"1407","relation":"later_version","status":"public"}]},"date_created":"2018-12-11T11:53:29Z","date_updated":"2023-09-20T09:43:09Z","oa_version":"Preprint","_id":"1689","year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","status":"public","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","publisher":"ACM","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"day":"14","month":"04","scopus_import":1,"conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2015-04-16","location":"Seattle, WA, United States","start_date":"2015-04-14"},"date_published":"2015-04-14T00:00:00Z","doi":"10.1145/2728606.2728608","language":[{"iso":"eng"}],"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","oa":1,"citation":{"ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728608","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 259–268.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–68, doi:10.1145/2728606.2728608.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–268."},"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"}],"page":"259 - 268"},{"pubrep_id":"448","file":[{"file_id":"4959","relation":"main_file","date_created":"2018-12-12T10:12:41Z","date_updated":"2020-07-14T12:45:12Z","checksum":"912e1acbaf201100f447a43e4d5958bd","file_name":"IST-2016-448-v1+1_games-06-00413.pdf","access_level":"open_access","creator":"system","file_size":518832,"content_type":"application/pdf"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1681","intvolume":" 6","ddc":["000"],"status":"public","title":"Evolution of decisions in population games with sequentially searching individuals","issue":"4","abstract":[{"lang":"eng","text":"In many social situations, individuals endeavor to find the single best possible partner, but are constrained to evaluate the candidates in sequence. Examples include the search for mates, economic partnerships, or any other long-term ties where the choice to interact involves two parties. Surprisingly, however, previous theoretical work on mutual choice problems focuses on finding equilibrium solutions, while ignoring the evolutionary dynamics of decisions. Empirically, this may be of high importance, as some equilibrium solutions can never be reached unless the population undergoes radical changes and a sufficient number of individuals change their decisions simultaneously. To address this question, we apply a mutual choice sequential search problem in an evolutionary game-theoretical model that allows one to find solutions that are favored by evolution. As an example, we study the influence of sequential search on the evolutionary dynamics of cooperation. For this, we focus on the classic snowdrift game and the prisoner’s dilemma game."}],"type":"journal_article","date_published":"2015-09-29T00:00:00Z","citation":{"short":"T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.","mla":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” Games, vol. 6, no. 4, MDPI, 2015, pp. 413–37, doi:10.3390/g6040413.","chicago":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” Games. MDPI, 2015. https://doi.org/10.3390/g6040413.","ama":"Priklopil T, Chatterjee K. Evolution of decisions in population games with sequentially searching individuals. Games. 2015;6(4):413-437. doi:10.3390/g6040413","apa":"Priklopil, T., & Chatterjee, K. (2015). Evolution of decisions in population games with sequentially searching individuals. Games. MDPI. https://doi.org/10.3390/g6040413","ieee":"T. Priklopil and K. Chatterjee, “Evolution of decisions in population games with sequentially searching individuals,” Games, vol. 6, no. 4. MDPI, pp. 413–437, 2015.","ista":"Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games with sequentially searching individuals. Games. 6(4), 413–437."},"publication":"Games","page":"413 - 437","article_type":"original","has_accepted_license":"1","article_processing_charge":"No","day":"29","scopus_import":"1","author":[{"full_name":"Priklopil, Tadeas","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","last_name":"Priklopil","first_name":"Tadeas"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"}],"volume":6,"date_updated":"2023-10-17T11:42:52Z","date_created":"2018-12-11T11:53:26Z","year":"2015","publisher":"MDPI","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"publication_status":"published","publist_id":"5467","ec_funded":1,"file_date_updated":"2020-07-14T12:45:12Z","doi":"10.3390/g6040413","language":[{"iso":"eng"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"quality_controlled":"1","publication_identifier":{"eissn":["2073-4336"]},"month":"09"},{"abstract":[{"lang":"eng","text":"For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour."}],"type":"conference","alternative_title":["LNCS"],"oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1603","intvolume":" 9206","title":"Counterexample explanation by learning small strategies in Markov decision processes","status":"public","day":"16","scopus_import":1,"date_published":"2015-07-16T00:00:00Z","citation":{"mla":"Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_10.","ama":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:10.1007/978-3-319-21690-4_10","ista":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., & Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-319-21690-4_10"},"page":"158 - 177","ec_funded":1,"publist_id":"5564","related_material":{"record":[{"id":"5549","status":"public","relation":"research_paper"}]},"author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Fellner, Andreas","first_name":"Andreas","last_name":"Fellner","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan"}],"volume":9206,"date_created":"2018-12-11T11:52:58Z","date_updated":"2024-02-21T13:52:07Z","acknowledgement":"This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734.","year":"2015","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","publication_identifier":{"eisbn":["978-3-319-21690-4"]},"month":"07","doi":"10.1007/978-3-319-21690-4_10","conference":{"name":"CAV: Computer Aided Verification","end_date":"2015-07-24","location":"San Francisco, CA, United States","start_date":"2015-07-18"},"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.02834"}],"oa":1,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"}],"quality_controlled":"1"},{"file_date_updated":"2020-07-14T12:47:00Z","ec_funded":1,"publist_id":"5564","license":"https://creativecommons.org/publicdomain/zero/1.0/","year":"2015","publisher":"Institute of Science and Technology Austria","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"author":[{"first_name":"Andreas","last_name":"Fellner","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","full_name":"Fellner, Andreas"}],"contributor":[{"last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"id":"1603","status":"public","relation":"popular_science"}]},"date_updated":"2024-02-21T13:52:07Z","date_created":"2018-12-12T12:31:29Z","month":"08","tmp":{"short":"CC0 (1.0)","image":"/images/cc_0.png","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)"},"oa":1,"project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"doi":"10.15479/AT:ISTA:28","datarep_id":"28","type":"research_data","abstract":[{"text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication.","lang":"eng"}],"_id":"5549","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","ddc":["004"],"status":"public","file":[{"creator":"system","content_type":"application/zip","file_size":49557109,"access_level":"open_access","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","checksum":"b8bcb43c0893023cda66c1b69c16ac62","date_created":"2018-12-12T13:02:31Z","date_updated":"2020-07-14T12:47:00Z","file_id":"5597","relation":"main_file"}],"oa_version":"Published Version","keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"day":"13","article_processing_charge":"No","has_accepted_license":"1","citation":{"mla":"Fellner, Andreas. Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria, 2015, doi:10.15479/AT:ISTA:28.","short":"A. Fellner, (2015).","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. https://doi.org/10.15479/AT:ISTA:28.","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:10.15479/AT:ISTA:28","ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, 10.15479/AT:ISTA:28.","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:28","ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015."},"date_published":"2015-08-13T00:00:00Z"},{"language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-54013-4_15","conference":{"location":"San Diego, CA, United States","start_date":"2014-01-19","end_date":"2014-01-21","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation"},"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"quality_controlled":"1","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.1311.4425","open_access":"1"}],"oa":1,"external_id":{"arxiv":["1311.4425"]},"publication_identifier":{"isbn":["9783642540127"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783642540134"]},"month":"01","volume":8318,"date_created":"2022-03-18T13:01:22Z","date_updated":"2022-05-17T08:36:01Z","author":[{"full_name":"Aminof, Benjamin","id":"4A55BD00-F248-11E8-B48F-1D18A9856A87","last_name":"Aminof","first_name":"Benjamin"},{"full_name":"Jacobs, Swen","last_name":"Jacobs","first_name":"Swen"},{"last_name":"Khalimov","first_name":"Ayrat","full_name":"Khalimov, Ayrat"},{"full_name":"Rubin, Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","first_name":"Sasha","last_name":"Rubin"}],"publisher":"Springer Nature","department":[{"_id":"KrCh"}],"publication_status":"published","acknowledgement":"This work was supported by the Austrian Science Fund through grant P23499-N23\r\nand through the RiSE network (S11403, S11405, S11406, S11407-N23); ERC Starting Grant (279307: Graph Games); Vienna Science and Technology Fund (WWTF)\r\ngrants PROSEED, ICT12-059, and VRG11-005.","year":"2014","ec_funded":1,"date_published":"2014-01-30T00:00:00Z","page":"262-281","citation":{"ista":"Aminof B, Jacobs S, Khalimov A, Rubin S. 2014. Parameterized model checking of token-passing systems. Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 262–281.","apa":"Aminof, B., Jacobs, S., Khalimov, A., & Rubin, S. (2014). Parameterized model checking of token-passing systems. In Verification, Model Checking, and Abstract Interpretation (Vol. 8318, pp. 262–281). San Diego, CA, United States: Springer Nature. https://doi.org/10.1007/978-3-642-54013-4_15","ieee":"B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, “Parameterized model checking of token-passing systems,” in Verification, Model Checking, and Abstract Interpretation, San Diego, CA, United States, 2014, vol. 8318, pp. 262–281.","ama":"Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized model checking of token-passing systems. In: Verification, Model Checking, and Abstract Interpretation. Vol 8318. Springer Nature; 2014:262-281. doi:10.1007/978-3-642-54013-4_15","chicago":"Aminof, Benjamin, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. “Parameterized Model Checking of Token-Passing Systems.” In Verification, Model Checking, and Abstract Interpretation, 8318:262–81. Springer Nature, 2014. https://doi.org/10.1007/978-3-642-54013-4_15.","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Token-Passing Systems.” Verification, Model Checking, and Abstract Interpretation, vol. 8318, Springer Nature, 2014, pp. 262–81, doi:10.1007/978-3-642-54013-4_15.","short":"B. Aminof, S. Jacobs, A. Khalimov, S. Rubin, in:, Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 262–281."},"publication":"Verification, Model Checking, and Abstract Interpretation","article_processing_charge":"No","day":"30","scopus_import":"1","oa_version":"Preprint","intvolume":" 8318","title":"Parameterized model checking of token-passing systems","status":"public","_id":"10884","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We revisit the parameterized model checking problem for token-passing systems and specifications in indexed CTL ∗ \\X. Emerson and Namjoshi (1995, 2003) have shown that parameterized model checking of indexed CTL ∗ \\X in uni-directional token rings can be reduced to checking rings up to some cutoff size. Clarke et al. (2004) have shown a similar result for general topologies and indexed LTL \\X, provided processes cannot choose the directions for sending or receiving the token.\r\nWe unify and substantially extend these results by systematically exploring fragments of indexed CTL ∗ \\X with respect to general topologies. For each fragment we establish whether a cutoff exists, and for some concrete topologies, such as rings, cliques and stars, we infer small cutoffs. Finally, we show that the problem becomes undecidable, and thus no cutoffs exist, if processes are allowed to choose the directions in which they send or from which they receive the token."}],"alternative_title":["LNCS"],"type":"conference"},{"article_processing_charge":"No","day":"28","scopus_import":"1","date_published":"2014-08-28T00:00:00Z","page":"104 - 116","article_type":"original","citation":{"chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, Veronika Loitzenbauer, and Michael Raskin. “Approximating the Minimum Cycle Mean.” Theoretical Computer Science. Elsevier, 2014. https://doi.org/10.1016/j.tcs.2014.06.031.","mla":"Chatterjee, Krishnendu, et al. “Approximating the Minimum Cycle Mean.” Theoretical Computer Science, vol. 547, no. C, Elsevier, 2014, pp. 104–16, doi:10.1016/j.tcs.2014.06.031.","short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, V. Loitzenbauer, M. Raskin, Theoretical Computer Science 547 (2014) 104–116.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. 2014. Approximating the minimum cycle mean. Theoretical Computer Science. 547(C), 104–116.","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., Loitzenbauer, V., & Raskin, M. (2014). Approximating the minimum cycle mean. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2014.06.031","ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, V. Loitzenbauer, and M. Raskin, “Approximating the minimum cycle mean,” Theoretical Computer Science, vol. 547, no. C. Elsevier, pp. 104–116, 2014.","ama":"Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. Approximating the minimum cycle mean. Theoretical Computer Science. 2014;547(C):104-116. doi:10.1016/j.tcs.2014.06.031"},"publication":"Theoretical Computer Science","issue":"C","abstract":[{"text":"We consider directed graphs where each edge is labeled with an integer weight and study the fundamental algorithmic question of computing the value of a cycle with minimum mean weight. Our contributions are twofold: (1) First we show that the algorithmic question is reducible to the problem of a logarithmic number of min-plus matrix multiplications of n×n-matrices, where n is the number of vertices of the graph. (2) Second, when the weights are nonnegative, we present the first (1+ε)-approximation algorithm for the problem and the running time of our algorithm is Õ(nωlog3(nW/ε)/ε),1 where O(nω) is the time required for the classic n×n-matrix multiplication and W is the maximum value of the weights. With an additional O(log(nW/ε)) factor in space a cycle with approximately optimal weight can be computed within the same time bound.","lang":"eng"}],"type":"journal_article","oa_version":"Preprint","intvolume":" 547","status":"public","title":"Approximating the minimum cycle mean","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1375","month":"08","language":[{"iso":"eng"}],"doi":"10.1016/j.tcs.2014.06.031","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","external_id":{"arxiv":["1307.4473"]},"oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1307.4473","open_access":"1"}],"publist_id":"5836","ec_funded":1,"volume":547,"date_updated":"2022-09-09T11:50:58Z","date_created":"2018-12-11T11:51:40Z","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","last_name":"Henzinger","full_name":"Henzinger, Monika H"},{"first_name":"Sebastian","last_name":"Krinninger","full_name":"Krinninger, Sebastian"},{"last_name":"Loitzenbauer","first_name":"Veronika","full_name":"Loitzenbauer, Veronika"},{"full_name":"Raskin, Michael","last_name":"Raskin","first_name":"Michael"}],"department":[{"_id":"KrCh"}],"publisher":"Elsevier","publication_status":"published","year":"2014"},{"citation":{"ieee":"S. Jha, S. Tripakis, S. Seshia, and K. Chatterjee, “Game theoretic secure localization in wireless sensor networks,” presented at the IOT: Internet of Things, Cambridge, USA, 2014, pp. 85–90.","apa":"Jha, S., Tripakis, S., Seshia, S., & Chatterjee, K. (2014). Game theoretic secure localization in wireless sensor networks (pp. 85–90). Presented at the IOT: Internet of Things, Cambridge, USA: IEEE. https://doi.org/10.1109/IOT.2014.7030120","ista":"Jha S, Tripakis S, Seshia S, Chatterjee K. 2014. Game theoretic secure localization in wireless sensor networks. IOT: Internet of Things, 85–90.","ama":"Jha S, Tripakis S, Seshia S, Chatterjee K. Game theoretic secure localization in wireless sensor networks. In: IEEE; 2014:85-90. doi:10.1109/IOT.2014.7030120","chicago":"Jha, Susmit, Stavros Tripakis, Sanjit Seshia, and Krishnendu Chatterjee. “Game Theoretic Secure Localization in Wireless Sensor Networks,” 85–90. IEEE, 2014. https://doi.org/10.1109/IOT.2014.7030120.","short":"S. Jha, S. Tripakis, S. Seshia, K. Chatterjee, in:, IEEE, 2014, pp. 85–90.","mla":"Jha, Susmit, et al. Game Theoretic Secure Localization in Wireless Sensor Networks. IEEE, 2014, pp. 85–90, doi:10.1109/IOT.2014.7030120."},"page":"85 - 90","quality_controlled":"1","date_published":"2014-02-03T00:00:00Z","doi":"10.1109/IOT.2014.7030120","conference":{"name":"IOT: Internet of Things","start_date":"2014-10-06","location":"Cambridge, USA","end_date":"2014-10-08"},"language":[{"iso":"eng"}],"month":"02","day":"03","_id":"1853","year":"2014","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"publisher":"IEEE","publication_status":"published","title":"Game theoretic secure localization in wireless sensor networks","status":"public","author":[{"full_name":"Jha, Susmit","first_name":"Susmit","last_name":"Jha"},{"first_name":"Stavros","last_name":"Tripakis","full_name":"Tripakis, Stavros"},{"full_name":"Seshia, Sanjit","first_name":"Sanjit","last_name":"Seshia"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"None","date_updated":"2021-01-12T06:53:38Z","date_created":"2018-12-11T11:54:22Z","type":"conference","publist_id":"5247","abstract":[{"text":"Wireless sensor networks (WSNs) composed of low-power, low-cost sensor nodes are expected to form the backbone of future intelligent networks for a broad range of civil, industrial and military applications. These sensor nodes are often deployed through random spreading, and function in dynamic environments. Many applications of WSNs such as pollution tracking, forest fire detection, and military surveillance require knowledge of the location of constituent nodes. But the use of technologies such as GPS on all nodes is prohibitive due to power and cost constraints. So, the sensor nodes need to autonomously determine their locations. Most localization techniques use anchor nodes with known locations to determine the position of remaining nodes. Localization techniques have two conflicting requirements. On one hand, an ideal localization technique should be computationally simple and on the other hand, it must be resistant to attacks that compromise anchor nodes. In this paper, we propose a computationally light-weight game theoretic secure localization technique and demonstrate its effectiveness in comparison to existing techniques.","lang":"eng"}]},{"type":"journal_article","abstract":[{"lang":"eng","text":"Unbiased high-throughput massively parallel sequencing methods have transformed the process of discovery of novel putative driver gene mutations in cancer. In chronic lymphocytic leukemia (CLL), these methods have yielded several unexpected findings, including the driver genes SF3B1, NOTCH1 and POT1. Recent analysis, utilizing down-sampling of existing datasets, has shown that the discovery process of putative drivers is far from complete across cancer. In CLL, while driver gene mutations affecting >10% of patients were efficiently discovered with previously published CLL cohorts of up to 160 samples subjected to whole exome sequencing (WES), this sample size has only 0.78 power to detect drivers affecting 5% of patients, and only 0.12 power for drivers affecting 2% of patients. These calculations emphasize the need to apply unbiased WES to larger patient cohorts."}],"issue":"21","publist_id":"5211","title":"Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples","status":"public","publication_status":"published","department":[{"_id":"KrCh"}],"intvolume":" 124","publisher":"American Society of Hematology","year":"2014","_id":"1884","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:54:32Z","date_updated":"2021-01-12T06:53:50Z","volume":124,"oa_version":"None","author":[{"full_name":"Landau, Dan","first_name":"Dan","last_name":"Landau"},{"first_name":"Chip","last_name":"Stewart","full_name":"Stewart, Chip"},{"full_name":"Reiter, Johannes","first_name":"Johannes","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353"},{"last_name":"Lawrence","first_name":"Michael","full_name":"Lawrence, Michael"},{"last_name":"Sougnez","first_name":"Carrie","full_name":"Sougnez, Carrie"},{"last_name":"Brown","first_name":"Jennifer","full_name":"Brown, Jennifer"},{"full_name":"Lopez Guillermo, Armando","last_name":"Lopez Guillermo","first_name":"Armando"},{"full_name":"Gabriel, Stacey","first_name":"Stacey","last_name":"Gabriel"},{"full_name":"Lander, Eric","last_name":"Lander","first_name":"Eric"},{"first_name":"Donna","last_name":"Neuberg","full_name":"Neuberg, Donna"},{"last_name":"López Otín","first_name":"Carlos","full_name":"López Otín, Carlos"},{"last_name":"Campo","first_name":"Elias","full_name":"Campo, Elias"},{"first_name":"Gad","last_name":"Getz","full_name":"Getz, Gad"},{"full_name":"Wu, Catherine","first_name":"Catherine","last_name":"Wu"}],"day":"04","month":"12","page":"1952 - 1952","publication":"Blood","citation":{"ama":"Landau D, Stewart C, Reiter J, et al. Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. Blood. 2014;124(21):1952-1952.","ista":"Landau D, Stewart C, Reiter J, Lawrence M, Sougnez C, Brown J, Lopez Guillermo A, Gabriel S, Lander E, Neuberg D, López Otín C, Campo E, Getz G, Wu C. 2014. Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. Blood. 124(21), 1952–1952.","apa":"Landau, D., Stewart, C., Reiter, J., Lawrence, M., Sougnez, C., Brown, J., … Wu, C. (2014). Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. Blood. American Society of Hematology.","ieee":"D. Landau et al., “Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples,” Blood, vol. 124, no. 21. American Society of Hematology, pp. 1952–1952, 2014.","mla":"Landau, Dan, et al. “Novel Putative Driver Gene Mutations in Chronic Lymphocytic Leukemia (CLL): Results from a Combined Analysis of Whole Exome Sequencing of 262 Primary CLL Aamples.” Blood, vol. 124, no. 21, American Society of Hematology, 2014, pp. 1952–1952.","short":"D. Landau, C. Stewart, J. Reiter, M. Lawrence, C. Sougnez, J. Brown, A. Lopez Guillermo, S. Gabriel, E. Lander, D. Neuberg, C. López Otín, E. Campo, G. Getz, C. Wu, Blood 124 (2014) 1952–1952.","chicago":"Landau, Dan, Chip Stewart, Johannes Reiter, Michael Lawrence, Carrie Sougnez, Jennifer Brown, Armando Lopez Guillermo, et al. “Novel Putative Driver Gene Mutations in Chronic Lymphocytic Leukemia (CLL): Results from a Combined Analysis of Whole Exome Sequencing of 262 Primary CLL Aamples.” Blood. American Society of Hematology, 2014."},"main_file_link":[{"url":"http://www.bloodjournal.org/content/124/21/1952?sso-checked=true"}],"language":[{"iso":"eng"}],"date_published":"2014-12-04T00:00:00Z"},{"publist_id":"5046","ec_funded":1,"publication_status":"published","editor":[{"full_name":"Cassez, Franck","first_name":"Franck","last_name":"Cassez"},{"first_name":"Jean-François","last_name":"Raskin","full_name":"Raskin, Jean-François"}],"publisher":"Society of Industrial and Applied Mathematics","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2014","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1.","date_created":"2018-12-11T11:55:17Z","date_updated":"2021-01-12T06:54:49Z","volume":8837,"author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"full_name":"Kwiatkowska, Marta","first_name":"Marta","last_name":"Kwiatkowska"},{"last_name":"Parker","first_name":"David","full_name":"Parker, David"},{"full_name":"Ujma, Mateusz","first_name":"Mateusz","last_name":"Ujma"}],"month":"11","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"LIGHT-REGULATED LIGAND TRAPS FOR SPATIO-TEMPORAL INHIBITION OF CELL SIGNALING","_id":"26241A12-B435-11E9-9278-68D0E5697425","grant_number":"24696"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1402.2967","open_access":"1"}],"language":[{"iso":"eng"}],"conference":{"location":"Sydney, Australia","start_date":"2014-11-03","end_date":"2014-11-07","name":"ALENEX: Algorithm Engineering and Experiments"},"doi":"10.1007/978-3-319-11936-6_8","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples."}],"status":"public","title":"Verification of markov decision processes using learning algorithms","intvolume":" 8837","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"2027","oa_version":"Submitted Version","day":"01","page":"98 - 114","publication":" Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","citation":{"chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:98–114. Society of Industrial and Applied Mathematics, 2014. https://doi.org/10.1007/978-3-319-11936-6_8.","mla":"Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Society of Industrial and Applied Mathematics, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014, pp. 98–114.","ista":"Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.","ieee":"T. Brázdil et al., “Verification of markov decision processes using learning algorithms,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 98–114.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of markov decision processes using learning algorithms. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 98–114). Sydney, Australia: Society of Industrial and Applied Mathematics. https://doi.org/10.1007/978-3-319-11936-6_8","ama":"Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision processes using learning algorithms. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Society of Industrial and Applied Mathematics; 2014:98-114. doi:10.1007/978-3-319-11936-6_8"},"date_published":"2014-11-01T00:00:00Z"},{"doi":"10.1007/978-3-662-44584-6_18","conference":{"name":"CONCUR: Concurrency Theory","location":"Rome, Italy","start_date":"2014-09-02","end_date":"2014-09-05"},"language":[{"iso":"eng"}],"oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1404.5084","open_access":"1"}],"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"}],"month":"09","author":[{"last_name":"Hermanns","first_name":"Holger","full_name":"Hermanns, Holger"},{"first_name":"Jan","last_name":"Krčál","full_name":"Krčál, Jan"},{"first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan"}],"volume":8704,"date_updated":"2021-01-12T06:55:00Z","date_created":"2018-12-11T11:55:27Z","acknowledgement":"This work is supported by the EU 7th Framework Programme under grant agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.","year":"2014","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","editor":[{"full_name":"Baldan, Paolo","first_name":"Paolo","last_name":"Baldan"},{"last_name":"Gorla","first_name":"Daniele","full_name":"Gorla, Daniele"}],"publication_status":"published","ec_funded":1,"publist_id":"4993","date_published":"2014-09-01T00:00:00Z","citation":{"ieee":"H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 249–265.","apa":"Hermanns, H., Krčál, J., & Kretinsky, J. (2014). Probabilistic bisimulation: Naturally on distributions. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 249–265). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_18","ista":"Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265.","ama":"Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on distributions. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:249-265. doi:10.1007/978-3-662-44584-6_18","chicago":"Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation: Naturally on Distributions.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_18.","short":"H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–265.","mla":"Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:10.1007/978-3-662-44584-6_18."},"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","page":"249 - 265","day":"01","oa_version":"Submitted Version","_id":"2053","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","intvolume":" 8704","status":"public","title":"Probabilistic bisimulation: Naturally on distributions","abstract":[{"lang":"eng","text":"In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems."}],"type":"conference","alternative_title":["LNCS"]},{"language":[{"iso":"eng"}],"date_published":"2014-09-01T00:00:00Z","doi":"10.1007/978-3-662-44584-6_9","conference":{"name":"CONCUR: Concurrency Theory","end_date":"2014-09-05","location":"Rome, Italy","start_date":"2014-09-02"},"page":"109 - 124","quality_controlled":"1","citation":{"ama":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H. Parameterized model checking of rendezvous systems. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:109-124. doi:10.1007/978-3-662-44584-6_9","ista":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H. 2014. Parameterized model checking of rendezvous systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 109–124.","ieee":"B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith, “Parameterized model checking of rendezvous systems,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 109–124.","apa":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2014). Parameterized model checking of rendezvous systems. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 109–124). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_9","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Rendezvous Systems.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 109–24, doi:10.1007/978-3-662-44584-6_9.","short":"B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 109–124.","chicago":"Aminof, Benjamin, Tomer Kotek, Sacha Rubin, Francesco Spegni, and Helmut Veith. “Parameterized Model Checking of Rendezvous Systems.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:109–24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_9."},"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","day":"01","month":"09","oa_version":"None","volume":8704,"date_updated":"2021-01-12T06:54:59Z","date_created":"2018-12-11T11:55:26Z","author":[{"id":"4A55BD00-F248-11E8-B48F-1D18A9856A87","first_name":"Benjamin","last_name":"Aminof","full_name":"Aminof, Benjamin"},{"last_name":"Kotek","first_name":"Tomer","full_name":"Kotek, Tomer"},{"first_name":"Sacha","last_name":"Rubin","full_name":"Rubin, Sacha"},{"first_name":"Francesco","last_name":"Spegni","full_name":"Spegni, Francesco"},{"first_name":"Helmut","last_name":"Veith","full_name":"Veith, Helmut"}],"editor":[{"first_name":"Paolo","last_name":"Baldan","full_name":"Baldan, Paolo"},{"last_name":"Gorla","first_name":"Daniele","full_name":"Gorla, Daniele"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","intvolume":" 8704","department":[{"_id":"KrCh"}],"publication_status":"published","title":"Parameterized model checking of rendezvous systems","status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"2052","year":"2014","acknowledgement":"The second, third, fourth and fifth authors were supported by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grants PROSEED, ICT12-059, and VRG11-005.","publist_id":"4994","abstract":[{"lang":"eng","text":"A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finite-state systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Büchi word automaton), and establish tight bounds on the sizes of such automata."}],"alternative_title":["LNCS"],"type":"conference"}]