[{"oa_version":"Published Version","department":[{"_id":"KrCh"}],"year":"2013","day":"12","type":"research_data_reference","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","month":"12","date_updated":"2025-09-29T14:30:03Z","citation":{"mla":"Zagorsky, Benjamin, et al. Forgiver Triumphs in Alternating Prisoner’s Dilemma . Public Library of Science, 2013, doi:10.1371/journal.pone.0080814.s001.","ieee":"B. Zagorsky, J. Reiter, K. Chatterjee, and M. Nowak, “Forgiver triumphs in alternating prisoner’s dilemma .” Public Library of Science, 2013.","short":"B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, (2013).","chicago":"Zagorsky, Benjamin, Johannes Reiter, Krishnendu Chatterjee, and Martin Nowak. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” Public Library of Science, 2013. https://doi.org/10.1371/journal.pone.0080814.s001.","ama":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. Forgiver triumphs in alternating prisoner’s dilemma . 2013. doi:10.1371/journal.pone.0080814.s001","ista":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. 2013. Forgiver triumphs in alternating prisoner’s dilemma , Public Library of Science, 10.1371/journal.pone.0080814.s001.","apa":"Zagorsky, B., Reiter, J., Chatterjee, K., & Nowak, M. (2013). Forgiver triumphs in alternating prisoner’s dilemma . Public Library of Science. https://doi.org/10.1371/journal.pone.0080814.s001"},"publisher":"Public Library of Science","_id":"9749","related_material":{"record":[{"id":"2247","status":"public","relation":"used_in_publication"}]},"doi":"10.1371/journal.pone.0080814.s001","date_created":"2021-07-28T15:45:07Z","status":"public","article_processing_charge":"No","title":"Forgiver triumphs in alternating prisoner's dilemma ","author":[{"full_name":"Zagorsky, Benjamin","last_name":"Zagorsky","first_name":"Benjamin"},{"last_name":"Reiter","first_name":"Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","full_name":"Reiter, Johannes","orcid":"0000-0002-0170-7353"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"abstract":[{"text":"Cooperative behavior, where one individual incurs a cost to help another, is a wide spread phenomenon. Here we study direct reciprocity in the context of the alternating Prisoner's Dilemma. We consider all strategies that can be implemented by one and two-state automata. We calculate the payoff matrix of all pairwise encounters in the presence of noise. We explore deterministic selection dynamics with and without mutation. Using different error rates and payoff values, we observe convergence to a small number of distinct equilibria. Two of them are uncooperative strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium is mixed and represents a cooperative alliance of several strategies, dominated by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent has cooperated; it defects once when the opponent has defected, but subsequently Forgiver attempts to re-establish cooperation even if the opponent has defected again. Forgiver is not an evolutionarily stable strategy, but the alliance, which it rules, is asymptotically stable. For a wide range of parameter values the most commonly observed outcome is convergence to the mixed equilibrium, dominated by Forgiver. Our results show that although forgiving might incur a short-term loss it can lead to a long-term gain. Forgiveness facilitates stable cooperation in the presence of exploitation and noise.","lang":"eng"}],"date_published":"2013-12-12T00:00:00Z"},{"day":"21","year":"2013","department":[{"_id":"CaGu"}],"oa":1,"oa_version":"Published Version","related_material":{"record":[{"id":"2853","status":"public","relation":"used_in_publication"}]},"_id":"9751","status":"public","doi":"10.5061/dryad.b1q2n","date_created":"2021-07-30T08:08:09Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5061/dryad.b1q2n"}],"publisher":"Dryad","citation":{"ama":"Refardt D, Bergmiller T, Kümmerli R. Data from: Altruism can evolve when relatedness is low: evidence from bacteria committing suicide upon phage infection. 2013. doi:10.5061/dryad.b1q2n","chicago":"Refardt, Dominik, Tobias Bergmiller, and Rolf Kümmerli. “Data from: Altruism Can Evolve When Relatedness Is Low: Evidence from Bacteria Committing Suicide upon Phage Infection.” Dryad, 2013. https://doi.org/10.5061/dryad.b1q2n.","short":"D. Refardt, T. Bergmiller, R. Kümmerli, (2013).","mla":"Refardt, Dominik, et al. Data from: Altruism Can Evolve When Relatedness Is Low: Evidence from Bacteria Committing Suicide upon Phage Infection. Dryad, 2013, doi:10.5061/dryad.b1q2n.","ieee":"D. Refardt, T. Bergmiller, and R. Kümmerli, “Data from: Altruism can evolve when relatedness is low: evidence from bacteria committing suicide upon phage infection.” Dryad, 2013.","apa":"Refardt, D., Bergmiller, T., & Kümmerli, R. (2013). Data from: Altruism can evolve when relatedness is low: evidence from bacteria committing suicide upon phage infection. Dryad. https://doi.org/10.5061/dryad.b1q2n","ista":"Refardt D, Bergmiller T, Kümmerli R. 2013. Data from: Altruism can evolve when relatedness is low: evidence from bacteria committing suicide upon phage infection, Dryad, 10.5061/dryad.b1q2n."},"type":"research_data_reference","month":"03","date_updated":"2025-09-29T13:41:12Z","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","article_processing_charge":"No","date_published":"2013-03-21T00:00:00Z","abstract":[{"text":"High relatedness among interacting individuals has generally been considered a precondition for the evolution of altruism. However, kin-selection theory also predicts the evolution of altruism when relatedness is low, as long as the cost of the altruistic act is minor compared to its benefit. Here, we demonstrate evidence for a low-cost altruistic act in bacteria. We investigated Escherichia coli responding to the attack of an obligately lytic phage by committing suicide in order to prevent parasite transmission to nearby relatives. We found that bacterial suicide provides large benefits to survivors at marginal costs to committers. The cost of suicide was low because infected cells are moribund, rapidly dying upon phage infection, such that no more opportunity for reproduction remains. As a consequence of its marginal cost, host suicide was selectively favoured even when relatedness between committers and survivors approached zero. Altogether, our findings demonstrate that low-cost suicide can evolve with ease, represents an effective host-defence strategy, and seems to be widespread among microbes. Moreover, low-cost suicide might also occur in higher organisms as exemplified by infected social insect workers leaving the colony to die in isolation.","lang":"eng"}],"author":[{"full_name":"Refardt, Dominik","first_name":"Dominik","last_name":"Refardt"},{"last_name":"Bergmiller","first_name":"Tobias","orcid":"0000-0001-5396-4346","id":"2C471CFA-F248-11E8-B48F-1D18A9856A87","full_name":"Bergmiller, Tobias"},{"first_name":"Rolf","last_name":"Kümmerli","full_name":"Kümmerli, Rolf"}],"title":"Data from: Altruism can evolve when relatedness is low: evidence from bacteria committing suicide upon phage infection"},{"type":"research_data_reference","date_updated":"2025-09-29T11:38:51Z","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","month":"10","publisher":"Dryad","citation":{"ama":"Hearn J, Stone G, Barton NH, Lohse K, Bunnefeld L. Data from: Likelihood-based inference of population history from low coverage de novo genome assemblies. 2013. doi:10.5061/dryad.r3r60","chicago":"Hearn, Jack, Graham Stone, Nicholas H Barton, Konrad Lohse, and Lynsey Bunnefeld. “Data from: Likelihood-Based Inference of Population History from Low Coverage de Novo Genome Assemblies.” Dryad, 2013. https://doi.org/10.5061/dryad.r3r60.","short":"J. Hearn, G. Stone, N.H. Barton, K. Lohse, L. Bunnefeld, (2013).","ieee":"J. Hearn, G. Stone, N. H. Barton, K. Lohse, and L. Bunnefeld, “Data from: Likelihood-based inference of population history from low coverage de novo genome assemblies.” Dryad, 2013.","mla":"Hearn, Jack, et al. Data from: Likelihood-Based Inference of Population History from Low Coverage de Novo Genome Assemblies. Dryad, 2013, doi:10.5061/dryad.r3r60.","apa":"Hearn, J., Stone, G., Barton, N. H., Lohse, K., & Bunnefeld, L. (2013). Data from: Likelihood-based inference of population history from low coverage de novo genome assemblies. Dryad. https://doi.org/10.5061/dryad.r3r60","ista":"Hearn J, Stone G, Barton NH, Lohse K, Bunnefeld L. 2013. Data from: Likelihood-based inference of population history from low coverage de novo genome assemblies, Dryad, 10.5061/dryad.r3r60."},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.5061/dryad.r3r60"}],"_id":"9754","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"2170"}]},"date_created":"2021-07-30T08:31:22Z","status":"public","doi":"10.5061/dryad.r3r60","oa_version":"Published Version","oa":1,"department":[{"_id":"NiBa"}],"year":"2013","day":"01","title":"Data from: Likelihood-based inference of population history from low coverage de novo genome assemblies","author":[{"full_name":"Hearn, Jack","first_name":"Jack","last_name":"Hearn"},{"full_name":"Stone, Graham","last_name":"Stone","first_name":"Graham"},{"first_name":"Nicholas H","last_name":"Barton","full_name":"Barton, Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8548-5240"},{"full_name":"Lohse, Konrad","first_name":"Konrad","last_name":"Lohse"},{"first_name":"Lynsey","last_name":"Bunnefeld","full_name":"Bunnefeld, Lynsey"}],"abstract":[{"lang":"eng","text":"Short-read sequencing technologies have in principle made it feasible to draw detailed inferences about the recent history of any organism. In practice, however, this remains challenging due to the difficulty of genome assembly in most organisms and the lack of statistical methods powerful enough to discriminate among recent, non-equilibrium histories. We address both the assembly and inference challenges. We develop a bioinformatic pipeline for generating outgroup-rooted alignments of orthologous sequence blocks from de novo low-coverage short-read data for a small number of genomes, and show how such sequence blocks can be used to fit explicit models of population divergence and admixture in a likelihood framework. To illustrate our approach, we reconstruct the Pleistocene history of an oak-feeding insect (the oak gallwasp Biorhiza pallida) which, in common with many other taxa, was restricted during Pleistocene ice ages to a longitudinal series of southern refugia spanning theWestern Palaearctic. Our analysis of sequence blocks sampled from a single genome from each of three major glacial refugia reveals support for an unexpected history dominated by recent admixture. Despite the fact that 80% of the genome is affected by admixture during the last glacial cycle, we are able to infer the deeper divergence history of these populations. These inferences are robust to variation in block length, mutation model, and the sampling location of individual genomes within refugia. This combination of de novo assembly and numerical likelihood calculation provides a powerful framework for estimating recent population history that can be applied to any organism without the need for prior genetic resources."}],"date_published":"2013-10-01T00:00:00Z","article_processing_charge":"No"},{"publication_status":"published","_id":"6440","publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"124","status":"public","doi":"10.15479/AT:IST-2013-124-v1-1","date_created":"2019-05-13T14:13:27Z","type":"technical_report","month":"06","date_updated":"2020-07-14T23:06:19Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","citation":{"apa":"Henzinger, T. A., Payer, H., & Sezgin, A. (2013). Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria. https://doi.org/10.15479/AT:IST-2013-124-v1-1","ista":"Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation to achieve scalable lock-free FIFO queues , IST Austria, 23p.","chicago":"Henzinger, Thomas A, Hannes Payer, and Ali Sezgin. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-124-v1-1.","ama":"Henzinger TA, Payer H, Sezgin A. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria; 2013. doi:10.15479/AT:IST-2013-124-v1-1","ieee":"T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria, 2013.","mla":"Henzinger, Thomas A., et al. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013, doi:10.15479/AT:IST-2013-124-v1-1.","short":"T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013."},"year":"2013","language":[{"iso":"eng"}],"day":"13","oa_version":"Published Version","oa":1,"file":[{"creator":"dernst","file_size":549684,"content_type":"application/pdf","date_updated":"2020-07-14T12:47:30Z","relation":"main_file","checksum":"a219ba4eada6cd62befed52262ee15d4","date_created":"2019-05-13T14:11:39Z","access_level":"open_access","file_name":"2013_TechRep_Henzinger.pdf","file_id":"6441"}],"department":[{"_id":"ToHe"}],"alternative_title":["IST Austria Technical Report"],"abstract":[{"text":"In order to guarantee that each method of a data structure updates the logical state exactly once, al-most all non-blocking implementations employ Compare-And-Swap (CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods competing among themselves to update the same variable, the tail or the head, respectively, leading to high contention and poor scalability. Recent non-blocking queue implementations try to alleviate high contentionby increasing the number of contention points, all the while using CAS-based synchronization. Furthermore, obtaining a wait-free implementation with competition is achieved by additional synchronization which leads to further degradation of performance.In this paper we formalize the notion of competitiveness of a synchronizing statement which can beused as a measure for the scalability of concurrent implementations. We present a new queue implementation, the Speculative Pairing (SP) queue, which, as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead of CAS. We prove that the SP queue is linearizable and lock-free.We also show that replacing CAS with FAI leads to wait-freedom for dequeue methods without an adverse effect on performance. In fact, our experiments suggest that the SP queue can perform and scale better than the state-of-the-art queue implementations.","lang":"eng"}],"ddc":["000","005"],"date_published":"2013-06-13T00:00:00Z","file_date_updated":"2020-07-14T12:47:30Z","title":"Replacing competition with cooperation to achieve scalable lock-free FIFO queues ","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Hannes","last_name":"Payer","full_name":"Payer, Hannes"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali","last_name":"Sezgin","first_name":"Ali"}],"page":"23","has_accepted_license":"1"},{"department":[{"_id":"HaJa"}],"oa_version":"None","day":"23","quality_controlled":"1","language":[{"iso":"eng"}],"year":"2012","scopus_import":"1","citation":{"ista":"zur Nedden S, Doney AS, Frenguelli BG. 2012.The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books. In: Adenosine. , 109–129.","apa":"zur Nedden, S., Doney, A. S., & Frenguelli, B. G. (2012). The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books. In S. Masino & D. Boison (Eds.), Adenosine (1st ed., pp. 109–129). New York: Springer. https://doi.org/10.1007/978-1-4614-3903-5_6","mla":"zur Nedden, Stephanie, et al. “The Double-Edged Sword: Gaining Adenosine at the Expense of ATP. How to Balance the Books.” Adenosine, edited by Susan Masino and Detlev Boison, 1st ed., Springer, 2012, pp. 109–29, doi:10.1007/978-1-4614-3903-5_6.","ieee":"S. zur Nedden, A. S. Doney, and B. G. Frenguelli, “The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books,” in Adenosine, 1st ed., S. Masino and D. Boison, Eds. New York: Springer, 2012, pp. 109–129.","short":"S. zur Nedden, A.S. Doney, B.G. Frenguelli, in:, S. Masino, D. Boison (Eds.), Adenosine, 1st ed., Springer, New York, 2012, pp. 109–129.","chicago":"Nedden, Stephanie zur, Alexander S. Doney, and Bruno G. Frenguelli. “The Double-Edged Sword: Gaining Adenosine at the Expense of ATP. How to Balance the Books.” In Adenosine, edited by Susan Masino and Detlev Boison, 1st ed., 109–29. New York: Springer, 2012. https://doi.org/10.1007/978-1-4614-3903-5_6.","ama":"zur Nedden S, Doney AS, Frenguelli BG. The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books. In: Masino S, Boison D, eds. Adenosine. 1st ed. New York: Springer; 2012:109-129. doi:10.1007/978-1-4614-3903-5_6"},"publisher":"Springer","date_updated":"2022-06-21T11:51:58Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07","type":"book_chapter","doi":"10.1007/978-1-4614-3903-5_6","status":"public","date_created":"2022-03-21T07:16:12Z","_id":"10896","publication_status":"published","publication_identifier":{"eisbn":["9781461439035"],"isbn":["9781461439028"]},"acknowledgement":"We are grateful to Research into Ageing/Ageing UK and The Dunhill Trust for funding SzN’s graduate studies, and to Prof Nicholas Dale for his valuable input.","page":"109-129","article_processing_charge":"No","place":"New York","editor":[{"full_name":"Masino, Susan","last_name":"Masino","first_name":"Susan"},{"last_name":"Boison","first_name":"Detlev","full_name":"Boison, Detlev"}],"author":[{"full_name":"zur Nedden, Stephanie","id":"3C77F464-F248-11E8-B48F-1D18A9856A87","first_name":"Stephanie","last_name":"zur Nedden"},{"last_name":"Doney","first_name":"Alexander S.","full_name":"Doney, Alexander S."},{"last_name":"Frenguelli","first_name":"Bruno G.","full_name":"Frenguelli, Bruno G."}],"title":"The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books","date_published":"2012-07-23T00:00:00Z","abstract":[{"lang":"eng","text":"Under physiological conditions the brain, via the purine salvage pathway, reuses the preformed purine bases hypoxanthine, derived from ATP degradation, and adenine (Ade), derived from polyamine synthesis, to restore its ATP pool. However, the massive degradation of ATP during ischemia, although providing valuable neuroprotective adenosine, results in the accumulation and loss of diffusible purine metabolites and thereby leads to a protracted reduction in the post-ischemic ATP pool size. In vivo, this may both limit the ability to deploy ATP-dependent reparative mechanisms and reduce the subsequent availability of adenosine, whilst in brain slices results in tissue with substantially lower levels of ATP than in vivo. In the present review, we describe the mechanisms by which brain tissue replenishes its ATP, how this can be improved with the clinically tolerated chemicals D-ribose and adenine, and the functional, and potential therapeutic, implications of doing so."}],"publication":"Adenosine","edition":"1"},{"date_published":"2012-10-15T00:00:00Z","corr_author":"1","author":[{"full_name":"Bouajjani, Ahmed","first_name":"Ahmed","last_name":"Bouajjani"},{"first_name":"Cezara","last_name":"Dragoi","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Enea","first_name":"Constantin","full_name":"Enea, Constantin"},{"first_name":"Mihaela","last_name":"Sighireanu","full_name":"Sighireanu, Mihaela"}],"intvolume":" 7561","place":"Berlin, Heidelberg","status":"public","publication_status":"published","series_title":"LNCS","publisher":"Springer","date_updated":"2024-10-09T21:02:34Z","day":"15","year":"2012","abstract":[{"lang":"eng","text":"We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas."}],"publication":"Automated Technology for Verification and Analysis","alternative_title":["LNCS"],"volume":7561,"title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","article_processing_charge":"No","page":"167-182","conference":{"location":"Thiruvananthapuram, India","name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2012-10-03","end_date":"2012-10-06"},"date_created":"2022-03-21T07:58:39Z","doi":"10.1007/978-3-642-33386-6_14","publication_identifier":{"isbn":["9783642333859"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783642333866"]},"_id":"10903","acknowledgement":"This work has been partially supported by the French ANR project Veridyc","scopus_import":"1","citation":{"ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in Automated Technology for Verification and Analysis, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182.","mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” Automated Technology for Verification and Analysis, vol. 7561, Springer, 2012, pp. 167–82, doi:10.1007/978-3-642-33386-6_14.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In Automated Technology for Verification and Analysis, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-33386-6_14.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:10.1007/978-3-642-33386-6_14","ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182.","apa":"Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In Automated Technology for Verification and Analysis (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-33386-6_14"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"10","type":"conference","quality_controlled":"1","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"oa_version":"None"},{"title":"Strategy synthesis for multi-dimensional quantitative objectives","abstract":[{"lang":"eng","text":"Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts."}],"publication":"CONCUR 2012 - Concurrency Theory","alternative_title":["LNCS"],"ec_funded":1,"volume":7454,"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"article_processing_charge":"No","conference":{"name":"CONCUR: Conference on Concurrency Theory","location":"Newcastle upon Tyne, United Kingdom","start_date":"2012-09-04","end_date":"2012-09-07"},"external_id":{"arxiv":["1201.5073"]},"page":"115-131","arxiv":1,"scopus_import":"1","citation":{"ista":"Chatterjee K, Randour M, Raskin J-F. 2012. Strategy synthesis for multi-dimensional quantitative objectives. CONCUR 2012 - Concurrency Theory. CONCUR: Conference on Concurrency Theory, LNCS, vol. 7454, 115–131.","apa":"Chatterjee, K., Randour, M., & Raskin, J.-F. (2012). Strategy synthesis for multi-dimensional quantitative objectives. In M. Koutny & I. Ulidowski (Eds.), CONCUR 2012 - Concurrency Theory (Vol. 7454, pp. 115–131). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-32940-1_10","mla":"Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” CONCUR 2012 - Concurrency Theory, edited by Maciej Koutny and Irek Ulidowski, vol. 7454, Springer, 2012, pp. 115–31, doi:10.1007/978-3-642-32940-1_10.","ieee":"K. Chatterjee, M. Randour, and J.-F. Raskin, “Strategy synthesis for multi-dimensional quantitative objectives,” in CONCUR 2012 - Concurrency Theory, Newcastle upon Tyne, United Kingdom, 2012, vol. 7454, pp. 115–131.","short":"K. Chatterjee, M. Randour, J.-F. Raskin, in:, M. Koutny, I. Ulidowski (Eds.), CONCUR 2012 - Concurrency Theory, Springer, Berlin, Heidelberg, 2012, pp. 115–131.","chicago":"Chatterjee, Krishnendu, Mickael Randour, and Jean-François Raskin. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” In CONCUR 2012 - Concurrency Theory, edited by Maciej Koutny and Irek Ulidowski, 7454:115–31. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-32940-1_10.","ama":"Chatterjee K, Randour M, Raskin J-F. Strategy synthesis for multi-dimensional quantitative objectives. In: Koutny M, Ulidowski I, eds. CONCUR 2012 - Concurrency Theory. Vol 7454. Berlin, Heidelberg: Springer; 2012:115-131. doi:10.1007/978-3-642-32940-1_10"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"09","type":"conference","doi":"10.1007/978-3-642-32940-1_10","date_created":"2022-03-21T08:00:21Z","_id":"10904","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783642329401"],"isbn":["9783642329395"]},"related_material":{"record":[{"id":"2716","status":"public","relation":"later_version"}]},"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1201.5073","open_access":"1"}],"acknowledgement":"Author supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407 (RiSE), ERC Start Grant (279307: Graph Games), Microsoft faculty fellowship.","department":[{"_id":"KrCh"}],"oa":1,"oa_version":"Preprint","quality_controlled":"1","language":[{"iso":"eng"}],"OA_place":"repository","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Randour","first_name":"Mickael","full_name":"Randour, Mickael"},{"full_name":"Raskin, Jean-François","last_name":"Raskin","first_name":"Jean-François"}],"date_published":"2012-09-15T00:00:00Z","corr_author":"1","OA_type":"green","place":"Berlin, Heidelberg","editor":[{"last_name":"Koutny","first_name":"Maciej","full_name":"Koutny, Maciej"},{"last_name":"Ulidowski","first_name":"Irek","full_name":"Ulidowski, Irek"}],"intvolume":" 7454","publisher":"Springer","date_updated":"2025-09-29T11:10:44Z","status":"public","publication_status":"published","day":"15","year":"2012"},{"arxiv":1,"project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"external_id":{"arxiv":["1604.08234"]},"article_processing_charge":"No","page":"301-312","conference":{"name":"ESA: European Symposium on Algorithms","location":"Ljubljana, Slovenia","end_date":"2012-09-12","start_date":"2012-09-10"},"alternative_title":["LNCS"],"ec_funded":1,"volume":7501,"publication":"Algorithms – ESA 2012","abstract":[{"lang":"eng","text":"Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While the existence of polynomial-time algorithms has been a major open problem for decades, there is no algorithm that solves any non-trivial subclass in polynomial time.\r\nIn this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several counter examples that show that many previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting graph structures need not help."}],"title":"Polynomial-time algorithms for energy games with special weight structures","quality_controlled":"1","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"oa_version":"Preprint","oa":1,"_id":"10905","related_material":{"record":[{"id":"535","relation":"later_version","status":"public"}]},"publication_identifier":{"issn":["0302-9743"],"eisbn":["9783642330902"],"eissn":["1611-3349"],"isbn":["9783642330896"]},"date_created":"2022-03-21T08:01:45Z","doi":"10.1007/978-3-642-33090-2_27","main_file_link":[{"url":"https://arxiv.org/abs/1604.08234","open_access":"1"}],"acknowledgement":"Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games), and a Microsoft Faculty Fellows Award","citation":{"apa":"Chatterjee, K., Henzinger, M., Krinninger, S., & Nanongkai, D. (2012). Polynomial-time algorithms for energy games with special weight structures. In Algorithms – ESA 2012 (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer. https://doi.org/10.1007/978-3-642-33090-2_27","ista":"Chatterjee K, Henzinger M, Krinninger S, Nanongkai D. 2012. Polynomial-time algorithms for energy games with special weight structures. Algorithms – ESA 2012. ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.","ama":"Chatterjee K, Henzinger M, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. In: Algorithms – ESA 2012. Vol 7501. Springer; 2012:301-312. doi:10.1007/978-3-642-33090-2_27","chicago":"Chatterjee, Krishnendu, Monika Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” In Algorithms – ESA 2012, 7501:301–12. Springer, 2012. https://doi.org/10.1007/978-3-642-33090-2_27.","short":"K. Chatterjee, M. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms – ESA 2012, Springer, 2012, pp. 301–312.","ieee":"K. Chatterjee, M. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” in Algorithms – ESA 2012, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312.","mla":"Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithms – ESA 2012, vol. 7501, Springer, 2012, pp. 301–12, doi:10.1007/978-3-642-33090-2_27."},"scopus_import":"1","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","intvolume":" 7501","date_published":"2012-10-01T00:00:00Z","corr_author":"1","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","last_name":"Henzinger"},{"full_name":"Krinninger, Sebastian","first_name":"Sebastian","last_name":"Krinninger"},{"full_name":"Nanongkai, Danupon","last_name":"Nanongkai","first_name":"Danupon"}],"day":"01","year":"2012","publication_status":"published","status":"public","publisher":"Springer","date_updated":"2025-09-29T13:18:37Z"},{"scopus_import":"1","citation":{"ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-28756-5_46.","short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:10.1007/978-3-642-28756-5_46.","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46","ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"04","type":"conference","date_created":"2022-03-21T08:03:30Z","doi":"10.1007/978-3-642-28756-5_46","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783642287565"],"isbn":["9783642287558"]},"_id":"10906","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"department":[{"_id":"ToHe"}],"oa":1,"oa_version":"Published Version","quality_controlled":"1","language":[{"iso":"eng"}],"title":"HSF(C): A software verifier based on Horn clauses","abstract":[{"text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.","lang":"eng"}],"publication":"Tools and Algorithms for the Construction and Analysis of Systems","volume":7214,"alternative_title":["LNCS"],"page":"549-551","article_processing_charge":"No","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Tallinn, Estonia","start_date":"2012-03-24","end_date":"2012-04-01"},"series_title":"LNCS","publisher":"Springer","date_updated":"2026-06-18T10:45:24Z","status":"public","publication_status":"published","day":"01","year":"2012","author":[{"full_name":"Grebenshchikov, Sergey","last_name":"Grebenshchikov","first_name":"Sergey"},{"last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"last_name":"Lopes","first_name":"Nuno P.","full_name":"Lopes, Nuno P."},{"full_name":"Popeea, Corneliu","first_name":"Corneliu","last_name":"Popeea"},{"full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko","first_name":"Andrey"}],"ddc":["000"],"date_published":"2012-04-01T00:00:00Z","corr_author":"1","place":"Berlin, Heidelberg","editor":[{"full_name":"Flanagan, Cormac","first_name":"Cormac","last_name":"Flanagan"},{"first_name":"Barbara","last_name":"König","full_name":"König, Barbara"}],"intvolume":" 7214"},{"extern":"1","intvolume":" 335","date_published":"2012-02-02T00:00:00Z","author":[{"last_name":"Savas","first_name":"Jeffrey N.","full_name":"Savas, Jeffrey N."},{"full_name":"Toyama, Brandon H.","last_name":"Toyama","first_name":"Brandon H."},{"full_name":"Xu, Tao","first_name":"Tao","last_name":"Xu"},{"full_name":"Yates, John R.","first_name":"John R.","last_name":"Yates"},{"id":"86c0d31b-b4eb-11ec-ac5a-eae7b2e135ed","full_name":"HETZER, Martin W","orcid":"0000-0002-2111-992X","last_name":"HETZER","first_name":"Martin W"}],"day":"02","year":"2012","pmid":1,"publication_status":"published","status":"public","publisher":"American Association for the Advancement of Science","article_type":"letter_note","date_updated":"2025-12-15T10:03:06Z","page":"942-942","external_id":{"pmid":["22300851"]},"article_processing_charge":"No","volume":335,"abstract":[{"lang":"eng","text":"To combat the functional decline of the proteome, cells use the process of protein turnover to replace potentially impaired polypeptides with new functional copies. We found that extremely long-lived proteins (ELLPs) did not turn over in postmitotic cells of the rat central nervous system. These ELLPs were associated with chromatin and the nuclear pore complex, the central transport channels that mediate all molecular trafficking in and out of the nucleus. The longevity of these proteins would be expected to expose them to potentially harmful metabolites, putting them at risk of accumulating damage over extended periods of time. Thus, it is possible that failure to maintain proper levels and functional integrity of ELLPs in nonproliferative cells might contribute to age-related deterioration in cell and tissue function."}],"publication":"Science","title":"Extremely long-lived nuclear pore proteins in the rat brain","quality_controlled":"1","language":[{"iso":"eng"}],"issue":"6071","department":[{"_id":"MaHe"}],"oa_version":"None","publication_identifier":{"eissn":["1095-9203"],"issn":["0036-8075"]},"_id":"11092","doi":"10.1126/science.1217421","date_created":"2022-04-07T07:52:01Z","citation":{"ama":"Savas JN, Toyama BH, Xu T, Yates JR, Hetzer M. Extremely long-lived nuclear pore proteins in the rat brain. Science. 2012;335(6071):942-942. doi:10.1126/science.1217421","chicago":"Savas, Jeffrey N., Brandon H. Toyama, Tao Xu, John R. Yates, and Martin Hetzer. “Extremely Long-Lived Nuclear Pore Proteins in the Rat Brain.” Science. American Association for the Advancement of Science, 2012. https://doi.org/10.1126/science.1217421.","short":"J.N. Savas, B.H. Toyama, T. Xu, J.R. Yates, M. Hetzer, Science 335 (2012) 942–942.","ieee":"J. N. Savas, B. H. Toyama, T. Xu, J. R. Yates, and M. Hetzer, “Extremely long-lived nuclear pore proteins in the rat brain,” Science, vol. 335, no. 6071. American Association for the Advancement of Science, pp. 942–942, 2012.","mla":"Savas, Jeffrey N., et al. “Extremely Long-Lived Nuclear Pore Proteins in the Rat Brain.” Science, vol. 335, no. 6071, American Association for the Advancement of Science, 2012, pp. 942–942, doi:10.1126/science.1217421.","apa":"Savas, J. N., Toyama, B. H., Xu, T., Yates, J. R., & Hetzer, M. (2012). Extremely long-lived nuclear pore proteins in the rat brain. Science. American Association for the Advancement of Science. https://doi.org/10.1126/science.1217421","ista":"Savas JN, Toyama BH, Xu T, Yates JR, Hetzer M. 2012. Extremely long-lived nuclear pore proteins in the rat brain. Science. 335(6071), 942–942."},"scopus_import":"1","type":"journal_article","month":"02","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"12","type":"journal_article","scopus_import":"1","citation":{"short":"H. Liang, S. Hippenmeyer, H. Ghashghaei, Biology Open 1 (2012) 1200–1203.","ieee":"H. Liang, S. Hippenmeyer, and H. Ghashghaei, “A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic neural progenitors,” Biology open, vol. 1, no. 12. The Company of Biologists, pp. 1200–1203, 2012.","mla":"Liang, Huixuan, et al. “A Nestin-Cre Transgenic Mouse Is Insufficient for Recombination in Early Embryonic Neural Progenitors.” Biology Open, vol. 1, no. 12, The Company of Biologists, 2012, pp. 1200–03, doi:10.1242/bio.20122287.","ama":"Liang H, Hippenmeyer S, Ghashghaei H. A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic neural progenitors. Biology open. 2012;1(12):1200-1203. doi:10.1242/bio.20122287","chicago":"Liang, Huixuan, Simon Hippenmeyer, and H. Ghashghaei. “A Nestin-Cre Transgenic Mouse Is Insufficient for Recombination in Early Embryonic Neural Progenitors.” Biology Open. The Company of Biologists, 2012. https://doi.org/10.1242/bio.20122287.","ista":"Liang H, Hippenmeyer S, Ghashghaei H. 2012. A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic neural progenitors. Biology open. 1(12), 1200–1203.","apa":"Liang, H., Hippenmeyer, S., & Ghashghaei, H. (2012). A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic neural progenitors. Biology Open. The Company of Biologists. https://doi.org/10.1242/bio.20122287"},"doi":"10.1242/bio.20122287","date_created":"2018-12-11T11:56:38Z","_id":"2263","oa_version":"Published Version","oa":1,"department":[{"_id":"SiHi"}],"issue":"12","quality_controlled":"1","language":[{"iso":"eng"}],"title":"A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic neural progenitors","abstract":[{"text":"Nestin-cre transgenic mice have been widely used to direct recombination to neural stem cells (NSCs) and intermediate neural progenitor cells (NPCs). Here we report that a readily utilized, and the only commercially available, Nestin-cre line is insufficient for directing recombination in early embryonic NSCs and NPCs. Analysis of recombination efficiency in multiple cre-dependent reporters and a genetic mosaic line revealed consistent temporal and spatial patterns of recombination in NSCs and NPCs. For comparison we utilized a knock-in Emx1cre line and found robust recombination in NSCs and NPCs in ventricular and subventricular zones of the cerebral cortices as early as embryonic day 12.5. In addition we found that the rate of Nestin-cre driven recombination only reaches sufficiently high levels in NSCs and NPCs during late embryonic and early postnatal periods. These findings are important when commercially available cre lines are considered for directing recombination to embryonic NSCs and NPCs.","lang":"eng"}],"publication":"Biology open","volume":1,"file_date_updated":"2020-07-14T12:45:35Z","external_id":{"isi":["000209205700005"]},"page":"1200 - 1203","article_processing_charge":"No","date_updated":"2025-09-30T08:22:45Z","publisher":"The Company of Biologists","pubrep_id":"387","status":"public","publication_status":"published","file":[{"file_id":"4990","file_name":"IST-2015-387-v1+1_1200.full.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:45:35Z","file_size":726695,"creator":"system","access_level":"open_access","date_created":"2018-12-12T10:13:09Z","relation":"main_file","checksum":"605a1800b81227848c361fd6ba7d22ba"}],"year":"2012","day":"15","author":[{"first_name":"Huixuan","last_name":"Liang","full_name":"Liang, Huixuan"},{"id":"37B36620-F248-11E8-B48F-1D18A9856A87","full_name":"Hippenmeyer, Simon","orcid":"0000-0003-2279-1061","last_name":"Hippenmeyer","first_name":"Simon"},{"last_name":"Ghashghaei","first_name":"H.","full_name":"Ghashghaei, H."}],"publist_id":"4682","ddc":["576"],"date_published":"2012-12-15T00:00:00Z","has_accepted_license":"1","intvolume":" 1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode","short":"CC BY-NC-SA (4.0)","image":"/images/cc_by_nc_sa.png","name":"Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)"},"isi":1},{"article_processing_charge":"No","page":"310 - 322","external_id":{"pmid":["22778152"],"isi":["000323504100006"]},"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"ec_funded":1,"volume":10,"publication":"IEEE ACM Transactions on Computational Biology and Bioinformatics","abstract":[{"text":"We introduce propagation models (PMs), a formalism able to express several kinds of equations that describe the behavior of biochemical reaction networks. Furthermore, we introduce the propagation abstract data type (PADT), which separates concerns regarding different numerical algorithms for the transient analysis of biochemical reaction networks from concerns regarding their implementation, thus allowing for portable and efficient solutions. The state of a propagation abstract data type is given by a vector that assigns mass values to a set of nodes, and its (next) operator propagates mass values through this set of nodes. We propose an approximate implementation of the (next) operator, based on threshold abstraction, which propagates only "significant" mass values and thus achieves a compromise between efficiency and accuracy. Finally, we give three use cases for propagation models: the chemical master equation (CME), the reaction rate equation (RRE), and a hybrid method that combines these two equations. These three applications use propagation models in order to propagate probabilities and/or expected values and variances of the model's variables.","lang":"eng"}],"title":"The propagation approach for computing biochemical reaction networks","language":[{"iso":"eng"}],"quality_controlled":"1","issue":"2","oa_version":"None","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"_id":"2302","doi":"10.1109/TCBB.2012.91","date_created":"2018-12-11T11:56:52Z","type":"journal_article","month":"07","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"short":"T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology and Bioinformatics 10 (2012) 310–322.","mla":"Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology and Bioinformatics, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:10.1109/TCBB.2012.91.","ieee":"T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical reaction networks,” IEEE ACM Transactions on Computational Biology and Bioinformatics, vol. 10, no. 2. IEEE, pp. 310–322, 2012.","ama":"Henzinger TA, Mateescu M. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 2012;10(2):310-322. doi:10.1109/TCBB.2012.91","chicago":"Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology and Bioinformatics. IEEE, 2012. https://doi.org/10.1109/TCBB.2012.91.","ista":"Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 10(2), 310–322.","apa":"Henzinger, T. A., & Mateescu, M. (2012). The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. IEEE. https://doi.org/10.1109/TCBB.2012.91"},"scopus_import":"1","intvolume":" 10","isi":1,"corr_author":"1","date_published":"2012-07-03T00:00:00Z","author":[{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Mateescu, Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria","last_name":"Mateescu"}],"publist_id":"4625","year":"2012","day":"03","publication_status":"published","pmid":1,"status":"public","date_updated":"2025-09-29T14:17:43Z","publisher":"IEEE"},{"author":[{"full_name":"Seiringer, Robert","id":"4AFD0470-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6781-0521","first_name":"Robert","last_name":"Seiringer"}],"publist_id":"4609","corr_author":"1","date_published":"2012-06-24T00:00:00Z","intvolume":" 2","isi":1,"date_updated":"2025-09-30T08:22:10Z","publisher":"European Mathematical Society","status":"public","publication_status":"published","year":"2012","day":"24","title":"Absence of bound states implies non-negativity of the scattering length","publication":"Journal of Spectral Theory","abstract":[{"lang":"eng","text":"We show that bosons interacting via pair potentials with negative scattering length form bound states for a suitable number of particles. In other words, the absence of many-particle bound states of any kind implies the non-negativity of the scattering length of the interaction potential. "}],"volume":2,"page":"321-328","article_processing_charge":"No","external_id":{"isi":["000209021900004"],"arxiv":["1204.0435"]},"arxiv":1,"month":"06","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","type":"journal_article","citation":{"chicago":"Seiringer, Robert. “Absence of Bound States Implies Non-Negativity of the Scattering Length.” Journal of Spectral Theory. European Mathematical Society, 2012. https://doi.org/10.4171/JST/31.","ama":"Seiringer R. Absence of bound states implies non-negativity of the scattering length. Journal of Spectral Theory. 2012;2(3):321-328. doi:10.4171/JST/31","mla":"Seiringer, Robert. “Absence of Bound States Implies Non-Negativity of the Scattering Length.” Journal of Spectral Theory, vol. 2, no. 3, European Mathematical Society, 2012, pp. 321–28, doi:10.4171/JST/31.","ieee":"R. Seiringer, “Absence of bound states implies non-negativity of the scattering length,” Journal of Spectral Theory, vol. 2, no. 3. European Mathematical Society, pp. 321–328, 2012.","short":"R. Seiringer, Journal of Spectral Theory 2 (2012) 321–328.","apa":"Seiringer, R. (2012). Absence of bound states implies non-negativity of the scattering length. Journal of Spectral Theory. European Mathematical Society. https://doi.org/10.4171/JST/31","ista":"Seiringer R. 2012. Absence of bound states implies non-negativity of the scattering length. Journal of Spectral Theory. 2(3), 321–328."},"acknowledgement":"Partial financial support by NSERC ","main_file_link":[{"url":"http://arxiv.org/abs/1204.0435","open_access":"1"}],"doi":"10.4171/JST/31","date_created":"2018-12-11T11:56:58Z","_id":"2318","oa":1,"oa_version":"Preprint","department":[{"_id":"RoSe"}],"issue":"3","quality_controlled":"1","language":[{"iso":"eng"}]},{"ddc":["570","576"],"date_published":"2012-05-01T00:00:00Z","author":[{"full_name":"Ebersberger, Ingo","first_name":"Ingo","last_name":"Ebersberger"},{"first_name":"Ricardo","last_name":"De Matos Simoes","full_name":"De Matos Simoes, Ricardo"},{"full_name":"Kupczok, Anne","id":"2BB22BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Anne","last_name":"Kupczok"},{"first_name":"Matthias","last_name":"Gube","full_name":"Gube, Matthias"},{"first_name":"Erika","last_name":"Kothe","full_name":"Kothe, Erika"},{"full_name":"Voigt, Kerstin","last_name":"Voigt","first_name":"Kerstin"},{"full_name":"Von Haeseler, Arndt","last_name":"Von Haeseler","first_name":"Arndt"}],"publist_id":"4515","tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)","image":"/images/cc_by_nc.png","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode"},"isi":1,"intvolume":" 29","has_accepted_license":"1","publication_status":"published","pubrep_id":"384","status":"public","publisher":"Oxford University Press","date_updated":"2025-09-30T08:21:34Z","day":"01","year":"2012","file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:45:40Z","file_size":754922,"creator":"system","access_level":"open_access","relation":"main_file","checksum":"d565dcac27d1736c0c378ea6fcf22d69","date_created":"2018-12-12T10:13:30Z","file_id":"5013","file_name":"IST-2015-384-v1+1_Mol_Biol_Evol-2012-Ebersberger-1319-34.pdf"}],"license":"https://creativecommons.org/licenses/by-nc/4.0/","file_date_updated":"2020-07-14T12:45:40Z","volume":29,"publication":"Molecular Biology and Evolution","abstract":[{"text":"The kingdom of fungi provides model organisms for biotechnology, cell biology, genetics, and life sciences in general. Only when their phylogenetic relationships are stably resolved, can individual results from fungal research be integrated into a holistic picture of biology. However, and despite recent progress, many deep relationships within the fungi remain unclear. Here, we present the first phylogenomic study of an entire eukaryotic kingdom that uses a consistency criterion to strengthen phylogenetic conclusions. We reason that branches (splits) recovered with independent data and different tree reconstruction methods are likely to reflect true evolutionary relationships. Two complementary phylogenomic data sets based on 99 fungal genomes and 109 fungal expressed sequence tag (EST) sets analyzed with four different tree reconstruction methods shed light from different angles on the fungal tree of life. Eleven additional data sets address specifically the phylogenetic position of Blastocladiomycota, Ustilaginomycotina, and Dothideomycetes, respectively. The combined evidence from the resulting trees supports the deep-level stability of the fungal groups toward a comprehensive natural system of the fungi. In addition, our analysis reveals methodologically interesting aspects. Enrichment for EST encoded data-a common practice in phylogenomic analyses-introduces a strong bias toward slowly evolving and functionally correlated genes. Consequently, the generalization of phylogenomic data sets as collections of randomly selected genes cannot be taken for granted. A thorough characterization of the data to assess possible influences on the tree reconstruction should therefore become a standard in phylogenomic analyses.","lang":"eng"}],"title":"A consistent phylogenetic backbone for the fungi","article_processing_charge":"No","page":"1319 - 1334","external_id":{"isi":["000303603300004"]},"_id":"2411","doi":"10.1093/molbev/msr285","date_created":"2018-12-11T11:57:30Z","citation":{"apa":"Ebersberger, I., De Matos Simoes, R., Kupczok, A., Gube, M., Kothe, E., Voigt, K., & Von Haeseler, A. (2012). A consistent phylogenetic backbone for the fungi. Molecular Biology and Evolution. Oxford University Press. https://doi.org/10.1093/molbev/msr285","ista":"Ebersberger I, De Matos Simoes R, Kupczok A, Gube M, Kothe E, Voigt K, Von Haeseler A. 2012. A consistent phylogenetic backbone for the fungi. Molecular Biology and Evolution. 29(5), 1319–1334.","chicago":"Ebersberger, Ingo, Ricardo De Matos Simoes, Anne Kupczok, Matthias Gube, Erika Kothe, Kerstin Voigt, and Arndt Von Haeseler. “A Consistent Phylogenetic Backbone for the Fungi.” Molecular Biology and Evolution. Oxford University Press, 2012. https://doi.org/10.1093/molbev/msr285.","ama":"Ebersberger I, De Matos Simoes R, Kupczok A, et al. A consistent phylogenetic backbone for the fungi. Molecular Biology and Evolution. 2012;29(5):1319-1334. doi:10.1093/molbev/msr285","ieee":"I. Ebersberger et al., “A consistent phylogenetic backbone for the fungi,” Molecular Biology and Evolution, vol. 29, no. 5. Oxford University Press, pp. 1319–1334, 2012.","mla":"Ebersberger, Ingo, et al. “A Consistent Phylogenetic Backbone for the Fungi.” Molecular Biology and Evolution, vol. 29, no. 5, Oxford University Press, 2012, pp. 1319–34, doi:10.1093/molbev/msr285.","short":"I. Ebersberger, R. De Matos Simoes, A. Kupczok, M. Gube, E. Kothe, K. Voigt, A. Von Haeseler, Molecular Biology and Evolution 29 (2012) 1319–1334."},"scopus_import":"1","type":"journal_article","month":"05","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"quality_controlled":"1","issue":"5","department":[{"_id":"JoBo"}],"oa":1,"oa_version":"Published Version"},{"ddc":["000"],"date_published":"2012-12-10T00:00:00Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Joglekar, Manas","first_name":"Manas","last_name":"Joglekar"},{"full_name":"Shah, Nisarg","first_name":"Nisarg","last_name":"Shah"}],"publist_id":"4180","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"intvolume":" 18","has_accepted_license":"1","publication_status":"published","pubrep_id":"525","status":"public","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2025-09-23T08:00:31Z","day":"10","year":"2012","file":[{"file_id":"5040","file_name":"IST-2016-525-v1+1_42_1_.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:45:45Z","file_size":519040,"creator":"system","access_level":"open_access","relation":"main_file","date_created":"2018-12-12T10:13:53Z","checksum":"d4d644ed1a885dbfc4fa1ef4c5724dab"}],"file_date_updated":"2020-07-14T12:45:45Z","ec_funded":1,"alternative_title":["LIPIcs"],"volume":18,"abstract":[{"text":"We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning vertices from where the objective can be ensured with probability 1. We study for the first time the average case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average case running time is linear (as compared to the worst case linear number of iterations and quadratic time complexity). Second, for the average case analysis over all MDPs we show that the expected number of iterations is constant and the average case running time is linear (again as compared to the worst case linear number of iterations and quadratic time complexity). Finally we also show that given that all MDPs are equally likely, the probability that the classical algorithm requires more than constant number of iterations is exponentially small.","lang":"eng"}],"title":"Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"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"}],"page":"461 - 473","conference":{"start_date":"2012-12-15","end_date":"2012-12-17","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","location":"Hyderabad, India"},"related_material":{"record":[{"relation":"later_version","status":"public","id":"1598"}]},"_id":"2715","date_created":"2018-12-11T11:59:13Z","doi":"10.4230/LIPIcs.FSTTCS.2012.461","citation":{"apa":"Chatterjee, K., Joglekar, M., & Shah, N. (2012). Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives (Vol. 18, pp. 461–473). Presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461","ista":"Chatterjee K, Joglekar M, Shah N. 2012. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 461–473.","ama":"Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. In: Vol 18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2012:461-473. doi:10.4230/LIPIcs.FSTTCS.2012.461","chicago":"Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives,” 18:461–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461.","short":"K. Chatterjee, M. Joglekar, N. Shah, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 461–473.","mla":"Chatterjee, Krishnendu, et al. Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives. Vol. 18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 461–73, doi:10.4230/LIPIcs.FSTTCS.2012.461.","ieee":"K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives,” presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India, 2012, vol. 18, pp. 461–473."},"scopus_import":1,"type":"conference","month":"12","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"oa_version":"Published Version","oa":1},{"citation":{"short":"C. Lampert, in:, Neural Information Processing Systems Foundation, 2012, pp. 82–90.","mla":"Lampert, Christoph. Dynamic Pruning of Factor Graphs for Maximum Marginal Prediction. Vol. 1, Neural Information Processing Systems Foundation, 2012, pp. 82–90.","ieee":"C. Lampert, “Dynamic pruning of factor graphs for maximum marginal prediction,” presented at the NIPS: Neural Information Processing Systems, Lake Tahoe, NV, United States, 2012, vol. 1, pp. 82–90.","ama":"Lampert C. Dynamic pruning of factor graphs for maximum marginal prediction. In: Vol 1. Neural Information Processing Systems Foundation; 2012:82-90.","chicago":"Lampert, Christoph. “Dynamic Pruning of Factor Graphs for Maximum Marginal Prediction,” 1:82–90. Neural Information Processing Systems Foundation, 2012.","ista":"Lampert C. 2012. Dynamic pruning of factor graphs for maximum marginal prediction. NIPS: Neural Information Processing Systems vol. 1, 82–90.","apa":"Lampert, C. (2012). Dynamic pruning of factor graphs for maximum marginal prediction (Vol. 1, pp. 82–90). Presented at the NIPS: Neural Information Processing Systems, Lake Tahoe, NV, United States: Neural Information Processing Systems Foundation."},"publisher":"Neural Information Processing Systems Foundation","scopus_import":"1","type":"conference","month":"12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-06-03T11:46:36Z","publication_status":"published","_id":"2825","status":"public","date_created":"2018-12-11T11:59:48Z","department":[{"_id":"ChLa"}],"oa_version":"None","language":[{"iso":"eng"}],"quality_controlled":"1","day":"01","year":"2012","publist_id":"3975","author":[{"first_name":"Christoph","last_name":"Lampert","full_name":"Lampert, Christoph","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8622-7887"}],"title":"Dynamic pruning of factor graphs for maximum marginal prediction","date_published":"2012-12-01T00:00:00Z","volume":1,"corr_author":"1","abstract":[{"text":"We study the problem of maximum marginal prediction (MMP) in probabilistic graphical models, a task that occurs, for example, as the Bayes optimal decision rule under a Hamming loss. MMP is typically performed as a two-stage procedure: one estimates each variable's marginal probability and then forms a prediction from the states of maximal probability. In this work we propose a simple yet effective technique for accelerating MMP when inference is sampling-based: instead of the above two-stage procedure we directly estimate the posterior probability of each decision variable. This allows us to identify the point of time when we are sufficiently certain about any individual decision. Whenever this is the case, we dynamically prune the variables we are confident about from the underlying factor graph. Consequently, at any time only samples of variables whose decision is still uncertain need to be created. Experiments in two prototypical scenarios, multi-label classification and image inpainting, show that adaptive sampling can drastically accelerate MMP without sacrificing prediction accuracy.","lang":"eng"}],"page":"82 - 90","article_processing_charge":"No","conference":{"location":"Lake Tahoe, NV, United States","name":"NIPS: Neural Information Processing Systems","end_date":"2012-12-06","start_date":"2012-12-03"},"intvolume":" 1"},{"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736","first_name":"Damien","last_name":"Zufferey"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"publist_id":"3946","corr_author":"1","date_published":"2012-05-21T00:00:00Z","intvolume":" 301","isi":1,"date_updated":"2025-09-30T08:20:22Z","publisher":"Elsevier","pmid":1,"publication_status":"published","status":"public","year":"2012","day":"21","title":"Evolutionary game dynamics in populations with different learners","ec_funded":1,"volume":301,"abstract":[{"text":"We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics.","lang":"eng"}],"publication":"Journal of Theoretical Biology","external_id":{"pmid":["22394652"],"isi":["000303079500016"]},"article_processing_charge":"No","page":"161 - 173","project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","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"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"type":"journal_article","month":"05","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ista":"Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 301, 161–173.","apa":"Chatterjee, K., Zufferey, D., & Nowak, M. (2012). Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. Elsevier. https://doi.org/10.1016/j.jtbi.2012.02.021","ieee":"K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations with different learners,” Journal of Theoretical Biology, vol. 301. Elsevier, pp. 161–173, 2012.","mla":"Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with Different Learners.” Journal of Theoretical Biology, vol. 301, Elsevier, 2012, pp. 161–73, doi:10.1016/j.jtbi.2012.02.021.","short":"K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.","chicago":"Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary Game Dynamics in Populations with Different Learners.” Journal of Theoretical Biology. Elsevier, 2012. https://doi.org/10.1016/j.jtbi.2012.02.021.","ama":"Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 2012;301:161-173. doi:10.1016/j.jtbi.2012.02.021"},"scopus_import":"1","main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/"}],"_id":"2848","date_created":"2018-12-11T11:59:55Z","doi":"10.1016/j.jtbi.2012.02.021","oa_version":"Submitted Version","oa":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","language":[{"iso":"eng"}]},{"oa_version":"Submitted Version","oa":1,"department":[{"_id":"HeEd"}],"language":[{"iso":"eng"}],"quality_controlled":"1","issue":"6","type":"journal_article","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"01","citation":{"apa":"Edelsbrunner, H., & Strelkova, N. (2012). On the configuration space of Steiner minimal trees. Russian Mathematical Surveys. IOP Publishing. https://doi.org/10.1070/RM2012v067n06ABEH004820","ista":"Edelsbrunner H, Strelkova N. 2012. On the configuration space of Steiner minimal trees. Russian Mathematical Surveys. 67(6), 1167–1168.","chicago":"Edelsbrunner, Herbert, and Nataliya Strelkova. “On the Configuration Space of Steiner Minimal Trees.” Russian Mathematical Surveys. IOP Publishing, 2012. https://doi.org/10.1070/RM2012v067n06ABEH004820.","ama":"Edelsbrunner H, Strelkova N. On the configuration space of Steiner minimal trees. Russian Mathematical Surveys. 2012;67(6):1167-1168. doi:10.1070/RM2012v067n06ABEH004820","mla":"Edelsbrunner, Herbert, and Nataliya Strelkova. “On the Configuration Space of Steiner Minimal Trees.” Russian Mathematical Surveys, vol. 67, no. 6, IOP Publishing, 2012, pp. 1167–68, doi:10.1070/RM2012v067n06ABEH004820.","ieee":"H. Edelsbrunner and N. Strelkova, “On the configuration space of Steiner minimal trees,” Russian Mathematical Surveys, vol. 67, no. 6. IOP Publishing, pp. 1167–1168, 2012.","short":"H. Edelsbrunner, N. Strelkova, Russian Mathematical Surveys 67 (2012) 1167–1168."},"scopus_import":"1","_id":"2849","date_created":"2018-12-11T11:59:55Z","doi":"10.1070/RM2012v067n06ABEH004820","page":"1167 - 1168","article_processing_charge":"No","external_id":{"isi":["000315950100005"]},"title":"On the configuration space of Steiner minimal trees","volume":67,"publication":"Russian Mathematical Surveys","file_date_updated":"2020-07-14T12:45:51Z","file":[{"creator":"system","file_size":392021,"date_updated":"2020-07-14T12:45:51Z","content_type":"application/pdf","relation":"main_file","checksum":"44ee8d173487e8ed41a51136816bbeb4","date_created":"2018-12-12T10:14:26Z","access_level":"open_access","file_name":"IST-2016-546-v1+1_2014-J-05-SteinerMinTrees.pdf","file_id":"5078"}],"year":"2012","day":"01","date_updated":"2025-09-30T08:19:37Z","publisher":"IOP Publishing","publication_status":"published","pubrep_id":"546","status":"public","has_accepted_license":"1","intvolume":" 67","isi":1,"author":[{"first_name":"Herbert","last_name":"Edelsbrunner","full_name":"Edelsbrunner, Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9823-6833"},{"full_name":"Strelkova, Nataliya","last_name":"Strelkova","first_name":"Nataliya"}],"publist_id":"3943","date_published":"2012-01-01T00:00:00Z","ddc":["000"]},{"intvolume":" 7590","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"publist_id":"3870","date_published":"2012-09-01T00:00:00Z","OA_type":"closed access","corr_author":"1","day":"01","year":"2012","publisher":"Springer","date_updated":"2025-05-20T07:30:56Z","status":"public","publication_status":"published","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"article_processing_charge":"No","page":"1 - 2","conference":{"location":"Innsbruck, Austria","name":"MODELS: Model-driven Engineering Languages and Systems","end_date":"2012-10-05","start_date":"2012-09-30"},"title":"Quantitative reactive models","publication":"15th International Conference on Model Driven Engineering Languages and Systems","abstract":[{"lang":"eng","text":"Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria."}],"ec_funded":1,"volume":7590,"alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"oa_version":"None","language":[{"iso":"eng"}],"quality_controlled":"1","scopus_import":"1","citation":{"mla":"Henzinger, Thomas A. “Quantitative Reactive Models.” 15th International Conference on Model Driven Engineering Languages and Systems, vol. 7590, Springer, 2012, pp. 1–2, doi:10.1007/978-3-642-33666-9_1.","ieee":"T. A. Henzinger, “Quantitative reactive models,” in 15th International Conference on Model Driven Engineering Languages and Systems, Innsbruck, Austria, 2012, vol. 7590, pp. 1–2.","short":"T.A. Henzinger, in:, 15th International Conference on Model Driven Engineering Languages and Systems, Springer, 2012, pp. 1–2.","chicago":"Henzinger, Thomas A. “Quantitative Reactive Models.” In 15th International Conference on Model Driven Engineering Languages and Systems, 7590:1–2. Springer, 2012. https://doi.org/10.1007/978-3-642-33666-9_1.","ama":"Henzinger TA. Quantitative reactive models. In: 15th International Conference on Model Driven Engineering Languages and Systems. Vol 7590. Springer; 2012:1-2. doi:10.1007/978-3-642-33666-9_1","ista":"Henzinger TA. 2012. Quantitative reactive models. 15th International Conference on Model Driven Engineering Languages and Systems. MODELS: Model-driven Engineering Languages and Systems, LNCS, vol. 7590, 1–2.","apa":"Henzinger, T. A. (2012). Quantitative reactive models. In 15th International Conference on Model Driven Engineering Languages and Systems (Vol. 7590, pp. 1–2). Innsbruck, Austria: Springer. https://doi.org/10.1007/978-3-642-33666-9_1"},"month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","doi":"10.1007/978-3-642-33666-9_1","date_created":"2018-12-11T12:00:09Z","publication_identifier":{"eisbn":["9783642336669"],"eissn":["1611-3349"]},"_id":"2888"},{"page":"53 - 62","conference":{"end_date":"2012-10-12","start_date":"2012-10-07","location":"Tampere, Finland","name":"EMSOFT: Embedded Software "},"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"abstract":[{"text":"Systems are often specified using multiple requirements on their behavior. In practice, these requirements can be contradictory. The classical approach to specification, verification, and synthesis demands more detailed specifications that resolve any contradictions in the requirements. These detailed specifications are usually large, cumbersome, and hard to maintain or modify. In contrast, quantitative frameworks allow the formalization of the intuitive idea that what is desired is an implementation that comes "closest" to satisfying the mutually incompatible requirements, according to a measure of fit that can be defined by the requirements engineer. One flexible framework for quantifying how "well" an implementation satisfies a specification is offered by simulation distances that are parameterized by an error model. We introduce this framework, study its properties, and provide an algorithmic solution for the following quantitative synthesis question: given two (or more) behavioral requirements specified by possibly incompatible finite-state machines, and an error model, find the finite-state implementation that minimizes the maximal simulation distance to the given requirements. Furthermore, we generalize the framework to handle infinite alphabets (for example, realvalued domains). We also demonstrate how quantitative specifications based on simulation distances might lead to smaller and easier to modify specifications. Finally, we illustrate our approach using case studies on error correcting codes and scheduler synthesis.","lang":"eng"}],"publication":"Proceedings of the tenth ACM international conference on Embedded software","ec_funded":1,"date_published":"2012-10-01T00:00:00Z","title":"Synthesis from incompatible specifications","author":[{"first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Gopi, Sivakanth","last_name":"Gopi","first_name":"Sivakanth"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Nishant","last_name":"Totla","full_name":"Totla, Nishant"}],"publist_id":"3868","year":"2012","day":"01","quality_controlled":"1","language":[{"iso":"eng"}],"oa_version":"None","department":[{"_id":"ToHe"}],"doi":"10.1145/2380356.2380371","status":"public","date_created":"2018-12-11T12:00:10Z","publication_status":"published","_id":"2890","date_updated":"2021-01-12T07:00:30Z","month":"10","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","type":"conference","scopus_import":1,"publisher":"ACM","citation":{"apa":"Cerny, P., Gopi, S., Henzinger, T. A., Radhakrishna, A., & Totla, N. (2012). Synthesis from incompatible specifications. In Proceedings of the tenth ACM international conference on Embedded software (pp. 53–62). Tampere, Finland: ACM. https://doi.org/10.1145/2380356.2380371","ista":"Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. 2012. Synthesis from incompatible specifications. Proceedings of the tenth ACM international conference on Embedded software. EMSOFT: Embedded Software , 53–62.","ama":"Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. Synthesis from incompatible specifications. In: Proceedings of the Tenth ACM International Conference on Embedded Software. ACM; 2012:53-62. doi:10.1145/2380356.2380371","chicago":"Cerny, Pavol, Sivakanth Gopi, Thomas A Henzinger, Arjun Radhakrishna, and Nishant Totla. “Synthesis from Incompatible Specifications.” In Proceedings of the Tenth ACM International Conference on Embedded Software, 53–62. ACM, 2012. https://doi.org/10.1145/2380356.2380371.","short":"P. Cerny, S. Gopi, T.A. Henzinger, A. Radhakrishna, N. Totla, in:, Proceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 53–62.","mla":"Cerny, Pavol, et al. “Synthesis from Incompatible Specifications.” Proceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 53–62, doi:10.1145/2380356.2380371.","ieee":"P. Cerny, S. Gopi, T. A. Henzinger, A. Radhakrishna, and N. Totla, “Synthesis from incompatible specifications,” in Proceedings of the tenth ACM international conference on Embedded software, Tampere, Finland, 2012, pp. 53–62."}}]