[{"conference":{"name":"CAV: Computer Aided Verification"},"title":"Intra-module Inference","page":"493 - 508","day":"01","date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:08:32Z","status":"public","date_updated":"2021-01-12T07:56:30Z","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>.","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>","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>","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>.","ista":"Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module Inference. CAV: Computer Aided Verification, LNCS 5643, , 493–508."},"type":"conference","month":"01","year":"2009","alternative_title":["LNCS 5643"],"publisher":"Springer","doi":"1555","publist_id":"1082","publication_status":"published","author":[{"first_name":"Shuvendu","last_name":"Lahiri","full_name":"Lahiri,Shuvendu K."},{"full_name":"Qadeer,Shaz","last_name":"Qadeer","first_name":"Shaz"},{"last_name":"Galeotti","first_name":"Juan","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"}],"quality_controlled":0,"_id":"4375","extern":1},{"_id":"4376","quality_controlled":0,"extern":1,"publication_status":"published","author":[{"first_name":"Roberto","last_name":"Lublinerman","full_name":"Lublinerman,Roberto"},{"last_name":"Chaudhuri","first_name":"Swarat","full_name":"Chaudhuri,Swarat"},{"full_name":"Pavol Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","last_name":"Cerny"}],"publisher":"ACM","publist_id":"1083","doi":"1546","month":"01","type":"conference","year":"2009","citation":{"ista":"Lublinerman R, Chaudhuri S, Cerny P. 2009. Parallel programming with object assemblies. Oopsla Object Oriented Programming Systems Languages and Applications, 61–80.","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>.","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>","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>","short":"R. Lublinerman, S. Chaudhuri, P. Cerny, in:, ACM, 2009, pp. 61–80.","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>.","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."},"date_created":"2018-12-11T12:08:32Z","date_published":"2009-01-01T00:00:00Z","date_updated":"2021-01-12T07:56:30Z","status":"public","page":"61 - 80","title":"Parallel programming with object assemblies","conference":{"name":"Oopsla Object Oriented Programming Systems Languages and Applications"},"day":"01"},{"publist_id":"1079","doi":"1557","publisher":"Springer","alternative_title":["LNCS 5850"],"publication_status":"published","author":[{"last_name":"Hoenicke","first_name":"Jochen","full_name":"Hoenicke,Jochen"},{"first_name":"K Rustan","last_name":"Leino","full_name":"Leino, K Rustan"},{"full_name":"Podelski,Andreas","first_name":"Andreas","last_name":"Podelski"},{"last_name":"Schäf","first_name":"Martin","full_name":"Schäf,Martin"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Wies","last_name":"Wies","first_name":"Thomas"}],"extern":1,"_id":"4377","quality_controlled":0,"day":"01","page":"338 - 353","title":"It's Doomed; We Can Prove It","conference":{"name":"FM: Formal Methods"},"status":"public","date_updated":"2021-01-12T07:56:31Z","date_created":"2018-12-11T12:08:32Z","date_published":"2009-01-01T00:00:00Z","citation":{"short":"J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Springer, 2009, pp. 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.","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>.","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>","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>","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>.","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."},"year":"2009","month":"01","type":"conference"},{"publication_status":"published","oa":1,"author":[{"last_name":"Guerraoui","first_name":"Rachid","full_name":"Guerraoui, Rachid"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Vasu","last_name":"Singh","full_name":"Vasu Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer","file":[{"relation":"main_file","file_size":265763,"date_created":"2018-12-12T10:14:50Z","access_level":"open_access","file_name":"IST-2012-45-v1+1_Software_transactional_memory_on_relaxed_memory_models.pdf","file_id":"5105","date_updated":"2020-07-14T12:46:28Z","checksum":"df3c3e6306afd3f630a9146f91642f0a","creator":"system","content_type":"application/pdf"}],"alternative_title":["LNCS"],"publist_id":"1074","doi":"10.1007/978-3-642-02658-4_26","quality_controlled":0,"_id":"4383","acknowledgement":"This research was supported by the Swiss National Science Foundation.","file_date_updated":"2020-07-14T12:46:28Z","extern":1,"intvolume":"      5643","date_created":"2018-12-11T12:08:34Z","date_published":"2009-06-19T00:00:00Z","date_updated":"2021-01-12T07:56:34Z","status":"public","page":"321 - 336","conference":{"name":"CAV: Computer Aided Verification"},"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"}],"day":"19","month":"06","type":"conference","year":"2009","volume":5643,"pubrep_id":"45","citation":{"short":"R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2009, pp. 321–336.","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>.","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.","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>","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>","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>.","ista":"Guerraoui R, Henzinger TA, Singh V. 2009. Software transactional memory on relaxed memory models. CAV: Computer Aided Verification, LNCS, vol. 5643, 321–336."}},{"author":[{"last_name":"Dragojevic","first_name":"Aleksandar","full_name":"Dragojevic,Aleksandar"},{"first_name":"Rachid","last_name":"Guerraoui","full_name":"Guerraoui, Rachid"},{"full_name":"Singh, Anmol V","last_name":"Singh","first_name":"Anmol"},{"last_name":"Singh","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Vasu Singh"}],"publication_status":"published","doi":"1533","publist_id":"1070","publisher":"ACM","extern":1,"quality_controlled":0,"_id":"4385","status":"public","date_updated":"2021-01-12T07:56:34Z","date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:08:35Z","day":"01","conference":{"name":"POPL: Principles of Programming Languages"},"title":"Preventing versus curing: avoiding conflicts in transactional memories","page":"7 - 16","year":"2009","type":"conference","month":"01","citation":{"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>","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>","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.","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>.","short":"A. Dragojevic, R. Guerraoui, A. Singh, V. Singh, in:, ACM, 2009, pp. 7–16.","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.","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>."}},{"author":[{"full_name":"Pavol Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","last_name":"Cerny"},{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"}],"publication_status":"published","alternative_title":["LNCS"],"publisher":"Springer","doi":"1548","publist_id":"1067","quality_controlled":0,"_id":"4391","extern":1,"date_published":"2009-07-01T00:00:00Z","date_created":"2018-12-11T12:08:36Z","date_updated":"2021-01-12T07:56:37Z","status":"public","title":"Automated Analysis of Java Methods for Confidentiality","conference":{"name":"CAV: Computer Aided Verification"},"page":"173 - 187","day":"01","type":"conference","month":"07","year":"2009","citation":{"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>","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>","ieee":"P. Cerny and R. Alur, “Automated Analysis of Java Methods for Confidentiality,” presented at the CAV: Computer Aided Verification, 2009, pp. 173–187.","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>.","short":"P. Cerny, R. Alur, in:, Springer, 2009, pp. 173–187.","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>."}},{"intvolume":"      5771","extern":"1","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"4403","quality_controlled":"1","oa":1,"author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Weinstein, Scott","first_name":"Scott","last_name":"Weinstein"}],"publication_status":"published","doi":"10.1007/978-3-642-04027-6_9","publist_id":"1056","alternative_title":["LNCS"],"publisher":"Springer","volume":5771,"year":"2009","type":"conference","month":"09","language":[{"iso":"eng"}],"oa_version":"Submitted Version","citation":{"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>","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>","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.","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>.","short":"R. Alur, P. Cerny, S. Weinstein, in:, Springer, 2009, pp. 86–101.","ista":"Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101.","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>."},"date_updated":"2023-02-23T11:06:20Z","status":"public","main_file_link":[{"url":"http://repository.upenn.edu/cis_reports/894/","open_access":"1"}],"date_published":"2009-09-01T00:00:00Z","date_created":"2018-12-11T12:08:40Z","day":"01","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"}],"conference":{"start_date":"2009-09-07","location":"Coimbra, Portugal","name":"CSL: Computer Science Logic","end_date":"2009-09-11"},"title":"Algorithmic analysis of array-accessing programs","related_material":{"record":[{"relation":"later_version","id":"2967","status":"public"}]},"page":"86 - 101"},{"oa":1,"publication_status":"published","author":[{"full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"id":"3B43276C-F248-11E8-B48F-1D18A9856A87","full_name":"Maria Mateescu","last_name":"Mateescu","first_name":"Maria"},{"last_name":"Wolf","first_name":"Verena","full_name":"Wolf, Verena"}],"alternative_title":["LNCS"],"file":[{"content_type":"application/pdf","creator":"system","checksum":"36b974111521ea534aae294166e93a63","date_updated":"2020-07-14T12:46:30Z","file_id":"4938","date_created":"2018-12-12T10:12:20Z","file_name":"IST-2012-40-v1+1_Sliding-window_abstraction_for_infinite_markov_chains.pdf","access_level":"open_access","file_size":804295,"relation":"main_file"}],"publisher":"Springer","doi":"10.1007/978-3-642-02658-4_27","publist_id":"278","acknowledgement":"The research has been partially funded by the Swiss National Science Foundation under grant 205321-111840.","file_date_updated":"2020-07-14T12:46:30Z","_id":"4453","quality_controlled":0,"intvolume":"      5643","extern":1,"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/sliding-window_abstraction_for_infinite_markov_chains.pdf","open_access":"0"}],"date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:08:55Z","date_updated":"2021-01-12T07:57:04Z","status":"public","conference":{"name":"CAV: Computer Aided Verification"},"title":"Sliding-window abstraction for infinite Markov chains","page":"337 - 352","day":"01","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"}],"type":"conference","month":"01","pubrep_id":"40","volume":5643,"year":"2009","citation":{"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>.","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.","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>","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>","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>.","ista":"Henzinger TA, Mateescu M, Wolf V. 2009. Sliding-window abstraction for infinite Markov chains. CAV: Computer Aided Verification, LNCS, vol. 5643, 337–352."}},{"citation":{"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.","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>.","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>","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>","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.","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>.","short":"F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 173–188."},"type":"conference","month":"08","volume":5688,"year":"2009","conference":{"name":"CMSB: Computational Methods in Systems Biology"},"title":"Approximation of event probabilities in noisy cellular processes","related_material":{"record":[{"status":"public","id":"3364","relation":"later_version"}]},"page":"173 - 188","day":"17","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."}],"date_published":"2009-08-17T00:00:00Z","date_created":"2018-12-11T12:09:21Z","date_updated":"2023-02-23T11:24:03Z","status":"public","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.","quality_controlled":0,"_id":"4535","intvolume":"      5688","extern":1,"alternative_title":["LNCS"],"publisher":"Springer","doi":"10.1007/978-3-642-03845-7_12","publist_id":"189","author":[{"full_name":"Didier, Frédéric","first_name":"Frédéric","last_name":"Didier"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"last_name":"Mateescu","first_name":"Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","full_name":"Maria Mateescu"},{"full_name":"Wolf, Verena","last_name":"Wolf","first_name":"Verena"}],"publication_status":"published"},{"doi":"10.1109/LICS.2009.16","publist_id":"181","publisher":"IEEE","publication_status":"published","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"extern":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"4540","article_processing_charge":"No","quality_controlled":"1","day":"01","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"}],"conference":{"name":"LICS: Logic in Computer Science"},"related_material":{"record":[{"status":"public","id":"3867","relation":"later_version"}]},"title":"Expressiveness and closure properties for quantitative languages","page":"199 - 208","date_updated":"2023-02-23T11:46:11Z","status":"public","date_published":"2009-01-01T00:00:00Z","date_created":"2018-12-11T12:09:23Z","language":[{"iso":"eng"}],"oa_version":"None","citation":{"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>.","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>","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>","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>.","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.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, IEEE, 2009, pp. 199–208."},"scopus_import":"1","pubrep_id":"55","year":"2009","type":"conference","month":"01"},{"oa_version":"Submitted Version","citation":{"short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 3–13.","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.","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>","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>","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>.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Alternating weighted automata. FCT: Fundamentals of Computation Theory, LNCS, vol. 5699, 3–13."},"type":"conference","scopus_import":1,"volume":5699,"year":"2009","title":"Alternating weighted automata","abstract":[{"lang":"eng","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."}],"date_published":"2009-09-10T00:00:00Z","ddc":["004"],"date_updated":"2021-01-12T07:59:34Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"4542","project":[{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","name":"Design for Embedded Systems","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"}],"ec_funded":1,"alternative_title":["LNCS"],"publisher":"Springer","doi":"10.1007/978-3-642-03409-1_2","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"month":"09","pubrep_id":"39","conference":{"start_date":"2009-09-02","location":"Wroclaw, Poland","name":"FCT: Fundamentals of Computation Theory","end_date":"2009-09-04"},"page":"3 - 13","day":"10","date_created":"2018-12-11T12:09:23Z","status":"public","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.","file_date_updated":"2020-07-14T12:46:31Z","quality_controlled":"1","intvolume":"      5699","file":[{"file_name":"IST-2012-39-v1+1_Alternating_Weighted_Automata.pdf","access_level":"open_access","date_created":"2018-12-12T10:15:09Z","file_size":164428,"checksum":"e8f53abb63579de3f2bff58b2a1188e2","date_updated":"2020-07-14T12:46:31Z","file_id":"5126","content_type":"application/pdf","creator":"system","relation":"main_file"}],"has_accepted_license":"1","publist_id":"180","oa":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.","quality_controlled":"1","intvolume":"      5734","publist_id":"178","language":[{"iso":"eng"}],"month":"08","conference":{"end_date":"2009-08-28","name":"MFCS: Mathematical Foundations of Computer Science","location":"High Tatras, Slovakia","start_date":"2009-08-24"},"page":"34 - 54","day":"01","date_created":"2018-12-11T12:09:24Z","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"4543","project":[{"name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","grant_number":"214373","call_identifier":"FP7"}],"alternative_title":["LNCS"],"ec_funded":1,"publisher":"Springer","doi":"10.1007/978-3-642-03816-7_4","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"id":"37327ACE-F248-11E8-B48F-1D18A9856A87","full_name":"Horn, Florian","last_name":"Horn","first_name":"Florian"}],"publication_status":"published","department":[{"_id":"KrCh"}],"oa_version":"None","citation":{"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.","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>.","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>","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>","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."},"type":"conference","scopus_import":1,"year":"2009","volume":5734,"title":"Stochastic games with finitary objectives","abstract":[{"lang":"eng","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."}],"date_published":"2009-08-01T00:00:00Z","date_updated":"2021-01-12T07:59:35Z"},{"page":"197 - 206","conference":{"name":"SODA: Symposium on Discrete Algorithms"},"title":"Termination criteria for solving concurrent safety and reachability games","abstract":[{"lang":"eng","text":"We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. We present in this paper a strategy improvement algorithm for computing the value of a concurrent safety game, that is, the maximal probability with which player 1 can enforce the safety objective. The algorithm yields a sequence of player-1 strategies which ensure probabilities of winning that converge monotonically to the value of the safety game. Our result is significant because the strategy improvement algorithm provides, for the first time, a way to approximate the value of a concurrent safety game from below. Since a value iteration algorithm, or a strategy improvement algorithm for reachability games, can be used to approximate the same value from above, the combination of both algorithms yields a method for computing a converging sequence of upper and lower bounds for the values of concurrent reachability and safety games. Previous methods could approximate the values of these games only from one direction, and as no rates of convergence are known, they did not provide a practical way to solve these games."}],"day":"01","date_created":"2018-12-11T12:09:24Z","date_published":"2009-01-01T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://repository.ist.ac.at/id/eprint/37"}],"status":"public","date_updated":"2021-01-12T07:59:35Z","citation":{"ama":"Chatterjee K, De Alfaro L, Henzinger TA. Termination criteria for solving concurrent safety and reachability games. In: SIAM; 2009:197-206. doi:<a href=\"https://doi.org/10.1137/1.9781611973068.23\">10.1137/1.9781611973068.23</a>","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2009). Termination criteria for solving concurrent safety and reachability games (pp. 197–206). Presented at the SODA: Symposium on Discrete Algorithms, SIAM. <a href=\"https://doi.org/10.1137/1.9781611973068.23\">https://doi.org/10.1137/1.9781611973068.23</a>","mla":"Chatterjee, Krishnendu, et al. <i>Termination Criteria for Solving Concurrent Safety and Reachability Games</i>. SIAM, 2009, pp. 197–206, doi:<a href=\"https://doi.org/10.1137/1.9781611973068.23\">10.1137/1.9781611973068.23</a>.","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Termination criteria for solving concurrent safety and reachability games,” presented at the SODA: Symposium on Discrete Algorithms, 2009, pp. 197–206.","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, SIAM, 2009, pp. 197–206.","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2009. Termination criteria for solving concurrent safety and reachability games. SODA: Symposium on Discrete Algorithms, 197–206.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Termination Criteria for Solving Concurrent Safety and Reachability Games,” 197–206. SIAM, 2009. <a href=\"https://doi.org/10.1137/1.9781611973068.23\">https://doi.org/10.1137/1.9781611973068.23</a>."},"month":"01","type":"conference","year":"2009","pubrep_id":"37","publisher":"SIAM","file":[{"creator":"system","content_type":"application/pdf","file_id":"4662","date_updated":"2020-07-14T12:46:31Z","checksum":"ce7dc1667502e26b23c07a767ac41ae6","file_size":212369,"access_level":"open_access","date_created":"2018-12-12T10:08:03Z","file_name":"IST-2012-37-v1+1_Termination_criteria_for_solving_concurrent_safety_and_reachability_games.pdf","relation":"main_file"}],"publist_id":"176","doi":"10.1137/1.9781611973068.23","oa":1,"publication_status":"published","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee"},{"full_name":"de Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"}],"_id":"4544","quality_controlled":0,"file_date_updated":"2020-07-14T12:46:31Z","extern":1},{"type":"conference","volume":5556,"year":"2009","scopus_import":1,"citation":{"apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). A survey of stochastic games with limsup and liminf objectives (Vol. 5556, pp. 1–15). Presented at the ICALP: Automata, Languages and Programming, Rhodos, Greece: Springer. <a href=\"https://doi.org/10.1007/978-3-642-02930-1_1\">https://doi.org/10.1007/978-3-642-02930-1_1</a>","ama":"Chatterjee K, Doyen L, Henzinger TA. A survey of stochastic games with limsup and liminf objectives. In: Vol 5556. Springer; 2009:1-15. doi:<a href=\"https://doi.org/10.1007/978-3-642-02930-1_1\">10.1007/978-3-642-02930-1_1</a>","mla":"Chatterjee, Krishnendu, et al. <i>A Survey of Stochastic Games with Limsup and Liminf Objectives</i>. Vol. 5556, Springer, 2009, pp. 1–15, doi:<a href=\"https://doi.org/10.1007/978-3-642-02930-1_1\">10.1007/978-3-642-02930-1_1</a>.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of stochastic games with limsup and liminf objectives,” presented at the ICALP: Automata, Languages and Programming, Rhodos, Greece, 2009, vol. 5556, pp. 1–15.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 1–15.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. A survey of stochastic games with limsup and liminf objectives. ICALP: Automata, Languages and Programming, LNCS, vol. 5556, 1–15.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey of Stochastic Games with Limsup and Liminf Objectives,” 5556:1–15. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02930-1_1\">https://doi.org/10.1007/978-3-642-02930-1_1</a>."},"oa_version":"Submitted Version","ddc":["000","005"],"date_published":"2009-06-24T00:00:00Z","date_updated":"2021-01-12T07:59:35Z","title":"A survey of stochastic games with limsup and liminf objectives","abstract":[{"text":"A stochastic game is a two-player game played oil a graph, where in each state the successor is chosen either by One of the players, or according to a probability distribution. We Survey Stochastic games with limsup and liminf objectives. A real-valued re-ward is assigned to each state, and the value of all infinite path is the limsup (resp. liminf) of all rewards along the path. The value of a stochastic game is the maximal expected value of an infinite path that call he achieved by resolving the decisions of the first player. We present the complexity of computing values of Stochastic games and their subclasses, and the complexity, of optimal strategies in such games. ","lang":"eng"}],"project":[{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543"}],"_id":"4545","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"}],"publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"Springer","alternative_title":["LNCS"],"ec_funded":1,"doi":"10.1007/978-3-642-02930-1_1","month":"06","pubrep_id":"38","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:24Z","status":"public","page":"1 - 15","conference":{"location":"Rhodos, Greece","start_date":"2009-07-05","end_date":"2009-07-12","name":"ICALP: Automata, Languages and Programming"},"day":"24","quality_controlled":"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), by the European projects COMBEST, Quasimodo, Gasics, 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.","file_date_updated":"2020-07-14T12:46:31Z","intvolume":"      5556","oa":1,"file":[{"creator":"system","content_type":"application/pdf","file_size":187419,"date_created":"2018-12-12T10:13:11Z","file_name":"IST-2012-38-v1+1_A_survey_of_stochastic_games_with_limsup_and_liminf_objectives.pdf","access_level":"open_access","file_id":"4992","checksum":"dabb6d24428a000254c95493d9c492e6","date_updated":"2020-07-14T12:46:31Z","relation":"main_file"}],"publist_id":"177","has_accepted_license":"1"},{"intvolume":"      5643","acknowledgement":"This research was supported by the Swiss National Science Foundation (Indo-Swiss Research Program and NCCR MICS) and the European Union projects COMBEST and COCONUT.","quality_controlled":"1","publist_id":"141","external_id":{"arxiv":["0904.2638"]},"oa":1,"language":[{"iso":"eng"}],"month":"06","day":"19","conference":{"name":"CAV: Computer Aided Verification","end_date":"2009-07-02","location":"Grenoble, France","start_date":"2009-06-26"},"page":"140 - 156","status":"public","date_created":"2018-12-11T12:09:31Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"4569","project":[{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"}],"doi":"10.1007/978-3-642-02658-4_14","alternative_title":["LNCS"],"ec_funded":1,"arxiv":1,"publisher":"Springer","department":[{"_id":"KrCh"}],"author":[{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Jobstmann, Barbara","first_name":"Barbara","last_name":"Jobstmann"}],"publication_status":"published","oa_version":"Preprint","citation":{"ista":"Bloem R, Chatterjee K, Henzinger TA, Jobstmann B. 2009. Better quality in synthesis through quantitative objectives. CAV: Computer Aided Verification, LNCS, vol. 5643, 140–156.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara Jobstmann. “Better Quality in Synthesis through Quantitative Objectives,” 5643:140–56. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_14\">https://doi.org/10.1007/978-3-642-02658-4_14</a>.","ama":"Bloem R, Chatterjee K, Henzinger TA, Jobstmann B. Better quality in synthesis through quantitative objectives. In: Vol 5643. Springer; 2009:140-156. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_14\">10.1007/978-3-642-02658-4_14</a>","apa":"Bloem, R., Chatterjee, K., Henzinger, T. A., &#38; Jobstmann, B. (2009). Better quality in synthesis through quantitative objectives (Vol. 5643, pp. 140–156). Presented at the CAV: Computer Aided Verification, Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_14\">https://doi.org/10.1007/978-3-642-02658-4_14</a>","short":"R. Bloem, K. Chatterjee, T.A. Henzinger, B. Jobstmann, in:, Springer, 2009, pp. 140–156.","ieee":"R. Bloem, K. Chatterjee, T. A. Henzinger, and B. Jobstmann, “Better quality in synthesis through quantitative objectives,” presented at the CAV: Computer Aided Verification, Grenoble, France, 2009, vol. 5643, pp. 140–156.","mla":"Bloem, Roderick, et al. <i>Better Quality in Synthesis through Quantitative Objectives</i>. Vol. 5643, Springer, 2009, pp. 140–56, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_14\">10.1007/978-3-642-02658-4_14</a>."},"year":"2009","volume":5643,"type":"conference","abstract":[{"text":"Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another. For example, if a specification asks that every request is followed by a response, one may prefer an implementation that generates responses quickly but does not generate unnecessary responses. We use quantitative properties to measure the “goodness” of an implementation. Using games with corresponding quantitative objectives, we can synthesize “optimal” implementations, which are preferred among the set of possible implementations that satisfy a given specification.\r\nIn particular, we show how automata with lexicographic mean-payoff conditions can be used to express many interesting quantitative properties for reactive systems. In this framework, the synthesis of optimal implementations requires the solution of lexicographic mean-payoff games (for safety requirements), and the solution of games with both lexicographic mean-payoff and parity objectives (for liveness requirements). We present algorithms for solving both kinds of novel graph games.","lang":"eng"}],"title":"Better quality in synthesis through quantitative objectives","date_updated":"2021-01-12T07:59:46Z","date_published":"2009-06-19T00:00:00Z","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/0904.2638"}]},{"title":"Alpaga: A tool for solving parity games with imperfect information","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"page":"58 - 61","day":"09","abstract":[{"lang":"eng","text":"Alpaga is a solver for two-player parity games with imperfect information. Given the description of a game, it determines whether the first player can ensure to win and, if so, it constructs a winning strategy. The tool provides a symbolic implementation of a recent algorithm based on antichains."}],"main_file_link":[{"open_access":"1","url":"https://repository.ist.ac.at/35/"}],"date_published":"2009-03-09T00:00:00Z","date_created":"2018-12-11T12:09:35Z","status":"public","date_updated":"2021-01-12T07:59:52Z","citation":{"chicago":"Berwanger, Dietmar, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, and Thomas A Henzinger. “Alpaga: A Tool for Solving Parity Games with Imperfect Information,” 5505:58–61. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-00768-2_7\">https://doi.org/10.1007/978-3-642-00768-2_7</a>.","ista":"Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. 2009. Alpaga: A tool for solving parity games with imperfect information. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 5505, 58–61.","short":"D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 58–61.","ieee":"D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, and T. A. Henzinger, “Alpaga: A tool for solving parity games with imperfect information,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2009, vol. 5505, pp. 58–61.","mla":"Berwanger, Dietmar, et al. <i>Alpaga: A Tool for Solving Parity Games with Imperfect Information</i>. Vol. 5505, Springer, 2009, pp. 58–61, doi:<a href=\"https://doi.org/10.1007/978-3-642-00768-2_7\">10.1007/978-3-642-00768-2_7</a>.","ama":"Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. Alpaga: A tool for solving parity games with imperfect information. In: Vol 5505. Springer; 2009:58-61. doi:<a href=\"https://doi.org/10.1007/978-3-642-00768-2_7\">10.1007/978-3-642-00768-2_7</a>","apa":"Berwanger, D., Chatterjee, K., De Wulf, M., Doyen, L., &#38; Henzinger, T. A. (2009). Alpaga: A tool for solving parity games with imperfect information (Vol. 5505, pp. 58–61). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. <a href=\"https://doi.org/10.1007/978-3-642-00768-2_7\">https://doi.org/10.1007/978-3-642-00768-2_7</a>"},"type":"conference","month":"03","year":"2009","volume":5505,"pubrep_id":"35","file":[{"file_id":"5168","checksum":"d52b55a10a47b3e3b0e016ea9bf85c41","date_updated":"2020-07-14T12:46:32Z","file_size":212180,"access_level":"open_access","file_name":"IST-2012-35-v1+1_Alpaga_-_A_tool_for_solving_parity_games_with_imperfect_information.pdf","date_created":"2018-12-12T10:15:45Z","creator":"system","content_type":"application/pdf","relation":"main_file"}],"alternative_title":["LNCS"],"publisher":"Springer","doi":"10.1007/978-3-642-00768-2_7","publist_id":"127","author":[{"full_name":"Berwanger, Dietmar","last_name":"Berwanger","first_name":"Dietmar"},{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"De Wulf","first_name":"Martin","full_name":"De Wulf, Martin"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"}],"publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:46:32Z","_id":"4580","quality_controlled":0,"intvolume":"      5505","extern":1},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"12656","extern":"1","publisher":"Wiley","doi":"10.1002/hyp.7085","publication_status":"published","author":[{"last_name":"Pellicciotti","first_name":"Francesca","id":"b28f055a-81ea-11ed-b70c-a9fe7f7b0e70","full_name":"Pellicciotti, Francesca"},{"full_name":"Helbing, Jakob","last_name":"Helbing","first_name":"Jakob"},{"full_name":"Rivera, Andrés","last_name":"Rivera","first_name":"Andrés"},{"full_name":"Favier, Vincent","first_name":"Vincent","last_name":"Favier"},{"full_name":"Corripio, Javier","last_name":"Corripio","first_name":"Javier"},{"full_name":"Araos, José","last_name":"Araos","first_name":"José"},{"last_name":"Sicart","first_name":"Jean-Emmanuel","full_name":"Sicart, Jean-Emmanuel"},{"full_name":"Carenzo, Marco","last_name":"Carenzo","first_name":"Marco"}],"oa_version":"None","citation":{"mla":"Pellicciotti, Francesca, et al. “A Study of the Energy Balance and Melt Regime on Juncal Norte Glacier, Semi-Arid Andes of Central Chile, Using Melt Models of Different Complexity.” <i>Hydrological Processes</i>, vol. 22, no. 19, Wiley, 2008, pp. 3980–97, doi:<a href=\"https://doi.org/10.1002/hyp.7085\">10.1002/hyp.7085</a>.","ieee":"F. Pellicciotti <i>et al.</i>, “A study of the energy balance and melt regime on Juncal Norte Glacier, semi-arid Andes of central Chile, using melt models of different complexity,” <i>Hydrological Processes</i>, vol. 22, no. 19. Wiley, pp. 3980–3997, 2008.","short":"F. Pellicciotti, J. Helbing, A. Rivera, V. Favier, J. Corripio, J. Araos, J.-E. Sicart, M. Carenzo, Hydrological Processes 22 (2008) 3980–3997.","apa":"Pellicciotti, F., Helbing, J., Rivera, A., Favier, V., Corripio, J., Araos, J., … Carenzo, M. (2008). A study of the energy balance and melt regime on Juncal Norte Glacier, semi-arid Andes of central Chile, using melt models of different complexity. <i>Hydrological Processes</i>. Wiley. <a href=\"https://doi.org/10.1002/hyp.7085\">https://doi.org/10.1002/hyp.7085</a>","ama":"Pellicciotti F, Helbing J, Rivera A, et al. A study of the energy balance and melt regime on Juncal Norte Glacier, semi-arid Andes of central Chile, using melt models of different complexity. <i>Hydrological Processes</i>. 2008;22(19):3980-3997. doi:<a href=\"https://doi.org/10.1002/hyp.7085\">10.1002/hyp.7085</a>","chicago":"Pellicciotti, Francesca, Jakob Helbing, Andrés Rivera, Vincent Favier, Javier Corripio, José Araos, Jean-Emmanuel Sicart, and Marco Carenzo. “A Study of the Energy Balance and Melt Regime on Juncal Norte Glacier, Semi-Arid Andes of Central Chile, Using Melt Models of Different Complexity.” <i>Hydrological Processes</i>. Wiley, 2008. <a href=\"https://doi.org/10.1002/hyp.7085\">https://doi.org/10.1002/hyp.7085</a>.","ista":"Pellicciotti F, Helbing J, Rivera A, Favier V, Corripio J, Araos J, Sicart J-E, Carenzo M. 2008. A study of the energy balance and melt regime on Juncal Norte Glacier, semi-arid Andes of central Chile, using melt models of different complexity. Hydrological Processes. 22(19), 3980–3997."},"keyword":["Water Science and Technology"],"type":"journal_article","publication_identifier":{"eissn":["1099-1085"],"issn":["0885-6087"]},"scopus_import":"1","year":"2008","volume":22,"title":"A study of the energy balance and melt regime on Juncal Norte Glacier, semi-arid Andes of central Chile, using melt models of different complexity","abstract":[{"lang":"eng","text":"We use meteorological data from two automatic weather stations (AWS) on Juncal Norte Glacier, central Chile, to investigate the glacier–climate interaction and to test ablation models of different complexity. The semi-arid Central Andes are characterized by dry summers, with precipitation close to zero, low relative humidity and intense solar radiation. We show that katabatic forcing is dominant both on the glacier tongue and in the fore field, and that low humidity and absence of clouds cause strong radiative cooling of the glacier surface. Surface albedo is basically constant for snow and ice, because of the scarcity of solid precipitation. The energy balance of the glacier is simulated for a 2-month period in austral summer using two models of different complexity, which differ in the inclusion of the heat conduction flux into the snowpack and in the parameterization of the incoming longwave radiation. Net shortwave radiation is the dominant component of the energy balance. The sensible heat flux is always positive, while both the net longwave radiation and latent heat flux are negative. Neglecting the subsurface heat flux and corresponding variations in surface temperature leads to an overestimation of ablation of 2% over a total of 3695 mm water equivalent (w.e.) at the end of the season. Correct modelling of incoming longwave radiation is crucial, and we suggest that parameterizations based on vapour pressure and air temperature should be used rather than on computed cloud amount. We also used an enhanced temperature-index model incorporating the shortwave radiation flux, which has two empirical parameters. We apply it both with values of parameters obtained for Alpine glaciers and recalibrated on Juncal Norte. The model recalibrated against the correct energy balance simulations performs very well. The model parameters respond to the meteorological conditions typical of this climatic setting."}],"date_published":"2008-09-15T00:00:00Z","issue":"19","date_updated":"2023-02-20T08:48:33Z","quality_controlled":"1","article_processing_charge":"No","intvolume":"        22","language":[{"iso":"eng"}],"month":"09","article_type":"original","publication":"Hydrological Processes","page":"3980-3997","day":"15","date_created":"2023-02-20T08:18:45Z","status":"public"},{"issue":"5","date_created":"2018-12-11T11:51:13Z","date_published":"2008-03-11T00:00:00Z","status":"public","date_updated":"2021-01-12T06:49:42Z","page":"368 - 374","publication":"Current Biology","title":"Response properties of motion sensitive visual interneurons in the Lobula plate of Drosophila melanogaster","abstract":[{"lang":"eng","text":"The crystalline-like structure of the optic lobes of the fruit fly Drosophila melanogaster has made them a model system for the study of neuronal cell-fate determination, axonal path finding, and target selection. For functional studies, however, the small size of the constituting visual interneurons has so far presented a formidable barrier. We have overcome this problem by establishing in vivo whole-cell recordings [1] from genetically targeted visual interneurons of Drosophila. Here, we describe the response properties of six motion-sensitive large-field neurons in the lobula plate that form a network consisting of individually identifiable, directionally selective cells most sensitive to vertical image motion (VS cells [2, 3]). Individual VS cell responses to visual motion stimuli exhibit all the characteristics that are indicative of presynaptic input from elementary motion detectors of the correlation type [4, 5]. Different VS cells possess distinct receptive fields that are arranged sequentially along the eye's azimuth, corresponding to their characteristic cellular morphology and position within the retinotopically organized lobula plate. In addition, lateral connections between individual VS cells cause strongly overlapping receptive fields that are wider than expected from their dendritic input. Our results suggest that motion vision in different dipteran fly species is accomplished in similar circuitries and according to common algorithmic rules. The underlying neural mechanisms of population coding within the VS cell network and of elementary motion detection, respectively, can now be analyzed by the combination of electrophysiology and genetic intervention in Drosophila."}],"day":"11","month":"03","type":"journal_article","year":"2008","volume":18,"citation":{"ama":"Jösch MA, Plett J, Borst A, Reiff D. Response properties of motion sensitive visual interneurons in the Lobula plate of Drosophila melanogaster. <i>Current Biology</i>. 2008;18(5):368-374. doi:<a href=\"https://doi.org/10.1016/j.cub.2008.02.022\">10.1016/j.cub.2008.02.022</a>","apa":"Jösch, M. A., Plett, J., Borst, A., &#38; Reiff, D. (2008). Response properties of motion sensitive visual interneurons in the Lobula plate of Drosophila melanogaster. <i>Current Biology</i>. Cell Press. <a href=\"https://doi.org/10.1016/j.cub.2008.02.022\">https://doi.org/10.1016/j.cub.2008.02.022</a>","ieee":"M. A. Jösch, J. Plett, A. Borst, and D. Reiff, “Response properties of motion sensitive visual interneurons in the Lobula plate of Drosophila melanogaster,” <i>Current Biology</i>, vol. 18, no. 5. Cell Press, pp. 368–374, 2008.","mla":"Jösch, Maximilian A., et al. “Response Properties of Motion Sensitive Visual Interneurons in the Lobula Plate of Drosophila Melanogaster.” <i>Current Biology</i>, vol. 18, no. 5, Cell Press, 2008, pp. 368–74, doi:<a href=\"https://doi.org/10.1016/j.cub.2008.02.022\">10.1016/j.cub.2008.02.022</a>.","short":"M.A. Jösch, J. Plett, A. Borst, D. Reiff, Current Biology 18 (2008) 368–374.","ista":"Jösch MA, Plett J, Borst A, Reiff D. 2008. Response properties of motion sensitive visual interneurons in the Lobula plate of Drosophila melanogaster. Current Biology. 18(5), 368–374.","chicago":"Jösch, Maximilian A, Johannes Plett, Alexander Borst, and Dierk Reiff. “Response Properties of Motion Sensitive Visual Interneurons in the Lobula Plate of Drosophila Melanogaster.” <i>Current Biology</i>. Cell Press, 2008. <a href=\"https://doi.org/10.1016/j.cub.2008.02.022\">https://doi.org/10.1016/j.cub.2008.02.022</a>."},"publication_status":"published","author":[{"full_name":"Maximilian Jösch","orcid":"0000-0002-3937-1330","id":"2BD278E6-F248-11E8-B48F-1D18A9856A87","first_name":"Maximilian A","last_name":"Jösch"},{"first_name":"Johannes","last_name":"Plett","full_name":"Plett, Johannes"},{"full_name":"Borst, Alexander","last_name":"Borst","first_name":"Alexander"},{"full_name":"Reiff, Dierk F","last_name":"Reiff","first_name":"Dierk"}],"publisher":"Cell Press","publist_id":"5973","doi":"10.1016/j.cub.2008.02.022","quality_controlled":0,"_id":"1296","acknowledgement":"This work was supported by the Max-Planck-Society and by a Human Frontier Science Program (HFSP) grant to K. Ito, A.B., and B. Nelson.","extern":1,"intvolume":"        18"},{"month":"11","type":"journal_article","year":"2008","volume":4,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"},"citation":{"ista":"Schmidt S, Gerasimova A, Kondrashov F, Adzuhbei I, Kondrashov A, Sunyaev S. 2008. Hypermutable non-synonymous sites are under stronger negative selection. PLoS Genetics. 4(11).","chicago":"Schmidt, Steffen, Anna Gerasimova, Fyodor Kondrashov, Ivan Adzuhbei, Alexey Kondrashov, and Shamil Sunyaev. “Hypermutable Non-Synonymous Sites Are under Stronger Negative Selection.” <i>PLoS Genetics</i>. Public Library of Science, 2008. <a href=\"https://doi.org/10.1371/journal.pgen.1000281\">https://doi.org/10.1371/journal.pgen.1000281</a>.","ama":"Schmidt S, Gerasimova A, Kondrashov F, Adzuhbei I, Kondrashov A, Sunyaev S. Hypermutable non-synonymous sites are under stronger negative selection. <i>PLoS Genetics</i>. 2008;4(11). doi:<a href=\"https://doi.org/10.1371/journal.pgen.1000281\">10.1371/journal.pgen.1000281</a>","apa":"Schmidt, S., Gerasimova, A., Kondrashov, F., Adzuhbei, I., Kondrashov, A., &#38; Sunyaev, S. (2008). Hypermutable non-synonymous sites are under stronger negative selection. <i>PLoS Genetics</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pgen.1000281\">https://doi.org/10.1371/journal.pgen.1000281</a>","ieee":"S. Schmidt, A. Gerasimova, F. Kondrashov, I. Adzuhbei, A. Kondrashov, and S. Sunyaev, “Hypermutable non-synonymous sites are under stronger negative selection,” <i>PLoS Genetics</i>, vol. 4, no. 11. Public Library of Science, 2008.","mla":"Schmidt, Steffen, et al. “Hypermutable Non-Synonymous Sites Are under Stronger Negative Selection.” <i>PLoS Genetics</i>, vol. 4, no. 11, Public Library of Science, 2008, doi:<a href=\"https://doi.org/10.1371/journal.pgen.1000281\">10.1371/journal.pgen.1000281</a>.","short":"S. Schmidt, A. Gerasimova, F. Kondrashov, I. Adzuhbei, A. Kondrashov, S. Sunyaev, PLoS Genetics 4 (2008)."},"date_created":"2018-12-11T11:48:48Z","issue":"11","date_published":"2008-11-01T00:00:00Z","date_updated":"2021-01-12T08:19:16Z","status":"public","license":"https://creativecommons.org/licenses/by/4.0/","title":"Hypermutable non-synonymous sites are under stronger negative selection","publication":"PLoS Genetics","abstract":[{"lang":"eng","text":"Mutation rate varies greatly between nucleotide sites of the human genome and depends both on the global genomic location and the local sequence context of a site. In particular, CpG context elevates the mutation rate by an order of magnitude. Mutations also vary widely in their effect on the molecular function, phenotype, and fitness. Independence of the probability of occurrence of a new mutation's effect has been a fundamental premise in genetics. However, highly mutable contexts may be preserved by negative selection at important sites but destroyed by mutation at sites under no selection. Thus, there may be a positive correlation between the rate of mutations at a nucleotide site and the magnitude of their effect on fitness. We studied the impact of CpG context on the rate of human-chimpanzee divergence and on intrahuman nucleotide diversity at non-synonymous coding sites. We compared nucleotides that occupy identical positions within codons of identical amino acids and only differ by being within versus outside CpG context. Nucleotides within CpG context are under a stronger negative selection, as revealed by their lower, proportionally to the mutation rate, rate of evolution and nucleotide diversity. In particular, the probability of fixation of a non-synonymous transition at a CpG site is two times lower than at a CpG site. Thus, sites with different mutation rates are not necessarily selectively equivalent. This suggests that the mutation rate may complement sequence conservation as a characteristic predictive of functional importance of nucleotide sites."}],"day":"01","_id":"844","quality_controlled":0,"acknowledgement":"This work was supported in part by NIH grants R01 GM078598 and U54 LM008748.","extern":1,"intvolume":"         4","publication_status":"published","author":[{"full_name":"Schmidt, Steffen","first_name":"Steffen","last_name":"Schmidt"},{"full_name":"Gerasimova, Anna","last_name":"Gerasimova","first_name":"Anna"},{"first_name":"Fyodor","last_name":"Kondrashov","full_name":"Fyodor Kondrashov","orcid":"0000-0001-8243-4694","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Adzuhbei, Ivan A","last_name":"Adzuhbei","first_name":"Ivan"},{"full_name":"Kondrashov, Alexey S","first_name":"Alexey","last_name":"Kondrashov"},{"full_name":"Sunyaev, Shamil R","last_name":"Sunyaev","first_name":"Shamil"}],"publisher":"Public Library of Science","publist_id":"6800","doi":"10.1371/journal.pgen.1000281"},{"author":[{"first_name":"Paul","last_name":"Schanda","orcid":"0000-0002-9350-7606","full_name":"Schanda, Paul","id":"7B541462-FAF6-11E9-A490-E8DFE5697425"},{"last_name":"Brutscher","first_name":"Bernhard","full_name":"Brutscher, Bernhard"},{"last_name":"Konrat","first_name":"Robert","full_name":"Konrat, Robert"},{"full_name":"Tollinger, Martin","first_name":"Martin","last_name":"Tollinger"}],"publication_status":"published","publisher":"Elsevier","doi":"10.1016/j.jmb.2008.05.040","_id":"8480","article_processing_charge":"No","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","extern":"1","intvolume":"       380","issue":"4","date_created":"2020-09-18T10:12:29Z","date_published":"2008-07-18T00:00:00Z","status":"public","date_updated":"2021-01-12T08:19:34Z","page":"726-741","title":"Folding of the KIX domain: Characterization of the equilibrium analog of a folding intermediate using 15N/13C relaxation dispersion and fast 1H/2H amide exchange NMR spectroscopy","publication":"Journal of Molecular Biology","abstract":[{"text":"The KIX domain of the transcription co-activator CBP is a three-helix bundle protein that folds via rapid accumulation of an intermediate state, followed by a slower folding phase. Recent NMR relaxation dispersion studies revealed the presence of a low-populated (excited) state of KIX that exists in equilibrium with the natively folded form under non-denaturing conditions, and likely represents the equilibrium analog of the folding intermediate. Here, we combine amide hydrogen/deuterium exchange measurements using rapid NMR data acquisition techniques with backbone 15N and 13C relaxation dispersion experiments to further investigate the equilibrium folding of the KIX domain. Residual structure within the folding intermediate is detected by both methods, and their combination enables reliable quantification of the amount of persistent residual structure. Three well-defined folding subunits are found, which display variable stability and correspond closely to the individual helices in the native state. While two of the three helices (α2 and α3) are partially formed in the folding intermediate (to ∼ 50% and ∼ 80%, respectively, at 20 °C), the third helix is disordered. The observed helical content within the excited state exceeds the helical propensities predicted for the corresponding peptide regions, suggesting that the two helices are weakly mutually stabilized, while methyl 13C relaxation dispersion data indicate that a defined packing arrangement is unlikely. Temperature-dependent experiments reveal that the largest enthalpy and entropy changes along the folding reaction occur during the final transition from the intermediate to the native state. Our experimental data are consistent with a folding mechanism where helices α2 and α3 form rapidly, although to different extents, while helix α1 consolidates only as folding proceeds to complete the native state-structure.","lang":"eng"}],"day":"18","month":"07","article_type":"original","publication_identifier":{"issn":["0022-2836"]},"type":"journal_article","volume":380,"year":"2008","citation":{"ista":"Schanda P, Brutscher B, Konrat R, Tollinger M. 2008. Folding of the KIX domain: Characterization of the equilibrium analog of a folding intermediate using 15N/13C relaxation dispersion and fast 1H/2H amide exchange NMR spectroscopy. Journal of Molecular Biology. 380(4), 726–741.","chicago":"Schanda, Paul, Bernhard Brutscher, Robert Konrat, and Martin Tollinger. “Folding of the KIX Domain: Characterization of the Equilibrium Analog of a Folding Intermediate Using 15N/13C Relaxation Dispersion and Fast 1H/2H Amide Exchange NMR Spectroscopy.” <i>Journal of Molecular Biology</i>. Elsevier, 2008. <a href=\"https://doi.org/10.1016/j.jmb.2008.05.040\">https://doi.org/10.1016/j.jmb.2008.05.040</a>.","apa":"Schanda, P., Brutscher, B., Konrat, R., &#38; Tollinger, M. (2008). Folding of the KIX domain: Characterization of the equilibrium analog of a folding intermediate using 15N/13C relaxation dispersion and fast 1H/2H amide exchange NMR spectroscopy. <i>Journal of Molecular Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jmb.2008.05.040\">https://doi.org/10.1016/j.jmb.2008.05.040</a>","ama":"Schanda P, Brutscher B, Konrat R, Tollinger M. Folding of the KIX domain: Characterization of the equilibrium analog of a folding intermediate using 15N/13C relaxation dispersion and fast 1H/2H amide exchange NMR spectroscopy. <i>Journal of Molecular Biology</i>. 2008;380(4):726-741. doi:<a href=\"https://doi.org/10.1016/j.jmb.2008.05.040\">10.1016/j.jmb.2008.05.040</a>","mla":"Schanda, Paul, et al. “Folding of the KIX Domain: Characterization of the Equilibrium Analog of a Folding Intermediate Using 15N/13C Relaxation Dispersion and Fast 1H/2H Amide Exchange NMR Spectroscopy.” <i>Journal of Molecular Biology</i>, vol. 380, no. 4, Elsevier, 2008, pp. 726–41, doi:<a href=\"https://doi.org/10.1016/j.jmb.2008.05.040\">10.1016/j.jmb.2008.05.040</a>.","ieee":"P. Schanda, B. Brutscher, R. Konrat, and M. Tollinger, “Folding of the KIX domain: Characterization of the equilibrium analog of a folding intermediate using 15N/13C relaxation dispersion and fast 1H/2H amide exchange NMR spectroscopy,” <i>Journal of Molecular Biology</i>, vol. 380, no. 4. Elsevier, pp. 726–741, 2008.","short":"P. Schanda, B. Brutscher, R. Konrat, M. Tollinger, Journal of Molecular Biology 380 (2008) 726–741."},"keyword":["Molecular Biology"],"oa_version":"None","language":[{"iso":"eng"}]}]