[{"publisher":"Cell Press","quality_controlled":0,"page":"707 - 718","intvolume":"       139","publication":"Cell","issue":"4","publication_status":"published","_id":"4228","author":[{"full_name":"Bollenbach, Tobias","first_name":"Tobias","last_name":"Bollenbach"},{"full_name":"Quan, Selwyn","last_name":"Quan","first_name":"Selwyn"},{"full_name":"Remy Chait","id":"3464AE84-F248-11E8-B48F-1D18A9856A87","first_name":"Remy P","last_name":"Chait","orcid":"0000-0003-0876-3187"},{"last_name":"Kishony","first_name":"Roy","full_name":"Kishony, Roy"}],"extern":1,"abstract":[{"lang":"eng","text":"Suppressive drug interactions, in which one antibiotic can actually help bacterial cells to grow faster in the presence of another, occur between protein and DNA synthesis inhibitors. Here, we show that this suppression results from nonoptimal regulation of ribosomal genes in the presence of DNA stress. Using GFP-tagged transcription reporters in Escherichia coli, we find that ribosomal genes are not directly regulated by DNA stress, leading to an imbalance between cellular DNA and protein content. To test whether ribosomal gene expression under DNA stress is nonoptimal for growth rate, we sequentially deleted up to six of the seven ribosomal RNA operons. These synthetic manipulations of ribosomal gene expression correct the protein-DNA imbalance, lead to improved survival and growth, and completely remove the suppressive drug interaction. A simple mathematical model explains the nonoptimal regulation in different nutrient environments. These results reveal the genetic mechanism underlying an important class of suppressive drug interactions."}],"title":"Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions","status":"public","citation":{"ieee":"T. Bollenbach, S. Quan, R. P. Chait, and R. Kishony, “Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions,” <i>Cell</i>, vol. 139, no. 4. Cell Press, pp. 707–718, 2009.","apa":"Bollenbach, T., Quan, S., Chait, R. P., &#38; Kishony, R. (2009). Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions. <i>Cell</i>. Cell Press. <a href=\"https://doi.org/10.1016/j.cell.2009.10.025\">https://doi.org/10.1016/j.cell.2009.10.025</a>","short":"T. Bollenbach, S. Quan, R.P. Chait, R. Kishony, Cell 139 (2009) 707–718.","chicago":"Bollenbach, Tobias, Selwyn Quan, Remy P Chait, and Roy Kishony. “Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions.” <i>Cell</i>. Cell Press, 2009. <a href=\"https://doi.org/10.1016/j.cell.2009.10.025\">https://doi.org/10.1016/j.cell.2009.10.025</a>.","mla":"Bollenbach, Tobias, et al. “Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions.” <i>Cell</i>, vol. 139, no. 4, Cell Press, 2009, pp. 707–18, doi:<a href=\"https://doi.org/10.1016/j.cell.2009.10.025\">10.1016/j.cell.2009.10.025</a>.","ama":"Bollenbach T, Quan S, Chait RP, Kishony R. Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions. <i>Cell</i>. 2009;139(4):707-718. doi:<a href=\"https://doi.org/10.1016/j.cell.2009.10.025\">10.1016/j.cell.2009.10.025</a>","ista":"Bollenbach T, Quan S, Chait RP, Kishony R. 2009. Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions. Cell. 139(4), 707–718."},"day":"01","date_updated":"2021-01-12T07:55:27Z","year":"2009","type":"journal_article","date_created":"2018-12-11T12:07:43Z","date_published":"2009-01-01T00:00:00Z","month":"01","volume":139,"doi":"10.1016/j.cell.2009.10.025","publist_id":"1890"},{"volume":181,"publist_id":"1882","doi":"10.1534/genetics.108.099309","oa_version":"None","date_published":"2009-03-01T00:00:00Z","date_created":"2018-12-11T12:07:44Z","month":"03","scopus_import":1,"year":"2009","type":"journal_article","day":"01","citation":{"short":"N.H. Barton, H. De Vladar, Genetics 181 (2009) 997–1011.","apa":"Barton, N. H., &#38; De Vladar, H. (2009). Statistical mechanics and the evolution of polygenic quantitative traits. <i>Genetics</i>. Genetics Society of America. <a href=\"https://doi.org/10.1534/genetics.108.099309\">https://doi.org/10.1534/genetics.108.099309</a>","ieee":"N. H. Barton and H. De Vladar, “Statistical mechanics and the evolution of polygenic quantitative traits,” <i>Genetics</i>, vol. 181, no. 3. Genetics Society of America, pp. 997–1011, 2009.","chicago":"Barton, Nicholas H, and Harold De Vladar. “Statistical Mechanics and the Evolution of Polygenic Quantitative Traits.” <i>Genetics</i>. Genetics Society of America, 2009. <a href=\"https://doi.org/10.1534/genetics.108.099309\">https://doi.org/10.1534/genetics.108.099309</a>.","ista":"Barton NH, De Vladar H. 2009. Statistical mechanics and the evolution of polygenic quantitative traits. Genetics. 181(3), 997–1011.","ama":"Barton NH, De Vladar H. Statistical mechanics and the evolution of polygenic quantitative traits. <i>Genetics</i>. 2009;181(3):997-1011. doi:<a href=\"https://doi.org/10.1534/genetics.108.099309\">10.1534/genetics.108.099309</a>","mla":"Barton, Nicholas H., and Harold De Vladar. “Statistical Mechanics and the Evolution of Polygenic Quantitative Traits.” <i>Genetics</i>, vol. 181, no. 3, Genetics Society of America, 2009, pp. 997–1011, doi:<a href=\"https://doi.org/10.1534/genetics.108.099309\">10.1534/genetics.108.099309</a>."},"date_updated":"2021-01-12T07:55:29Z","title":"Statistical mechanics and the evolution of polygenic quantitative traits","abstract":[{"text":"The evolution of quantitative characters depends on the frequencies of the alleles involved, yet these frequencies cannot usually be measured. Previous groups have proposed an approximation to the dynamics of quantitative traits, based on an analogy with statistical mechanics. We present a modified version of that approach, which makes the analogy more precise and applies quite generally to describe the evolution of allele frequencies. We calculate explicitly how the macroscopic quantities (i.e., quantities that depend on the quantitative trait) depend on evolutionary forces, in a way that is independent of the microscopic details. We first show that the stationary distribution of allele frequencies under drift, selection, and mutation maximizes a certain measure of entropy, subject to constraints on the expectation of observable quantities. We then approximate the dynamical changes in these expectations, assuming that the distribution of allele frequencies always maximizes entropy, conditional on the expected values. When applied to directional selection on an additive trait, this gives a very good approximation to the evolution of the trait mean and the genetic variance, when the number of mutations per generation is sufficiently high (4Nμ &gt; 1). We show how the method can be modified for small mutation rates (4Nμ → 0). We outline how this method describes epistatic interactions as, for example, with stabilizing selection.","lang":"eng"}],"status":"public","author":[{"full_name":"Barton, Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H","last_name":"Barton","orcid":"0000-0002-8548-5240"},{"first_name":"Harold","last_name":"De Vladar","full_name":"De Vladar, Harold"}],"acknowledgement":"N.B. was supported by the Engineering and Physical Sciences Research Council (GR/T11753 and GR/T19537) and by the Royal Society.\r\nWe are grateful to Ellen Baake for helping to initiate this project and for her comments on this manuscript. We also thank Michael Turelli for his comments on the manuscript and I. Pen for discussions and support in this project. This project was a result of a collaboration supported by the European Science Foundation grant “Integrating population genetics and conservation biology.” ","issue":"3","publication_status":"published","language":[{"iso":"eng"}],"_id":"4231","publisher":"Genetics Society of America","quality_controlled":"1","page":"997 - 1011","intvolume":"       181","department":[{"_id":"NiBa"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"Genetics"},{"quality_controlled":0,"publisher":"Faculty of mathematical and natural sciences, University of Groningen","_id":"4232","publication_status":"published","author":[{"full_name":"Harold Vladar","id":"2A181218-F248-11E8-B48F-1D18A9856A87","first_name":"Harold","last_name":"Vladar","orcid":"0000-0002-5985-7653"}],"title":"Stochasticity and Variability in the dynamics and genetics of populations","extern":1,"status":"public","day":"01","citation":{"apa":"de Vladar, H. (2009). <i>Stochasticity and Variability in the dynamics and genetics of populations</i>. Faculty of mathematical and natural sciences, University of Groningen. <a href=\"https://doi.org/3811\">https://doi.org/3811</a>","short":"H. de Vladar, Stochasticity and Variability in the Dynamics and Genetics of Populations, Faculty of mathematical and natural sciences, University of Groningen, 2009.","ieee":"H. de Vladar, “Stochasticity and Variability in the dynamics and genetics of populations,” Faculty of mathematical and natural sciences, University of Groningen, 2009.","ista":"de Vladar H. 2009. Stochasticity and Variability in the dynamics and genetics of populations. Faculty of mathematical and natural sciences, University of Groningen.","ama":"de Vladar H. Stochasticity and Variability in the dynamics and genetics of populations. 2009. doi:<a href=\"https://doi.org/3811\">3811</a>","mla":"de Vladar, Harold. <i>Stochasticity and Variability in the Dynamics and Genetics of Populations</i>. Faculty of mathematical and natural sciences, University of Groningen, 2009, doi:<a href=\"https://doi.org/3811\">3811</a>.","chicago":"Vladar, Harold de. “Stochasticity and Variability in the Dynamics and Genetics of Populations.” Faculty of mathematical and natural sciences, University of Groningen, 2009. <a href=\"https://doi.org/3811\">https://doi.org/3811</a>."},"date_updated":"2021-01-12T07:55:29Z","type":"dissertation","year":"2009","date_created":"2018-12-11T12:07:44Z","date_published":"2009-01-01T00:00:00Z","month":"01","doi":"3811","publist_id":"1883"},{"ddc":["570"],"publication_status":"published","_id":"4242","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"NiBa"}],"abstract":[{"text":"Felsenstein distinguished two ways by which selection can directly strengthen isolation. First, a modifier that strengthens prezygotic isolation can be favored everywhere. This fits with the traditional view of reinforcement as an adaptation to reduce deleterious hybridization by strengthening assortative mating. Second, selection can favor association between different incompatibilities, despite recombination. We generalize this “two allele” model to follow associations among any number of incompatibilities, which may include both assortment and hybrid inviability. Our key argument is that this process, of coupling between incompatibilities, may be quite different from the usual view of reinforcement: strong isolation can evolve through the coupling of any kind of incompatibility, whether prezygotic or postzygotic. Single locus incompatibilities become coupled because associations between them increase the variance in compatibility, which in turn increases mean fitness if there is positive epistasis. Multiple incompatibilities, each maintained by epistasis, can become coupled in the same way. In contrast, a single-locus incompatibility can become coupled with loci that reduce the viability of haploid hybrids because this reduces harmful recombination. We obtain simple approximations for the limits of tight linkage, and strong assortment, and show how assortment alleles can invade through associations with other components of reproductive isolation.","lang":"eng"}],"acknowledgement":"This work was supported by a Royal Society/Wolfson Research Merit award, and by a grant from the Natural Environment Research Council.\r\nWe are very grateful for insightful comments from S. P. Otto, and for helpful suggestions from the referees and the Associate Editor, Maria Servedio.","file_date_updated":"2020-07-14T12:46:25Z","scopus_import":1,"year":"2009","type":"journal_article","pubrep_id":"551","doi":"10.1111/j.1558-5646.2009.00622.x","publist_id":"1866","oa_version":"Submitted Version","issue":"5","intvolume":"        63","publication":"Evolution; International Journal of Organic Evolution","publisher":"Wiley","page":"1171 - 1190","quality_controlled":"1","status":"public","title":"The evolution of strong reproductive isolation","author":[{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","full_name":"Barton, Nicholas H","first_name":"Nicholas H","orcid":"0000-0002-8548-5240","last_name":"Barton"},{"full_name":"De Cara, Maria","last_name":"De Cara","first_name":"Maria"}],"oa":1,"date_updated":"2021-01-12T07:55:33Z","file":[{"date_created":"2018-12-12T10:11:46Z","creator":"system","relation":"main_file","file_id":"4903","file_size":720913,"access_level":"open_access","content_type":"application/pdf","file_name":"IST-2016-551-v1+1_BartonDeCaraRevNew.pdf","date_updated":"2020-07-14T12:46:25Z","checksum":"1920d2e25ef335833764256c1a47bbfb"},{"checksum":"c1c51bbc10d4f328fc96fc5b0e5dc25d","date_updated":"2020-07-14T12:46:25Z","file_name":"IST-2016-551-v1+2_BartonDeCaraRevNewSI.pdf","content_type":"application/pdf","access_level":"open_access","creator":"system","file_id":"4904","relation":"main_file","file_size":290160,"date_created":"2018-12-12T10:11:47Z"}],"citation":{"short":"N.H. Barton, M. De Cara, Evolution; International Journal of Organic Evolution 63 (2009) 1171–1190.","apa":"Barton, N. H., &#38; De Cara, M. (2009). The evolution of strong reproductive isolation. <i>Evolution; International Journal of Organic Evolution</i>. Wiley. <a href=\"https://doi.org/10.1111/j.1558-5646.2009.00622.x\">https://doi.org/10.1111/j.1558-5646.2009.00622.x</a>","ieee":"N. H. Barton and M. De Cara, “The evolution of strong reproductive isolation,” <i>Evolution; International Journal of Organic Evolution</i>, vol. 63, no. 5. Wiley, pp. 1171–1190, 2009.","ista":"Barton NH, De Cara M. 2009. The evolution of strong reproductive isolation. Evolution; International Journal of Organic Evolution. 63(5), 1171–1190.","ama":"Barton NH, De Cara M. The evolution of strong reproductive isolation. <i>Evolution; International Journal of Organic Evolution</i>. 2009;63(5):1171-1190. doi:<a href=\"https://doi.org/10.1111/j.1558-5646.2009.00622.x\">10.1111/j.1558-5646.2009.00622.x</a>","mla":"Barton, Nicholas H., and Maria De Cara. “The Evolution of Strong Reproductive Isolation.” <i>Evolution; International Journal of Organic Evolution</i>, vol. 63, no. 5, Wiley, 2009, pp. 1171–90, doi:<a href=\"https://doi.org/10.1111/j.1558-5646.2009.00622.x\">10.1111/j.1558-5646.2009.00622.x</a>.","chicago":"Barton, Nicholas H, and Maria De Cara. “The Evolution of Strong Reproductive Isolation.” <i>Evolution; International Journal of Organic Evolution</i>. Wiley, 2009. <a href=\"https://doi.org/10.1111/j.1558-5646.2009.00622.x\">https://doi.org/10.1111/j.1558-5646.2009.00622.x</a>."},"day":"01","volume":63,"has_accepted_license":"1","month":"05","date_created":"2018-12-11T12:07:48Z","date_published":"2009-05-01T00:00:00Z"},{"doi":"10.1534/genetics.107.085225","publist_id":"1101","volume":181,"date_created":"2018-12-11T12:08:26Z","date_published":"2009-01-01T00:00:00Z","month":"01","type":"journal_article","year":"2009","citation":{"short":"J.P. Bollback, J. Huelsenbeck, Genetics 181 (2009) 225–234.","apa":"Bollback, J. P., &#38; Huelsenbeck, J. (2009). Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence. <i>Genetics</i>. Genetics Society of America. <a href=\"https://doi.org/10.1534/genetics.107.085225\">https://doi.org/10.1534/genetics.107.085225</a>","ieee":"J. P. Bollback and J. Huelsenbeck, “Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence,” <i>Genetics</i>, vol. 181, no. 1. Genetics Society of America, pp. 225–234, 2009.","ama":"Bollback JP, Huelsenbeck J. Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence. <i>Genetics</i>. 2009;181(1):225-234. doi:<a href=\"https://doi.org/10.1534/genetics.107.085225\">10.1534/genetics.107.085225</a>","ista":"Bollback JP, Huelsenbeck J. 2009. Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence. Genetics. 181(1), 225–234.","mla":"Bollback, Jonathan P., and John Huelsenbeck. “Parallel Genetic Evolution within and between Bacteriophage Species of Varying Degrees of Divergence.” <i>Genetics</i>, vol. 181, no. 1, Genetics Society of America, 2009, pp. 225–34, doi:<a href=\"https://doi.org/10.1534/genetics.107.085225\">10.1534/genetics.107.085225</a>.","chicago":"Bollback, Jonathan P, and John Huelsenbeck. “Parallel Genetic Evolution within and between Bacteriophage Species of Varying Degrees of Divergence.” <i>Genetics</i>. Genetics Society of America, 2009. <a href=\"https://doi.org/10.1534/genetics.107.085225\">https://doi.org/10.1534/genetics.107.085225</a>."},"day":"01","date_updated":"2021-01-12T07:56:22Z","abstract":[{"lang":"eng","text":"Parallel evolution is the acquisition of identical adaptive traits in independently evolving populations. Understanding whether the genetic changes underlying adaptation to a common selective environment are parallel within and between species is interesting because it sheds light on the degree of evolutionary constraints. If parallel evolution is perfect, then the implication is that forces such as functional constraints, epistasis, and pleiotropy play an important role in shaping the outcomes of adaptive evolution. In addition, population genetic theory predicts that the probability of parallel evolution will decline with an increase in the number of adaptive solutions-if a single adaptive solution exists, then parallel evolution will be observed among highly divergent species. For this reason, it is predicted that close relatives-which likely overlap more in the details of their adaptive solutions-will show more parallel evolution. By adapting three related bacteriophage species to a novel environment we find (1) a high rate of parallel genetic evolution at orthologous nucleotide and amino acid residues within species, (2) parallel beneficial mutations do not occur in a common order in which they fix or appear in an evolving population, (3) low rates of parallel evolution and convergent evolution between species, and (4) the probability of parallel and convergent evolution between species is strongly effected by divergence."}],"title":"Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence","extern":1,"status":"public","author":[{"orcid":"0000-0002-4624-4612","last_name":"Bollback","first_name":"Jonathan P","full_name":"Jonathan Bollback","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Huelsenbeck, John P","last_name":"Huelsenbeck","first_name":"John"}],"issue":"1","_id":"4357","publication_status":"published","page":"225 - 234","quality_controlled":0,"publisher":"Genetics Society of America","publication":"Genetics","intvolume":"       181"},{"publisher":"Springer","page":"366 - 382","quality_controlled":0,"publication_status":"published","_id":"4360","alternative_title":["LNCS 5749"],"author":[{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","first_name":"Thomas","last_name":"Wies"},{"first_name":"Ruzica","last_name":"Piskac","full_name":"Piskac, Ruzica"},{"full_name":"Kuncak, Viktor","last_name":"Kuncak","first_name":"Viktor"}],"status":"public","extern":1,"title":"Combining Theories with Shared Set Operations","date_updated":"2021-01-12T07:56:24Z","day":"01","citation":{"chicago":"Wies, Thomas, Ruzica Piskac, and Viktor Kuncak. “Combining Theories with Shared Set Operations,” 366–82. Springer, 2009. <a href=\"https://doi.org/1558\">https://doi.org/1558</a>.","mla":"Wies, Thomas, et al. <i>Combining Theories with Shared Set Operations</i>. Springer, 2009, pp. 366–82, doi:<a href=\"https://doi.org/1558\">1558</a>.","ista":"Wies T, Piskac R, Kuncak V. 2009. Combining Theories with Shared Set Operations. FroCoS: Frontiers of Combining Systems, LNCS 5749, , 366–382.","ama":"Wies T, Piskac R, Kuncak V. Combining Theories with Shared Set Operations. In: Springer; 2009:366-382. doi:<a href=\"https://doi.org/1558\">1558</a>","ieee":"T. Wies, R. Piskac, and V. Kuncak, “Combining Theories with Shared Set Operations,” presented at the FroCoS: Frontiers of Combining Systems, 2009, pp. 366–382.","short":"T. Wies, R. Piskac, V. Kuncak, in:, Springer, 2009, pp. 366–382.","apa":"Wies, T., Piskac, R., &#38; Kuncak, V. (2009). Combining Theories with Shared Set Operations (pp. 366–382). Presented at the FroCoS: Frontiers of Combining Systems, Springer. <a href=\"https://doi.org/1558\">https://doi.org/1558</a>"},"conference":{"name":"FroCoS: Frontiers of Combining Systems"},"year":"2009","type":"conference","month":"01","date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:08:27Z","publist_id":"1098","doi":"1558"},{"publication":"Formalizing and Verifying Transactional Memories","publisher":"EPFL Lausanne","quality_controlled":0,"publication_status":"published","_id":"4363","author":[{"full_name":"Vasu Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","last_name":"Singh"}],"status":"public","extern":1,"title":"Formalizing and Verifying Transactional Memories","date_updated":"2021-01-12T07:56:25Z","citation":{"ieee":"V. Singh, “Formalizing and Verifying Transactional Memories,” EPFL Lausanne, 2009.","apa":"Singh, V. (2009). <i>Formalizing and Verifying Transactional Memories</i>. <i>Formalizing and Verifying Transactional Memories</i>. EPFL Lausanne.","short":"V. Singh, Formalizing and Verifying Transactional Memories, EPFL Lausanne, 2009.","chicago":"Singh, Vasu. “Formalizing and Verifying Transactional Memories.” <i>Formalizing and Verifying Transactional Memories</i>. EPFL Lausanne, 2009.","mla":"Singh, Vasu. “Formalizing and Verifying Transactional Memories.” <i>Formalizing and Verifying Transactional Memories</i>, EPFL Lausanne, 2009.","ista":"Singh V. 2009. Formalizing and Verifying Transactional Memories. EPFL Lausanne.","ama":"Singh V. Formalizing and Verifying Transactional Memories. <i>Formalizing and Verifying Transactional Memories</i>. 2009."},"day":"01","type":"dissertation","year":"2009","month":"01","date_created":"2018-12-11T12:08:28Z","date_published":"2009-01-01T00:00:00Z","publist_id":"1095"},{"page":"3 - 18","quality_controlled":0,"publisher":"Springer","_id":"4365","publication_status":"published","alternative_title":["LNCS 5673"],"author":[{"last_name":"Seghir","first_name":"Mohamed","full_name":"Seghir,Mohamed Nassim"},{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski,Andreas"},{"first_name":"Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies"}],"status":"public","title":"Abstraction Refinement for Quantified Array Assertions","extern":1,"date_updated":"2021-01-12T07:56:26Z","day":"01","citation":{"ieee":"M. Seghir, A. Podelski, and T. Wies, “Abstraction Refinement for Quantified Array Assertions,” presented at the SAS: Static Analysis Symposium, 2009, pp. 3–18.","apa":"Seghir, M., Podelski, A., &#38; Wies, T. (2009). Abstraction Refinement for Quantified Array Assertions (pp. 3–18). Presented at the SAS: Static Analysis Symposium, Springer. <a href=\"https://doi.org/1556\">https://doi.org/1556</a>","short":"M. Seghir, A. Podelski, T. Wies, in:, Springer, 2009, pp. 3–18.","mla":"Seghir, Mohamed, et al. <i>Abstraction Refinement for Quantified Array Assertions</i>. Springer, 2009, pp. 3–18, doi:<a href=\"https://doi.org/1556\">1556</a>.","ista":"Seghir M, Podelski A, Wies T. 2009. Abstraction Refinement for Quantified Array Assertions. SAS: Static Analysis Symposium, LNCS 5673, , 3–18.","ama":"Seghir M, Podelski A, Wies T. Abstraction Refinement for Quantified Array Assertions. In: Springer; 2009:3-18. doi:<a href=\"https://doi.org/1556\">1556</a>","chicago":"Seghir, Mohamed, Andreas Podelski, and Thomas Wies. “Abstraction Refinement for Quantified Array Assertions,” 3–18. Springer, 2009. <a href=\"https://doi.org/1556\">https://doi.org/1556</a>."},"conference":{"name":"SAS: Static Analysis Symposium"},"year":"2009","type":"conference","month":"01","date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:08:29Z","publist_id":"1094","doi":"1556"},{"date_updated":"2021-01-12T07:56:30Z","day":"01","citation":{"mla":"Lahiri, Shuvendu, et al. <i>Intra-Module Inference</i>. Springer, 2009, pp. 493–508, doi:<a href=\"https://doi.org/1555\">1555</a>.","ama":"Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. Intra-module Inference. In: Springer; 2009:493-508. doi:<a href=\"https://doi.org/1555\">1555</a>","ista":"Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module Inference. CAV: Computer Aided Verification, LNCS 5643, , 493–508.","chicago":"Lahiri, Shuvendu, Shaz Qadeer, Juan Galeotti, Jan Voung, and Thomas Wies. “Intra-Module Inference,” 493–508. Springer, 2009. <a href=\"https://doi.org/1555\">https://doi.org/1555</a>.","ieee":"S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, and T. Wies, “Intra-module Inference,” presented at the CAV: Computer Aided Verification, 2009, pp. 493–508.","short":"S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, Springer, 2009, pp. 493–508.","apa":"Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., &#38; Wies, T. (2009). Intra-module Inference (pp. 493–508). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/1555\">https://doi.org/1555</a>"},"conference":{"name":"CAV: Computer Aided Verification"},"type":"conference","year":"2009","month":"01","date_created":"2018-12-11T12:08:32Z","date_published":"2009-01-01T00:00:00Z","publist_id":"1082","doi":"1555","quality_controlled":0,"page":"493 - 508","publisher":"Springer","_id":"4375","publication_status":"published","alternative_title":["LNCS 5643"],"author":[{"last_name":"Lahiri","first_name":"Shuvendu","full_name":"Lahiri,Shuvendu K."},{"full_name":"Qadeer,Shaz","last_name":"Qadeer","first_name":"Shaz"},{"first_name":"Juan","last_name":"Galeotti","full_name":"Galeotti,Juan P."},{"full_name":"Voung,Jan W.","first_name":"Jan","last_name":"Voung"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","last_name":"Wies","first_name":"Thomas"}],"status":"public","title":"Intra-module Inference","extern":1},{"title":"Parallel programming with object assemblies","extern":1,"status":"public","author":[{"full_name":"Lublinerman,Roberto","first_name":"Roberto","last_name":"Lublinerman"},{"full_name":"Chaudhuri,Swarat","first_name":"Swarat","last_name":"Chaudhuri"},{"first_name":"Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Pavol Cerny"}],"_id":"4376","publication_status":"published","page":"61 - 80","quality_controlled":0,"publisher":"ACM","doi":"1546","publist_id":"1083","date_created":"2018-12-11T12:08:32Z","date_published":"2009-01-01T00:00:00Z","month":"01","year":"2009","type":"conference","conference":{"name":"Oopsla Object Oriented Programming Systems Languages and Applications"},"citation":{"chicago":"Lublinerman, Roberto, Swarat Chaudhuri, and Pavol Cerny. “Parallel Programming with Object Assemblies,” 61–80. ACM, 2009. <a href=\"https://doi.org/1546\">https://doi.org/1546</a>.","mla":"Lublinerman, Roberto, et al. <i>Parallel Programming with Object Assemblies</i>. ACM, 2009, pp. 61–80, doi:<a href=\"https://doi.org/1546\">1546</a>.","ista":"Lublinerman R, Chaudhuri S, Cerny P. 2009. Parallel programming with object assemblies. Oopsla Object Oriented Programming Systems Languages and Applications, 61–80.","ama":"Lublinerman R, Chaudhuri S, Cerny P. Parallel programming with object assemblies. In: ACM; 2009:61-80. doi:<a href=\"https://doi.org/1546\">1546</a>","ieee":"R. Lublinerman, S. Chaudhuri, and P. Cerny, “Parallel programming with object assemblies,” presented at the Oopsla Object Oriented Programming Systems Languages and Applications, 2009, pp. 61–80.","short":"R. Lublinerman, S. Chaudhuri, P. Cerny, in:, ACM, 2009, pp. 61–80.","apa":"Lublinerman, R., Chaudhuri, S., &#38; Cerny, P. (2009). Parallel programming with object assemblies (pp. 61–80). Presented at the Oopsla Object Oriented Programming Systems Languages and Applications, ACM. <a href=\"https://doi.org/1546\">https://doi.org/1546</a>"},"day":"01","date_updated":"2021-01-12T07:56:30Z"},{"alternative_title":["LNCS 5850"],"author":[{"full_name":"Hoenicke,Jochen","first_name":"Jochen","last_name":"Hoenicke"},{"full_name":"Leino, K Rustan","last_name":"Leino","first_name":"K Rustan"},{"full_name":"Podelski,Andreas","last_name":"Podelski","first_name":"Andreas"},{"full_name":"Schäf,Martin","last_name":"Schäf","first_name":"Martin"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","last_name":"Wies","first_name":"Thomas"}],"extern":1,"title":"It's Doomed; We Can Prove It","status":"public","publisher":"Springer","page":"338 - 353","quality_controlled":0,"publication_status":"published","_id":"4377","date_created":"2018-12-11T12:08:32Z","date_published":"2009-01-01T00:00:00Z","month":"01","publist_id":"1079","doi":"1557","citation":{"chicago":"Hoenicke, Jochen, K Rustan Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. “It’s Doomed; We Can Prove It,” 338–53. Springer, 2009. <a href=\"https://doi.org/1557\">https://doi.org/1557</a>.","mla":"Hoenicke, Jochen, et al. <i>It’s Doomed; We Can Prove It</i>. Springer, 2009, pp. 338–53, doi:<a href=\"https://doi.org/1557\">1557</a>.","ama":"Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. It’s Doomed; We Can Prove It. In: Springer; 2009:338-353. doi:<a href=\"https://doi.org/1557\">1557</a>","ista":"Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. 2009. It’s Doomed; We Can Prove It. FM: Formal Methods, LNCS 5850, , 338–353.","ieee":"J. Hoenicke, K. R. Leino, A. Podelski, M. Schäf, and T. Wies, “It’s Doomed; We Can Prove It,” presented at the FM: Formal Methods, 2009, pp. 338–353.","short":"J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Springer, 2009, pp. 338–353.","apa":"Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., &#38; Wies, T. (2009). It’s Doomed; We Can Prove It (pp. 338–353). Presented at the FM: Formal Methods, Springer. <a href=\"https://doi.org/1557\">https://doi.org/1557</a>"},"day":"01","date_updated":"2021-01-12T07:56:31Z","type":"conference","year":"2009","conference":{"name":"FM: Formal Methods"}},{"publication_status":"published","_id":"4383","publisher":"Springer","quality_controlled":0,"page":"321 - 336","intvolume":"      5643","extern":1,"title":"Software transactional memory on relaxed memory models","abstract":[{"text":"Pseudo-code descriptions of STMs assume sequentially consistent program execution and atomicity of high-level STM operations like read, write, and commit. These assumptions are often violated in realistic settings, as STM implementations run on relaxed memory models, with the atomicity of operations as provided by the hardware. This paper presents the first approach to verify STMs under relaxed memory models with atomicity of 32 bit loads and stores, and read-modify-write operations. We present RML, a new high-level language for expressing concurrent algorithms with a hardware-level atomicity of instructions, and whose semantics is parametrized by various relaxed memory models. We then present our tool, FOIL, which takes as input the RML description of an STM algorithm and the description of a memory model, and automatically determines the locations of fences, which if inserted, ensure the correctness of the STM algorithm under the given memory model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of sequential consistency, total store order, partial store order, and relaxed memory order.","lang":"eng"}],"status":"public","oa":1,"file_date_updated":"2020-07-14T12:46:28Z","acknowledgement":"This research was supported by the Swiss National Science Foundation.","author":[{"full_name":"Guerraoui, Rachid","first_name":"Rachid","last_name":"Guerraoui"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Vasu Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","last_name":"Singh"}],"alternative_title":["LNCS"],"year":"2009","type":"conference","conference":{"name":"CAV: Computer Aided Verification"},"file":[{"checksum":"df3c3e6306afd3f630a9146f91642f0a","file_name":"IST-2012-45-v1+1_Software_transactional_memory_on_relaxed_memory_models.pdf","date_updated":"2020-07-14T12:46:28Z","access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:14:50Z","file_size":265763,"file_id":"5105","relation":"main_file","creator":"system"}],"citation":{"ieee":"R. Guerraoui, T. A. Henzinger, and V. Singh, “Software transactional memory on relaxed memory models,” presented at the CAV: Computer Aided Verification, 2009, vol. 5643, pp. 321–336.","short":"R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2009, pp. 321–336.","apa":"Guerraoui, R., Henzinger, T. A., &#38; Singh, V. (2009). Software transactional memory on relaxed memory models (Vol. 5643, pp. 321–336). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">https://doi.org/10.1007/978-3-642-02658-4_26</a>","mla":"Guerraoui, Rachid, et al. <i>Software Transactional Memory on Relaxed Memory Models</i>. Vol. 5643, Springer, 2009, pp. 321–36, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">10.1007/978-3-642-02658-4_26</a>.","ama":"Guerraoui R, Henzinger TA, Singh V. Software transactional memory on relaxed memory models. In: Vol 5643. Springer; 2009:321-336. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">10.1007/978-3-642-02658-4_26</a>","ista":"Guerraoui R, Henzinger TA, Singh V. 2009. Software transactional memory on relaxed memory models. CAV: Computer Aided Verification, LNCS, vol. 5643, 321–336.","chicago":"Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Software Transactional Memory on Relaxed Memory Models,” 5643:321–36. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">https://doi.org/10.1007/978-3-642-02658-4_26</a>."},"day":"19","pubrep_id":"45","date_updated":"2021-01-12T07:56:34Z","volume":5643,"doi":"10.1007/978-3-642-02658-4_26","publist_id":"1074","date_published":"2009-06-19T00:00:00Z","date_created":"2018-12-11T12:08:34Z","month":"06"},{"date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:08:35Z","month":"01","doi":"1533","publist_id":"1070","day":"01","citation":{"apa":"Dragojevic, A., Guerraoui, R., Singh, A., &#38; Singh, V. (2009). Preventing versus curing: avoiding conflicts in transactional memories (pp. 7–16). Presented at the POPL: Principles of Programming Languages, ACM. <a href=\"https://doi.org/1533\">https://doi.org/1533</a>","short":"A. Dragojevic, R. Guerraoui, A. Singh, V. Singh, in:, ACM, 2009, pp. 7–16.","ieee":"A. Dragojevic, R. Guerraoui, A. Singh, and V. Singh, “Preventing versus curing: avoiding conflicts in transactional memories,” presented at the POPL: Principles of Programming Languages, 2009, pp. 7–16.","chicago":"Dragojevic, Aleksandar, Rachid Guerraoui, Anmol Singh, and Vasu Singh. “Preventing versus Curing: Avoiding Conflicts in Transactional Memories,” 7–16. ACM, 2009. <a href=\"https://doi.org/1533\">https://doi.org/1533</a>.","ama":"Dragojevic A, Guerraoui R, Singh A, Singh V. Preventing versus curing: avoiding conflicts in transactional memories. In: ACM; 2009:7-16. doi:<a href=\"https://doi.org/1533\">1533</a>","ista":"Dragojevic A, Guerraoui R, Singh A, Singh V. 2009. Preventing versus curing: avoiding conflicts in transactional memories. POPL: Principles of Programming Languages, 7–16.","mla":"Dragojevic, Aleksandar, et al. <i>Preventing versus Curing: Avoiding Conflicts in Transactional Memories</i>. ACM, 2009, pp. 7–16, doi:<a href=\"https://doi.org/1533\">1533</a>."},"date_updated":"2021-01-12T07:56:34Z","year":"2009","type":"conference","conference":{"name":"POPL: Principles of Programming Languages"},"author":[{"last_name":"Dragojevic","first_name":"Aleksandar","full_name":"Dragojevic,Aleksandar"},{"full_name":"Guerraoui, Rachid","last_name":"Guerraoui","first_name":"Rachid"},{"last_name":"Singh","first_name":"Anmol","full_name":"Singh, Anmol V"},{"first_name":"Vasu","last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Vasu Singh"}],"extern":1,"title":"Preventing versus curing: avoiding conflicts in transactional memories","status":"public","publisher":"ACM","quality_controlled":0,"page":"7 - 16","publication_status":"published","_id":"4385"},{"author":[{"full_name":"Pavol Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol"},{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"}],"alternative_title":["LNCS"],"status":"public","title":"Automated Analysis of Java Methods for Confidentiality","extern":1,"quality_controlled":0,"page":"173 - 187","publisher":"Springer","_id":"4391","publication_status":"published","month":"07","date_published":"2009-07-01T00:00:00Z","date_created":"2018-12-11T12:08:36Z","doi":"1548","publist_id":"1067","date_updated":"2021-01-12T07:56:37Z","day":"01","citation":{"mla":"Cerny, Pavol, and Rajeev Alur. <i>Automated Analysis of Java Methods for Confidentiality</i>. Springer, 2009, pp. 173–87, doi:<a href=\"https://doi.org/1548\">1548</a>.","ama":"Cerny P, Alur R. Automated Analysis of Java Methods for Confidentiality. In: Springer; 2009:173-187. doi:<a href=\"https://doi.org/1548\">1548</a>","ista":"Cerny P, Alur R. 2009. Automated Analysis of Java Methods for Confidentiality. CAV: Computer Aided Verification, LNCS, , 173–187.","chicago":"Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for Confidentiality,” 173–87. Springer, 2009. <a href=\"https://doi.org/1548\">https://doi.org/1548</a>.","ieee":"P. Cerny and R. Alur, “Automated Analysis of Java Methods for Confidentiality,” presented at the CAV: Computer Aided Verification, 2009, pp. 173–187.","short":"P. Cerny, R. Alur, in:, Springer, 2009, pp. 173–187.","apa":"Cerny, P., &#38; Alur, R. (2009). Automated Analysis of Java Methods for Confidentiality (pp. 173–187). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/1548\">https://doi.org/1548</a>"},"conference":{"name":"CAV: Computer Aided Verification"},"year":"2009","type":"conference"},{"conference":{"name":"CSL: Computer Science Logic","end_date":"2009-09-11","start_date":"2009-09-07","location":"Coimbra, Portugal"},"related_material":{"record":[{"id":"2967","relation":"later_version","status":"public"}]},"type":"conference","year":"2009","date_updated":"2023-02-23T11:06:20Z","day":"01","citation":{"apa":"Alur, R., Cerny, P., &#38; Weinstein, S. (2009). Algorithmic analysis of array-accessing programs (Vol. 5771, pp. 86–101). Presented at the CSL: Computer Science Logic, Coimbra, Portugal: Springer. <a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">https://doi.org/10.1007/978-3-642-04027-6_9</a>","short":"R. Alur, P. Cerny, S. Weinstein, in:, Springer, 2009, pp. 86–101.","ieee":"R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing programs,” presented at the CSL: Computer Science Logic, Coimbra, Portugal, 2009, vol. 5771, pp. 86–101.","ama":"Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. In: Vol 5771. Springer; 2009:86-101. doi:<a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">10.1007/978-3-642-04027-6_9</a>","ista":"Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101.","mla":"Alur, Rajeev, et al. <i>Algorithmic Analysis of Array-Accessing Programs</i>. Vol. 5771, Springer, 2009, pp. 86–101, doi:<a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">10.1007/978-3-642-04027-6_9</a>.","chicago":"Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of Array-Accessing Programs,” 5771:86–101. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">https://doi.org/10.1007/978-3-642-04027-6_9</a>."},"publist_id":"1056","doi":"10.1007/978-3-642-04027-6_9","volume":5771,"month":"09","date_published":"2009-09-01T00:00:00Z","date_created":"2018-12-11T12:08:40Z","oa_version":"Submitted Version","language":[{"iso":"eng"}],"_id":"4403","publication_status":"published","intvolume":"      5771","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"http://repository.upenn.edu/cis_reports/894/"}],"page":"86 - 101","publisher":"Springer","status":"public","abstract":[{"text":"For programs whose data variables range over boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this paper, we consider algorithmic verification of programs that use boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over a potentially unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) Pspace-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly-nested loops. The second result establishes connections to automata and logics defining languages over data words.","lang":"eng"}],"title":"Algorithmic analysis of array-accessing programs","extern":"1","alternative_title":["LNCS"],"author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol"},{"full_name":"Weinstein, Scott","last_name":"Weinstein","first_name":"Scott"}],"oa":1},{"page":"337 - 352","main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/sliding-window_abstraction_for_infinite_markov_chains.pdf"}],"quality_controlled":0,"publisher":"Springer","intvolume":"      5643","_id":"4453","publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:46:30Z","author":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Maria","last_name":"Mateescu","full_name":"Maria Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Wolf","first_name":"Verena","full_name":"Wolf, Verena"}],"alternative_title":["LNCS"],"acknowledgement":"The research has been partially funded by the Swiss National Science Foundation under grant 205321-111840.","abstract":[{"text":"We present an on-the-fly abstraction technique for infinite-state continuous -time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time instances by solving a sequence of dynamically constructed abstract models, each depending on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstraction can be computed, and the precision of the abstraction refined when desired. We implemented the algorithm and demonstrate its usefulness and efficiency on several case studies from systems biology.","lang":"eng"}],"title":"Sliding-window abstraction for infinite Markov chains","extern":1,"status":"public","citation":{"chicago":"Henzinger, Thomas A, Maria Mateescu, and Verena Wolf. “Sliding-Window Abstraction for Infinite Markov Chains,” 5643:337–52. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">https://doi.org/10.1007/978-3-642-02658-4_27</a>.","mla":"Henzinger, Thomas A., et al. <i>Sliding-Window Abstraction for Infinite Markov Chains</i>. Vol. 5643, Springer, 2009, pp. 337–52, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">10.1007/978-3-642-02658-4_27</a>.","ista":"Henzinger TA, Mateescu M, Wolf V. 2009. Sliding-window abstraction for infinite Markov chains. CAV: Computer Aided Verification, LNCS, vol. 5643, 337–352.","ama":"Henzinger TA, Mateescu M, Wolf V. Sliding-window abstraction for infinite Markov chains. In: Vol 5643. Springer; 2009:337-352. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">10.1007/978-3-642-02658-4_27</a>","ieee":"T. A. Henzinger, M. Mateescu, and V. Wolf, “Sliding-window abstraction for infinite Markov chains,” presented at the CAV: Computer Aided Verification, 2009, vol. 5643, pp. 337–352.","short":"T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 337–352.","apa":"Henzinger, T. A., Mateescu, M., &#38; Wolf, V. (2009). Sliding-window abstraction for infinite Markov chains (Vol. 5643, pp. 337–352). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">https://doi.org/10.1007/978-3-642-02658-4_27</a>"},"day":"01","file":[{"checksum":"36b974111521ea534aae294166e93a63","file_name":"IST-2012-40-v1+1_Sliding-window_abstraction_for_infinite_markov_chains.pdf","date_updated":"2020-07-14T12:46:30Z","access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:12:20Z","creator":"system","relation":"main_file","file_id":"4938","file_size":804295}],"date_updated":"2021-01-12T07:57:04Z","pubrep_id":"40","type":"conference","year":"2009","conference":{"name":"CAV: Computer Aided Verification"},"date_created":"2018-12-11T12:08:55Z","date_published":"2009-01-01T00:00:00Z","month":"01","doi":"10.1007/978-3-642-02658-4_27","publist_id":"278","volume":5643},{"status":"public","abstract":[{"lang":"eng","text":"Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete -state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive.\nWe present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required."}],"title":"Approximation of event probabilities in noisy cellular processes","extern":1,"acknowledgement":"This research was supported in part by the Swiss National Science Foundation under grant 205321-111840 and by the Excellence Cluster on Multimodal Computing and Interaction.","author":[{"last_name":"Didier","first_name":"Frédéric","full_name":"Didier, Frédéric"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Maria","last_name":"Mateescu","full_name":"Maria Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Wolf","first_name":"Verena","full_name":"Wolf, Verena"}],"alternative_title":["LNCS"],"_id":"4535","publication_status":"published","intvolume":"      5688","quality_controlled":0,"page":"173 - 188","publisher":"Springer","publist_id":"189","doi":"10.1007/978-3-642-03845-7_12","volume":5688,"month":"08","date_published":"2009-08-17T00:00:00Z","date_created":"2018-12-11T12:09:21Z","conference":{"name":"CMSB: Computational Methods in Systems Biology"},"related_material":{"record":[{"status":"public","relation":"later_version","id":"3364"}]},"type":"conference","year":"2009","date_updated":"2023-02-23T11:24:03Z","day":"17","citation":{"chicago":"Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf. “Approximation of Event Probabilities in Noisy Cellular Processes,” 5688:173–88. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">https://doi.org/10.1007/978-3-642-03845-7_12</a>.","mla":"Didier, Frédéric, et al. <i>Approximation of Event Probabilities in Noisy Cellular Processes</i>. Vol. 5688, Springer, 2009, pp. 173–88, doi:<a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">10.1007/978-3-642-03845-7_12</a>.","ista":"Didier F, Henzinger TA, Mateescu M, Wolf V. 2009. Approximation of event probabilities in noisy cellular processes. CMSB: Computational Methods in Systems Biology, LNCS, vol. 5688, 173–188.","ama":"Didier F, Henzinger TA, Mateescu M, Wolf V. Approximation of event probabilities in noisy cellular processes. In: Vol 5688. Springer; 2009:173-188. doi:<a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">10.1007/978-3-642-03845-7_12</a>","ieee":"F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Approximation of event probabilities in noisy cellular processes,” presented at the CMSB: Computational Methods in Systems Biology, 2009, vol. 5688, pp. 173–188.","short":"F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 173–188.","apa":"Didier, F., Henzinger, T. A., Mateescu, M., &#38; Wolf, V. (2009). Approximation of event probabilities in noisy cellular processes (Vol. 5688, pp. 173–188). Presented at the CMSB: Computational Methods in Systems Biology, Springer. <a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">https://doi.org/10.1007/978-3-642-03845-7_12</a>"}},{"publist_id":"181","doi":"10.1109/LICS.2009.16","date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:09:23Z","oa_version":"None","month":"01","year":"2009","type":"conference","scopus_import":"1","conference":{"name":"LICS: Logic in Computer Science"},"related_material":{"record":[{"status":"public","id":"3867","relation":"later_version"}]},"day":"01","citation":{"ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “Expressiveness and closure properties for quantitative languages,” presented at the LICS: Logic in Computer Science, 2009, pp. 199–208.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). Expressiveness and closure properties for quantitative languages (pp. 199–208). Presented at the LICS: Logic in Computer Science, IEEE. <a href=\"https://doi.org/10.1109/LICS.2009.16\">https://doi.org/10.1109/LICS.2009.16</a>","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, IEEE, 2009, pp. 199–208.","mla":"Chatterjee, Krishnendu, et al. <i>Expressiveness and Closure Properties for Quantitative Languages</i>. IEEE, 2009, pp. 199–208, doi:<a href=\"https://doi.org/10.1109/LICS.2009.16\">10.1109/LICS.2009.16</a>.","ama":"Chatterjee K, Doyen L, Henzinger TA. Expressiveness and closure properties for quantitative languages. In: IEEE; 2009:199-208. doi:<a href=\"https://doi.org/10.1109/LICS.2009.16\">10.1109/LICS.2009.16</a>","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Expressiveness and closure properties for quantitative languages. LICS: Logic in Computer Science, 199–208.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness and Closure Properties for Quantitative Languages,” 199–208. IEEE, 2009. <a href=\"https://doi.org/10.1109/LICS.2009.16\">https://doi.org/10.1109/LICS.2009.16</a>."},"date_updated":"2023-02-23T11:46:11Z","pubrep_id":"55","title":"Expressiveness and closure properties for quantitative languages","abstract":[{"text":"Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages L that assign to each word w a real number L(w). In the case of infinite words, the value of a run is naturally computed as the maximum, limsup, liminf, limit average, or discounted sum of the transition weights. We study expressiveness and closure questions about these quantitative languages. We first show that the set of words with value greater than a threshold can be non-w-regular for deterministic limit-average and discounted-sum automata, while this set is always w-regular when the threshold is isolated (i.e., some neighborhood around the threshold contains no word). In the latter case, we prove that the w-regular language is robust against small perturbations of the transition weights. We next consider automata with transition weights 0 or 1 and show that they are as expressive as general weighted automata in the limit-average case, but not in the discounted-sum case. Third, for quantitative languages L-1 and L-2, we consider the operations max(L-1, L-2), min(L-1, L-2), and 1-L-1, which generalize the boolean operations on languages, as well as the sum L-1 + L-2. We establish the closure properties of all classes of quantitative languages with respect to these four operations.","lang":"eng"}],"extern":"1","status":"public","article_processing_charge":"No","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"language":[{"iso":"eng"}],"_id":"4540","publication_status":"published","quality_controlled":"1","page":"199 - 208","publisher":"IEEE","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"pubrep_id":"39","type":"conference","year":"2009","scopus_import":1,"oa_version":"Submitted Version","doi":"10.1007/978-3-642-03409-1_2","publist_id":"180","project":[{"grant_number":"214373","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems"},{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"_id":"4542","ddc":["004"],"publication_status":"published","file_date_updated":"2020-07-14T12:46:31Z","acknowledgement":"This research was supported in part by the Swiss National Science Foundation under the Indo-Swiss Joint Research Programme, by the European Network of Excellence on Embedded Systems Design (ArtistDesign), by the European Combest, Quasimodo, and Gasics projects, by the PAI program Moves funded by the Belgian Federal Government, and by the CFV (Federated Center in Verification) funded by the F.R.S.-FNRS.","alternative_title":["LNCS"],"abstract":[{"text":"Weighted automata are finite automata with numerical weights on transitions. Nondeterministic weighted automata define quantitative languages L that assign to each word w a real number L(w) computed as the maximal value of all runs over w, and the value of a run r is a function of the sequence of weights that appear along r. There are several natural functions to consider such as Sup, LimSup, LimInf, limit average, and discounted sum of transition weights.\r\nWe introduce alternating weighted automata in which the transitions of the runs are chosen by two players in a turn-based fashion. Each word is assigned the maximal value of a run that the first player can enforce regardless of the choices made by the second player. We survey the results about closure properties, expressiveness, and decision problems for nondeterministic weighted automata, and we extend these results to alternating weighted automata.\r\nFor quantitative languages L 1 and L 2, we consider the pointwise operations max(L 1,L 2), min(L 1,L 2), 1 − L 1, and the sum L 1 + L 2. We establish the closure properties of all classes of alternating weighted automata with respect to these four operations.\r\nWe next compare the expressive power of the various classes of alternating and nondeterministic weighted automata over infinite words. In particular, for limit average and discounted sum, we show that alternation brings more expressive power than nondeterminism.\r\nFinally, we present decidability results and open questions for the quantitative extension of the classical decision problems in automata theory: emptiness, universality, language inclusion, and language equivalence.","lang":"eng"}],"ec_funded":1,"day":"10","citation":{"ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “Alternating weighted automata,” presented at the FCT: Fundamentals of Computation Theory, Wroclaw, Poland, 2009, vol. 5699, pp. 3–13.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). Alternating weighted automata (Vol. 5699, pp. 3–13). Presented at the FCT: Fundamentals of Computation Theory, Wroclaw, Poland: Springer. <a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">https://doi.org/10.1007/978-3-642-03409-1_2</a>","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 3–13.","mla":"Chatterjee, Krishnendu, et al. <i>Alternating Weighted Automata</i>. Vol. 5699, Springer, 2009, pp. 3–13, doi:<a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">10.1007/978-3-642-03409-1_2</a>.","ama":"Chatterjee K, Doyen L, Henzinger TA. Alternating weighted automata. In: Vol 5699. Springer; 2009:3-13. doi:<a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">10.1007/978-3-642-03409-1_2</a>","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Alternating weighted automata. FCT: Fundamentals of Computation Theory, LNCS, vol. 5699, 3–13.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Alternating Weighted Automata,” 5699:3–13. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">https://doi.org/10.1007/978-3-642-03409-1_2</a>."},"file":[{"access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:15:09Z","file_size":164428,"creator":"system","file_id":"5126","relation":"main_file","checksum":"e8f53abb63579de3f2bff58b2a1188e2","file_name":"IST-2012-39-v1+1_Alternating_Weighted_Automata.pdf","date_updated":"2020-07-14T12:46:31Z"}],"date_updated":"2021-01-12T07:59:34Z","conference":{"name":"FCT: Fundamentals of Computation Theory","location":"Wroclaw, Poland","start_date":"2009-09-02","end_date":"2009-09-04"},"date_published":"2009-09-10T00:00:00Z","date_created":"2018-12-11T12:09:23Z","month":"09","has_accepted_license":"1","volume":5699,"quality_controlled":"1","page":"3 - 13","publisher":"Springer","intvolume":"      5699","oa":1,"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"title":"Alternating weighted automata","status":"public"},{"title":"Stochastic games with finitary objectives","status":"public","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Horn","first_name":"Florian","full_name":"Horn, Florian","id":"37327ACE-F248-11E8-B48F-1D18A9856A87"}],"page":"34 - 54","quality_controlled":"1","publisher":"Springer","intvolume":"      5734","volume":5734,"date_published":"2009-08-01T00:00:00Z","date_created":"2018-12-11T12:09:24Z","month":"08","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","location":"High Tatras, Slovakia","start_date":"2009-08-24","end_date":"2009-08-28"},"citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Horn, F. (2009). Stochastic games with finitary objectives (Vol. 5734, pp. 34–54). Presented at the MFCS: Mathematical Foundations of Computer Science, High Tatras, Slovakia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">https://doi.org/10.1007/978-3-642-03816-7_4</a>","short":"K. Chatterjee, T.A. Henzinger, F. Horn, in:, Springer, 2009, pp. 34–54.","ieee":"K. Chatterjee, T. A. Henzinger, and F. Horn, “Stochastic games with finitary objectives,” presented at the MFCS: Mathematical Foundations of Computer Science, High Tatras, Slovakia, 2009, vol. 5734, pp. 34–54.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “Stochastic Games with Finitary Objectives,” 5734:34–54. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">https://doi.org/10.1007/978-3-642-03816-7_4</a>.","ista":"Chatterjee K, Henzinger TA, Horn F. 2009. Stochastic games with finitary objectives. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 5734, 34–54.","ama":"Chatterjee K, Henzinger TA, Horn F. Stochastic games with finitary objectives. In: Vol 5734. Springer; 2009:34-54. doi:<a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">10.1007/978-3-642-03816-7_4</a>","mla":"Chatterjee, Krishnendu, et al. <i>Stochastic Games with Finitary Objectives</i>. Vol. 5734, Springer, 2009, pp. 34–54, doi:<a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">10.1007/978-3-642-03816-7_4</a>."},"day":"01","date_updated":"2021-01-12T07:59:35Z","abstract":[{"text":"The synthesis of a reactive system with respect to all omega-regular specification requires the solution of a graph game. Such games have been extended in two natural ways. First, a game graph can be equipped with probabilistic choices between alternative transitions, thus allowing the, modeling of uncertain behaviour. These are called stochastic games. Second, a liveness specification can he strengthened to require satisfaction within all unknown but bounded amount of time. These are called finitary objectives. We study. for the first time, the, combination of Stochastic games and finitary objectives. We characterize the requirements on optimal strategies and provide algorithms for Computing the maximal achievable probability of winning stochastic games with finitary parity or Street, objectives. Most notably the set of state's from which a player can win with probability . for a finitary parity objective can he computed in polynomial time even though no polynomial-time algorithm is known in the nonfinitary case.","lang":"eng"}],"ec_funded":1,"acknowledgement":"This research was supported in part by the Swiss National Science Foundation under the Indo-Swiss Joint Research Programme, by the European Network of Excellence on Embedded Systems Design (ArtistDesign), and by the European project Combest.","alternative_title":["LNCS"],"_id":"4543","language":[{"iso":"eng"}],"publication_status":"published","project":[{"grant_number":"215543","call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","call_identifier":"FP7","name":"Design for Embedded Systems"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"publist_id":"178","doi":"10.1007/978-3-642-03816-7_4","oa_version":"None","year":"2009","type":"conference","scopus_import":1}]