--- _id: '1709' 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. 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.' article_processing_charge: No article_type: original author: - first_name: Johannes full_name: Reiter, Johannes id: 4A918E98-F248-11E8-B48F-1D18A9856A87 last_name: Reiter orcid: 0000-0002-0170-7353 - first_name: Ayush full_name: Kanodia, Ayush last_name: Kanodia - first_name: Raghav full_name: Gupta, Raghav last_name: Gupta - first_name: Martin full_name: Nowak, Martin last_name: Nowak - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: 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 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 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. 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). 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. short: J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of the Royal Society of London Series B Biological Sciences 282 (2015). date_created: 2018-12-11T11:53:35Z date_published: 2015-07-15T00:00:00Z date_updated: 2023-09-07T11:40:43Z day: '15' department: - _id: KrCh doi: 10.1098/rspb.2015.1041 external_id: pmid: - '26180069' intvolume: ' 282' issue: '1812' language: - iso: eng main_file_link: - open_access: '1' url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4528522/ month: '07' oa: 1 oa_version: Submitted Version pmid: 1 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Proceedings of the Royal Society of London Series B Biological Sciences publication_status: published publisher: Royal Society publist_id: '5425' quality_controlled: '1' related_material: record: - id: '1400' relation: dissertation_contains status: public scopus_import: 1 status: public title: Biological auctions with multiple rewards type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 282 year: '2015' ... --- _id: '1400' abstract: - lang: eng 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. alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Johannes full_name: Reiter, Johannes id: 4A918E98-F248-11E8-B48F-1D18A9856A87 last_name: Reiter orcid: 0000-0002-0170-7353 citation: ama: Reiter J. The subclonal evolution of cancer. 2015. apa: Reiter, J. (2015). The subclonal evolution of cancer. Institute of Science and Technology Austria. chicago: Reiter, Johannes. “The Subclonal Evolution of Cancer.” Institute of Science and Technology Austria, 2015. ieee: J. Reiter, “The subclonal evolution of cancer,” Institute of Science and Technology Austria, 2015. ista: Reiter J. 2015. The subclonal evolution of cancer. Institute of Science and Technology Austria. mla: Reiter, Johannes. The Subclonal Evolution of Cancer. Institute of Science and Technology Austria, 2015. short: J. Reiter, The Subclonal Evolution of Cancer, Institute of Science and Technology Austria, 2015. date_created: 2018-12-11T11:51:48Z date_published: 2015-04-01T00:00:00Z date_updated: 2023-09-07T11:40:44Z day: '01' degree_awarded: PhD department: - _id: KrCh language: - iso: eng month: '04' oa_version: None page: '183' publication_identifier: issn: - 2663-337X publication_status: published publisher: Institute of Science and Technology Austria publist_id: '5807' related_material: record: - id: '1709' relation: part_of_dissertation status: public - id: '2000' relation: part_of_dissertation status: public - id: '2247' relation: part_of_dissertation status: public - id: '2816' relation: part_of_dissertation status: public - id: '2858' relation: part_of_dissertation status: public - id: '3157' relation: part_of_dissertation status: public - id: '3260' relation: part_of_dissertation status: public status: public supervisor: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X title: The subclonal evolution of cancer type: dissertation user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2015' ... --- _id: '1502' abstract: - lang: eng 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. 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." alternative_title: - 'Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering ' author: - first_name: Nikola full_name: Beneš, Nikola last_name: Beneš - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Dejan full_name: Nickovic, Dejan last_name: Nickovic citation: 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' 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' 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. 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.' 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.' 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. conference: end_date: 2015-05-08 location: Montreal, QC, Canada name: 'CBSE: Component-Based Software Engineering ' start_date: 2015-05-04 date_created: 2018-12-11T11:52:24Z date_published: 2015-05-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' ddc: - '000' department: - _id: ToHe - _id: KrCh doi: 10.1145/2737166.2737175 ec_funded: 1 file: - access_level: open_access checksum: c6ce681035c163a158751f240cb7d389 content_type: application/pdf creator: system date_created: 2018-12-12T10:17:46Z date_updated: 2020-07-14T12:44:59Z file_id: '5303' file_name: IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf file_size: 467561 relation: main_file file_date_updated: 2020-07-14T12:44:59Z has_accepted_license: '1' language: - iso: eng month: '05' oa: 1 oa_version: Submitted Version page: 101 - 110 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication_identifier: isbn: - 978-1-4503-3471-6 publication_status: published publisher: ACM publist_id: '5676' pubrep_id: '625' quality_controlled: '1' related_material: record: - id: '1155' relation: dissertation_contains status: public scopus_import: 1 status: public title: Complete composition operators for IOCO-testing theory type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1501' 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. ' 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).' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca 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 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 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. 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. 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. 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. date_created: 2018-12-11T11:52:23Z date_published: 2015-10-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/s10703-015-0235-2 ec_funded: 1 intvolume: ' 47' issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1405.0835 month: '10' oa: 1 oa_version: Preprint page: 230 - 264 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '5677' quality_controlled: '1' related_material: record: - id: '1155' relation: dissertation_contains status: public scopus_import: 1 status: public title: CEGAR for compositional analysis of qualitative properties in Markov decision processes type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 47 year: '2015' ... --- _id: '1602' abstract: - lang: eng text: Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks. acknowledgement: We thank anonymous reviewers for helpful comments to improve the presentation of the paper. author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Prateesh full_name: Goyal, Prateesh last_name: Goyal citation: 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 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' 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. 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. 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. 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. conference: end_date: 2015-01-17 location: Mumbai, India name: 'SIGPLAN: Symposium on Principles of Programming Languages' start_date: 2015-01-15 date_created: 2018-12-11T11:52:58Z date_published: 2015-01-01T00:00:00Z date_updated: 2023-09-07T12:01:58Z day: '01' department: - _id: KrCh doi: 10.1145/2676726.2676979 ec_funded: 1 external_id: arxiv: - '1410.7724' intvolume: ' 50' issue: '1' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1410.7724 month: '01' oa: 1 oa_version: Preprint page: 97 - 109 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: ACM SIGPLAN Notices publication_status: published publisher: ACM publist_id: '5565' quality_controlled: '1' related_material: record: - id: '821' relation: dissertation_contains status: public scopus_import: 1 status: public title: Faster algorithms for algebraic path properties in recursive state machines with constant treewidth type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 50 year: '2015' ...