[{"conference":{"end_date":"2009-08-12","location":"Calgary, Canada","start_date":"2009-08-10","name":"POPL: Principles of Programming Languages"},"author":[{"last_name":"Dragojevic","full_name":"Dragojevic, Aleksandar","first_name":"Aleksandar"},{"first_name":"Rachid","last_name":"Guerraoui","full_name":"Guerraoui, Rachid"},{"first_name":"Anmol","last_name":"Singh","full_name":"Singh, Anmol"},{"first_name":"Vasu","full_name":"Singh, Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh"}],"extern":"1","_id":"4385","title":"Preventing versus curing: Avoiding conflicts in transactional memories","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-07-02T06:35:49Z","type":"conference","abstract":[{"lang":"eng","text":"Transactional memories are typically speculative and rely on contention managers to cure conflicts. This paper explores a complementary approach that prevents conflicts by scheduling transactions according to predictions on their access sets.\r\nWe first explore the theoretical boundaries of this approach and prove that (1) a TM scheduler with an accurate prediction can be 2-competitive with an optimal offline TM scheduler, but (2) even a slight inaccuracy in prediction makes the competitive ratio of the TM scheduler in the order of the number of transactions.\r\nWe then show that, in practice, there is room for a pragmatic approach with good average case performance. We present Shrink, a scheduler that (1) bases its prediction of transactional accesses on the access patterns of the past transactions from the same thread, and (2) uses a novel heuristic, which we call serialization affinity, to schedule transactions with a probability proportional to the current amount of contention. Shrink obtains roughly 70% accurate read and write access predictions on STMBench7 and STAMP. In our experimental evaluation, Shrink significantly improves STM performance in cases the number of executing threads is higher than the number of available CPU cores. For SwissTM, Shrink improves the performance by up to 55% on STMBench7, and up to 120% on STAMP. For TinySTM, Shrink drastically improves the performance on STMBench7 and STAMP benchmarks."}],"publist_id":"1070","date_created":"2018-12-11T12:08:35Z","publication":"Proceedings of the 28th ACM symposium on Principles of distributed computing","article_processing_charge":"No","language":[{"iso":"eng"}],"page":"7 - 16","oa_version":"None","quality_controlled":"1","month":"08","date_published":"2009-08-10T00:00:00Z","day":"10","doi":"10.1145/1582716.1582725","publication_status":"published","year":"2009","scopus_import":"1","publisher":"ACM","status":"public","citation":{"ista":"Dragojevic A, Guerraoui R, Singh A, Singh V. 2009. Preventing versus curing: Avoiding conflicts in transactional memories. Proceedings of the 28th ACM symposium on Principles of distributed computing. POPL: Principles of Programming Languages, 7–16.","short":"A. Dragojevic, R. Guerraoui, A. Singh, V. Singh, in:, Proceedings of the 28th ACM Symposium on Principles of Distributed Computing, ACM, 2009, pp. 7–16.","mla":"Dragojevic, Aleksandar, et al. “Preventing versus Curing: Avoiding Conflicts in Transactional Memories.” <i>Proceedings of the 28th ACM Symposium on Principles of Distributed Computing</i>, ACM, 2009, pp. 7–16, doi:<a href=\"https://doi.org/10.1145/1582716.1582725\">10.1145/1582716.1582725</a>.","chicago":"Dragojevic, Aleksandar, Rachid Guerraoui, Anmol Singh, and Vasu Singh. “Preventing versus Curing: Avoiding Conflicts in Transactional Memories.” In <i>Proceedings of the 28th ACM Symposium on Principles of Distributed Computing</i>, 7–16. ACM, 2009. <a href=\"https://doi.org/10.1145/1582716.1582725\">https://doi.org/10.1145/1582716.1582725</a>.","apa":"Dragojevic, A., Guerraoui, R., Singh, A., &#38; Singh, V. (2009). Preventing versus curing: Avoiding conflicts in transactional memories. In <i>Proceedings of the 28th ACM symposium on Principles of distributed computing</i> (pp. 7–16). Calgary, Canada: ACM. <a href=\"https://doi.org/10.1145/1582716.1582725\">https://doi.org/10.1145/1582716.1582725</a>","ama":"Dragojevic A, Guerraoui R, Singh A, Singh V. Preventing versus curing: Avoiding conflicts in transactional memories. In: <i>Proceedings of the 28th ACM Symposium on Principles of Distributed Computing</i>. ACM; 2009:7-16. doi:<a href=\"https://doi.org/10.1145/1582716.1582725\">10.1145/1582716.1582725</a>","ieee":"A. Dragojevic, R. Guerraoui, A. Singh, and V. Singh, “Preventing versus curing: Avoiding conflicts in transactional memories,” in <i>Proceedings of the 28th ACM symposium on Principles of distributed computing</i>, Calgary, Canada, 2009, pp. 7–16."}},{"year":"2009","scopus_import":"1","status":"public","publisher":"Springer","citation":{"short":"P. Cerny, R. Alur, in:, 21st International Conference on Computer Aided Verification, Springer, 2009, pp. 173–187.","mla":"Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for Confidentiality.” <i>21st International Conference on Computer Aided Verification</i>, vol. 5643, Springer, 2009, pp. 173–87, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">10.1007/978-3-642-02658-4_16</a>.","chicago":"Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for Confidentiality.” In <i>21st International Conference on Computer Aided Verification</i>, 5643:173–87. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">https://doi.org/10.1007/978-3-642-02658-4_16</a>.","ista":"Cerny P, Alur R. 2009. Automated analysis of Java methods for confidentiality. 21st International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 5643, 173–187.","ieee":"P. Cerny and R. Alur, “Automated analysis of Java methods for confidentiality,” in <i>21st International Conference on Computer Aided Verification</i>, 2009, vol. 5643, pp. 173–187.","apa":"Cerny, P., &#38; Alur, R. (2009). Automated analysis of Java methods for confidentiality. In <i>21st International Conference on Computer Aided Verification</i> (Vol. 5643, pp. 173–187). Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">https://doi.org/10.1007/978-3-642-02658-4_16</a>","ama":"Cerny P, Alur R. Automated analysis of Java methods for confidentiality. In: <i>21st International Conference on Computer Aided Verification</i>. Vol 5643. Springer; 2009:173-187. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">10.1007/978-3-642-02658-4_16</a>"},"article_processing_charge":"No","page":"173 - 187","oa_version":"None","quality_controlled":"1","language":[{"iso":"eng"}],"month":"07","date_published":"2009-07-01T00:00:00Z","publication_status":"published","doi":"10.1007/978-3-642-02658-4_16","day":"01","volume":5643,"type":"conference","date_updated":"2025-07-02T06:32:32Z","abstract":[{"text":"We address the problem of analyzing programs such as J2ME midlets for mobile devices, where a central correctness requirement concerns confidentiality of data that the user wants to keep secret. Existing software model checking tools analyze individual program executions, and are not applicable to checking confidentiality properties that require reasoning about equivalence among executions. We develop an automated analysis technique for such properties. We show that both over- and under- approximation is needed for sound analysis. Given a program and a confidentiality requirement, our technique produces a formula that is satisfiable if the requirement holds. We evaluate the approach by analyzing bytecode of a set of Java (J2ME) methods.","lang":"eng"}],"intvolume":"      5643","publication":"21st International Conference on Computer Aided Verification","date_created":"2018-12-11T12:08:36Z","publist_id":"1067","author":[{"first_name":"Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol"},{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"}],"conference":{"name":"CAV: Computer Aided Verification"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"title":"Automated analysis of Java methods for confidentiality","_id":"4391","extern":"1"},{"citation":{"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>","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>","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.","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>.","ista":"Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101."},"status":"public","main_file_link":[{"open_access":"1","url":"http://repository.upenn.edu/cis_reports/894/"}],"day":"01","doi":"10.1007/978-3-642-04027-6_9","publication_status":"published","month":"09","related_material":{"record":[{"relation":"later_version","id":"2967","status":"public"}]},"oa_version":"Submitted Version","quality_controlled":"1","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:08:40Z","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"}],"date_updated":"2025-09-30T08:04:32Z","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Algorithmic analysis of array-accessing programs","oa":1,"conference":{"start_date":"2009-09-07","name":"CSL: Computer Science Logic","end_date":"2009-09-11","location":"Coimbra, Portugal"},"publisher":"Springer","year":"2009","date_published":"2009-09-01T00:00:00Z","page":"86 - 101","article_processing_charge":"No","publist_id":"1056","intvolume":"      5771","volume":5771,"_id":"4403","extern":"1","alternative_title":["LNCS"],"author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"first_name":"Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol"},{"first_name":"Scott","full_name":"Weinstein, Scott","last_name":"Weinstein"}]},{"oa":1,"conference":{"name":"CAV: Computer Aided Verification"},"author":[{"last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"full_name":"Maria Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","last_name":"Mateescu","first_name":"Maria"},{"first_name":"Verena","last_name":"Wolf","full_name":"Wolf, Verena"}],"extern":1,"_id":"4453","alternative_title":["LNCS"],"title":"Sliding-window abstraction for infinite Markov chains","date_updated":"2021-01-12T07:57:04Z","type":"conference","file_date_updated":"2020-07-14T12:46:30Z","volume":5643,"publist_id":"278","date_created":"2018-12-11T12:08:55Z","intvolume":"      5643","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"}],"page":"337 - 352","quality_controlled":0,"doi":"10.1007/978-3-642-02658-4_27","day":"01","publication_status":"published","date_published":"2009-01-01T00:00:00Z","month":"01","pubrep_id":"40","year":"2009","acknowledgement":"The research has been partially funded by the Swiss National Science Foundation under grant 205321-111840.","file":[{"file_size":804295,"creator":"system","date_updated":"2020-07-14T12:46:30Z","file_name":"IST-2012-40-v1+1_Sliding-window_abstraction_for_infinite_markov_chains.pdf","file_id":"4938","date_created":"2018-12-12T10:12:20Z","relation":"main_file","checksum":"36b974111521ea534aae294166e93a63","content_type":"application/pdf","access_level":"open_access"}],"citation":{"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.","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>","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>","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>.","short":"T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 337–352.","ista":"Henzinger TA, Mateescu M, Wolf V. 2009. Sliding-window abstraction for infinite Markov chains. CAV: Computer Aided Verification, LNCS, vol. 5643, 337–352."},"publisher":"Springer","status":"public","main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/sliding-window_abstraction_for_infinite_markov_chains.pdf","open_access":"0"}]},{"citation":{"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.","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.","short":"F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 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>.","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>."},"status":"public","publisher":"Springer","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.","year":"2009","publication_status":"published","doi":"10.1007/978-3-642-03845-7_12","day":"17","related_material":{"record":[{"status":"public","relation":"later_version","id":"3364"}]},"date_published":"2009-08-17T00:00:00Z","month":"08","page":"173 - 188","quality_controlled":0,"date_created":"2018-12-11T12:09:21Z","publist_id":"189","intvolume":"      5688","abstract":[{"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.","lang":"eng"}],"type":"conference","date_updated":"2025-09-30T09:03:30Z","volume":5688,"alternative_title":["LNCS"],"title":"Approximation of event probabilities in noisy cellular processes","_id":"4535","extern":1,"author":[{"last_name":"Didier","full_name":"Didier, Frédéric","first_name":"Frédéric"},{"last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"last_name":"Mateescu","full_name":"Maria Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria"},{"full_name":"Wolf, Verena","last_name":"Wolf","first_name":"Verena"}],"conference":{"name":"CMSB: Computational Methods in Systems Biology"}},{"publisher":"IEEE","status":"public","citation":{"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>","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>","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.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Expressiveness and closure properties for quantitative languages. LICS: Logic in Computer Science, 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>.","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>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, IEEE, 2009, pp. 199–208."},"pubrep_id":"55","scopus_import":"1","year":"2009","month":"01","date_published":"2009-01-01T00:00:00Z","related_material":{"record":[{"id":"3867","relation":"later_version","status":"public"}]},"day":"01","doi":"10.1109/LICS.2009.16","publication_status":"published","article_processing_charge":"No","oa_version":"None","page":"199 - 208","language":[{"iso":"eng"}],"quality_controlled":"1","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"}],"publist_id":"181","date_created":"2018-12-11T12:09:23Z","date_updated":"2025-09-30T09:30:59Z","type":"conference","extern":"1","_id":"4540","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Expressiveness and closure properties for quantitative languages","conference":{"name":"LICS: Logic in Computer Science"},"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}]},{"corr_author":"1","month":"09","publication_status":"published","department":[{"_id":"KrCh"}],"day":"10","doi":"10.1007/978-3-642-03409-1_2","ec_funded":1,"language":[{"iso":"eng"}],"oa_version":"Submitted Version","quality_controlled":"1","status":"public","file":[{"access_level":"open_access","content_type":"application/pdf","checksum":"e8f53abb63579de3f2bff58b2a1188e2","relation":"main_file","file_id":"5126","date_created":"2018-12-12T10:15:09Z","file_name":"IST-2012-39-v1+1_Alternating_Weighted_Automata.pdf","date_updated":"2020-07-14T12:46:31Z","creator":"system","file_size":164428}],"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.","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>.","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>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 3–13.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Alternating weighted automata. FCT: Fundamentals of Computation Theory, LNCS, vol. 5699, 3–13."},"scopus_import":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 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.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Alternating weighted automata","conference":{"name":"FCT: Fundamentals of Computation Theory","start_date":"2009-09-02","location":"Wroclaw, Poland","end_date":"2009-09-04"},"has_accepted_license":"1","oa":1,"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"}],"date_created":"2018-12-11T12:09:23Z","file_date_updated":"2020-07-14T12:46:31Z","type":"conference","date_updated":"2024-10-09T20:53:55Z","date_published":"2009-09-10T00:00:00Z","page":"3 - 13","project":[{"grant_number":"214373","call_identifier":"FP7","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425"},{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543"}],"publisher":"Springer","ddc":["004"],"year":"2009","pubrep_id":"39","alternative_title":["LNCS"],"_id":"4542","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"intvolume":"      5699","publist_id":"180","volume":5699},{"year":"2009","publisher":"Springer","project":[{"name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"},{"grant_number":"214373","name":"Design for Embedded Systems","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"page":"34 - 54","date_published":"2009-08-01T00:00:00Z","volume":5734,"intvolume":"      5734","publist_id":"178","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Florian","id":"37327ACE-F248-11E8-B48F-1D18A9856A87","full_name":"Horn, Florian","last_name":"Horn"}],"_id":"4543","alternative_title":["LNCS"],"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.","scopus_import":1,"status":"public","citation":{"ista":"Chatterjee K, Henzinger TA, Horn F. 2009. Stochastic games with finitary objectives. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 5734, 34–54.","short":"K. Chatterjee, T.A. Henzinger, F. Horn, in:, Springer, 2009, 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>.","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>.","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>","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."},"language":[{"iso":"eng"}],"quality_controlled":"1","oa_version":"None","corr_author":"1","month":"08","ec_funded":1,"doi":"10.1007/978-3-642-03816-7_4","day":"01","publication_status":"published","department":[{"_id":"KrCh"}],"date_updated":"2024-10-09T20:53:54Z","type":"conference","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"}],"date_created":"2018-12-11T12:09:24Z","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2009-08-24","location":"High Tatras, Slovakia","end_date":"2009-08-28"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Stochastic games with finitary objectives"},{"file_date_updated":"2020-07-14T12:46:31Z","date_updated":"2021-01-12T07:59:35Z","type":"conference","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."}],"publist_id":"176","date_created":"2018-12-11T12:09:24Z","conference":{"name":"SODA: Symposium on Discrete Algorithms"},"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Krishnendu Chatterjee","last_name":"Chatterjee"},{"first_name":"Luca","last_name":"De Alfaro","full_name":"de Alfaro, Luca"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"extern":1,"_id":"4544","title":"Termination criteria for solving concurrent safety and reachability games","pubrep_id":"37","year":"2009","publisher":"SIAM","main_file_link":[{"open_access":"1","url":"https://repository.ist.ac.at/id/eprint/37"}],"status":"public","citation":{"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>.","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>.","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.","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.","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>","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>"},"file":[{"content_type":"application/pdf","checksum":"ce7dc1667502e26b23c07a767ac41ae6","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:46:31Z","creator":"system","file_size":212369,"date_created":"2018-12-12T10:08:03Z","file_id":"4662","file_name":"IST-2012-37-v1+1_Termination_criteria_for_solving_concurrent_safety_and_reachability_games.pdf"}],"page":"197 - 206","quality_controlled":0,"month":"01","date_published":"2009-01-01T00:00:00Z","doi":"10.1137/1.9781611973068.23","day":"01","publication_status":"published"},{"has_accepted_license":"1","oa":1,"conference":{"start_date":"2009-07-05","name":"ICALP: Automata, Languages and Programming","end_date":"2009-07-12","location":"Rhodos, Greece"},"title":"A survey of stochastic games with limsup and liminf objectives","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2024-10-09T20:53:54Z","type":"conference","file_date_updated":"2020-07-14T12:46:31Z","date_created":"2018-12-11T12:09:24Z","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"}],"language":[{"iso":"eng"}],"oa_version":"Submitted Version","quality_controlled":"1","doi":"10.1007/978-3-642-02930-1_1","ec_funded":1,"day":"24","department":[{"_id":"KrCh"}],"publication_status":"published","month":"06","corr_author":"1","scopus_import":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","creator":"system","file_size":187419,"file_id":"4992","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","content_type":"application/pdf","checksum":"dabb6d24428a000254c95493d9c492e6","relation":"main_file","access_level":"open_access"}],"citation":{"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.","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>.","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>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 1–15.","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>","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."},"status":"public","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"_id":"4545","alternative_title":["LNCS"],"volume":5556,"publist_id":"177","intvolume":"      5556","page":"1 - 15","date_published":"2009-06-24T00:00:00Z","pubrep_id":"38","year":"2009","ddc":["000","005"],"publisher":"Springer","project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7","grant_number":"215543"}]},{"date_updated":"2024-10-21T06:03:07Z","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"}],"date_created":"2018-12-11T12:09:31Z","conference":{"location":"Grenoble, France","end_date":"2009-07-02","name":"CAV: Computer Aided Verification","start_date":"2009-06-26"},"oa":1,"title":"Better quality in synthesis through quantitative objectives","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","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.","status":"public","main_file_link":[{"url":"http://arxiv.org/abs/0904.2638","open_access":"1"}],"citation":{"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>","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>","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.","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.","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>.","short":"R. Bloem, K. Chatterjee, T.A. Henzinger, B. Jobstmann, in:, Springer, 2009, pp. 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>."},"arxiv":1,"quality_controlled":"1","oa_version":"Preprint","language":[{"iso":"eng"}],"month":"06","doi":"10.1007/978-3-642-02658-4_14","ec_funded":1,"day":"19","publication_status":"published","department":[{"_id":"KrCh"}],"volume":5643,"intvolume":"      5643","publist_id":"141","author":[{"last_name":"Bloem","full_name":"Bloem, Roderick","first_name":"Roderick"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Barbara","full_name":"Jobstmann, Barbara","last_name":"Jobstmann"}],"_id":"4569","external_id":{"arxiv":["0904.2638"]},"alternative_title":["LNCS"],"year":"2009","publisher":"Springer","project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543"}],"page":"140 - 156","date_published":"2009-06-19T00:00:00Z"},{"oa":1,"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"author":[{"first_name":"Dietmar","last_name":"Berwanger","full_name":"Berwanger, Dietmar"},{"full_name":"Krishnendu Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"De Wulf","full_name":"De Wulf, Martin","first_name":"Martin"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","last_name":"Henzinger"}],"_id":"4580","extern":1,"title":"Alpaga: A tool for solving parity games with imperfect information","alternative_title":["LNCS"],"date_updated":"2021-01-12T07:59:52Z","type":"conference","file_date_updated":"2020-07-14T12:46:32Z","volume":5505,"publist_id":"127","date_created":"2018-12-11T12:09:35Z","intvolume":"      5505","abstract":[{"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.","lang":"eng"}],"quality_controlled":0,"page":"58 - 61","day":"09","doi":"10.1007/978-3-642-00768-2_7","publication_status":"published","month":"03","date_published":"2009-03-09T00:00:00Z","pubrep_id":"35","year":"2009","file":[{"file_size":212180,"creator":"system","date_updated":"2020-07-14T12:46:32Z","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","file_id":"5168","relation":"main_file","checksum":"d52b55a10a47b3e3b0e016ea9bf85c41","content_type":"application/pdf","access_level":"open_access"}],"citation":{"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.","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>.","short":"D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, T.A. Henzinger, in:, Springer, 2009, 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>","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."},"publisher":"Springer","status":"public","main_file_link":[{"open_access":"1","url":"https://repository.ist.ac.at/35/"}]},{"date_published":"2009-11-02T00:00:00Z","page":"17","ddc":["005"],"publisher":"IST Austria","year":"2009","pubrep_id":"28","alternative_title":["IST Austria Technical Report"],"_id":"5392","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"}],"department":[{"_id":"KrCh"}],"publication_status":"published","doi":"10.15479/AT:IST-2009-0004","day":"02","related_material":{"record":[{"status":"public","relation":"later_version","id":"3857"}]},"month":"11","corr_author":"1","oa_version":"Published Version","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","relation":"main_file","checksum":"fb7563150231325b00b1718d956f687b","access_level":"open_access","date_updated":"2020-07-14T12:46:43Z","file_size":311065,"creator":"system","date_created":"2018-12-12T11:54:08Z","file_id":"5530","file_name":"IST-2009-0004_IST-2009-0004.pdf"}],"citation":{"ieee":"K. Chatterjee, <i>Probabilistic automata on infinite words: Decidability and undecidability results</i>. IST Austria, 2009.","ama":"Chatterjee K. <i>Probabilistic Automata on Infinite Words: Decidability and Undecidability Results</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">10.15479/AT:IST-2009-0004</a>","apa":"Chatterjee, K. (2009). <i>Probabilistic automata on infinite words: Decidability and undecidability results</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">https://doi.org/10.15479/AT:IST-2009-0004</a>","mla":"Chatterjee, Krishnendu. <i>Probabilistic Automata on Infinite Words: Decidability and Undecidability Results</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">10.15479/AT:IST-2009-0004</a>.","short":"K. Chatterjee, Probabilistic Automata on Infinite Words: Decidability and Undecidability Results, IST Austria, 2009.","chicago":"Chatterjee, Krishnendu. <i>Probabilistic Automata on Infinite Words: Decidability and Undecidability Results</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">https://doi.org/10.15479/AT:IST-2009-0004</a>.","ista":"Chatterjee K. 2009. Probabilistic automata on infinite words: Decidability and undecidability results, IST Austria, 17p."},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Probabilistic automata on infinite words: Decidability and undecidability results","oa":1,"has_accepted_license":"1","date_created":"2018-12-12T11:39:04Z","publication_identifier":{"issn":["2664-1690"]},"abstract":[{"text":"We consider probabilistic automata on infinite words with acceptance defined by safety, reachability, Büchi, coBüchi and limit-average conditions. We consider quantitative and qualitative decision problems. We present extensions and adaptations of proofs of [GO09] and present a precise characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems.","lang":"eng"}],"type":"technical_report","date_updated":"2025-04-14T13:37:25Z","file_date_updated":"2020-07-14T12:46:43Z"},{"title":"Gist: A solver for probabilistic games","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","oa":1,"abstract":[{"lang":"eng","text":"Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides efficient implementations of several reduction based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications."}],"publication_identifier":{"issn":["2664-1690"]},"date_created":"2018-12-12T11:39:05Z","file_date_updated":"2020-07-14T12:46:43Z","date_updated":"2025-04-14T13:37:27Z","type":"technical_report","corr_author":"1","month":"10","related_material":{"record":[{"id":"4388","relation":"later_version","status":"public"}]},"doi":"10.15479/AT:IST-2009-0003","day":"09","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"status":"public","file":[{"access_level":"open_access","relation":"main_file","checksum":"49551ac552915b17593a14c993845274","content_type":"application/pdf","file_name":"IST-2009-0003_IST-2009-0003.pdf","date_created":"2018-12-12T11:52:58Z","file_id":"5459","file_size":386866,"creator":"system","date_updated":"2020-07-14T12:46:43Z"}],"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, <i>Gist: A solver for probabilistic games</i>. IST Austria, 2009.","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. <i>Gist: A Solver for Probabilistic Games</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">10.15479/AT:IST-2009-0003</a>","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Radhakrishna, A. (2009). <i>Gist: A solver for probabilistic games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">https://doi.org/10.15479/AT:IST-2009-0003</a>","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, Gist: A Solver for Probabilistic Games, IST Austria, 2009.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun Radhakrishna. <i>Gist: A Solver for Probabilistic Games</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">https://doi.org/10.15479/AT:IST-2009-0003</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Gist: A Solver for Probabilistic Games</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">10.15479/AT:IST-2009-0003</a>.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2009. Gist: A solver for probabilistic games, IST Austria, 12p."},"_id":"5393","alternative_title":["IST Austria Technical Report"],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","first_name":"Arjun"}],"date_published":"2009-10-09T00:00:00Z","page":"12","publisher":"IST Austria","ddc":["000","005"],"pubrep_id":"29","year":"2009"},{"day":"09","doi":"10.15479/AT:IST-2009-0002","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"corr_author":"1","date_published":"2009-09-09T00:00:00Z","month":"09","oa_version":"Published Version","page":"11","language":[{"iso":"eng"}],"file":[{"access_level":"open_access","content_type":"application/pdf","checksum":"1c50a9723fbae1b2c46d18138968efb3","relation":"main_file","file_id":"5511","date_created":"2018-12-12T11:53:50Z","file_name":"IST-2009-0002_IST-2009-0002.pdf","date_updated":"2020-07-14T12:46:43Z","creator":"system","file_size":238091}],"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and F. Horn, <i>Improved lower bounds for request-response and finitary Streett games</i>. IST Austria, 2009.","ama":"Chatterjee K, Henzinger TA, Horn F. <i>Improved Lower Bounds for Request-Response and Finitary Streett Games</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">10.15479/AT:IST-2009-0002</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Horn, F. (2009). <i>Improved lower bounds for request-response and finitary Streett games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">https://doi.org/10.15479/AT:IST-2009-0002</a>","mla":"Chatterjee, Krishnendu, et al. <i>Improved Lower Bounds for Request-Response and Finitary Streett Games</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">10.15479/AT:IST-2009-0002</a>.","short":"K. Chatterjee, T.A. Henzinger, F. Horn, Improved Lower Bounds for Request-Response and Finitary Streett Games, IST Austria, 2009.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. <i>Improved Lower Bounds for Request-Response and Finitary Streett Games</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">https://doi.org/10.15479/AT:IST-2009-0002</a>.","ista":"Chatterjee K, Henzinger TA, Horn F. 2009. Improved lower bounds for request-response and finitary Streett games, IST Austria, 11p."},"ddc":["004"],"publisher":"IST Austria","status":"public","pubrep_id":"30","year":"2009","_id":"5394","title":"Improved lower bounds for request-response and finitary Streett games","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"has_accepted_license":"1","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Florian","last_name":"Horn","id":"37327ACE-F248-11E8-B48F-1D18A9856A87","full_name":"Horn, Florian"}],"publication_identifier":{"issn":["2664-1690"]},"date_created":"2018-12-12T11:39:05Z","abstract":[{"lang":"eng","text":"We consider two-player games played on graphs with request-response and finitary Streett objectives. We show these games are PSPACE-hard, improving the previous known NP-hardness. We also improve the lower bounds on memory required by the winning strategies for the players."}],"date_updated":"2024-10-09T21:08:23Z","type":"technical_report","file_date_updated":"2020-07-14T12:46:43Z"},{"ddc":["005"],"publisher":"IST Austria","pubrep_id":"31","year":"2009","date_published":"2009-09-09T00:00:00Z","page":"20","_id":"5395","alternative_title":["IST Austria Technical Report"],"author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"file":[{"content_type":"application/pdf","checksum":"04d9cc065cc19598a4e8631c47f1a562","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:46:43Z","creator":"system","file_size":342088,"file_id":"5486","date_created":"2018-12-12T11:53:25Z","file_name":"IST-2009-0001_IST-2009-0001.pdf"}],"citation":{"ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, <i>Qualitative analysis of partially-observable Markov decision processes</i>. IST Austria, 2009.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). <i>Qualitative analysis of partially-observable Markov decision processes</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">https://doi.org/10.15479/AT:IST-2009-0001</a>","ama":"Chatterjee K, Doyen L, Henzinger TA. <i>Qualitative Analysis of Partially-Observable Markov Decision Processes</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">10.15479/AT:IST-2009-0001</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. <i>Qualitative Analysis of Partially-Observable Markov Decision Processes</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">https://doi.org/10.15479/AT:IST-2009-0001</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, Qualitative Analysis of Partially-Observable Markov Decision Processes, IST Austria, 2009.","mla":"Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of Partially-Observable Markov Decision Processes</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">10.15479/AT:IST-2009-0001</a>.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Qualitative analysis of partially-observable Markov decision processes, IST Austria, 20p."},"status":"public","doi":"10.15479/AT:IST-2009-0001","day":"09","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","corr_author":"1","month":"09","related_material":{"record":[{"status":"public","id":"3855","relation":"later_version"}]},"oa_version":"Published Version","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"date_created":"2018-12-12T11:39:05Z","abstract":[{"text":"We study observation-based strategies for partially-observable Markov decision processes (POMDPs) with omega-regular objectives. An observation-based strategy relies on partial information about the history of a play, namely, on the past sequence of observa- tions. We consider the qualitative analysis problem: given a POMDP with an omega-regular objective, whether there is an observation-based strategy to achieve the objective with probability 1 (almost-sure winning), or with positive probability (positive winning). Our main results are twofold. First, we present a complete picture of the computational complexity of the qualitative analysis of POMDPs with parity objectives (a canonical form to express omega-regular objectives) and its subclasses. Our contribution consists in establishing several upper and lower bounds that were not known in literature. Second, we present optimal bounds (matching upper and lower bounds) on the memory required by pure and randomized observation-based strategies for the qualitative analysis of POMDPs with parity objectives and its subclasses.","lang":"eng"}],"date_updated":"2025-04-14T13:37:25Z","type":"technical_report","file_date_updated":"2020-07-14T12:46:43Z","title":"Qualitative analysis of partially-observable Markov decision processes","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","oa":1},{"year":"2009","publisher":"Cold Spring Harbor Laboratory Press","status":"public","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC2648653/"}],"citation":{"ista":"Knuesel M, Meyer K, Bernecky C, Taatjes D. 2009. The human CDK8 subcomplex is a molecular switch that controls Mediator coactivator function. Genes and Development. 23(4), 439–451.","mla":"Knuesel, Matthew, et al. “The Human CDK8 Subcomplex Is a Molecular Switch That Controls Mediator Coactivator Function.” <i>Genes and Development</i>, vol. 23, no. 4, Cold Spring Harbor Laboratory Press, 2009, pp. 439–51, doi:<a href=\"https://doi.org/10.1101/gad.1767009\">10.1101/gad.1767009</a>.","short":"M. Knuesel, K. Meyer, C. Bernecky, D. Taatjes, Genes and Development 23 (2009) 439–451.","chicago":"Knuesel, Matthew, Krista Meyer, Carrie Bernecky, and Dylan Taatjes. “The Human CDK8 Subcomplex Is a Molecular Switch That Controls Mediator Coactivator Function.” <i>Genes and Development</i>. Cold Spring Harbor Laboratory Press, 2009. <a href=\"https://doi.org/10.1101/gad.1767009\">https://doi.org/10.1101/gad.1767009</a>.","apa":"Knuesel, M., Meyer, K., Bernecky, C., &#38; Taatjes, D. (2009). The human CDK8 subcomplex is a molecular switch that controls Mediator coactivator function. <i>Genes and Development</i>. Cold Spring Harbor Laboratory Press. <a href=\"https://doi.org/10.1101/gad.1767009\">https://doi.org/10.1101/gad.1767009</a>","ama":"Knuesel M, Meyer K, Bernecky C, Taatjes D. The human CDK8 subcomplex is a molecular switch that controls Mediator coactivator function. <i>Genes and Development</i>. 2009;23(4):439-451. doi:<a href=\"https://doi.org/10.1101/gad.1767009\">10.1101/gad.1767009</a>","ieee":"M. Knuesel, K. Meyer, C. Bernecky, and D. Taatjes, “The human CDK8 subcomplex is a molecular switch that controls Mediator coactivator function,” <i>Genes and Development</i>, vol. 23, no. 4. Cold Spring Harbor Laboratory Press, pp. 439–451, 2009."},"article_processing_charge":"No","language":[{"iso":"eng"}],"page":"439 - 451","oa_version":"None","month":"02","date_published":"2009-02-15T00:00:00Z","doi":"10.1101/gad.1767009","day":"15","publication_status":"published","volume":23,"date_updated":"2021-01-12T08:05:32Z","type":"journal_article","intvolume":"        23","abstract":[{"lang":"eng","text":"The human CDK8 subcomplex (CDK8, cyclin C, Med12, and Med13) negatively regulates transcription in ways not completely defined; past studies suggested CDK8 kinase activity was required for its repressive function. Using a reconstituted transcription system together with recombinant or endogenous CDK8 subcomplexes, we demonstrate that, in fact, Med12 and Med13 are critical for subcomplex-dependent repression, whereas CDK8 kinase activity is not. A hallmark of activated transcription is efficient reinitiation from promoter-bound scaffold complexes that recruit a series of pol II enzymes to the gene. Notably, the CDK8 submodule strongly represses even reinitiation events, suggesting a means to fine tune transcript levels. Structural and biochemical studies confirm the CDK8 submodule binds the Mediator leg/tail domain via the Med13 subunit, and this submodule-Mediator association precludes pol II recruitment. Collectively, these results reveal the CDK8 subcomplex functions as a simple switch that controls the Mediator-pol II interaction to help regulate transcription initiation and reinitiation events. As Mediator is generally required for expression of protein-coding genes, this may reflect a common mechanism by which activated transcription is shut down in human cells."}],"publist_id":"7211","date_created":"2018-12-11T11:47:25Z","publication":"Genes and Development","author":[{"last_name":"Knuesel","full_name":"Knuesel, Matthew","first_name":"Matthew"},{"first_name":"Krista","full_name":"Meyer, Krista","last_name":"Meyer"},{"first_name":"Carrie A","orcid":"0000-0003-0893-7036","id":"2CB9DFE2-F248-11E8-B48F-1D18A9856A87","full_name":"Bernecky, Carrie A","last_name":"Bernecky"},{"full_name":"Taatjes, Dylan","last_name":"Taatjes","first_name":"Dylan"}],"oa":1,"issue":"4","_id":"599","extern":"1","title":"The human CDK8 subcomplex is a molecular switch that controls Mediator coactivator function","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"oa_version":"None","quality_controlled":"1","page":"1030-1033","language":[{"iso":"eng"}],"day":"23","doi":"10.1038/nature07820","publication_status":"published","month":"04","date_published":"2009-04-23T00:00:00Z","pmid":1,"year":"2009","citation":{"short":"A. Persson, E. Gross, P. Laurent, K.E. Busch, H. Bretes, M. de Bono, Nature 458 (2009) 1030–1033.","chicago":"Persson, Annelie, Einav Gross, Patrick Laurent, Karl Emanuel Busch, Hugo Bretes, and Mario de Bono. “Natural Variation in a Neural Globin Tunes Oxygen Sensing in Wild Caenorhabditis Elegans.” <i>Nature</i>. Springer Nature, 2009. <a href=\"https://doi.org/10.1038/nature07820\">https://doi.org/10.1038/nature07820</a>.","mla":"Persson, Annelie, et al. “Natural Variation in a Neural Globin Tunes Oxygen Sensing in Wild Caenorhabditis Elegans.” <i>Nature</i>, vol. 458, no. 7241, Springer Nature, 2009, pp. 1030–33, doi:<a href=\"https://doi.org/10.1038/nature07820\">10.1038/nature07820</a>.","ista":"Persson A, Gross E, Laurent P, Busch KE, Bretes H, de Bono M. 2009. Natural variation in a neural globin tunes oxygen sensing in wild Caenorhabditis elegans. Nature. 458(7241), 1030–1033.","ieee":"A. Persson, E. Gross, P. Laurent, K. E. Busch, H. Bretes, and M. de Bono, “Natural variation in a neural globin tunes oxygen sensing in wild Caenorhabditis elegans,” <i>Nature</i>, vol. 458, no. 7241. Springer Nature, pp. 1030–1033, 2009.","apa":"Persson, A., Gross, E., Laurent, P., Busch, K. E., Bretes, H., &#38; de Bono, M. (2009). Natural variation in a neural globin tunes oxygen sensing in wild Caenorhabditis elegans. <i>Nature</i>. Springer Nature. <a href=\"https://doi.org/10.1038/nature07820\">https://doi.org/10.1038/nature07820</a>","ama":"Persson A, Gross E, Laurent P, Busch KE, Bretes H, de Bono M. Natural variation in a neural globin tunes oxygen sensing in wild Caenorhabditis elegans. <i>Nature</i>. 2009;458(7241):1030-1033. doi:<a href=\"https://doi.org/10.1038/nature07820\">10.1038/nature07820</a>"},"publisher":"Springer Nature","status":"public","author":[{"last_name":"Persson","full_name":"Persson, Annelie","first_name":"Annelie"},{"first_name":"Einav","last_name":"Gross","full_name":"Gross, Einav"},{"first_name":"Patrick","full_name":"Laurent, Patrick","last_name":"Laurent"},{"first_name":"Karl Emanuel","full_name":"Busch, Karl Emanuel","last_name":"Busch"},{"last_name":"Bretes","full_name":"Bretes, Hugo","first_name":"Hugo"},{"last_name":"de Bono","id":"4E3FF80E-F248-11E8-B48F-1D18A9856A87","full_name":"de Bono, Mario","first_name":"Mario","orcid":"0000-0001-8347-0443"}],"external_id":{"pmid":["19262507"]},"_id":"6144","extern":"1","issue":"7241","title":"Natural variation in a neural globin tunes oxygen sensing in wild Caenorhabditis elegans","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T08:06:20Z","type":"journal_article","volume":458,"publication_identifier":{"issn":["0028-0836","1476-4687"]},"date_created":"2019-03-21T07:48:44Z","publication":"Nature","abstract":[{"text":"Behaviours evolve by iterations of natural selection, but we have few insights into the molecular and neural mechanisms involved. Here we show that some Caenorhabditis elegans wild strains switch between two foraging behaviours in response to subtle changes in ambient oxygen. This finely tuned switch is conferred by a naturally variable hexacoordinated globin, GLB-5. GLB-5 acts with the atypical soluble guanylate cyclases1,2,3, which are a different type of oxygen binding protein, to tune the dynamic range of oxygen-sensing neurons close to atmospheric (21%) concentrations. Calcium imaging indicates that one group of these neurons is activated when oxygen rises towards 21%, and is inhibited as oxygen drops below 21%. The soluble guanylate cyclase GCY-35 is required for high oxygen to activate the neurons; GLB-5 provides inhibitory input when oxygen decreases below 21%. Together, these oxygen binding proteins tune neuronal and behavioural responses to a narrow oxygen concentration range close to atmospheric levels. The effect of the glb-5 gene on oxygen sensing and foraging is modified by the naturally variable neuropeptide receptor npr-1 (refs 4, 5), providing insights into how polygenic variation reshapes neural circuit function.","lang":"eng"}],"intvolume":"       458"},{"publication_identifier":{"issn":["1550-4131"]},"publication":"Cell Metabolism","date_created":"2019-03-21T07:57:52Z","intvolume":"         9","date_updated":"2021-01-12T08:06:20Z","type":"journal_article","volume":9,"_id":"6145","external_id":{"pmid":["19356718"]},"extern":"1","issue":"4","title":"Coordinated regulation of foraging and metabolism in C. elegans by RFamide neuropeptide signaling","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Cohen","full_name":"Cohen, Merav","first_name":"Merav"},{"first_name":"Vincenzina","last_name":"Reale","full_name":"Reale, Vincenzina"},{"full_name":"Olofsson, Birgitta","last_name":"Olofsson","first_name":"Birgitta"},{"last_name":"Knights","full_name":"Knights, Andrew","first_name":"Andrew"},{"full_name":"Evans, Peter","last_name":"Evans","first_name":"Peter"},{"first_name":"Mario","orcid":"0000-0001-8347-0443","last_name":"de Bono","id":"4E3FF80E-F248-11E8-B48F-1D18A9856A87","full_name":"de Bono, Mario"}],"citation":{"chicago":"Cohen, Merav, Vincenzina Reale, Birgitta Olofsson, Andrew Knights, Peter Evans, and Mario de Bono. “Coordinated Regulation of Foraging and Metabolism in C. Elegans by RFamide Neuropeptide Signaling.” <i>Cell Metabolism</i>. Elsevier, 2009. <a href=\"https://doi.org/10.1016/j.cmet.2009.02.003\">https://doi.org/10.1016/j.cmet.2009.02.003</a>.","mla":"Cohen, Merav, et al. “Coordinated Regulation of Foraging and Metabolism in C. Elegans by RFamide Neuropeptide Signaling.” <i>Cell Metabolism</i>, vol. 9, no. 4, Elsevier, 2009, pp. 375–85, doi:<a href=\"https://doi.org/10.1016/j.cmet.2009.02.003\">10.1016/j.cmet.2009.02.003</a>.","short":"M. Cohen, V. Reale, B. Olofsson, A. Knights, P. Evans, M. de Bono, Cell Metabolism 9 (2009) 375–385.","ista":"Cohen M, Reale V, Olofsson B, Knights A, Evans P, de Bono M. 2009. Coordinated regulation of foraging and metabolism in C. elegans by RFamide neuropeptide signaling. Cell Metabolism. 9(4), 375–385.","ieee":"M. Cohen, V. Reale, B. Olofsson, A. Knights, P. Evans, and M. de Bono, “Coordinated regulation of foraging and metabolism in C. elegans by RFamide neuropeptide signaling,” <i>Cell Metabolism</i>, vol. 9, no. 4. Elsevier, pp. 375–385, 2009.","ama":"Cohen M, Reale V, Olofsson B, Knights A, Evans P, de Bono M. Coordinated regulation of foraging and metabolism in C. elegans by RFamide neuropeptide signaling. <i>Cell Metabolism</i>. 2009;9(4):375-385. doi:<a href=\"https://doi.org/10.1016/j.cmet.2009.02.003\">10.1016/j.cmet.2009.02.003</a>","apa":"Cohen, M., Reale, V., Olofsson, B., Knights, A., Evans, P., &#38; de Bono, M. (2009). Coordinated regulation of foraging and metabolism in C. elegans by RFamide neuropeptide signaling. <i>Cell Metabolism</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.cmet.2009.02.003\">https://doi.org/10.1016/j.cmet.2009.02.003</a>"},"publisher":"Elsevier","status":"public","year":"2009","doi":"10.1016/j.cmet.2009.02.003","day":"08","publication_status":"published","pmid":1,"date_published":"2009-04-08T00:00:00Z","month":"04","quality_controlled":"1","page":"375-385","language":[{"iso":"eng"}],"oa_version":"None"},{"publication_status":"published","doi":"10.1016/j.jsb.2009.03.016","day":"01","month":"10","date_published":"2009-10-01T00:00:00Z","page":"143 - 151","quality_controlled":0,"citation":{"ista":"Loose M, Schwille P. 2009. Biomimetic membrane systems to study cellular organization. Journal of Structural Biology. 168(1), 143–151.","mla":"Loose, Martin, and Petra Schwille. “Biomimetic Membrane Systems to Study Cellular Organization.” <i>Journal of Structural Biology</i>, vol. 168, no. 1, Academic Press, 2009, pp. 143–51, doi:<a href=\"https://doi.org/10.1016/j.jsb.2009.03.016\">10.1016/j.jsb.2009.03.016</a>.","chicago":"Loose, Martin, and Petra Schwille. “Biomimetic Membrane Systems to Study Cellular Organization.” <i>Journal of Structural Biology</i>. Academic Press, 2009. <a href=\"https://doi.org/10.1016/j.jsb.2009.03.016\">https://doi.org/10.1016/j.jsb.2009.03.016</a>.","short":"M. Loose, P. Schwille, Journal of Structural Biology 168 (2009) 143–151.","ama":"Loose M, Schwille P. Biomimetic membrane systems to study cellular organization. <i>Journal of Structural Biology</i>. 2009;168(1):143-151. doi:<a href=\"https://doi.org/10.1016/j.jsb.2009.03.016\">10.1016/j.jsb.2009.03.016</a>","apa":"Loose, M., &#38; Schwille, P. (2009). Biomimetic membrane systems to study cellular organization. <i>Journal of Structural Biology</i>. Academic Press. <a href=\"https://doi.org/10.1016/j.jsb.2009.03.016\">https://doi.org/10.1016/j.jsb.2009.03.016</a>","ieee":"M. Loose and P. Schwille, “Biomimetic membrane systems to study cellular organization,” <i>Journal of Structural Biology</i>, vol. 168, no. 1. Academic Press, pp. 143–151, 2009."},"status":"public","publisher":"Academic Press","year":"2009","title":"Biomimetic membrane systems to study cellular organization","_id":"1983","extern":1,"issue":"1","author":[{"full_name":"Martin Loose","id":"462D4284-F248-11E8-B48F-1D18A9856A87","last_name":"Loose","orcid":"0000-0001-7309-9724","first_name":"Martin"},{"last_name":"Schwille","full_name":"Schwille, Petra ","first_name":"Petra"}],"publication":"Journal of Structural Biology","date_created":"2018-12-11T11:55:03Z","publist_id":"5099","abstract":[{"text":"During many cellular processes such as cell division, polarization and motility, the plasma membrane does not only represent a passive physical barrier, but also provides a highly dynamic platform for the interplay between lipids, membrane binding proteins and cytoskeletal elements. Even though many regulators of these interactions are known, their mutual interdependence appears to be highly complex and difficult to study in a living cell. Over the past few years, in vitro studies on membrane-cytoskeleton interactions using biomimetic membranes turned out to be extremely helpful to get better mechanistic insight into the dynamics of these processes. In this review, we discuss some of the recent developments using in vitro assays to dissect the role of the players involved: lipids in the membrane, proteins binding to membranes and proteins binding to membrane proteins. We also summarize advantages and disadvantages of supported lipid bilayers as model membrane.","lang":"eng"}],"intvolume":"       168","type":"journal_article","date_updated":"2021-01-12T06:54:30Z","volume":168}]