[{"publication_status":"published","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","issue":"3","oa_version":"None","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.1142/S0129054112400308","publist_id":"3326","type":"journal_article","page":"609 - 625","status":"public","scopus_import":1,"year":"2012","title":"Discounting and averaging in games across time scales","citation":{"ista":"Chatterjee K, Majumdar R. 2012. Discounting and averaging in games across time scales. International Journal of Foundations of Computer Science. 23(3), 609–625.","chicago":"Chatterjee, Krishnendu, and Ritankar Majumdar. “Discounting and Averaging in Games across Time Scales.” International Journal of Foundations of Computer Science. World Scientific Publishing, 2012. https://doi.org/10.1142/S0129054112400308.","mla":"Chatterjee, Krishnendu, and Ritankar Majumdar. “Discounting and Averaging in Games across Time Scales.” International Journal of Foundations of Computer Science, vol. 23, no. 3, World Scientific Publishing, 2012, pp. 609–25, doi:10.1142/S0129054112400308.","ieee":"K. Chatterjee and R. Majumdar, “Discounting and averaging in games across time scales,” International Journal of Foundations of Computer Science, vol. 23, no. 3. World Scientific Publishing, pp. 609–625, 2012.","apa":"Chatterjee, K., & Majumdar, R. (2012). Discounting and averaging in games across time scales. International Journal of Foundations of Computer Science. World Scientific Publishing. https://doi.org/10.1142/S0129054112400308","ama":"Chatterjee K, Majumdar R. Discounting and averaging in games across time scales. International Journal of Foundations of Computer Science. 2012;23(3):609-625. doi:10.1142/S0129054112400308","short":"K. Chatterjee, R. Majumdar, International Journal of Foundations of Computer Science 23 (2012) 609–625."},"month":"04","intvolume":" 23","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar","first_name":"Ritankar"}],"_id":"3314","publisher":"World Scientific Publishing","day":"01","quality_controlled":"1","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"abstract":[{"text":"We introduce two-level discounted and mean-payoff games played by two players on a perfect-information stochastic game graph. The upper level game is a discounted or mean-payoff game and the lower level game is a (undiscounted) reachability game. Two-level games model hierarchical and sequential decision making under uncertainty across different time scales. For both discounted and mean-payoff two-level games, we show the existence of pure memoryless optimal strategies for both players and an ordered field property. We show that if there is only one player (Markov decision processes), then the values can be computed in polynomial time. It follows that whether the value of a player is equal to a given rational constant in two-level discounted or mean-payoff games can be decided in NP ∩ coNP. We also give an alternate strategy improvement algorithm to compute the value. © 2012 World Scientific Publishing Company.","lang":"eng"}],"volume":23,"date_created":"2018-12-11T12:02:37Z","date_updated":"2021-01-12T07:42:35Z","publication":"International Journal of Foundations of Computer Science","date_published":"2012-04-01T00:00:00Z"},{"place":"New York","day":"23","publisher":"Springer","_id":"10896","month":"07","author":[{"full_name":"zur Nedden, Stephanie","first_name":"Stephanie","id":"3C77F464-F248-11E8-B48F-1D18A9856A87","last_name":"zur Nedden"},{"last_name":"Doney","first_name":"Alexander S.","full_name":"Doney, Alexander S."},{"full_name":"Frenguelli, Bruno G.","first_name":"Bruno G.","last_name":"Frenguelli"}],"citation":{"ama":"zur Nedden S, Doney AS, Frenguelli BG. The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books. In: Masino S, Boison D, eds. Adenosine. 1st ed. New York: Springer; 2012:109-129. doi:10.1007/978-1-4614-3903-5_6","apa":"zur Nedden, S., Doney, A. S., & Frenguelli, B. G. (2012). The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books. In S. Masino & D. Boison (Eds.), Adenosine (1st ed., pp. 109–129). New York: Springer. https://doi.org/10.1007/978-1-4614-3903-5_6","short":"S. zur Nedden, A.S. Doney, B.G. Frenguelli, in:, S. Masino, D. Boison (Eds.), Adenosine, 1st ed., Springer, New York, 2012, pp. 109–129.","ieee":"S. zur Nedden, A. S. Doney, and B. G. Frenguelli, “The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books,” in Adenosine, 1st ed., S. Masino and D. Boison, Eds. New York: Springer, 2012, pp. 109–129.","mla":"zur Nedden, Stephanie, et al. “The Double-Edged Sword: Gaining Adenosine at the Expense of ATP. How to Balance the Books.” Adenosine, edited by Susan Masino and Detlev Boison, 1st ed., Springer, 2012, pp. 109–29, doi:10.1007/978-1-4614-3903-5_6.","chicago":"Nedden, Stephanie zur, Alexander S. Doney, and Bruno G. Frenguelli. “The Double-Edged Sword: Gaining Adenosine at the Expense of ATP. How to Balance the Books.” In Adenosine, edited by Susan Masino and Detlev Boison, 1st ed., 109–29. New York: Springer, 2012. https://doi.org/10.1007/978-1-4614-3903-5_6.","ista":"zur Nedden S, Doney AS, Frenguelli BG. 2012.The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books. In: Adenosine. , 109–129."},"department":[{"_id":"HaJa"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"Under physiological conditions the brain, via the purine salvage pathway, reuses the preformed purine bases hypoxanthine, derived from ATP degradation, and adenine (Ade), derived from polyamine synthesis, to restore its ATP pool. However, the massive degradation of ATP during ischemia, although providing valuable neuroprotective adenosine, results in the accumulation and loss of diffusible purine metabolites and thereby leads to a protracted reduction in the post-ischemic ATP pool size. In vivo, this may both limit the ability to deploy ATP-dependent reparative mechanisms and reduce the subsequent availability of adenosine, whilst in brain slices results in tissue with substantially lower levels of ATP than in vivo. In the present review, we describe the mechanisms by which brain tissue replenishes its ATP, how this can be improved with the clinically tolerated chemicals D-ribose and adenine, and the functional, and potential therapeutic, implications of doing so."}],"date_created":"2022-03-21T07:16:12Z","acknowledgement":"We are grateful to Research into Ageing/Ageing UK and The Dunhill Trust for funding SzN’s graduate studies, and to Prof Nicholas Dale for his valuable input.","edition":"1","language":[{"iso":"eng"}],"date_published":"2012-07-23T00:00:00Z","publication":"Adenosine","date_updated":"2022-06-21T11:51:58Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","editor":[{"last_name":"Masino","full_name":"Masino, Susan","first_name":"Susan"},{"last_name":"Boison","full_name":"Boison, Detlev","first_name":"Detlev"}],"publication_status":"published","article_processing_charge":"No","oa_version":"None","publication_identifier":{"isbn":["9781461439028"],"eisbn":["9781461439035"]},"status":"public","year":"2012","scopus_import":"1","title":"The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance the books","page":"109-129","type":"book_chapter","doi":"10.1007/978-1-4614-3903-5_6"},{"acknowledgement":"This work has been partially supported by the French ANR project Veridyc","publication":"Automated Technology for Verification and Analysis","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","location":"Thiruvananthapuram, India","end_date":"2012-10-06","start_date":"2012-10-03"},"date_published":"2012-10-15T00:00:00Z","month":"10","intvolume":" 7561","author":[{"last_name":"Bouajjani","full_name":"Bouajjani, Ahmed","first_name":"Ahmed"},{"first_name":"Cezara","full_name":"Dragoi, Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Enea","full_name":"Enea, Constantin","first_name":"Constantin"},{"full_name":"Sighireanu, Mihaela","first_name":"Mihaela","last_name":"Sighireanu"}],"place":"Berlin, Heidelberg","quality_controlled":"1","doi":"10.1007/978-3-642-33386-6_14","year":"2012","article_processing_charge":"No","publication_status":"published","oa_version":"None","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas."}],"date_created":"2022-03-21T07:58:39Z","volume":7561,"date_updated":"2023-09-05T14:07:24Z","citation":{"apa":"Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In Automated Technology for Verification and Analysis (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-33386-6_14","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:10.1007/978-3-642-33386-6_14","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In Automated Technology for Verification and Analysis, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-33386-6_14.","mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” Automated Technology for Verification and Analysis, vol. 7561, Springer, 2012, pp. 167–82, doi:10.1007/978-3-642-33386-6_14.","ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182.","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in Automated Technology for Verification and Analysis, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182."},"day":"15","publisher":"Springer","_id":"10903","series_title":"LNCS","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"type":"conference","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642333859"],"eissn":["1611-3349"],"eisbn":["9783642333866"]},"status":"public","title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","page":"167-182","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1"},{"quality_controlled":"1","place":"Berlin, Heidelberg","intvolume":" 7454","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Randour","full_name":"Randour, Mickael","first_name":"Mickael"},{"last_name":"Raskin","full_name":"Raskin, Jean-François","first_name":"Jean-François"}],"month":"09","date_published":"2012-09-15T00:00:00Z","conference":{"location":"Newcastle upon Tyne, United Kingdom","name":"CONCUR: Conference on Concurrency Theory","end_date":"2012-09-07","start_date":"2012-09-04"},"external_id":{"arxiv":["1201.5073"]},"publication":"CONCUR 2012 - Concurrency Theory","acknowledgement":"Author supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407 (RiSE), ERC Start Grant (279307: Graph Games), Microsoft faculty fellowship.","arxiv":1,"oa_version":"Preprint","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publication_status":"published","editor":[{"last_name":"Koutny","full_name":"Koutny, Maciej","first_name":"Maciej"},{"last_name":"Ulidowski","first_name":"Irek","full_name":"Ulidowski, Irek"}],"article_processing_charge":"No","year":"2012","doi":"10.1007/978-3-642-32940-1_10","related_material":{"record":[{"relation":"later_version","status":"public","id":"2716"}]},"alternative_title":["LNCS"],"department":[{"_id":"KrCh"}],"_id":"10904","publisher":"Springer","day":"15","citation":{"ieee":"K. Chatterjee, M. Randour, and J.-F. Raskin, “Strategy synthesis for multi-dimensional quantitative objectives,” in CONCUR 2012 - Concurrency Theory, Newcastle upon Tyne, United Kingdom, 2012, vol. 7454, pp. 115–131.","ista":"Chatterjee K, Randour M, Raskin J-F. 2012. Strategy synthesis for multi-dimensional quantitative objectives. CONCUR 2012 - Concurrency Theory. CONCUR: Conference on Concurrency Theory, LNCS, vol. 7454, 115–131.","mla":"Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” CONCUR 2012 - Concurrency Theory, edited by Maciej Koutny and Irek Ulidowski, vol. 7454, Springer, 2012, pp. 115–31, doi:10.1007/978-3-642-32940-1_10.","chicago":"Chatterjee, Krishnendu, Mickael Randour, and Jean-François Raskin. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” In CONCUR 2012 - Concurrency Theory, edited by Maciej Koutny and Irek Ulidowski, 7454:115–31. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-32940-1_10.","ama":"Chatterjee K, Randour M, Raskin J-F. Strategy synthesis for multi-dimensional quantitative objectives. In: Koutny M, Ulidowski I, eds. CONCUR 2012 - Concurrency Theory. Vol 7454. Berlin, Heidelberg: Springer; 2012:115-131. doi:10.1007/978-3-642-32940-1_10","apa":"Chatterjee, K., Randour, M., & Raskin, J.-F. (2012). Strategy synthesis for multi-dimensional quantitative objectives. In M. Koutny & I. Ulidowski (Eds.), CONCUR 2012 - Concurrency Theory (Vol. 7454, pp. 115–131). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-32940-1_10","short":"K. Chatterjee, M. Randour, J.-F. Raskin, in:, M. Koutny, I. Ulidowski (Eds.), CONCUR 2012 - Concurrency Theory, Springer, Berlin, Heidelberg, 2012, pp. 115–131."},"date_updated":"2023-02-23T10:55:06Z","abstract":[{"text":"Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.","lang":"eng"}],"date_created":"2022-03-21T08:00:21Z","volume":7454,"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"page":"115-131","publication_identifier":{"issn":["0302-9743","1611-3349"],"eisbn":["9783642329401"],"isbn":["9783642329395"]},"status":"public","scopus_import":"1","title":"Strategy synthesis for multi-dimensional quantitative objectives","type":"conference"},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","ec_funded":1,"status":"public","title":"Polynomial-time algorithms for energy games with special weight structures","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642330896"],"eisbn":["9783642330902"],"eissn":["1611-3349"]},"page":"301-312","type":"conference","alternative_title":["LNCS"],"department":[{"_id":"KrCh"}],"day":"01","_id":"10905","publisher":"Springer","citation":{"ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” in Algorithms – ESA 2012, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” In Algorithms – ESA 2012, 7501:301–12. Springer, 2012. https://doi.org/10.1007/978-3-642-33090-2_27.","mla":"Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithms – ESA 2012, vol. 7501, Springer, 2012, pp. 301–12, doi:10.1007/978-3-642-33090-2_27.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2012. Polynomial-time algorithms for energy games with special weight structures. Algorithms – ESA 2012. ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.","short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms – ESA 2012, Springer, 2012, pp. 301–312.","ama":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. In: Algorithms – ESA 2012. Vol 7501. Springer; 2012:301-312. doi:10.1007/978-3-642-33090-2_27","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2012). Polynomial-time algorithms for energy games with special weight structures. In Algorithms – ESA 2012 (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer. https://doi.org/10.1007/978-3-642-33090-2_27"},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.08234"}],"date_updated":"2023-09-05T14:09:30Z","date_created":"2022-03-21T08:01:45Z","volume":7501,"abstract":[{"lang":"eng","text":"Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While the existence of polynomial-time algorithms has been a major open problem for decades, there is no algorithm that solves any non-trivial subclass in polynomial time.\r\nIn this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several counter examples that show that many previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting graph structures need not help."}],"language":[{"iso":"eng"}],"oa_version":"Preprint","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publication_status":"published","article_processing_charge":"No","year":"2012","doi":"10.1007/978-3-642-33090-2_27","related_material":{"record":[{"id":"535","relation":"later_version","status":"public"}]},"quality_controlled":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Monika H","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Krinninger","full_name":"Krinninger, Sebastian","first_name":"Sebastian"},{"last_name":"Nanongkai","first_name":"Danupon","full_name":"Nanongkai, Danupon"}],"intvolume":" 7501","month":"10","conference":{"location":"Ljubljana, Slovenia","name":"ESA: European Symposium on Algorithms","end_date":"2012-09-12","start_date":"2012-09-10"},"date_published":"2012-10-01T00:00:00Z","publication":"Algorithms – ESA 2012","external_id":{"arxiv":["1604.08234"]},"arxiv":1,"acknowledgement":"Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games), and a Microsoft Faculty Fellows Award"},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","type":"conference","page":"549-551","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783642287565"],"eissn":["1611-3349"],"isbn":["9783642287558"]},"title":"HSF(C): A software verifier based on Horn clauses","status":"public","scopus_import":"1","citation":{"short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.","ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-28756-5_46.","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:10.1007/978-3-642-28756-5_46."},"_id":"10906","publisher":"Springer","series_title":"LNCS","day":"01","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}],"date_created":"2022-03-21T08:03:30Z","abstract":[{"text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.","lang":"eng"}],"volume":7214,"date_updated":"2023-09-05T14:09:54Z","main_file_link":[{"url":"https://doi.org/10.1007/978-3-642-28756-5_46","open_access":"1"}],"oa":1,"article_processing_charge":"No","publication_status":"published","editor":[{"full_name":"Flanagan, Cormac","first_name":"Cormac","last_name":"Flanagan"},{"full_name":"König, Barbara","first_name":"Barbara","last_name":"König"}],"oa_version":"Published Version","doi":"10.1007/978-3-642-28756-5_46","year":"2012","month":"04","author":[{"full_name":"Grebenshchikov, Sergey","first_name":"Sergey","last_name":"Grebenshchikov"},{"first_name":"Ashutosh","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta"},{"last_name":"Lopes","first_name":"Nuno P.","full_name":"Lopes, Nuno P."},{"first_name":"Corneliu","full_name":"Popeea, Corneliu","last_name":"Popeea"},{"last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey","first_name":"Andrey"}],"intvolume":" 7214","place":"Berlin, Heidelberg","quality_controlled":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems","date_published":"2012-04-01T00:00:00Z","conference":{"end_date":"2012-04-01","start_date":"2012-03-24","location":"Tallinn, Estonia","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"}},{"alternative_title":["IST Austria Technical Report"],"department":[{"_id":"KrCh"}],"day":"16","_id":"5387","publisher":"IST Austria","pubrep_id":"23","month":"02","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"citation":{"ieee":"K. Chatterjee and L. Doyen, Energy and mean-payoff parity Markov decision processes. IST Austria, 2011.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. Energy and Mean-Payoff Parity Markov Decision Processes. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0001.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. Energy and Mean-Payoff Parity Markov Decision Processes. IST Austria, 2011, doi:10.15479/AT:IST-2011-0001.","ista":"Chatterjee K, Doyen L. 2011. Energy and mean-payoff parity Markov decision processes, IST Austria, 20p.","short":"K. Chatterjee, L. Doyen, Energy and Mean-Payoff Parity Markov Decision Processes, IST Austria, 2011.","ama":"Chatterjee K, Doyen L. Energy and Mean-Payoff Parity Markov Decision Processes. IST Austria; 2011. doi:10.15479/AT:IST-2011-0001","apa":"Chatterjee, K., & Doyen, L. (2011). Energy and mean-payoff parity Markov decision processes. IST Austria. https://doi.org/10.15479/AT:IST-2011-0001"},"date_published":"2011-02-16T00:00:00Z","oa":1,"date_updated":"2023-02-23T11:23:11Z","date_created":"2018-12-12T11:39:02Z","abstract":[{"lang":"eng","text":"We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound."}],"language":[{"iso":"eng"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","file_date_updated":"2020-07-14T12:46:41Z","year":"2011","status":"public","publication_identifier":{"issn":["2664-1690"]},"title":"Energy and mean-payoff parity Markov decision processes","page":"20","type":"technical_report","has_accepted_license":"1","file":[{"checksum":"824d6c70e6d3feb3e836b009e0b3cf73","file_size":329976,"file_id":"5458","date_updated":"2020-07-14T12:46:41Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"system","date_created":"2018-12-12T11:52:57Z","file_name":"IST-2011-0001_IST-2011-0001.pdf"}],"doi":"10.15479/AT:IST-2011-0001","ddc":["000","005"],"related_material":{"record":[{"id":"3345","relation":"later_version","status":"public"}]}},{"quality_controlled":"1","intvolume":" 101","author":[{"first_name":"Heungwon","full_name":"Park, Heungwon","last_name":"Park"},{"first_name":"Panos","full_name":"Oikonomou, Panos","last_name":"Oikonomou"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","orcid":"0000-0001-6220-2052","full_name":"Guet, Calin C","first_name":"Calin C"},{"first_name":"Philippe","full_name":"Cluzel, Philippe","last_name":"Cluzel"}],"month":"11","publication":"Biophysical Journal","external_id":{"pmid":["22098731"]},"date_published":"2011-11-16T00:00:00Z","pmid":1,"oa_version":"Published Version","article_processing_charge":"No","publication_status":"published","doi":"10.1016/j.bpj.2011.09.040","year":"2011","department":[{"_id":"CaGu"}],"citation":{"apa":"Park, H., Oikonomou, P., Guet, C. C., & Cluzel, P. (2011). Noise underlies switching behavior of the bacterial flagellum. Biophysical Journal. Elsevier. https://doi.org/10.1016/j.bpj.2011.09.040","ama":"Park H, Oikonomou P, Guet CC, Cluzel P. Noise underlies switching behavior of the bacterial flagellum. Biophysical Journal. 2011;101(10):2336-2340. doi:10.1016/j.bpj.2011.09.040","short":"H. Park, P. Oikonomou, C.C. Guet, P. Cluzel, Biophysical Journal 101 (2011) 2336–2340.","chicago":"Park, Heungwon, Panos Oikonomou, Calin C Guet, and Philippe Cluzel. “Noise Underlies Switching Behavior of the Bacterial Flagellum.” Biophysical Journal. Elsevier, 2011. https://doi.org/10.1016/j.bpj.2011.09.040.","mla":"Park, Heungwon, et al. “Noise Underlies Switching Behavior of the Bacterial Flagellum.” Biophysical Journal, vol. 101, no. 10, Elsevier, 2011, pp. 2336–40, doi:10.1016/j.bpj.2011.09.040.","ista":"Park H, Oikonomou P, Guet CC, Cluzel P. 2011. Noise underlies switching behavior of the bacterial flagellum. Biophysical Journal. 101(10), 2336–2340.","ieee":"H. Park, P. Oikonomou, C. C. Guet, and P. Cluzel, “Noise underlies switching behavior of the bacterial flagellum,” Biophysical Journal, vol. 101, no. 10. Elsevier, pp. 2336–2340, 2011."},"publisher":"Elsevier","_id":"6496","day":"16","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3218319/"}],"date_updated":"2021-04-16T11:54:49Z","oa":1,"language":[{"iso":"eng"}],"volume":101,"abstract":[{"text":"We report the switching behavior of the full bacterial flagellum system that includes the filament and the motor in wild-type Escherichia coli cells. In sorting the motor behavior by the clockwise bias, we find that the distributions of the clockwise (CW) and counterclockwise (CCW) intervals are either exponential or nonexponential with long tails. At low bias, CW intervals are exponentially distributed and CCW intervals exhibit long tails. At intermediate CW bias (0.5) both CW and CCW intervals are mainly exponentially distributed. A simple model suggests that these two distinct switching behaviors are governed by the presence of signaling noise within the chemotaxis network. Low noise yields exponentially distributed intervals, whereas large noise yields nonexponential behavior with long tails. These drastically different motor statistics may play a role in optimizing bacterial behavior for a wide range of environmental conditions.","lang":"eng"}],"date_created":"2019-05-28T11:54:29Z","issue":"10","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","page":"2336-2340","status":"public","title":"Noise underlies switching behavior of the bacterial flagellum","publication_identifier":{"issn":["0006-3495"]},"scopus_import":"1"},{"doi":"10.1073/pnas.1019273108","year":"2011","oa_version":"Published Version","article_processing_charge":"No","publication_status":"published","publication":"Proceedings of the National Academy of Sciences","external_id":{"pmid":["21257907"]},"date_published":"2011-02-01T00:00:00Z","pmid":1,"quality_controlled":"1","intvolume":" 108","month":"02","author":[{"full_name":"Hsieh, Tzung-Fu","first_name":"Tzung-Fu","last_name":"Hsieh"},{"last_name":"Shin","full_name":"Shin, Juhyun","first_name":"Juhyun"},{"last_name":"Uzawa","first_name":"Rie","full_name":"Uzawa, Rie"},{"last_name":"Silva","full_name":"Silva, Pedro","first_name":"Pedro"},{"last_name":"Cohen","first_name":"Stephanie","full_name":"Cohen, Stephanie"},{"first_name":"Matthew J.","full_name":"Bauer, Matthew J.","last_name":"Bauer"},{"full_name":"Hashimoto, Meryl","first_name":"Meryl","last_name":"Hashimoto"},{"last_name":"Kirkbride","first_name":"Ryan C.","full_name":"Kirkbride, Ryan C."},{"last_name":"Harada","full_name":"Harada, John J.","first_name":"John J."},{"first_name":"Daniel","full_name":"Zilberman, Daniel","orcid":"0000-0002-0123-8649","last_name":"Zilberman","id":"6973db13-dd5f-11ea-814e-b3e5455e9ed1"},{"full_name":"Fischer, Robert L.","first_name":"Robert L.","last_name":"Fischer"}],"extern":"1","type":"journal_article","status":"public","publication_identifier":{"issn":["0027-8424"],"eissn":["1091-6490"]},"scopus_import":"1","title":"Regulation of imprinted gene expression in Arabidopsis endosperm","page":"1755-1762","issue":"5","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_type":"original","date_updated":"2021-12-14T08:33:49Z","main_file_link":[{"url":"https://doi.org/10.1073/pnas.1019273108","open_access":"1"}],"oa":1,"language":[{"iso":"eng"}],"volume":108,"date_created":"2021-06-07T07:40:38Z","abstract":[{"text":"Imprinted genes are expressed primarily or exclusively from either the maternal or paternal allele, a phenomenon that occurs in flowering plants and mammals. Flowering plant imprinted gene expression has been described primarily in endosperm, a terminal nutritive tissue consumed by the embryo during seed development or after germination. Imprinted expression in Arabidopsis thaliana endosperm is orchestrated by differences in cytosine DNA methylation between the paternal and maternal genomes as well as by Polycomb group proteins. Currently, only 11 imprinted A. thaliana genes are known. Here, we use extensive sequencing of cDNA libraries to identify 9 paternally expressed and 34 maternally expressed imprinted genes in A. thaliana endosperm that are regulated by the DNA-demethylating glycosylase DEMETER, the DNA methyltransferase MET1, and/or the core Polycomb group protein FIE. These genes encode transcription factors, proteins involved in hormone signaling, components of the ubiquitin protein degradation pathway, regulators of histone and DNA methylation, and small RNA pathway proteins. We also identify maternally expressed genes that may be regulated by unknown mechanisms or deposited from maternal tissues. We did not detect any imprinted genes in the embryo. Our results show that imprinted gene expression is an extensive mechanistically complex phenomenon that likely affects multiple aspects of seed development.","lang":"eng"}],"department":[{"_id":"DaZi"}],"citation":{"ama":"Hsieh T-F, Shin J, Uzawa R, et al. Regulation of imprinted gene expression in Arabidopsis endosperm. Proceedings of the National Academy of Sciences. 2011;108(5):1755-1762. doi:10.1073/pnas.1019273108","apa":"Hsieh, T.-F., Shin, J., Uzawa, R., Silva, P., Cohen, S., Bauer, M. J., … Fischer, R. L. (2011). Regulation of imprinted gene expression in Arabidopsis endosperm. Proceedings of the National Academy of Sciences. National Academy of Sciences. https://doi.org/10.1073/pnas.1019273108","short":"T.-F. Hsieh, J. Shin, R. Uzawa, P. Silva, S. Cohen, M.J. Bauer, M. Hashimoto, R.C. Kirkbride, J.J. Harada, D. Zilberman, R.L. Fischer, Proceedings of the National Academy of Sciences 108 (2011) 1755–1762.","ieee":"T.-F. Hsieh et al., “Regulation of imprinted gene expression in Arabidopsis endosperm,” Proceedings of the National Academy of Sciences, vol. 108, no. 5. National Academy of Sciences, pp. 1755–1762, 2011.","chicago":"Hsieh, Tzung-Fu, Juhyun Shin, Rie Uzawa, Pedro Silva, Stephanie Cohen, Matthew J. Bauer, Meryl Hashimoto, et al. “Regulation of Imprinted Gene Expression in Arabidopsis Endosperm.” Proceedings of the National Academy of Sciences. National Academy of Sciences, 2011. https://doi.org/10.1073/pnas.1019273108.","ista":"Hsieh T-F, Shin J, Uzawa R, Silva P, Cohen S, Bauer MJ, Hashimoto M, Kirkbride RC, Harada JJ, Zilberman D, Fischer RL. 2011. Regulation of imprinted gene expression in Arabidopsis endosperm. Proceedings of the National Academy of Sciences. 108(5), 1755–1762.","mla":"Hsieh, Tzung-Fu, et al. “Regulation of Imprinted Gene Expression in Arabidopsis Endosperm.” Proceedings of the National Academy of Sciences, vol. 108, no. 5, National Academy of Sciences, 2011, pp. 1755–62, doi:10.1073/pnas.1019273108."},"day":"01","_id":"9483","publisher":"National Academy of Sciences"},{"type":"other_academic_publication","page":"735-736","publication_identifier":{"issn":["1534-5807"],"eissn":["1878-1551"]},"title":"Balancing parental contributions in plant embryonic gene activation","status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","issue":"6","language":[{"iso":"eng"}],"volume":20,"date_created":"2021-06-08T06:23:39Z","abstract":[{"text":"Little is known about chromatin remodeling events immediately after fertilization. A recent report by Autran et al. (2011) in Cell now shows that chromatin regulatory pathways that silence transposable elements are responsible for global delayed activation of gene expression in the early Arabidopsis embryo.","lang":"eng"}],"main_file_link":[{"url":"https://doi.org/10.1016/j.devcel.2011.05.018","open_access":"1"}],"date_updated":"2021-12-14T08:34:37Z","oa":1,"citation":{"mla":"Zilberman, Daniel. “Balancing Parental Contributions in Plant Embryonic Gene Activation.” Developmental Cell, vol. 20, no. 6, Elsevier, 2011, pp. 735–36, doi:10.1016/j.devcel.2011.05.018.","ista":"Zilberman D. 2011. Balancing parental contributions in plant embryonic gene activation, Elsevier,p.","chicago":"Zilberman, Daniel. Balancing Parental Contributions in Plant Embryonic Gene Activation. Developmental Cell. Vol. 20. Elsevier, 2011. https://doi.org/10.1016/j.devcel.2011.05.018.","ieee":"D. Zilberman, Balancing parental contributions in plant embryonic gene activation, vol. 20, no. 6. Elsevier, 2011, pp. 735–736.","apa":"Zilberman, D. (2011). Balancing parental contributions in plant embryonic gene activation. Developmental Cell (Vol. 20, pp. 735–736). Elsevier. https://doi.org/10.1016/j.devcel.2011.05.018","ama":"Zilberman D. Balancing Parental Contributions in Plant Embryonic Gene Activation. Vol 20. Elsevier; 2011:735-736. doi:10.1016/j.devcel.2011.05.018","short":"D. Zilberman, Balancing Parental Contributions in Plant Embryonic Gene Activation, Elsevier, 2011."},"_id":"9522","publisher":"Elsevier","day":"14","department":[{"_id":"DaZi"}],"doi":"10.1016/j.devcel.2011.05.018","year":"2011","article_processing_charge":"No","publication_status":"published","oa_version":"Published Version","pmid":1,"external_id":{"pmid":["21664571"]},"publication":"Developmental Cell","date_published":"2011-06-14T00:00:00Z","intvolume":" 20","author":[{"orcid":"0000-0002-0123-8649","first_name":"Daniel","full_name":"Zilberman, Daniel","id":"6973db13-dd5f-11ea-814e-b3e5455e9ed1","last_name":"Zilberman"}],"month":"06","extern":"1","quality_controlled":"1"},{"date_published":"2011-08-01T00:00:00Z","conference":{"end_date":"2011-08-31","start_date":"2011-08-29","name":"CAIP: International Conference on Computer Analysis of Images and Patterns","location":"Seville, Spain"},"publication":"Computer Analysis of Images and Patterns","quality_controlled":"1","intvolume":" 6854","author":[{"last_name":"Gonzalez-Diaz","full_name":"Gonzalez-Diaz, Rocio","first_name":"Rocio"},{"last_name":"Ion","id":"29F89302-F248-11E8-B48F-1D18A9856A87","full_name":"Ion, Adrian","first_name":"Adrian"},{"last_name":"Jimenez","full_name":"Jimenez, Maria Jose","first_name":"Maria Jose"},{"last_name":"Poyatos","first_name":"Regina","full_name":"Poyatos, Regina"}],"month":"08","year":"2011","doi":"10.1007/978-3-642-23672-3_35","oa_version":"Published Version","publication_status":"published","article_processing_charge":"No","oa":1,"date_updated":"2021-08-12T13:53:17Z","main_file_link":[{"open_access":"1","url":"http://hdl.handle.net/11441/30766"}],"abstract":[{"text":"In this paper, we establish a correspondence between the incremental algorithm for computing AT-models [8,9] and the one for computing persistent homology [6,14,15]. We also present a decremental algorithm for computing AT-models that allows to extend the persistence computation to a wider setting. Finally, we show how to combine incremental and decremental techniques for persistent homology computation.","lang":"eng"}],"date_created":"2021-07-11T22:01:19Z","volume":6854,"language":[{"iso":"eng"}],"department":[{"_id":"HeEd"}],"alternative_title":["LNCS"],"publisher":"Springer Nature","_id":"9648","day":"01","citation":{"apa":"Gonzalez-Diaz, R., Ion, A., Jimenez, M. J., & Poyatos, R. (2011). Incremental-decremental algorithm for computing AT-models and persistent homology. In Computer Analysis of Images and Patterns (Vol. 6854, pp. 286–293). Seville, Spain: Springer Nature. https://doi.org/10.1007/978-3-642-23672-3_35","ama":"Gonzalez-Diaz R, Ion A, Jimenez MJ, Poyatos R. Incremental-decremental algorithm for computing AT-models and persistent homology. In: Computer Analysis of Images and Patterns. Vol 6854. Springer Nature; 2011:286-293. doi:10.1007/978-3-642-23672-3_35","short":"R. Gonzalez-Diaz, A. Ion, M.J. Jimenez, R. Poyatos, in:, Computer Analysis of Images and Patterns, Springer Nature, 2011, pp. 286–293.","ista":"Gonzalez-Diaz R, Ion A, Jimenez MJ, Poyatos R. 2011. Incremental-decremental algorithm for computing AT-models and persistent homology. Computer Analysis of Images and Patterns. CAIP: International Conference on Computer Analysis of Images and Patterns, LNCS, vol. 6854, 286–293.","mla":"Gonzalez-Diaz, Rocio, et al. “Incremental-Decremental Algorithm for Computing AT-Models and Persistent Homology.” Computer Analysis of Images and Patterns, vol. 6854, Springer Nature, 2011, pp. 286–93, doi:10.1007/978-3-642-23672-3_35.","chicago":"Gonzalez-Diaz, Rocio, Adrian Ion, Maria Jose Jimenez, and Regina Poyatos. “Incremental-Decremental Algorithm for Computing AT-Models and Persistent Homology.” In Computer Analysis of Images and Patterns, 6854:286–93. Springer Nature, 2011. https://doi.org/10.1007/978-3-642-23672-3_35.","ieee":"R. Gonzalez-Diaz, A. Ion, M. J. Jimenez, and R. Poyatos, “Incremental-decremental algorithm for computing AT-models and persistent homology,” in Computer Analysis of Images and Patterns, Seville, Spain, 2011, vol. 6854, pp. 286–293."},"page":"286-293","status":"public","publication_identifier":{"isbn":["9783642236716"],"eissn":["16113349"],"issn":["03029743"]},"title":"Incremental-decremental algorithm for computing AT-models and persistent homology","scopus_import":"1","type":"conference","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf"},{"year":"2011","status":"public","title":"Data from: Effect of oceanographic barriers and overfishing on the population genetic structure of the European spiny lobster (Palinurus elephas)","type":"research_data_reference","doi":"10.5061/dryad.299h8","related_material":{"record":[{"id":"3395","relation":"used_in_publication","status":"public"}]},"oa_version":"Published Version","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","article_processing_charge":"No","oa":1,"date_published":"2011-05-12T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5061/dryad.299h8"}],"date_updated":"2023-02-23T11:25:25Z","abstract":[{"text":"Defining population structure and genetic diversity levels is of the utmost importance for developing efficient conservation strategies. Overfishing has caused mean annual catches of the European spiny lobster (Palinurus elephas) to decrease alarmingly along its distribution area. In this context, there is a need for comprehensive studies to evaluate the genetic health of the exploited populations. The present work is based on a set of 10 nuclear markers amplified in 331 individuals from 10 different localities covering most of P. elephas distribution area. Samples from Atlantic and Mediterranean basins showed small but significant differences, indicating that P. elephas populations do not behave as a single panmictic unit but form two partially-overlapping groups. Despite intense overfishing, our dataset did not recover a recent bottleneck signal, and showed a large and stable historical effective size instead. This result could be accounted for by specific life history traits (reproduction and longevity) and the limitations of molecular markers in covering very recent timescales for non temporal samples. Our study emphasizes the necessity of integrating information on effective population sizes and life history parameters when evaluating population connectivity levels from genetic data.","lang":"eng"}],"date_created":"2021-08-02T07:11:19Z","department":[{"_id":"NiBa"}],"day":"12","_id":"9762","publisher":"IST Austria","month":"05","author":[{"last_name":"Palero","id":"3F0E2A22-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0343-8329","full_name":"Palero, Ferran","first_name":"Ferran"},{"first_name":"Pere","full_name":"Abello, Pere","last_name":"Abello"},{"first_name":"Enrique","full_name":"Macpherson, Enrique","last_name":"Macpherson"},{"last_name":"Beaumont","first_name":"Mark","full_name":"Beaumont, Mark"},{"first_name":"Marta","full_name":"Pascual, Marta","last_name":"Pascual"}],"citation":{"short":"F. Palero, P. Abello, E. Macpherson, M. Beaumont, M. Pascual, (2011).","ama":"Palero F, Abello P, Macpherson E, Beaumont M, Pascual M. Data from: Effect of oceanographic barriers and overfishing on the population genetic structure of the European spiny lobster (Palinurus elephas). 2011. doi:10.5061/dryad.299h8","apa":"Palero, F., Abello, P., Macpherson, E., Beaumont, M., & Pascual, M. (2011). Data from: Effect of oceanographic barriers and overfishing on the population genetic structure of the European spiny lobster (Palinurus elephas). IST Austria. https://doi.org/10.5061/dryad.299h8","ieee":"F. Palero, P. Abello, E. Macpherson, M. Beaumont, and M. Pascual, “Data from: Effect of oceanographic barriers and overfishing on the population genetic structure of the European spiny lobster (Palinurus elephas).” IST Austria, 2011.","ista":"Palero F, Abello P, Macpherson E, Beaumont M, Pascual M. 2011. Data from: Effect of oceanographic barriers and overfishing on the population genetic structure of the European spiny lobster (Palinurus elephas), IST Austria, 10.5061/dryad.299h8.","chicago":"Palero, Ferran, Pere Abello, Enrique Macpherson, Mark Beaumont, and Marta Pascual. “Data from: Effect of Oceanographic Barriers and Overfishing on the Population Genetic Structure of the European Spiny Lobster (Palinurus Elephas).” IST Austria, 2011. https://doi.org/10.5061/dryad.299h8.","mla":"Palero, Ferran, et al. Data from: Effect of Oceanographic Barriers and Overfishing on the Population Genetic Structure of the European Spiny Lobster (Palinurus Elephas). IST Austria, 2011, doi:10.5061/dryad.299h8."}},{"citation":{"apa":"Eggermann, E., & Jonas, P. M. (2011). How the “slow” Ca(2+) buffer parvalbumin affects transmitter release in nanodomain coupling regimes at GABAergic synapses. Nature Neuroscience. Nature Publishing Group. https://doi.org/10.1038/nn.3002","ama":"Eggermann E, Jonas PM. How the “slow” Ca(2+) buffer parvalbumin affects transmitter release in nanodomain coupling regimes at GABAergic synapses. Nature Neuroscience. 2011;15:20-22. doi:10.1038/nn.3002","short":"E. Eggermann, P.M. Jonas, Nature Neuroscience 15 (2011) 20–22.","chicago":"Eggermann, Emmanuel, and Peter M Jonas. “How the ‘Slow’ Ca(2+) Buffer Parvalbumin Affects Transmitter Release in Nanodomain Coupling Regimes at GABAergic Synapses.” Nature Neuroscience. Nature Publishing Group, 2011. https://doi.org/10.1038/nn.3002.","ista":"Eggermann E, Jonas PM. 2011. How the “slow” Ca(2+) buffer parvalbumin affects transmitter release in nanodomain coupling regimes at GABAergic synapses. Nature Neuroscience. 15, 20–22.","mla":"Eggermann, Emmanuel, and Peter M. Jonas. “How the ‘Slow’ Ca(2+) Buffer Parvalbumin Affects Transmitter Release in Nanodomain Coupling Regimes at GABAergic Synapses.” Nature Neuroscience, vol. 15, Nature Publishing Group, 2011, pp. 20–22, doi:10.1038/nn.3002.","ieee":"E. Eggermann and P. M. Jonas, “How the ‘slow’ Ca(2+) buffer parvalbumin affects transmitter release in nanodomain coupling regimes at GABAergic synapses,” Nature Neuroscience, vol. 15. Nature Publishing Group, pp. 20–22, 2011."},"month":"12","author":[{"last_name":"Eggermann","first_name":"Emmanuel","full_name":"Eggermann, Emmanuel"},{"orcid":"0000-0001-5001-4804","full_name":"Jonas, Peter M","first_name":"Peter M","id":"353C1B58-F248-11E8-B48F-1D18A9856A87","last_name":"Jonas"}],"intvolume":" 15","publisher":"Nature Publishing Group","_id":"3318","day":"04","quality_controlled":"1","department":[{"_id":"PeJo"}],"language":[{"iso":"eng"}],"volume":15,"abstract":[{"lang":"eng","text":"Parvalbumin is thought to act in a manner similar to EGTA, but how a slow Ca2+ buffer affects nanodomain-coupling regimes at GABAergic synapses is unclear. Direct measurements of parvalbumin concentration and paired recordings in rodent hippocampus and cerebellum revealed that parvalbumin affects synaptic dynamics only when expressed at high levels. Modeling suggests that, in high concentrations, parvalbumin may exert BAPTA-like effects, modulating nanodomain coupling via competition with local saturation of endogenous fixed buffers."}],"date_created":"2018-12-11T12:02:38Z","date_updated":"2021-01-12T07:42:37Z","main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3631701/"}],"publication":"Nature Neuroscience","date_published":"2011-12-04T00:00:00Z","oa":1,"publication_status":"published","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","doi":"10.1038/nn.3002","type":"journal_article","publist_id":"3321","page":"20 - 22","title":"How the “slow” Ca(2+) buffer parvalbumin affects transmitter release in nanodomain coupling regimes at GABAergic synapses","status":"public","year":"2011","scopus_import":1},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","article_processing_charge":"No","oa_version":"None","status":"public","year":"2011","scopus_import":"1","title":"Learning multi-view neighborhood preserving projections","page":"425 - 432","publist_id":"3316","type":"conference","day":"01","publisher":"ML Research Press","_id":"3319","month":"01","author":[{"last_name":"Quadrianto","first_name":"Novi","full_name":"Quadrianto, Novi"},{"last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8622-7887","full_name":"Lampert, Christoph","first_name":"Christoph"}],"citation":{"short":"N. Quadrianto, C. Lampert, in:, ML Research Press, 2011, pp. 425–432.","apa":"Quadrianto, N., & Lampert, C. (2011). Learning multi-view neighborhood preserving projections (pp. 425–432). Presented at the ICML: International Conference on Machine Learning, Bellevue, United States: ML Research Press.","ama":"Quadrianto N, Lampert C. Learning multi-view neighborhood preserving projections. In: ML Research Press; 2011:425-432.","chicago":"Quadrianto, Novi, and Christoph Lampert. “Learning Multi-View Neighborhood Preserving Projections,” 425–32. ML Research Press, 2011.","mla":"Quadrianto, Novi, and Christoph Lampert. Learning Multi-View Neighborhood Preserving Projections. ML Research Press, 2011, pp. 425–32.","ista":"Quadrianto N, Lampert C. 2011. Learning multi-view neighborhood preserving projections. ICML: International Conference on Machine Learning, 425–432.","ieee":"N. Quadrianto and C. Lampert, “Learning multi-view neighborhood preserving projections,” presented at the ICML: International Conference on Machine Learning, Bellevue, United States, 2011, pp. 425–432."},"department":[{"_id":"ChLa"}],"abstract":[{"text":"We address the problem of metric learning for multi-view data, namely the construction of embedding projections from data in different representations into a shared feature space, such that the Euclidean distance in this space provides a meaningful within-view as well as between-view similarity. Our motivation stems from the problem of cross-media retrieval tasks, where the availability of a joint Euclidean distance function is a pre-requisite to allow fast, in particular hashing-based, nearest neighbor queries. We formulate an objective function that expresses the intuitive concept that matching samples are mapped closely together in the output space, whereas non-matching samples are pushed apart, no matter in which view they are available. The resulting optimization problem is not convex, but it can be decomposed explicitly into a convex and a concave part, thereby allowing efficient optimization using the convex-concave procedure. Experiments on an image retrieval task show that nearest-neighbor based cross-view retrieval is indeed possible, and the proposed technique improves the retrieval accuracy over baseline techniques.","lang":"eng"}],"date_created":"2018-12-11T12:02:39Z","language":[{"iso":"eng"}],"conference":{"location":"Bellevue, United States","name":"ICML: International Conference on Machine Learning","end_date":"2011-07-02","start_date":"2011-06-28"},"date_published":"2011-01-01T00:00:00Z","date_updated":"2023-10-17T11:59:50Z"},{"issue":"3-4","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2020-07-14T12:46:07Z","status":"public","title":"Structured learning and prediction in computer vision","scopus_import":"1","page":"185 - 365","type":"journal_article","publist_id":"3315","department":[{"_id":"ChLa"}],"day":"23","_id":"3320","publisher":"Now Publishers","citation":{"ieee":"S. Nowozin and C. Lampert, “Structured learning and prediction in computer vision,” Foundations and Trends in Computer Graphics and Vision, vol. 6, no. 3–4. Now Publishers, pp. 185–365, 2011.","ista":"Nowozin S, Lampert C. 2011. Structured learning and prediction in computer vision. Foundations and Trends in Computer Graphics and Vision. 6(3–4), 185–365.","mla":"Nowozin, Sebastian, and Christoph Lampert. “Structured Learning and Prediction in Computer Vision.” Foundations and Trends in Computer Graphics and Vision, vol. 6, no. 3–4, Now Publishers, 2011, pp. 185–365, doi:10.1561/0600000033.","chicago":"Nowozin, Sebastian, and Christoph Lampert. “Structured Learning and Prediction in Computer Vision.” Foundations and Trends in Computer Graphics and Vision. Now Publishers, 2011. https://doi.org/10.1561/0600000033.","short":"S. Nowozin, C. Lampert, Foundations and Trends in Computer Graphics and Vision 6 (2011) 185–365.","ama":"Nowozin S, Lampert C. Structured learning and prediction in computer vision. Foundations and Trends in Computer Graphics and Vision. 2011;6(3-4):185-365. doi:10.1561/0600000033","apa":"Nowozin, S., & Lampert, C. (2011). Structured learning and prediction in computer vision. Foundations and Trends in Computer Graphics and Vision. Now Publishers. https://doi.org/10.1561/0600000033"},"oa":1,"date_updated":"2023-10-17T11:52:46Z","article_type":"original","abstract":[{"text":"Powerful statistical models that can be learned efficiently from large amounts of data are currently revolutionizing computer vision. These models possess a rich internal structure reflecting task-specific relations and constraints. This monograph introduces the reader to the most popular classes of structured models in computer vision. Our focus is discrete undirected graphical models which we cover in detail together with a description of algorithms for both probabilistic inference and maximum a posteriori inference. We discuss separately recently successful techniques for prediction in general structured models. In the second part of this monograph we describe methods for parameter learning where we distinguish the classic maximum likelihood based methods from the more recent prediction-based parameter learning methods. We highlight developments to enhance current models and discuss kernelized models and latent variable models. To make the monograph more practical and to provide links to further study we provide examples of successful application of many methods in the computer vision literature.","lang":"eng"}],"date_created":"2018-12-11T12:02:39Z","volume":6,"language":[{"iso":"eng"}],"oa_version":"Published Version","publication_status":"published","article_processing_charge":"No","year":"2011","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"7837","date_updated":"2020-07-14T12:46:07Z","file_name":"2011_CompGraphicsVision_Nowozin.pdf","date_created":"2020-05-14T14:34:47Z","creator":"dernst","access_level":"open_access","file_size":3745064,"checksum":"f1043ef389f1558e2a226bb51568511f"}],"has_accepted_license":"1","doi":"10.1561/0600000033","ddc":["000"],"quality_controlled":"1","intvolume":" 6","month":"05","author":[{"last_name":"Nowozin","full_name":"Nowozin, Sebastian","first_name":"Sebastian"},{"last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8622-7887","first_name":"Christoph","full_name":"Lampert, Christoph"}],"date_published":"2011-05-23T00:00:00Z","publication":"Foundations and Trends in Computer Graphics and Vision"},{"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","oa_version":"None","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3163"}]},"type":"conference_poster","publist_id":"3313","title":"Maximum margin multi label structured prediction","year":"2011","status":"public","author":[{"first_name":"Christoph","orcid":"0000-0001-8622-7887","full_name":"Lampert, Christoph","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","last_name":"Lampert"}],"month":"12","citation":{"ama":"Lampert C. Maximum Margin Multi Label Structured Prediction. Neural Information Processing Systems Foundation; 2011.","apa":"Lampert, C. (2011). Maximum margin multi label structured prediction. NIPS: Neural Information Processing Systems. Neural Information Processing Systems Foundation.","short":"C. Lampert, Maximum Margin Multi Label Structured Prediction, Neural Information Processing Systems Foundation, 2011.","ieee":"C. Lampert, Maximum margin multi label structured prediction. Neural Information Processing Systems Foundation, 2011.","mla":"Lampert, Christoph. “Maximum Margin Multi Label Structured Prediction.” NIPS: Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2011.","chicago":"Lampert, Christoph. Maximum Margin Multi Label Structured Prediction. NIPS: Neural Information Processing Systems. Neural Information Processing Systems Foundation, 2011.","ista":"Lampert C. 2011. Maximum margin multi label structured prediction, Neural Information Processing Systems Foundation,p."},"day":"13","publisher":"Neural Information Processing Systems Foundation","_id":"3322","department":[{"_id":"ChLa"}],"language":[{"iso":"eng"}],"date_created":"2018-12-11T12:02:40Z","abstract":[{"lang":"eng","text":"We study multi-label prediction for structured output spaces, a problem that occurs, for example, in object detection in images, secondary structure prediction in computational biology, and graph matching with symmetries. Conventional multi-label classification techniques are typically not applicable in this situation, because they require explicit enumeration of the label space, which is infeasible in case of structured outputs. Relying on techniques originally designed for single- label structured prediction, in particular structured support vector machines, results in reduced prediction accuracy, or leads to infeasible optimization problems. In this work we derive a maximum-margin training formulation for multi-label structured prediction that remains computationally tractable while achieving high prediction accuracy. It also shares most beneficial properties with single-label maximum-margin approaches, in particular a formulation as a convex optimization problem, efficient working set training, and PAC-Bayesian generalization bounds."}],"publication":"NIPS: Neural Information Processing Systems","date_updated":"2023-10-17T11:47:36Z","date_published":"2011-12-13T00:00:00Z"},{"related_material":{"record":[{"id":"5383","relation":"earlier_version","status":"public"}]},"page":"476 - 491","year":"2011","title":"An efficient decision procedure for imperative tree data structures","status":"public","scopus_import":1,"doi":"10.1007/978-3-642-22438-6_36","type":"conference","publist_id":"3312","publication_status":"published","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","oa_version":"None","abstract":[{"lang":"eng","text":"We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures."}],"volume":6803,"date_created":"2018-12-11T12:02:40Z","language":[{"iso":"eng"}],"date_published":"2011-07-19T00:00:00Z","conference":{"start_date":"2011-07-31","end_date":"2011-08-05","name":"CADE 23: Automated Deduction ","location":"Wrocław, Poland"},"date_updated":"2023-02-23T12:23:48Z","_id":"3323","publisher":"Springer","day":"19","citation":{"apa":"Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36","ama":"Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:10.1007/978-3-642-22438-6_36","short":"T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.","chicago":"Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. https://doi.org/10.1007/978-3-642-22438-6_36.","ista":"Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.","mla":"Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36.","ieee":"T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław, Poland, 2011, vol. 6803, pp. 476–491."},"intvolume":" 6803","author":[{"full_name":"Wies, Thomas","first_name":"Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Muñiz","full_name":"Muñiz, Marco","first_name":"Marco"},{"full_name":"Kuncak, Viktor","first_name":"Viktor","last_name":"Kuncak"}],"month":"07","department":[{"_id":"ToHe"}],"alternative_title":["LNAI "],"quality_controlled":"1"},{"publist_id":"3311","type":"conference","page":"371 - 386","status":"public","scopus_import":1,"title":"Decision procedures for automating termination proofs","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T07:42:39Z","main_file_link":[{"open_access":"1","url":"https://infoscience.epfl.ch/record/170697/"}],"oa":1,"language":[{"iso":"eng"}],"date_created":"2018-12-11T12:02:40Z","volume":6538,"abstract":[{"lang":"eng","text":"Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs."}],"alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"citation":{"ieee":"R. Piskac and T. Wies, “Decision procedures for automating termination proofs,” presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA, 2011, vol. 6538, pp. 371–386.","chicago":"Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011. https://doi.org/10.1007/978-3-642-18275-4_26.","mla":"Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:10.1007/978-3-642-18275-4_26.","ista":"Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.","ama":"Piskac R, Wies T. Decision procedures for automating termination proofs. In: Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:10.1007/978-3-642-18275-4_26","apa":"Piskac, R., & Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26","short":"R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386."},"_id":"3324","publisher":"Springer","day":"01","doi":"10.1007/978-3-642-18275-4_26","year":"2011","oa_version":"Submitted Version","editor":[{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"last_name":"Schmidt","full_name":"Schmidt, David","first_name":"David"}],"publication_status":"published","date_published":"2011-01-01T00:00:00Z","conference":{"location":"Texas, USA","name":"VMCAI: Verification Model Checking and Abstract Interpretation","end_date":"2011-01-25","start_date":"2011-01-23"},"quality_controlled":"1","author":[{"last_name":"Piskac","full_name":"Piskac, Ruzica","first_name":"Ruzica"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas","full_name":"Wies, Thomas"}],"intvolume":" 6538","month":"01"},{"language":[{"iso":"eng"}],"volume":46,"date_created":"2018-12-11T12:02:41Z","abstract":[{"lang":"eng","text":"We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data do- main that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next in- put symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenat- ing data-string variables and new symbols formed from data vari- ables, while avoiding duplication. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over in- put/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional pro- grams, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative pro- grams dynamically modify a singly-linked heap by changing next- pointers of heap-nodes and by adding new nodes. The main re- striction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse."}],"date_updated":"2022-03-21T08:12:51Z","conference":{"start_date":"2011-01-26","end_date":"2011-01-28","name":"POPL: Principles of Programming Languages","location":"Texas, USA"},"date_published":"2011-01-26T00:00:00Z","intvolume":" 46","month":"01","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","full_name":"Cerny, Pavol"}],"citation":{"ama":"Alur R, Cerny P. Streaming transducers for algorithmic verification of single pass list processing programs. In: Vol 46. ACM; 2011:599-610. doi:10.1145/1926385.1926454","apa":"Alur, R., & Cerny, P. (2011). Streaming transducers for algorithmic verification of single pass list processing programs (Vol. 46, pp. 599–610). Presented at the POPL: Principles of Programming Languages, Texas, USA: ACM. https://doi.org/10.1145/1926385.1926454","short":"R. Alur, P. Cerny, in:, ACM, 2011, pp. 599–610.","ieee":"R. Alur and P. Cerny, “Streaming transducers for algorithmic verification of single pass list processing programs,” presented at the POPL: Principles of Programming Languages, Texas, USA, 2011, vol. 46, no. 1, pp. 599–610.","mla":"Alur, Rajeev, and Pavol Cerny. Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs. Vol. 46, no. 1, ACM, 2011, pp. 599–610, doi:10.1145/1926385.1926454.","ista":"Alur R, Cerny P. 2011. Streaming transducers for algorithmic verification of single pass list processing programs. POPL: Principles of Programming Languages vol. 46, 599–610.","chicago":"Alur, Rajeev, and Pavol Cerny. “Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs,” 46:599–610. ACM, 2011. https://doi.org/10.1145/1926385.1926454."},"day":"26","_id":"3325","publisher":"ACM","quality_controlled":"1","department":[{"_id":"ToHe"}],"type":"conference","publist_id":"3310","doi":"10.1145/1926385.1926454","year":"2011","status":"public","scopus_import":"1","title":"Streaming transducers for algorithmic verification of single pass list processing programs","page":"599 - 610","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","oa_version":"None","issue":"1"},{"article_processing_charge":"No","publication_status":"published","oa_version":"Submitted Version","ddc":["000"],"doi":"10.1007/978-3-642-24372-1_37","has_accepted_license":"1","file":[{"checksum":"a7ca08a2cb1b6925f4c18a3034ae5659","file_size":182309,"relation":"main_file","content_type":"application/pdf","file_id":"7868","date_updated":"2020-07-14T12:46:07Z","creator":"dernst","date_created":"2020-05-19T16:08:32Z","file_name":"2011_LNCS_Almagor.pdf","access_level":"open_access"}],"year":"2011","author":[{"full_name":"Almagor, Shaull","first_name":"Shaull","last_name":"Almagor"},{"last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi","first_name":"Udi"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"intvolume":" 6996","month":"10","quality_controlled":"1","date_published":"2011-10-14T00:00:00Z","conference":{"end_date":"2011-10-14","start_date":"2011-10-11","location":"Taipei, Taiwan","name":"ATVA: Automated Technology for Verification and Analysis"},"file_date_updated":"2020-07-14T12:46:07Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","publist_id":"3309","page":"482 - 491","status":"public","title":"What’s decidable about weighted automata ","citation":{"ieee":"S. Almagor, U. Boker, and O. Kupferman, “What’s decidable about weighted automata ,” presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan, 2011, vol. 6996, pp. 482–491.","ista":"Almagor S, Boker U, Kupferman O. 2011. What’s decidable about weighted automata . ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 6996, 482–491.","mla":"Almagor, Shaull, et al. What’s Decidable about Weighted Automata . Vol. 6996, Springer, 2011, pp. 482–91, doi:10.1007/978-3-642-24372-1_37.","chicago":"Almagor, Shaull, Udi Boker, and Orna Kupferman. “What’s Decidable about Weighted Automata ,” 6996:482–91. Springer, 2011. https://doi.org/10.1007/978-3-642-24372-1_37.","short":"S. Almagor, U. Boker, O. Kupferman, in:, Springer, 2011, pp. 482–491.","ama":"Almagor S, Boker U, Kupferman O. What’s decidable about weighted automata . In: Vol 6996. Springer; 2011:482-491. doi:10.1007/978-3-642-24372-1_37","apa":"Almagor, S., Boker, U., & Kupferman, O. (2011). What’s decidable about weighted automata (Vol. 6996, pp. 482–491). Presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan: Springer. https://doi.org/10.1007/978-3-642-24372-1_37"},"publisher":"Springer","_id":"3326","day":"14","department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"language":[{"iso":"eng"}],"volume":6996,"date_created":"2018-12-11T12:02:41Z","abstract":[{"lang":"eng","text":"Weighted automata map input words to numerical values. Ap- plications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. A weighted au- tomaton is defined with respect to a semiring. For the tropical semiring, the weight of a run is the sum of the weights of the transitions taken along the run, and the value of a word is the minimal weight of an accepting run on it. In the 90’s, Krob studied the decidability of problems on rational series defined with respect to the tropical semiring. Rational series are strongly related to weighted automata, and Krob’s results apply to them. In par- ticular, it follows from Krob’s results that the universality problem (that is, deciding whether the values of all words are below some threshold) is decidable for weighted automata defined with respect to the tropical semir- ing with domain ∪ {∞}, and that the equality problem is undecidable when the domain is ∪ {∞}. In this paper we continue the study of the borders of decidability in weighted automata, describe alternative and direct proofs of the above results, and tighten them further. Unlike the proofs of Krob, which are algebraic in their nature, our proofs stay in the terrain of state machines, and the reduction is from the halting problem of a two-counter machine. This enables us to significantly simplify Krob’s reasoning, make the un- decidability result accessible to the automata-theoretic community, and strengthen it to apply already to a very simple class of automata: all the states are accepting, there are no initial nor final weights, and all the weights on the transitions are from the set {−1, 0, 1}. The fact we work directly with the automata enables us to tighten also the decidability re- sults and to show that the universality problem for weighted automata defined with respect to the tropical semiring with domain ∪ {∞}, and in fact even with domain ≥0 ∪ {∞}, is PSPACE-complete. Our results thus draw a sharper picture about the decidability of decision problems for weighted automata, in both the front of containment vs. universality and the front of the ∪ {∞} vs. the ∪ {∞} domains."}],"date_updated":"2021-01-12T07:42:40Z","oa":1}]